forgotten size_insert lemmas

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

Hide file tree

Showing 7 changed files with 65 additions and 1 deletion.
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -111,6 +111,22 @@ theorem size_insertSlow [TransOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.insertSlow k v).size = if t.contains k then t.size else t.size + 1 := by
   simp_to_model using List.length_insertEntry
 
+theorem size_le_size_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    t.size ≤ (t.insert k v h.balanced).impl.size := by
+  simp_to_model using List.length_le_length_insertEntry
+
+theorem size_le_size_insertSlow [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    t.size ≤ (t.insertSlow k v).size := by
+  simp_to_model using List.length_le_length_insertEntry
+
+theorem size_insert_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v h.balanced).impl.size ≤ t.size + 1 := by
+  simp_to_model using List.length_insertEntry_le
+
+theorem size_insertSlow_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertSlow k v).size ≤ t.size + 1 := by
+  simp_to_model using List.length_insertEntry_le
+
 theorem isEmpty_erase [TransOrd α] (h : t.WF) {k : α} :
     (t.erase k h.balanced).impl.isEmpty = (t.isEmpty || (t.size = 1 && t.contains k)) := by
   simp_to_model using List.isEmpty_eraseKey

diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -55,6 +55,14 @@ theorem size_insert [TransCmp cmp] {k : α} {v : β k} :
     (t.insert k v).size = if t.contains k then t.size else t.size + 1 :=
   Impl.size_insert t.wf
 
+theorem size_le_size_insert [TransCmp cmp] {k : α} {v : β k} :
+    t.size ≤ (t.insert k v).size :=
+  Impl.size_le_size_insert t.wf
+
+theorem size_insert_le [TransCmp cmp] {k : α} {v : β k} :
+    (t.insert k v).size ≤ t.size + 1 :=
+  Impl.size_insert_le t.wf
+
 theorem isEmpty_erase [TransCmp cmp] {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   Impl.isEmpty_erase t.wf

diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean
@@ -55,6 +55,14 @@ theorem size_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
     (t.insert k v).size = if t.contains k then t.size else t.size + 1 :=
   Impl.size_insertSlow h
 
+theorem size_le_size_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    t.size ≤ (t.insert k v).size :=
+  Impl.size_le_size_insertSlow h
+
+theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v).size ≤ t.size + 1 :=
+  Impl.size_insertSlow_le h
+
 theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   Impl.isEmpty_eraseSlow h

diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
@@ -53,6 +53,14 @@ theorem size_insert [TransCmp cmp] {k : α} {v : β} :
     (t.insert k v).size = if t.contains k then t.size else t.size + 1 :=
   DTreeMap.size_insert
 
+theorem size_le_size_insert [TransCmp cmp] {k : α} {v : β} :
+    t.size ≤ (t.insert k v).size :=
+  DTreeMap.size_le_size_insert
+
+theorem size_insert_le [TransCmp cmp] {k : α} {v : β} :
+    (t.insert k v).size ≤ t.size + 1 :=
+  DTreeMap.size_insert_le
+
 theorem isEmpty_erase [TransCmp cmp] {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   DTreeMap.isEmpty_erase

diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean
@@ -53,6 +53,14 @@ theorem size_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     (t.insert k v).size = if t.contains k then t.size else t.size + 1 :=
   DTreeMap.Raw.size_insert h
 
+theorem size_le_size_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    t.size ≤ (t.insert k v).size :=
+  DTreeMap.Raw.size_le_size_insert h
+
+theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insert k v).size ≤ t.size + 1 :=
+  DTreeMap.Raw.size_insert_le h
+
 theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   DTreeMap.Raw.isEmpty_erase h

diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
@@ -53,6 +53,14 @@ theorem size_insert [TransCmp cmp] {k : α} :
     (t.insert k).size = if t.contains k then t.size else t.size + 1 :=
   TreeMap.size_insert
 
+theorem size_le_size_insert [TransCmp cmp] {k : α} :
+    t.size ≤ (t.insert k).size :=
+  TreeMap.size_le_size_insert
+
+theorem size_insert_le [TransCmp cmp] {k : α} :
+    (t.insert k).size ≤ t.size + 1 :=
+  TreeMap.size_insert_le
+
 theorem isEmpty_erase [TransCmp cmp] {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   TreeMap.isEmpty_erase

diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean
@@ -49,10 +49,18 @@ theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} :
     (t.insert k).contains a = (cmp k a == .eq || t.contains a) :=
   TreeMap.Raw.contains_insert h
 
-theorem size_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+theorem size_insert [TransCmp cmp] (h : t.WF) {k : α} :
     (t.insert k).size = if t.contains k then t.size else t.size + 1 :=
   TreeMap.Raw.size_insert h
 
+theorem size_le_size_insert [TransCmp cmp] (h : t.WF) {k : α} :
+    t.size ≤ (t.insert k).size :=
+  DTreeMap.Raw.size_le_size_insert h
+
+theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.insert k).size ≤ t.size + 1 :=
+  DTreeMap.Raw.size_insert_le h
+
 theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} :
     (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
   TreeMap.Raw.isEmpty_erase h