Skip to content

Commit

Permalink
shrink this PR
Browse files Browse the repository at this point in the history
  • Loading branch information
@datokrat
datokrat committed Feb 11, 2025
1 parent 8c0d35b commit 9a611a8
Show file tree
Hide file tree
Showing 8 changed files with 0 additions and 1,322 deletions.
275 changes: 0 additions & 275 deletions src/Std/Data/DTreeMap/Internal/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,279 +101,4 @@ theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq
k ∈ t ↔ k' ∈ t := by
simp [mem_iff_contains, contains_congr h hab]

theorem contains_empty {a : α} : (empty : Impl α β).contains a = false := by
simp [contains, empty]

theorem not_mem_empty {a : α} : a ∉ (empty : Impl α β) := by
simp [mem_iff_contains, contains_empty]

theorem contains_of_isEmpty [TransOrd α] (h : t.WF) {a : α} :
t.isEmpty → t.contains a = false := by
simp_to_model; empty

theorem not_mem_of_isEmpty [TransOrd α] (h : t.WF) {a : α} :
t.isEmpty → a ∉ t := by
simpa [mem_iff_contains] using contains_of_isEmpty h

theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransOrd α] (h : t.WF) :
t.isEmpty = false ↔ ∃ a, t.contains a = true := by
simp_to_model using List.isEmpty_eq_false_iff_exists_containsKey

theorem isEmpty_eq_false_iff_exists_mem [TransOrd α] (h : t.WF) :
t.isEmpty = false ↔ ∃ a, a ∈ t := by
simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h

theorem isEmpty_iff_forall_contains [TransOrd α] (h : t.WF) :
t.isEmpty = true ↔ ∀ a, t.contains a = false := by
simp_to_model using List.isEmpty_iff_forall_containsKey

theorem isEmpty_iff_forall_not_mem [TransOrd α] (h : t.WF) :
t.isEmpty = true ↔ ∀ a, ¬a ∈ t := by
simpa [mem_iff_contains] using isEmpty_iff_forall_contains h

theorem contains_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insert k v h.balanced).impl.contains a = (compare k a == .eq || t.contains a) := by
simp_to_model [insert] using List.containsKey_insertEntry

theorem contains_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insert! k v).contains a = (compare k a == .eq || t.contains a) := by
simp_to_model [insert!] using List.containsKey_insertEntry

theorem mem_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ (t.insert k v h.balanced).impl ↔ compare k a = .eq ∨ a ∈ t := by
simp [mem_iff_contains, contains_insert h]

theorem mem_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ t.insert! k v ↔ compare k a = .eq ∨ a ∈ t := by
simp [mem_iff_contains, contains_insert! h]

theorem contains_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insert k v h.balanced).impl.contains k := by
simp_to_model [insert] using List.containsKey_insertEntry_self

theorem contains_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insert! k v).contains k := by
simp_to_model [insert!] using List.containsKey_insertEntry_self

theorem mem_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
k ∈ (t.insert k v h.balanced).impl := by
simpa [mem_iff_contains] using contains_insert_self h

theorem mem_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
k ∈ t.insert! k v := by
simpa [mem_iff_contains] using contains_insert!_self h

theorem contains_of_contains_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insert k v h.balanced).impl.contains a → ¬ compare k a = .eq → t.contains a := by
rw [← beq_iff_eq (b := Ordering.eq), ← beq_eq, Bool.not_eq_true]
simp_to_model [insert] using List.containsKey_of_containsKey_insertEntry

theorem contains_of_contains_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insert! k v).contains a → ¬ compare k a = .eq → t.contains a := by
rw [← beq_iff_eq (b := Ordering.eq), ← beq_eq, Bool.not_eq_true]
simp_to_model [insert!] using List.containsKey_of_containsKey_insertEntry

theorem mem_of_mem_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ (t.insert k v h.balanced).impl → ¬ compare k a = .eq → a ∈ t := by
simpa [mem_iff_contains] using contains_of_contains_insert h

theorem mem_of_mem_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ t.insert! k v → ¬ compare k a = .eq → a ∈ t := by
simpa [mem_iff_contains] using contains_of_contains_insert! h

theorem size_empty : (empty : Impl α β).size = 0 :=
rfl

