forgotten erase lemmas

leanprover · Jan 29, 2025 · 0dbf50f · 0dbf50f
1 parent 2a65a43
commit 0dbf50f
Show file tree

Hide file tree

Showing 3 changed files with 60 additions and 0 deletions.
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -67,4 +67,24 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   Impl.isEmpty_erase t.wf
 
+theorem contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a = (cmp k a != .eq && t.contains a) :=
+  Impl.contains_erase t.wf
+
+theorem contains_of_contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a → t.contains a :=
+  Impl.contains_of_contains_erase t.wf
+
+theorem size_erase [TransCmp cmp] {k : α} :
+    (t.erase k).size = if t.contains k then t.size - 1 else t.size :=
+  Impl.size_erase t.wf
+
+theorem size_erase_le [TransCmp cmp] {k : α} :
+    (t.erase k).size ≤ t.size :=
+  Impl.size_erase_le t.wf
+
+theorem size_le_size_erase [TransCmp cmp] {k : α} :
+    t.size ≤ (t.erase k).size + 1 :=
+  Impl.size_le_size_erase t.wf
+
 end Std.DTreeMap
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
@@ -65,4 +65,24 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   DTreeMap.isEmpty_erase
 
+theorem contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a = (cmp k a != .eq && t.contains a) :=
+  DTreeMap.contains_erase
+
+theorem contains_of_contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a → t.contains a :=
+  DTreeMap.contains_of_contains_erase
+
+theorem size_erase [TransCmp cmp] {k : α} :
+    (t.erase k).size = if t.contains k then t.size - 1 else t.size :=
+  DTreeMap.size_erase
+
+theorem size_erase_le [TransCmp cmp] {k : α} :
+    (t.erase k).size ≤ t.size :=
+  DTreeMap.size_erase_le
+
+theorem size_le_size_erase [TransCmp cmp] {k : α} :
+    t.size ≤ (t.erase k).size + 1 :=
+  DTreeMap.size_le_size_erase
+
 end Std.TreeMap
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
@@ -65,4 +65,24 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   TreeMap.isEmpty_erase
 
+theorem contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a = (cmp k a != .eq && t.contains a) :=
+  DTreeMap.contains_erase
+
+theorem contains_of_contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a → t.contains a :=
+  DTreeMap.contains_of_contains_erase
+
+theorem size_erase [TransCmp cmp] {k : α} :
+    (t.erase k).size = if t.contains k then t.size - 1 else t.size :=
+  DTreeMap.size_erase
+
+theorem size_erase_le [TransCmp cmp] {k : α} :
+    (t.erase k).size ≤ t.size :=
+  DTreeMap.size_erase_le
+
+theorem size_le_size_erase [TransCmp cmp] {k : α} :
+    t.size ≤ (t.erase k).size + 1 :=
+  DTreeMap.size_le_size_erase
+
 end Std.TreeSet