Skip to content

Commit 9cbff55

Browse files
wkrozowskiTwoFX
wkrozowski
and
TwoFX
authored
feat: add difference on ExtDTreeMap/ExtTreeMap/TreeSet (#11408)
This PR adds a difference operation on `ExtDTreeMap`/`ExtTreeMap`/`TreeSet` and proves several lemmas about it. Stacked on top of #11407 --------- Co-authored-by: Markus Himmel <[email protected]>
1 parent e0650a0 commit 9cbff55

File tree

6 files changed

+663
-0
lines changed

6 files changed

+663
-0
lines changed

‎src/Std/Data/ExtDTreeMap/Basic.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -924,6 +924,17 @@ def inter [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β
924924

925925
instance [TransCmp cmp] : Inter (ExtDTreeMap α β cmp) := ⟨inter⟩
926926

927+
@[inline, inherit_doc DTreeMap.diff]
928+
def diff [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β cmp := lift₂ (fun x y : DTreeMap α β cmp => mk (x.diff y))
929+
(fun a b c d equiv₁ equiv₂ => by
930+
simp only [DTreeMap.diff_eq, mk'.injEq]
931+
apply Quotient.sound
932+
apply DTreeMap.Equiv.diff_congr
933+
. exact equiv₁
934+
. exact equiv₂) m₁ m₂
935+
936+
instance [TransCmp cmp] : SDiff (ExtDTreeMap α β cmp) := ⟨diff⟩
937+
927938
instance [TransCmp cmp] [Repr α] [(a : α) → Repr (β a)] : Repr (ExtDTreeMap α β cmp) where
928939
reprPrec m prec := Repr.addAppParen ("Std.ExtDTreeMap.ofList " ++ repr m.toList) prec
929940

‎src/Std/Data/ExtDTreeMap/Lemmas.lean‎

Lines changed: 316 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2979,6 +2979,322 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β]
29792979

29802980
end Const
29812981

2982+
section Diff
2983+
2984+
variable {t₁ t₂ : ExtDTreeMap α β cmp}
2985+
2986+
@[simp]
2987+
theorem diff_eq [TransCmp cmp] : t₁.diff t₂ = t₁ \ t₂ := by
2988+
simp only [SDiff.sdiff]
2989+
2990+
/- contains -/
2991+
@[simp]
2992+
theorem contains_diff [TransCmp cmp] {k : α} :
2993+
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) :=
2994+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.contains_diff
2995+
2996+
/- mem -/
2997+
@[simp]
2998+
theorem mem_diff_iff [TransCmp cmp] {k : α} :
2999+
k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂ :=
3000+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.mem_diff_iff
3001+
3002+
theorem not_mem_diff_of_not_mem_left [TransCmp cmp]
3003+
{k : α} (h : ¬k ∈ t₁) :
3004+
¬k ∈ t₁ \ t₂ := by
3005+
revert h
3006+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.not_mem_diff_of_not_mem_left h
3007+
3008+
theorem not_mem_diff_of_mem_right [TransCmp cmp]
3009+
{k : α} (h : k ∈ t₂) :
3010+
¬k ∈ t₁ \ t₂ := by
3011+
revert h
3012+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.not_mem_diff_of_mem_right h
3013+
3014+
/- get? -/
3015+
theorem get?_diff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} :
3016+
(t₁ \ t₂).get? k =
3017+
if k ∈ t₂ then none else t₁.get? k :=
3018+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.get?_diff
3019+
3020+
theorem get?_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
3021+
{k : α} (h : ¬k ∈ t₂) :
3022+
(t₁ \ t₂).get? k = t₁.get? k := by
3023+
revert h
3024+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.get?_diff_of_not_mem_right h
3025+
3026+
theorem get?_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp]
3027+
{k : α} (h : ¬k ∈ t₁) :
3028+
(t₁ \ t₂).get? k = none := by
3029+
revert h
3030+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.get?_diff_of_not_mem_left h
3031+
3032+
theorem get?_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
3033+
{k : α} (h : k ∈ t₂) :
3034+
(t₁ \ t₂).get? k = none := by
3035+
revert h
3036+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.get?_diff_of_mem_right h
3037+
3038+
/- get -/
3039+
theorem get_diff [TransCmp cmp] [LawfulEqCmp cmp]
3040+
{k : α} {h_mem : k ∈ t₁ \ t₂} :
3041+
(t₁ \ t₂).get k h_mem =
3042+
t₁.get k (mem_diff_iff.1 h_mem).1 := by
3043+
induction t₁ with
3044+
| mk a =>
3045+
induction t₂ with
3046+
| mk b =>
3047+
apply DTreeMap.get_diff
3048+
3049+
/- getD -/
3050+
theorem getD_diff [TransCmp cmp] [LawfulEqCmp cmp]
3051+
{k : α} {fallback : β k} :
3052+
(t₁ \ t₂).getD k fallback =
3053+
if k ∈ t₂ then fallback else t₁.getD k fallback :=
3054+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.getD_diff
3055+
3056+
theorem getD_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
3057+
{k : α} {fallback : β k} (h : ¬k ∈ t₂) :
3058+
(t₁ \ t₂).getD k fallback = t₁.getD k fallback := by
3059+
revert h
3060+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getD_diff_of_not_mem_right h
3061+
3062+
theorem getD_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
3063+
{k : α} {fallback : β k} (h : k ∈ t₂) :
3064+
(t₁ \ t₂).getD k fallback = fallback := by
3065+
revert h
3066+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getD_diff_of_mem_right h
3067+
3068+
theorem getD_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp]
3069+
{k : α} {fallback : β k} (h : ¬k ∈ t₁) :
3070+
(t₁ \ t₂).getD k fallback = fallback := by
3071+
revert h
3072+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getD_diff_of_not_mem_left h
3073+
3074+
/- get! -/
3075+
theorem get!_diff [TransCmp cmp] [LawfulEqCmp cmp]
3076+
{k : α} [Inhabited (β k)] :
3077+
(t₁ \ t₂).get! k =
3078+
if k ∈ t₂ then default else t₁.get! k :=
3079+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.get!_diff
3080+
3081+
theorem get!_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
3082+
{k : α} [Inhabited (β k)] (h : ¬k ∈ t₂) :
3083+
(t₁ \ t₂).get! k = t₁.get! k := by
3084+
revert h
3085+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.get!_diff_of_not_mem_right h
3086+
3087+
theorem get!_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
3088+
{k : α} [Inhabited (β k)] (h : k ∈ t₂) :
3089+
(t₁ \ t₂).get! k = default := by
3090+
revert h
3091+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.get!_diff_of_mem_right h
3092+
3093+
theorem get!_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp]
3094+
{k : α} [Inhabited (β k)] (h : ¬k ∈ t₁) :
3095+
(t₁ \ t₂).get! k = default := by
3096+
revert h
3097+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.get!_diff_of_not_mem_left h
3098+
3099+
/- getKey? -/
3100+
theorem getKey?_diff [TransCmp cmp] {k : α} :
3101+
(t₁ \ t₂).getKey? k =
3102+
if k ∈ t₂ then none else t₁.getKey? k :=
3103+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.getKey?_diff
3104+
3105+
theorem getKey?_diff_of_not_mem_right [TransCmp cmp]
3106+
{k : α} (h : ¬k ∈ t₂) :
3107+
(t₁ \ t₂).getKey? k = t₁.getKey? k := by
3108+
revert h
3109+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKey?_diff_of_not_mem_right h
3110+
3111+
theorem getKey?_diff_of_not_mem_left [TransCmp cmp]
3112+
{k : α} (h : ¬k ∈ t₁) :
3113+
(t₁ \ t₂).getKey? k = none := by
3114+
revert h
3115+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKey?_diff_of_not_mem_left h
3116+
3117+
theorem getKey?_diff_of_mem_right [TransCmp cmp]
3118+
{k : α} (h : k ∈ t₂) :
3119+
(t₁ \ t₂).getKey? k = none := by
3120+
revert h
3121+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKey?_diff_of_mem_right h
3122+
3123+
/- getKey -/
3124+
theorem getKey_diff [TransCmp cmp]
3125+
{k : α} {h_mem : k ∈ t₁ \ t₂} :
3126+
(t₁ \ t₂).getKey k h_mem =
3127+
t₁.getKey k (mem_diff_iff.1 h_mem).1 := by
3128+
induction t₁ with
3129+
| mk a =>
3130+
induction t₂ with
3131+
| mk b =>
3132+
apply DTreeMap.getKey_diff
3133+
3134+
/- getKeyD -/
3135+
theorem getKeyD_diff [TransCmp cmp] {k fallback : α} :
3136+
(t₁ \ t₂).getKeyD k fallback =
3137+
if k ∈ t₂ then fallback else t₁.getKeyD k fallback :=
3138+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.getKeyD_diff
3139+
3140+
theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] {k fallback : α} (h : ¬k ∈ t₂) :
3141+
(t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := by
3142+
revert h
3143+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKeyD_diff_of_not_mem_right h
3144+
3145+
theorem getKeyD_diff_of_mem_right [TransCmp cmp] {k fallback : α} (h : k ∈ t₂) :
3146+
(t₁ \ t₂).getKeyD k fallback = fallback := by
3147+
revert h
3148+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKeyD_diff_of_mem_right h
3149+
3150+
theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] {k fallback : α} (h : ¬k ∈ t₁) :
3151+
(t₁ \ t₂).getKeyD k fallback = fallback := by
3152+
revert h
3153+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKeyD_diff_of_not_mem_left h
3154+
3155+
/- getKey! -/
3156+
theorem getKey!_diff [Inhabited α] [TransCmp cmp] {k : α} :
3157+
(t₁ \ t₂).getKey! k =
3158+
if k ∈ t₂ then default else t₁.getKey! k :=
3159+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.getKey!_diff
3160+
3161+
theorem getKey!_diff_of_not_mem_right [Inhabited α] [TransCmp cmp]
3162+
{k : α} (h : ¬k ∈ t₂) :
3163+
(t₁ \ t₂).getKey! k = t₁.getKey! k := by
3164+
revert h
3165+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKey!_diff_of_not_mem_right h
3166+
3167+
theorem getKey!_diff_of_mem_right [Inhabited α] [TransCmp cmp]
3168+
{k : α} (h : k ∈ t₂) :
3169+
(t₁ \ t₂).getKey! k = default := by
3170+
revert h
3171+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKey!_diff_of_mem_right h
3172+
3173+
theorem getKey!_diff_of_not_mem_left [Inhabited α] [TransCmp cmp]
3174+
{k : α} (h : ¬k ∈ t₁) :
3175+
(t₁ \ t₂).getKey! k = default := by
3176+
revert h
3177+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.getKey!_diff_of_not_mem_left h
3178+
3179+
/- size -/
3180+
theorem size_diff_le_size_left [TransCmp cmp] :
3181+
(t₁ \ t₂).size ≤ t₁.size :=
3182+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.size_diff_le_size_left
3183+
3184+
theorem size_diff_eq_size_left [TransCmp cmp]
3185+
(h : ∀ (a : α), a ∈ t₁ → a ∉ t₂) :
3186+
(t₁ \ t₂).size = t₁.size := by
3187+
revert h
3188+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.size_diff_eq_size_left h
3189+
3190+
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] :
3191+
(t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size :=
3192+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.size_diff_add_size_inter_eq_size_left
3193+
3194+
/- isEmpty -/
3195+
@[simp]
3196+
theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) :
3197+
(t₁ \ t₂).isEmpty = true := by
3198+
revert h
3199+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.isEmpty_diff_left h
3200+
3201+
theorem isEmpty_diff_iff [TransCmp cmp] :
3202+
(t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ :=
3203+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.isEmpty_diff_iff
3204+
3205+
end Diff
3206+
3207+
namespace Const
3208+
3209+
variable {β : Type v} {t₁ t₂ : ExtDTreeMap α (fun _ => β) cmp}
3210+
3211+
/- get? -/
3212+
theorem get?_diff [TransCmp cmp] {k : α} :
3213+
Const.get? (t₁ \ t₂) k =
3214+
if k ∈ t₂ then none else Const.get? t₁ k :=
3215+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.Const.get?_diff
3216+
3217+
theorem get?_diff_of_not_mem_right [TransCmp cmp]
3218+
{k : α} (h : ¬k ∈ t₂) :
3219+
Const.get? (t₁ \ t₂) k = Const.get? t₁ k := by
3220+
revert h
3221+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.get?_diff_of_not_mem_right h
3222+
3223+
theorem get?_diff_of_not_mem_left [TransCmp cmp]
3224+
{k : α} (h : ¬k ∈ t₁) :
3225+
Const.get? (t₁ \ t₂) k = none := by
3226+
revert h
3227+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.get?_diff_of_not_mem_left h
3228+
3229+
theorem get?_diff_of_mem_right [TransCmp cmp]
3230+
{k : α} (h : k ∈ t₂) :
3231+
Const.get? (t₁ \ t₂) k = none := by
3232+
revert h
3233+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.get?_diff_of_mem_right h
3234+
3235+
/- get -/
3236+
theorem get_diff [TransCmp cmp]
3237+
{k : α} {h_mem : k ∈ t₁ \ t₂} :
3238+
Const.get (t₁ \ t₂) k h_mem =
3239+
Const.get t₁ k (mem_diff_iff.1 h_mem).1 := by
3240+
induction t₁ with
3241+
| mk a =>
3242+
induction t₂ with
3243+
| mk b =>
3244+
apply DTreeMap.Const.get_diff
3245+
3246+
/- getD -/
3247+
theorem getD_diff [TransCmp cmp]
3248+
{k : α} {fallback : β} :
3249+
Const.getD (t₁ \ t₂) k fallback =
3250+
if k ∈ t₂ then fallback else Const.getD t₁ k fallback :=
3251+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.Const.getD_diff
3252+
3253+
theorem getD_diff_of_not_mem_right [TransCmp cmp]
3254+
{k : α} {fallback : β} (h : ¬k ∈ t₂) :
3255+
Const.getD (t₁ \ t₂) k fallback = Const.getD t₁ k fallback := by
3256+
revert h
3257+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.getD_diff_of_not_mem_right h
3258+
3259+
theorem getD_diff_of_mem_right [TransCmp cmp]
3260+
{k : α} {fallback : β} (h : k ∈ t₂) :
3261+
Const.getD (t₁ \ t₂) k fallback = fallback := by
3262+
revert h
3263+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.getD_diff_of_mem_right h
3264+
3265+
theorem getD_diff_of_not_mem_left [TransCmp cmp]
3266+
{k : α} {fallback : β} (h : ¬k ∈ t₁) :
3267+
Const.getD (t₁ \ t₂) k fallback = fallback := by
3268+
revert h
3269+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.getD_diff_of_not_mem_left h
3270+
3271+
/- get! -/
3272+
theorem get!_diff [TransCmp cmp] [Inhabited β]
3273+
{k : α} :
3274+
Const.get! (t₁ \ t₂) k =
3275+
if k ∈ t₂ then default else Const.get! t₁ k :=
3276+
t₁.inductionOn₂ t₂ fun _ _ => DTreeMap.Const.get!_diff
3277+
3278+
theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β]
3279+
{k : α} (h : ¬k ∈ t₂) :
3280+
Const.get! (t₁ \ t₂) k = Const.get! t₁ k := by
3281+
revert h
3282+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.get!_diff_of_not_mem_right h
3283+
3284+
theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β]
3285+
{k : α} (h : k ∈ t₂) :
3286+
Const.get! (t₁ \ t₂) k = default := by
3287+
revert h
3288+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.get!_diff_of_mem_right h
3289+
3290+
theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β]
3291+
{k : α} (h : ¬k ∈ t₁) :
3292+
Const.get! (t₁ \ t₂) k = default := by
3293+
revert h
3294+
exact t₁.inductionOn₂ t₂ fun _ _ h => DTreeMap.Const.get!_diff_of_not_mem_left h
3295+
3296+
end Const
3297+
29823298
section Alter
29833299

29843300
theorem alter_eq_empty_iff_erase_eq_empty [TransCmp cmp] [LawfulEqCmp cmp] {k : α}

‎src/Std/Data/ExtTreeMap/Basic.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -535,6 +535,11 @@ def inter [TransCmp cmp] (t₁ t₂ : ExtTreeMap α β cmp) : ExtTreeMap α β c
535535

536536
instance [TransCmp cmp] : Inter (ExtTreeMap α β cmp) := ⟨inter⟩
537537

538+
@[inline, inherit_doc ExtDTreeMap.diff]
539+
def diff [TransCmp cmp] (t₁ t₂ : ExtTreeMap α β cmp) : ExtTreeMap α β cmp := ⟨ExtDTreeMap.diff t₁.inner t₂.inner⟩
540+
541+
instance [TransCmp cmp] : SDiff (ExtTreeMap α β cmp) := ⟨diff⟩
542+
538543
@[inline, inherit_doc ExtDTreeMap.eraseMany]
539544
def eraseMany [TransCmp cmp] {ρ} [ForIn Id ρ α] (t : ExtTreeMap α β cmp) (l : ρ) : ExtTreeMap α β cmp :=
540545
⟨t.inner.eraseMany l⟩

0 commit comments

Comments
 (0)