theorem isEmpty_eq_size_eq_zero (h : t.WF) :
letI : BEq Nat := instBEqOfDecidableEq
t.isEmpty = (t.size == 0) := by
simp_to_model
rw [Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, Nat.beq_eq_true_eq]

theorem size_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insert k v h.balanced).impl.size = if t.contains k then t.size else t.size + 1 := by
simp_to_model [insert] using List.length_insertEntry

theorem size_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insert! k v).size = if t.contains k then t.size else t.size + 1 := by
simp_to_model [insert!] 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 [insert] using List.length_le_length_insertEntry

theorem size_le_size_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
t.size ≤ (t.insert! k v).size := by
simp_to_model [insert!] 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 [insert] using List.length_insertEntry_le

theorem size_insert!_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insert! k v).size ≤ t.size + 1 := by
simp_to_model [insert!] using List.length_insertEntry_le

theorem erase_empty {k : α} :
((empty : Impl α β).erase k balanced_empty).impl = empty :=
rfl

theorem erase!_empty {k : α} :
(empty : Impl α β).erase! k = empty :=
rfl

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 [erase] using List.isEmpty_eraseKey

theorem isEmpty_erase! [TransOrd α] (h : t.WF) {k : α} :
(t.erase! k).isEmpty = (t.isEmpty || (t.size = 1 && t.contains k)) := by
simp_to_model [erase!] using List.isEmpty_eraseKey

theorem contains_erase [TransOrd α] (h : t.WF) {k a : α} :
(t.erase k h.balanced).impl.contains a = (!(k == a) && t.contains a) := by
simp_to_model [erase] using List.containsKey_eraseKey

theorem contains_erase! [TransOrd α] (h : t.WF) {k a : α} :
(t.erase! k).contains a = (!(k == a) && t.contains a) := by
simp_to_model [erase!] using List.containsKey_eraseKey

theorem mem_erase [TransOrd α] (h : t.WF) {k a : α} :
a ∈ (t.erase k h.balanced).impl ↔ (k == a) = false ∧ a ∈ t := by
simp [mem_iff_contains, contains_erase h]

theorem mem_erase! [TransOrd α] (h : t.WF) {k a : α} :
a ∈ t.erase! k ↔ (k == a) = false ∧ a ∈ t := by
simp [mem_iff_contains, contains_erase! h]

theorem contains_of_contains_erase [TransOrd α] (h : t.WF) {k a : α} :
(t.erase k h.balanced).impl.contains a → t.contains a := by
simp_to_model [erase] using List.containsKey_of_containsKey_eraseKey

theorem contains_of_contains_erase! [TransOrd α] (h : t.WF) {k a : α} :
(t.erase! k).contains a → t.contains a := by
simp_to_model [erase!] using List.containsKey_of_containsKey_eraseKey

theorem mem_of_mem_erase [TransOrd α] (h : t.WF) {k a : α} :
a ∈ (t.erase k h.balanced).impl → a ∈ t := by
simpa [mem_iff_contains] using contains_of_contains_erase h

theorem mem_of_mem_erase! [TransOrd α] (h : t.WF) {k a : α} :
a ∈ t.erase! k → a ∈ t := by
simpa [mem_iff_contains] using contains_of_contains_erase! h

theorem size_erase [TransOrd α] (h : t.WF) {k : α} :
(t.erase k h.balanced).impl.size = if t.contains k then t.size - 1 else t.size := by
simp_to_model [erase] using List.length_eraseKey

theorem size_erase! [TransOrd α] (h : t.WF) {k : α} :
(t.erase! k).size = if t.contains k then t.size - 1 else t.size := by
simp_to_model [erase!] using List.length_eraseKey

theorem size_erase_le [TransOrd α] (h : t.WF) {k : α} :
(t.erase k h.balanced).impl.size ≤ t.size := by
simp_to_model [erase] using List.length_eraseKey_le

theorem size_erase!_le [TransOrd α] (h : t.WF) {k : α} :
(t.erase! k).size ≤ t.size := by
simp_to_model [erase!] using List.length_eraseKey_le

theorem size_le_size_erase [TransOrd α] (h : t.WF) {k : α} :
t.size ≤ (t.erase k h.balanced).impl.size + 1 := by
simp_to_model [erase] using List.length_le_length_eraseKey

theorem size_le_size_erase! [TransOrd α] (h : t.WF) {k : α} :
t.size ≤ (t.erase! k).size + 1 := by
simp_to_model [erase!] using List.length_le_length_eraseKey

@[simp]
theorem isEmpty_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insertIfNew k v h.balanced).impl.isEmpty = false := by
simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew

@[simp]
theorem isEmpty_insertIfNew! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insertIfNew! k v).isEmpty = false := by
simp_to_model [insertIfNew!] using List.isEmpty_insertEntryIfNew

@[simp]
theorem contains_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insertIfNew k v h.balanced).impl.contains a = (k == a || t.contains a) := by
simp_to_model [insertIfNew] using List.containsKey_insertEntryIfNew

@[simp]
theorem contains_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insertIfNew! k v).contains a = (k == a || t.contains a) := by
simp_to_model [insertIfNew!] using List.containsKey_insertEntryIfNew

@[simp]
theorem mem_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ (t.insertIfNew k v h.balanced).impl ↔ k == a ∨ a ∈ t := by
simp [mem_iff_contains, contains_insertIfNew, h]

@[simp]
theorem mem_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ t.insertIfNew! k v ↔ k == a ∨ a ∈ t := by
simp [mem_iff_contains, contains_insertIfNew, h]

theorem contains_insertIfNew_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insertIfNew k v h.balanced).impl.contains k := by
simp [contains_insertIfNew, h]

theorem contains_insertIfNew!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insertIfNew! k v).contains k := by
simp [contains_insertIfNew!, h]

theorem mem_insertIfNew_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
k ∈ (t.insertIfNew k v h.balanced).impl := by
simp [contains_insertIfNew, h]

theorem mem_insertIfNew!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
k ∈ t.insertIfNew! k v := by
simp [contains_insertIfNew!, h]

theorem contains_of_contains_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insertIfNew k v h.balanced).impl.contains a → (k == a) = false → t.contains a := by
simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew

theorem contains_of_contains_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
(t.insertIfNew! k v).contains a → (k == a) = false → t.contains a := by
simp_to_model [insertIfNew!] using List.containsKey_of_containsKey_insertEntryIfNew

theorem mem_of_mem_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ (t.insertIfNew k v h.balanced).impl → (k == a) = false → a ∈ t := by
simpa [mem_iff_contains] using contains_of_contains_insertIfNew h

theorem mem_of_mem_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ t.insertIfNew! k v → (k == a) = false → a ∈ t := by
simpa [mem_iff_contains] using contains_of_contains_insertIfNew! h

theorem size_insertIfNew [TransOrd α] {k : α} (h : t.WF) {v : β k} :
(t.insertIfNew k v h.balanced).impl.size = if k ∈ t then t.size else t.size + 1 := by
simp only [mem_iff_contains]
simp_to_model [insertIfNew] using List.length_insertEntryIfNew

theorem size_insertIfNew! [TransOrd α] {k : α} (h : t.WF) {v : β k} :
(t.insertIfNew! k v).size = if k ∈ t then t.size else t.size + 1 := by
simp only [mem_iff_contains]
simp_to_model [insertIfNew!] using List.length_insertEntryIfNew

theorem size_le_size_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
t.size ≤ (t.insertIfNew k v h.balanced).impl.size := by
simp_to_model [insertIfNew] using List.length_le_length_insertEntryIfNew

theorem size_le_size_insertIfNew! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
t.size ≤ (t.insertIfNew! k v).size := by
simp_to_model [insertIfNew!] using List.length_le_length_insertEntryIfNew

theorem size_insertIfNew_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insertIfNew k v h.balanced).impl.size ≤ t.size + 1 := by
simp_to_model [insertIfNew] using List.length_insertEntryIfNew_le

theorem size_insertIfNew!_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
(t.insertIfNew! k v).size ≤ t.size + 1 := by
simp_to_model [insertIfNew!] using List.length_insertEntryIfNew_le



end Std.DTreeMap.Internal.Impl
Loading

0 comments on commit 9a611a8

Please sign in to comment.