From 10551a8b059fbdca294004e7d16f3f7ddecc3e7e Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 6 Feb 2025 15:49:41 +0100 Subject: [PATCH 01/17] wip --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 185 +++++++++++++++++++++ src/Std/Data/DTreeMap/Lemmas.lean | 90 ++++++++++ src/Std/Data/DTreeMap/RawLemmas.lean | 90 ++++++++++ src/Std/Data/TreeMap/Lemmas.lean | 88 ++++++++++ src/Std/Data/TreeMap/RawLemmas.lean | 88 ++++++++++ src/Std/Data/TreeSet/Lemmas.lean | 88 ++++++++++ src/Std/Data/TreeSet/RawLemmas.lean | 88 ++++++++++ 7 files changed, 717 insertions(+) create mode 100644 src/Std/Data/DTreeMap/Internal/Lemmas.lean create mode 100644 src/Std/Data/DTreeMap/Lemmas.lean create mode 100644 src/Std/Data/DTreeMap/RawLemmas.lean create mode 100644 src/Std/Data/TreeMap/Lemmas.lean create mode 100644 src/Std/Data/TreeMap/RawLemmas.lean create mode 100644 src/Std/Data/TreeSet/Lemmas.lean create mode 100644 src/Std/Data/TreeSet/RawLemmas.lean diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean new file mode 100644 index 000000000000..14d100c2f7ff --- /dev/null +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -0,0 +1,185 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.HashMap.Basic +import Std.Data.DTreeMap.Internal.WF + +/-! +# API lemmas for `DTreeMap.Impl` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +open Std.Internal.List +open Std.Internal + +universe u v + +namespace Std.DTreeMap.Internal.Impl + +variable {α : Type u} {β : α → Type v} {_ : Ord α} {t : Impl α β} + +/-- Internal implementation detail of the tree map -/ +scoped macro "wf_trivial" : tactic => `(tactic| + repeat (first + | apply WF.ordered | apply WF.balanced | apply WF.insert | apply WF.insert! + | apply WF.erase | apply WF.erase! + | apply Ordered.distinctKeys + | assumption + )) + +/-- Internal implementation detail of the tree map -/ +scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } ) + +open Lean + +private def queryNames : Array Name := + #[``apply_isEmpty, ``apply_contains, ``apply_size] + +private def modifyMap : Std.HashMap Name Name := + .ofList + [⟨`insert, ``toListModel_insert⟩, + ⟨`insert!, ``toListModel_insert!⟩, + ⟨`erase, ``toListModel_erase⟩, + ⟨`erase!, ``toListModel_erase!⟩] + +private def congrNames : MacroM (Array (TSyntax `term)) := do + return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm), + ← `(_root_.List.Perm.length_eq), ← `(getValueCast?_of_perm _), + ← `(getValue?_of_perm _), ← `(getValue_of_perm _), ← `(getValueCast_of_perm _), + ← `(getValueCast!_of_perm _), ← `(getValueCastD_of_perm _), ← `(getValue!_of_perm _), + ← `(getValueD_of_perm _), ← `(getKey?_of_perm _), ← `(getKey_of_perm _), ← `(getKeyD_of_perm _), + ← `(getKey!_of_perm _)] + +/-- Internal implementation detail of the tree map -/ +scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic + +macro_rules +| `(tactic| simp_to_model $[[$modifyNames,*]]? $[using $using?]?) => do + let mut congrModify : Array (TSyntax `term) := #[] + if let some modifyNames := modifyNames then + for modify in modifyNames.getElems.flatMap + (fun n => modifyMap.get? (Lean.Syntax.getId n) |>.toArray) do + for congr in (← congrNames) do + congrModify := congrModify.push (← `($congr:term ($(mkIdent modify) ..))) + `(tactic| + (simp (discharger := wf_trivial) only + [$[$(Array.map Lean.mkIdent queryNames):term],*, $[$congrModify:term],*] + $[apply $(using?.toArray):term];*) + <;> wf_trivial) + +attribute [local instance] beqOfOrd +attribute [local instance] equivBEq_of_transOrd + +theorem isEmpty_empty : isEmpty (empty : Impl α β) := by + simp [Impl.apply_isEmpty] + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + Iff.rfl + +theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : k == k') : + t.contains k = t.contains k' := by + simp_to_model using List.containsKey_congr + +theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : k == k') : k ∈ t ↔ k' ∈ t := by + simp [mem_iff_contains, contains_congr h hab] + +theorem contains_empty {k : α} : (empty : Impl α β).contains k = false := by + simp [contains, empty] + +theorem mem_empty {k : α} : k ∉ (empty : Impl α β) := by + simp [mem_iff_contains, contains_empty] + +theorem isEmpty_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert k v h.balanced).impl.isEmpty = false := by + simp_to_model [insert] using List.isEmpty_insertEntry + +theorem isEmpty_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert! k v).isEmpty = false := by + simp_to_model [insert!] using List.isEmpty_insertEntry + +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 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 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 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 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 + +end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean new file mode 100644 index 000000000000..5f5c57877e86 --- /dev/null +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.DTreeMap.Internal.Lemmas +import Std.Data.DTreeMap.Basic + +/-! +# API lemmas for `DTreeMap` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +open Std.DTreeMap.Internal + +universe u v + +namespace Std.DTreeMap + +attribute [local instance] TransOrd.ofTransCmp + +variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} + +theorem isEmpty_empty : (empty : DTreeMap α β cmp).isEmpty := + Impl.isEmpty_empty + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + Impl.mem_iff_contains + +theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : + t.contains k = t.contains k' := + Impl.contains_congr t.wf hab + +theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := + Impl.mem_congr t.wf hab + +theorem contains_empty {k : α} : (empty : DTreeMap α β cmp).contains k = false := + Impl.contains_empty + +theorem mem_empty {k : α} : k ∉ (empty : DTreeMap α β cmp) := + Impl.mem_empty + +theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} : + (t.insert k v).isEmpty = false := + Impl.isEmpty_insert t.wf + +theorem contains_insert [TransCmp cmp] {k k' : α} {v : β k} : + (t.insert k v).contains k' = (cmp k k' == .eq || t.contains k') := + Impl.contains_insert t.wf + +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 + +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/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean new file mode 100644 index 000000000000..a01288ae6174 --- /dev/null +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.DTreeMap.Internal.Lemmas +import Std.Data.DTreeMap.Raw + +/-! +# API lemmas for `DTreeMap.Raw` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +open Std.DTreeMap.Internal + +universe u v + +namespace Std.DTreeMap.Raw + +attribute [local instance] TransOrd.ofTransCmp + +variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp} + +theorem isEmpty_empty : (empty : DTreeMap.Raw α β cmp).isEmpty := + Impl.isEmpty_empty + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + Impl.mem_iff_contains + +theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : + t.contains k = t.contains k' := + Impl.contains_congr h hab + +theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := + Impl.mem_congr h hab + +theorem contains_empty {k : α} : (empty : DTreeMap.Raw α β cmp).contains k = false := + Impl.contains_empty + +theorem mem_empty {k : α} : k ∉ (empty : DTreeMap.Raw α β cmp) := + Impl.mem_empty + +theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insert k v).isEmpty = false := + Impl.isEmpty_insertSlow h + +theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := + Impl.contains_insertSlow h + +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 + +theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).contains a = (cmp k a != .eq && t.contains a) := + Impl.contains_eraseSlow h + +theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).contains a → t.contains a := + Impl.contains_of_contains_eraseSlow h + +theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k).size = if t.contains k then t.size - 1 else t.size := + Impl.sizeSlow_erase h + +theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k).size ≤ t.size := + Impl.sizeSlow_erase_le h + +theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : + t.size ≤ (t.erase k).size + 1 := + Impl.sizeSlow_le_size_erase h + +end Std.DTreeMap.Raw diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean new file mode 100644 index 000000000000..2126bc9db192 --- /dev/null +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.DTreeMap.Lemmas +import Std.Data.TreeMap.Basic + +/-! +# API lemmas for `TreeMap` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +open Std.DTreeMap.Internal + +universe u v + +namespace Std.TreeMap + +variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap α β cmp} + +theorem isEmpty_empty : (empty : TreeMap α β cmp).isEmpty := + DTreeMap.isEmpty_empty + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + DTreeMap.mem_iff_contains + +theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : + t.contains k = t.contains k' := + DTreeMap.contains_congr hab + +theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := + DTreeMap.mem_congr hab + +theorem contains_empty {k : α} : (empty : TreeMap α β cmp).contains k = false := + DTreeMap.contains_empty + +theorem mem_empty {k : α} : k ∉ (empty : TreeMap α β cmp) := + DTreeMap.mem_empty + +theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} : + (t.insert k v).isEmpty = false := + DTreeMap.isEmpty_insert + +theorem contains_insert [h : TransCmp cmp] {k a : α} {v : β} : + (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := + DTreeMap.contains_insert + +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 + +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/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean new file mode 100644 index 000000000000..5d42c6ec3d2b --- /dev/null +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.DTreeMap.RawLemmas +import Std.Data.TreeMap.Raw + +/-! +# API lemmas for `TreeMap.Raw` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +universe u v + +namespace Std.TreeMap.Raw + +variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap.Raw α β cmp} + +attribute [local instance] TransOrd.ofTransCmp + +theorem isEmpty_empty : (empty : TreeMap.Raw α β cmp).isEmpty := + DTreeMap.Raw.isEmpty_empty + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + DTreeMap.Raw.mem_iff_contains + +theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : + t.contains k = t.contains k' := + DTreeMap.Raw.contains_congr h hab + +theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := + DTreeMap.Raw.mem_congr h hab + +theorem contains_empty {k : α} : (empty : TreeMap.Raw α β cmp).contains k = false := + DTreeMap.Raw.contains_empty + +theorem mem_empty {k : α} : k ∉ (empty : TreeMap.Raw α β cmp) := + DTreeMap.Raw.mem_empty + +theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insert k v).isEmpty = false := + DTreeMap.Raw.isEmpty_insert h + +theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := + DTreeMap.Raw.contains_insert h + +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 + +theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).contains a = (cmp k a != .eq && t.contains a) := + DTreeMap.Raw.contains_erase h + +theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).contains a → t.contains a := + DTreeMap.Raw.contains_of_contains_erase h + +theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k).size = if t.contains k then t.size - 1 else t.size := + DTreeMap.Raw.size_erase h + +theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k).size ≤ t.size := + DTreeMap.Raw.size_erase_le h + +theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : + t.size ≤ (t.erase k).size + 1 := + DTreeMap.Raw.size_le_size_erase h + +end Std.TreeMap.Raw diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean new file mode 100644 index 000000000000..cd681daf126b --- /dev/null +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.TreeMap.Lemmas +import Std.Data.TreeSet.Basic + +/-! +# API lemmas for `TreeMap` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +open Std.DTreeMap.Internal + +universe u v + +namespace Std.TreeSet + +variable {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} + +theorem isEmpty_empty : (empty : TreeSet α cmp).isEmpty := + TreeMap.isEmpty_empty + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + TreeMap.mem_iff_contains + +theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : + t.contains k = t.contains k' := + TreeMap.contains_congr hab + +theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := + TreeMap.mem_congr hab + +theorem contains_empty {k : α} : (empty : TreeSet α cmp).contains k = false := + TreeMap.contains_empty + +theorem mem_empty {k : α} : k ∉ (empty : TreeSet α cmp) := + TreeMap.mem_empty + +theorem isEmpty_insert [TransCmp cmp] {k : α} : + (t.insert k).isEmpty = false := + TreeMap.isEmpty_insert + +theorem contains_insert [h : TransCmp cmp] (t : TreeSet α cmp) {k a : α} : + (t.insert k).contains a = (cmp k a == .eq || t.contains a) := + TreeMap.contains_insert + +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 + +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 diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean new file mode 100644 index 000000000000..0fb39a631603 --- /dev/null +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +prelude +import Std.Data.TreeMap.RawLemmas +import Std.Data.TreeSet.Raw + +/-! +# API lemmas for `TreeMap.Raw` +-/ + +set_option linter.missingDocs true +set_option autoImplicit false + +universe u v + +namespace Std.TreeSet.Raw + +attribute [local instance] TransOrd.ofTransCmp + +variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeSet.Raw α cmp} + +theorem isEmpty_empty : (empty : TreeSet.Raw α cmp).isEmpty := + TreeMap.Raw.isEmpty_empty + +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + TreeMap.Raw.mem_iff_contains + +theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : + t.contains k = t.contains k' := + TreeMap.Raw.contains_congr h hab + +theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := + TreeMap.Raw.mem_congr h hab + +theorem contains_empty {k : α} : (empty : TreeSet.Raw α cmp).contains k = false := + TreeMap.Raw.contains_empty + +theorem mem_empty {k : α} : k ∉ (empty : TreeSet.Raw α cmp) := + TreeMap.Raw.mem_empty + +theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} : + (t.insert k).isEmpty = false := + TreeMap.Raw.isEmpty_insert h + +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 : α} : + (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 + +theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).contains a = (cmp k a != .eq && t.contains a) := + TreeMap.Raw.contains_erase h + +theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).contains a → t.contains a := + TreeMap.Raw.contains_of_contains_erase h + +theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k).size = if t.contains k then t.size - 1 else t.size := + TreeMap.Raw.size_erase h + +theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k).size ≤ t.size := + TreeMap.Raw.size_erase_le h + +theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : + t.size ≤ (t.erase k).size + 1 := + TreeMap.Raw.size_le_size_erase h + +end Std.TreeSet.Raw From d74ebcde30c98b83a31eb398692f820f5ba83ec8 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 7 Feb 2025 09:09:54 +0100 Subject: [PATCH 02/17] raw lemmas --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 246 ++++++++++++++++++++- src/Std/Data/DTreeMap/RawLemmas.lean | 197 +++++++++++++++-- src/Std/Data/HashSet/RawLemmas.lean | 2 +- src/Std/Data/TreeMap/RawLemmas.lean | 175 ++++++++++++++- src/Std/Data/TreeSet/RawLemmas.lean | 144 ++++++++++-- 5 files changed, 713 insertions(+), 51 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 14d100c2f7ff..913cec9f9271 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -21,12 +21,13 @@ universe u v namespace Std.DTreeMap.Internal.Impl -variable {α : Type u} {β : α → Type v} {_ : Ord α} {t : Impl α β} +variable {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} /-- Internal implementation detail of the tree map -/ scoped macro "wf_trivial" : tactic => `(tactic| repeat (first | apply WF.ordered | apply WF.balanced | apply WF.insert | apply WF.insert! + | apply WF.insertIfNew | apply WF.insertIfNew! | apply WF.erase | apply WF.erase! | apply Ordered.distinctKeys | assumption @@ -44,6 +45,8 @@ private def modifyMap : Std.HashMap Name Name := .ofList [⟨`insert, ``toListModel_insert⟩, ⟨`insert!, ``toListModel_insert!⟩, + ⟨`insertIfNew, ``toListModel_insertIfNew⟩, + ⟨`insertIfNew!, ``toListModel_insertIfNew!⟩, ⟨`erase, ``toListModel_erase⟩, ⟨`erase!, ``toListModel_erase!⟩] @@ -78,6 +81,14 @@ attribute [local instance] equivBEq_of_transOrd theorem isEmpty_empty : isEmpty (empty : Impl α β) := by simp [Impl.apply_isEmpty] +theorem isEmpty_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert k v h.balanced).impl.isEmpty = false := by + simp_to_model [insert] using List.isEmpty_insertEntry + +theorem isEmpty_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert! k v).isEmpty = false := by + simp_to_model [insert!] using List.isEmpty_insertEntry + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := Iff.rfl @@ -88,19 +99,35 @@ theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : k == k') : theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : k == k') : k ∈ t ↔ k' ∈ t := by simp [mem_iff_contains, contains_congr h hab] -theorem contains_empty {k : α} : (empty : Impl α β).contains k = false := by +theorem contains_empty {a : α} : (empty : Impl α β).contains a = false := by simp [contains, empty] -theorem mem_empty {k : α} : k ∉ (empty : Impl α β) := by +theorem not_mem_empty {a : α} : a ∉ (empty : Impl α β) := by simp [mem_iff_contains, contains_empty] -theorem isEmpty_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} : - (t.insert k v h.balanced).impl.isEmpty = false := by - simp_to_model [insert] using List.isEmpty_insertEntry +theorem contains_of_isEmpty [TransOrd α] (h : t.WF) {a : α} : + t.isEmpty → t.contains a = false := by + simp_to_model; empty -theorem isEmpty_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} : - (t.insert! k v).isEmpty = false := by - simp_to_model [insert!] using List.isEmpty_insertEntry +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 @@ -110,6 +137,55 @@ 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 → (k == a) = false → t.contains a := by + 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 → (k == a) = false → t.contains a := by + 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 → (k == a) = false → 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 → (k == a) = false → 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 @@ -134,6 +210,14 @@ 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 @@ -150,6 +234,14 @@ 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 @@ -158,11 +250,19 @@ 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 : α} : +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 @@ -170,7 +270,7 @@ 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 : α} : +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 @@ -178,8 +278,130 @@ 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 : α} : +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 + +/-- +This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. +-/ +theorem contains_of_contains_insertIfNew' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : + (t.insertIfNew k v h.balanced).impl.contains a → ¬((k == a) ∧ t.contains k = false) → t.contains a := by + simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew' + +/-- +This is a restatement of `contains_of_contains_insertIfNew!` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew!`. +-/ +theorem contains_of_contains_insertIfNew!' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : + (t.insertIfNew! k v).contains a → ¬((k == a) ∧ t.contains k = false) → t.contains a := by + simp_to_model [insertIfNew!] using List.containsKey_of_containsKey_insertEntryIfNew' + +/-- +This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. +-/ +theorem mem_of_mem_insertIfNew' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : + a ∈ (t.insertIfNew k v h.balanced).impl → ¬((k == a) ∧ ¬k ∈ t) → a ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h + +/-- +This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. +-/ +theorem mem_of_mem_insertIfNew!' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : + a ∈ t.insertIfNew! k v → ¬((k == a) ∧ ¬k ∈ t) → 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 diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index a01288ae6174..d76dd093ffcd 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -20,13 +20,24 @@ universe u v namespace Std.DTreeMap.Raw -attribute [local instance] TransOrd.ofTransCmp - variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp} +private theorem ext {t t' : Raw α β cmp} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl + +@[simp] theorem isEmpty_empty : (empty : DTreeMap.Raw α β cmp).isEmpty := Impl.isEmpty_empty +@[simp] +theorem isEmpty_emptyc : (∅ : DTreeMap.Raw α β cmp).isEmpty := + Impl.isEmpty_empty + +@[simp] +theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insert k v).isEmpty = false := + Impl.isEmpty_insert! h + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := Impl.mem_iff_contains @@ -37,54 +48,204 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr h hab -theorem contains_empty {k : α} : (empty : DTreeMap.Raw α β cmp).contains k = false := +@[simp] +theorem contains_empty {k : α} : (empty : Raw α β cmp).contains k = false := Impl.contains_empty -theorem mem_empty {k : α} : k ∉ (empty : DTreeMap.Raw α β cmp) := - Impl.mem_empty +@[simp] +theorem not_mem_empty {k : α} : k ∉ (empty : Raw α β cmp) := + Impl.not_mem_empty -theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - (t.insert k v).isEmpty = false := - Impl.isEmpty_insertSlow h +@[simp] +theorem contains_emptyc {k : α} : (∅ : Raw α β cmp).contains k = false := + Impl.contains_empty + +@[simp] +theorem not_mem_emptyc {k : α} : k ∉ (∅ : Raw α β cmp) := + Impl.not_mem_empty + +theorem contains_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty → t.contains a = false := + Impl.contains_of_isEmpty h + +theorem not_mem_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty → a ∉ t := + Impl.not_mem_of_isEmpty h + +theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] (h : t.WF) : + t.isEmpty = false ↔ ∃ a, t.contains a = true := + Impl.isEmpty_eq_false_iff_exists_contains_eq_true h + +theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) : + t.isEmpty = false ↔ ∃ a, a ∈ t := + Impl.isEmpty_eq_false_iff_exists_mem h + +theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) : + t.isEmpty = true ↔ ∀ a, t.contains a = false := + Impl.isEmpty_iff_forall_contains h +theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : + t.isEmpty = true ↔ ∀ a, ¬a ∈ t := + Impl.isEmpty_iff_forall_not_mem h + +@[simp] +theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p t = t.insert p.1 p.2 := + rfl + +@[simp] +theorem singleton_eq_insert {p : (a : α) × β a} : + Singleton.singleton p = (∅ : Raw α β cmp).insert p.1 p.2 := + rfl + +@[simp] theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := - Impl.contains_insertSlow h + Impl.contains_insert! h + +@[simp] +theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + Impl.mem_insert! h + +theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insert k v).contains k := + Impl.contains_insert!_self h + +theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + k ∈ t.insert k v := + Impl.mem_insert!_self h + +theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + Impl.contains_of_contains_insert! h + +theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + Impl.mem_of_mem_insert! h + +@[simp] +theorem size_empty : (empty : Raw α β cmp).size = 0 := + Impl.size_empty + +@[simp] +theorem size_emptyc : (∅ : Raw α β cmp).size = 0 := + Impl.size_empty + +theorem isEmpty_eq_size_eq_zero (h : t.WF) : + letI : BEq Nat := instBEqOfDecidableEq + t.isEmpty = (t.size == 0) := + Impl.isEmpty_eq_size_eq_zero h.out 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 + Impl.size_insert! 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 + Impl.size_le_size_insert! 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 + Impl.size_insert!_le h + +@[simp] +theorem erase_empty {k : α} : + (empty : Raw α β cmp).erase k = empty := + ext <| Impl.erase!_empty (instOrd := ⟨cmp⟩) (k := k) +@[simp] +theorem erase_emptyc {k : α} : + (∅ : Raw α β cmp).erase k = empty := + erase_empty + +@[simp] 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 + Impl.isEmpty_erase! h +@[simp] theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - Impl.contains_eraseSlow h + Impl.contains_erase! h + +@[simp] +theorem mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := + Impl.mem_erase! h theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a → t.contains a := - Impl.contains_of_contains_eraseSlow h + Impl.contains_of_contains_erase! h + +theorem mem_of_mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.erase k → a ∈ t := + Impl.mem_of_mem_erase! h theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).size = if t.contains k then t.size - 1 else t.size := - Impl.sizeSlow_erase h + Impl.size_erase! h theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).size ≤ t.size := - Impl.sizeSlow_erase_le h + Impl.size_erase!_le h theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : t.size ≤ (t.erase k).size + 1 := - Impl.sizeSlow_le_size_erase h + Impl.size_le_size_erase! h + +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew k v).isEmpty = false := + Impl.isEmpty_insertIfNew! h + +@[simp] +theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := + Impl.contains_insertIfNew! h + +@[simp] +theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := + Impl.mem_insertIfNew! h + +theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew k v).contains k := + Impl.contains_insertIfNew!_self h + +theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + k ∈ t.insertIfNew k v := + Impl.mem_insertIfNew!_self h + +theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := + Impl.contains_of_contains_insertIfNew! h + +theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := + Impl.contains_of_contains_insertIfNew! h + +/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the +proof obligation in the statement of `get_insertIfNew`. -/ +theorem contains_of_contains_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := + Impl.contains_of_contains_insertIfNew!' h + +/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the +proof obligation in the statement of `get_insertIfNew`. -/ +theorem mem_of_mem_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : + a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := + Impl.mem_of_mem_insertIfNew!' h + +theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β k} : + (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := + Impl.size_insertIfNew! h + +theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + t.size ≤ (t.insertIfNew k v).size := + Impl.size_le_size_insertIfNew! h + +theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew k v).size ≤ t.size + 1 := + Impl.size_insertIfNew!_le h end Std.DTreeMap.Raw diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 344cd8e2667f..a32e4d3ef43f 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -133,7 +133,7 @@ theorem contains_of_contains_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF HashMap.Raw.contains_of_contains_insertIfNew' h.out /-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation -in the statement of `get_insertIfNew`. -/ +in the statement of `get_insert`. -/ theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} : a ∈ m.insert k → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := HashMap.Raw.mem_of_mem_insertIfNew' h.out diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 5d42c6ec3d2b..3e20e98827c8 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -20,11 +20,22 @@ namespace Std.TreeMap.Raw variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap.Raw α β cmp} -attribute [local instance] TransOrd.ofTransCmp +private theorem ext {t t' : Raw α β cmp} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl +@[simp] theorem isEmpty_empty : (empty : TreeMap.Raw α β cmp).isEmpty := DTreeMap.Raw.isEmpty_empty +@[simp] +theorem isEmpty_emptyc : (∅ : TreeMap.Raw α β cmp).isEmpty := + DTreeMap.Raw.isEmpty_empty + +@[simp] +theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insert k v).isEmpty = false := + DTreeMap.Raw.isEmpty_insert h + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := DTreeMap.Raw.mem_iff_contains @@ -35,20 +46,94 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.Raw.mem_congr h hab -theorem contains_empty {k : α} : (empty : TreeMap.Raw α β cmp).contains k = false := +@[simp] +theorem contains_empty {k : α} : (empty : Raw α β cmp).contains k = false := DTreeMap.Raw.contains_empty -theorem mem_empty {k : α} : k ∉ (empty : TreeMap.Raw α β cmp) := - DTreeMap.Raw.mem_empty +@[simp] +theorem not_mem_empty {k : α} : k ∉ (empty : Raw α β cmp) := + DTreeMap.Raw.not_mem_empty -theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - (t.insert k v).isEmpty = false := - DTreeMap.Raw.isEmpty_insert h +@[simp] +theorem contains_emptyc {k : α} : (∅ : Raw α β cmp).contains k = false := + DTreeMap.Raw.contains_empty + +@[simp] +theorem not_mem_emptyc {k : α} : k ∉ (∅ : Raw α β cmp) := + DTreeMap.Raw.not_mem_empty + +theorem contains_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty → t.contains a = false := + DTreeMap.Raw.contains_of_isEmpty h + +theorem not_mem_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty → a ∉ t := + DTreeMap.Raw.not_mem_of_isEmpty h + +theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] (h : t.WF) : + t.isEmpty = false ↔ ∃ a, t.contains a = true := + DTreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h + +theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) : + t.isEmpty = false ↔ ∃ a, a ∈ t := + DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem h + +theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) : + t.isEmpty = true ↔ ∀ a, t.contains a = false := + DTreeMap.Raw.isEmpty_iff_forall_contains h +theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : + t.isEmpty = true ↔ ∀ a, ¬a ∈ t := + DTreeMap.Raw.isEmpty_iff_forall_not_mem h + +@[simp] +theorem insert_eq_insert {p : α × β} : Insert.insert p t = t.insert p.1 p.2 := + rfl + +@[simp] +theorem singleton_eq_insert {p : α × β} : + Singleton.singleton p = (∅ : Raw α β cmp).insert p.1 p.2 := + rfl + +@[simp] theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β} : (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := DTreeMap.Raw.contains_insert h +@[simp] +theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + DTreeMap.Raw.mem_insert h + +theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insert k v).contains k := + DTreeMap.Raw.contains_insert_self h + +theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + k ∈ t.insert k v := + DTreeMap.Raw.mem_insert_self h + +theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + DTreeMap.Raw.contains_of_contains_insert h + +theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + DTreeMap.Raw.mem_of_mem_insert h + +@[simp] +theorem size_empty : (empty : Raw α β cmp).size = 0 := + DTreeMap.Raw.size_empty + +@[simp] +theorem size_emptyc : (∅ : Raw α β cmp).size = 0 := + DTreeMap.Raw.size_empty + +theorem isEmpty_eq_size_eq_zero (h : t.WF) : + letI : BEq Nat := instBEqOfDecidableEq + t.isEmpty = (t.size == 0) := + DTreeMap.Raw.isEmpty_eq_size_eq_zero h.out + 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 @@ -61,18 +146,39 @@ 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 +@[simp] +theorem erase_empty {k : α} : + (empty : Raw α β cmp).erase k = empty := + ext <| DTreeMap.Raw.erase_empty + +@[simp] +theorem erase_emptyc {k : α} : + (empty : Raw α β cmp).erase k = empty := + erase_empty + +@[simp] 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 +@[simp] theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := DTreeMap.Raw.contains_erase h +@[simp] +theorem mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := + DTreeMap.Raw.mem_erase h + theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a → t.contains a := DTreeMap.Raw.contains_of_contains_erase h +theorem mem_of_mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.erase k → a ∈ t := + DTreeMap.Raw.mem_of_mem_erase h + theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).size = if t.contains k then t.size - 1 else t.size := DTreeMap.Raw.size_erase h @@ -85,4 +191,59 @@ theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : t.size ≤ (t.erase k).size + 1 := DTreeMap.Raw.size_le_size_erase h +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insertIfNew k v).isEmpty = false := + DTreeMap.Raw.isEmpty_insertIfNew h + +@[simp] +theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := + DTreeMap.Raw.contains_insertIfNew h + +@[simp] +theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := + DTreeMap.Raw.mem_insertIfNew h + +theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insertIfNew k v).contains k := + DTreeMap.Raw.contains_insertIfNew_self h + +theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + k ∈ t.insertIfNew k v := + DTreeMap.Raw.mem_insertIfNew_self h + +theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := + DTreeMap.Raw.contains_of_contains_insertIfNew h + +theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := + DTreeMap.Raw.contains_of_contains_insertIfNew h + +/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the +proof obligation in the statement of `get_insertIfNew`. -/ +theorem contains_of_contains_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := + DTreeMap.Raw.contains_of_contains_insertIfNew' h + +/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the +proof obligation in the statement of `get_insertIfNew`. -/ +theorem mem_of_mem_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : + a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := + DTreeMap.Raw.mem_of_mem_insertIfNew' h + +theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β} : + (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := + DTreeMap.Raw.size_insertIfNew h + +theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + t.size ≤ (t.insertIfNew k v).size := + DTreeMap.Raw.size_le_size_insertIfNew h + +theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insertIfNew k v).size ≤ t.size + 1 := + DTreeMap.Raw.size_insertIfNew_le h + end Std.TreeMap.Raw diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 0fb39a631603..2dae1ac8b5de 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -18,13 +18,24 @@ universe u v namespace Std.TreeSet.Raw -attribute [local instance] TransOrd.ofTransCmp - variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeSet.Raw α cmp} -theorem isEmpty_empty : (empty : TreeSet.Raw α cmp).isEmpty := +private theorem ext {t t' : Raw α cmp} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl + +@[simp] +theorem isEmpty_empty : (empty : Raw α cmp).isEmpty := + TreeMap.Raw.isEmpty_empty + +@[simp] +theorem isEmpty_emptyc : (∅ : Raw α cmp).isEmpty := TreeMap.Raw.isEmpty_empty +@[simp] +theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} : + (t.insert k).isEmpty = false := + TreeMap.Raw.isEmpty_insertIfNew h + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := TreeMap.Raw.mem_iff_contains @@ -35,44 +46,151 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := TreeMap.Raw.mem_congr h hab -theorem contains_empty {k : α} : (empty : TreeSet.Raw α cmp).contains k = false := +@[simp] +theorem contains_empty {k : α} : (empty : Raw α cmp).contains k = false := TreeMap.Raw.contains_empty -theorem mem_empty {k : α} : k ∉ (empty : TreeSet.Raw α cmp) := - TreeMap.Raw.mem_empty +@[simp] +theorem not_mem_empty {k : α} : k ∉ (empty : Raw α cmp) := + TreeMap.Raw.not_mem_empty -theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} : - (t.insert k).isEmpty = false := - TreeMap.Raw.isEmpty_insert h +@[simp] +theorem contains_emptyc {k : α} : (∅ : Raw α cmp).contains k = false := + TreeMap.Raw.contains_empty + +@[simp] +theorem not_mem_emptyc {k : α} : k ∉ (∅ : Raw α cmp) := + TreeMap.Raw.not_mem_empty + +theorem contains_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty → t.contains a = false := + DTreeMap.Raw.contains_of_isEmpty h +theorem not_mem_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty → a ∉ t := + DTreeMap.Raw.not_mem_of_isEmpty h + +theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] (h : t.WF) : + t.isEmpty = false ↔ ∃ a, t.contains a = true := + DTreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h + +theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) : + t.isEmpty = false ↔ ∃ a, a ∈ t := + DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem h + +theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) : + t.isEmpty = true ↔ ∀ a, t.contains a = false := + DTreeMap.Raw.isEmpty_iff_forall_contains h + +theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : + t.isEmpty = true ↔ ∀ a, ¬a ∈ t := + DTreeMap.Raw.isEmpty_iff_forall_not_mem h + +@[simp] +theorem insert_eq_insert {p : α} : Insert.insert p t = t.insert p := + rfl + +@[simp] +theorem singleton_eq_insert {p : α} : + Singleton.singleton p = (∅ : Raw α cmp).insert p := + rfl + +@[simp] 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 + TreeMap.Raw.contains_insertIfNew h + +@[simp] +theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.insert k ↔ cmp k a == .eq ∨ a ∈ t := + TreeMap.Raw.mem_insertIfNew h + +theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} : + (t.insert k).contains k := + TreeMap.Raw.contains_insertIfNew_self h + +theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.insert k := + TreeMap.Raw.mem_insertIfNew_self h + +theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} : + (t.insert k).contains a → (cmp k a == .eq) = false → t.contains a := + TreeMap.Raw.contains_of_contains_insertIfNew h + +theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.insert k → (cmp k a == .eq) = false → a ∈ t := + TreeMap.Raw.mem_of_mem_insertIfNew h + +/-- This is a restatement of `contains_of_contains_insert` that is written to exactly match the +proof obligation in the statement of `get_insert`. -/ +theorem contains_of_contains_insert' [TransCmp cmp] (h : t.WF) {k a : α} : + (t.insert k).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := + TreeMap.Raw.contains_of_contains_insertIfNew' h + +/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the +proof obligation in the statement of `get_insert`. -/ +theorem mem_of_mem_insert' [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.insert k → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := + TreeMap.Raw.mem_of_mem_insertIfNew' h + +@[simp] +theorem size_empty : (empty : Raw α cmp).size = 0 := + TreeMap.Raw.size_empty + +@[simp] +theorem size_emptyc : (∅ : Raw α cmp).size = 0 := + TreeMap.Raw.size_empty + +theorem isEmpty_eq_size_eq_zero (h : t.WF) : + letI : BEq Nat := instBEqOfDecidableEq + t.isEmpty = (t.size == 0) := + DTreeMap.Raw.isEmpty_eq_size_eq_zero h.out 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 + TreeMap.Raw.size_insertIfNew 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 + TreeMap.Raw.size_le_size_insertIfNew h theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} : (t.insert k).size ≤ t.size + 1 := - DTreeMap.Raw.size_insert_le h + TreeMap.Raw.size_insertIfNew_le h + +@[simp] +theorem erase_empty {k : α} : + (empty : Raw α cmp).erase k = empty := + ext <| TreeMap.Raw.erase_empty + +@[simp] +theorem erase_emptyc {k : α} : + (empty : Raw α cmp).erase k = empty := + erase_empty +@[simp] 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 +@[simp] theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := TreeMap.Raw.contains_erase h +@[simp] +theorem mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := + TreeMap.Raw.mem_erase h + theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a → t.contains a := TreeMap.Raw.contains_of_contains_erase h +theorem mem_of_mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : + a ∈ t.erase k → a ∈ t := + TreeMap.Raw.mem_of_mem_erase h + theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).size = if t.contains k then t.size - 1 else t.size := TreeMap.Raw.size_erase h From cfbaca91a6a0aaa503d40a2d1fc698f97dd5dfa3 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 7 Feb 2025 09:30:20 +0100 Subject: [PATCH 03/17] dtreemap lemmas --- src/Std/Data/DTreeMap/Lemmas.lean | 175 +++++++++++++++++++++++++-- src/Std/Data/DTreeMap/RawLemmas.lean | 1 - src/Std/Data/TreeMap/RawLemmas.lean | 1 - src/Std/Data/TreeSet/RawLemmas.lean | 1 - 4 files changed, 168 insertions(+), 10 deletions(-) diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 5f5c57877e86..465a7d99640a 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -20,13 +20,24 @@ universe u v namespace Std.DTreeMap -attribute [local instance] TransOrd.ofTransCmp - variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} +private theorem ext {t t' : DTreeMap α β cmp} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl + +@[simp] theorem isEmpty_empty : (empty : DTreeMap α β cmp).isEmpty := Impl.isEmpty_empty +@[simp] +theorem isEmpty_emptyc : (∅ : DTreeMap α β cmp).isEmpty := + Impl.isEmpty_empty + +@[simp] +theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} : + (t.insert k v).isEmpty = false := + Impl.isEmpty_insert t.wf + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := Impl.mem_iff_contains @@ -37,20 +48,93 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr t.wf hab +@[simp] theorem contains_empty {k : α} : (empty : DTreeMap α β cmp).contains k = false := Impl.contains_empty -theorem mem_empty {k : α} : k ∉ (empty : DTreeMap α β cmp) := - Impl.mem_empty +@[simp] +theorem not_mem_empty {k : α} : k ∉ (empty : DTreeMap α β cmp) := + Impl.not_mem_empty -theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} : - (t.insert k v).isEmpty = false := - Impl.isEmpty_insert t.wf +@[simp] +theorem contains_emptyc {k : α} : (∅ : DTreeMap α β cmp).contains k = false := + Impl.contains_empty + +@[simp] +theorem not_mem_emptyc {k : α} : k ∉ (∅ : DTreeMap α β cmp) := + Impl.not_mem_empty + +theorem contains_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty → t.contains a = false := + Impl.contains_of_isEmpty t.wf + +theorem not_mem_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty → a ∉ t := + Impl.not_mem_of_isEmpty t.wf + +theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] : + t.isEmpty = false ↔ ∃ a, t.contains a = true := + Impl.isEmpty_eq_false_iff_exists_contains_eq_true t.wf + +theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] : + t.isEmpty = false ↔ ∃ a, a ∈ t := + Impl.isEmpty_eq_false_iff_exists_mem t.wf +theorem isEmpty_iff_forall_contains [TransCmp cmp] : + t.isEmpty = true ↔ ∀ a, t.contains a = false := + Impl.isEmpty_iff_forall_contains t.wf + +theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : + t.isEmpty = true ↔ ∀ a, ¬a ∈ t := + Impl.isEmpty_iff_forall_not_mem t.wf + +@[simp] +theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p t = t.insert p.1 p.2 := + rfl + +@[simp] +theorem singleton_eq_insert {p : (a : α) × β a} : + Singleton.singleton p = (∅ : DTreeMap α β cmp).insert p.1 p.2 := + rfl + +@[simp] theorem contains_insert [TransCmp cmp] {k k' : α} {v : β k} : (t.insert k v).contains k' = (cmp k k' == .eq || t.contains k') := Impl.contains_insert t.wf +@[simp] +theorem mem_insert [TransCmp cmp] {k a : α} {v : β k} : + a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + Impl.mem_insert t.wf + +theorem contains_insert_self [TransCmp cmp] {k : α} {v : β k} : + (t.insert k v).contains k := + Impl.contains_insert_self t.wf + +theorem mem_insert_self [TransCmp cmp] {k : α} {v : β k} : + k ∈ t.insert k v := + Impl.mem_insert_self t.wf + +theorem contains_of_contains_insert [TransCmp cmp] {k a : α} {v : β k} : + (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + Impl.contains_of_contains_insert t.wf + +theorem mem_of_mem_insert [TransCmp cmp] {k a : α} {v : β k} : + a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + Impl.mem_of_mem_insert t.wf + +@[simp] +theorem size_empty : (empty : DTreeMap α β cmp).size = 0 := + Impl.size_empty + +@[simp] +theorem size_emptyc : (∅ : DTreeMap α β cmp).size = 0 := + Impl.size_empty + +theorem isEmpty_eq_size_eq_zero : + t.isEmpty = (t.size == 0) := + Impl.isEmpty_eq_size_eq_zero t.wf + 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 @@ -63,18 +147,39 @@ theorem size_insert_le [TransCmp cmp] {k : α} {v : β k} : (t.insert k v).size ≤ t.size + 1 := Impl.size_insert_le t.wf +@[simp] +theorem erase_empty {k : α} : + (empty : DTreeMap α β cmp).erase k = empty := + ext <| Impl.erase_empty (instOrd := ⟨cmp⟩) (k := k) + +@[simp] +theorem erase_emptyc {k : α} : + (∅ : DTreeMap α β cmp).erase k = empty := + erase_empty + +@[simp] theorem isEmpty_erase [TransCmp cmp] {k : α} : (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := Impl.isEmpty_erase t.wf +@[simp] theorem contains_erase [TransCmp cmp] {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := Impl.contains_erase t.wf +@[simp] +theorem mem_erase [TransCmp cmp] {k a : α} : + a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := + Impl.mem_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 mem_of_mem_erase [TransCmp cmp] {k a : α} : + a ∈ t.erase k → a ∈ t := + Impl.mem_of_mem_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 @@ -87,4 +192,60 @@ theorem size_le_size_erase [TransCmp cmp] {k : α} : t.size ≤ (t.erase k).size + 1 := Impl.size_le_size_erase t.wf +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β k} : + (t.insertIfNew k v).isEmpty = false := + Impl.isEmpty_insertIfNew t.wf + +@[simp] +theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : + (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := + Impl.contains_insertIfNew t.wf + +@[simp] +theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : + a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := + Impl.mem_insertIfNew t.wf + +@[simp] +theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} : + (t.insertIfNew k v).contains k := + Impl.contains_insertIfNew_self t.wf + +theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} : + k ∈ t.insertIfNew k v := + Impl.mem_insertIfNew_self t.wf + +theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : + (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := + Impl.contains_of_contains_insertIfNew t.wf + +theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : + a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := + Impl.contains_of_contains_insertIfNew t.wf + +/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. -/ +theorem contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} {v : β k} : + (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := + Impl.contains_of_contains_insertIfNew' t.wf + +/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. -/ +theorem mem_of_mem_insertIfNew' [TransCmp cmp] {k a : α} {v : β k} : + a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := + Impl.mem_of_mem_insertIfNew' t.wf + +theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β k} : + (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := + Impl.size_insertIfNew t.wf + +theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β k} : + t.size ≤ (t.insertIfNew k v).size := + Impl.size_le_size_insertIfNew t.wf + +theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β k} : + (t.insertIfNew k v).size ≤ t.size + 1 := + Impl.size_insertIfNew_le t.wf + end Std.DTreeMap diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index d76dd093ffcd..de3602047bdd 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -132,7 +132,6 @@ theorem size_emptyc : (∅ : Raw α β cmp).size = 0 := Impl.size_empty theorem isEmpty_eq_size_eq_zero (h : t.WF) : - letI : BEq Nat := instBEqOfDecidableEq t.isEmpty = (t.size == 0) := Impl.isEmpty_eq_size_eq_zero h.out diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 3e20e98827c8..4a0ef4c5451e 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -130,7 +130,6 @@ theorem size_emptyc : (∅ : Raw α β cmp).size = 0 := DTreeMap.Raw.size_empty theorem isEmpty_eq_size_eq_zero (h : t.WF) : - letI : BEq Nat := instBEqOfDecidableEq t.isEmpty = (t.size == 0) := DTreeMap.Raw.isEmpty_eq_size_eq_zero h.out diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 2dae1ac8b5de..7fb3cfcefead 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -142,7 +142,6 @@ theorem size_emptyc : (∅ : Raw α cmp).size = 0 := TreeMap.Raw.size_empty theorem isEmpty_eq_size_eq_zero (h : t.WF) : - letI : BEq Nat := instBEqOfDecidableEq t.isEmpty = (t.size == 0) := DTreeMap.Raw.isEmpty_eq_size_eq_zero h.out From 886465e2d571cf2e87e7a940b4546cdb011254ac Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 7 Feb 2025 09:43:41 +0100 Subject: [PATCH 04/17] treemap lemmas --- src/Std/Data/TreeMap/Lemmas.lean | 173 ++++++++++++++++++++++++++++++- 1 file changed, 168 insertions(+), 5 deletions(-) diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 2126bc9db192..8a2d1f4927a6 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -22,9 +22,22 @@ namespace Std.TreeMap variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap α β cmp} +private theorem ext {t t' : TreeMap α β cmp} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl + +@[simp] theorem isEmpty_empty : (empty : TreeMap α β cmp).isEmpty := DTreeMap.isEmpty_empty +@[simp] +theorem isEmpty_emptyc : (∅ : TreeMap α β cmp).isEmpty := + DTreeMap.isEmpty_empty + +@[simp] +theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} : + (t.insert k v).isEmpty = false := + DTreeMap.isEmpty_insert + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := DTreeMap.mem_iff_contains @@ -35,20 +48,93 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.mem_congr hab +@[simp] theorem contains_empty {k : α} : (empty : TreeMap α β cmp).contains k = false := DTreeMap.contains_empty -theorem mem_empty {k : α} : k ∉ (empty : TreeMap α β cmp) := - DTreeMap.mem_empty +@[simp] +theorem not_mem_empty {k : α} : k ∉ (empty : TreeMap α β cmp) := + DTreeMap.not_mem_empty -theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} : - (t.insert k v).isEmpty = false := - DTreeMap.isEmpty_insert +@[simp] +theorem contains_emptyc {k : α} : (∅ : TreeMap α β cmp).contains k = false := + DTreeMap.contains_empty + +@[simp] +theorem not_mem_emptyc {k : α} : k ∉ (∅ : TreeMap α β cmp) := + DTreeMap.not_mem_empty + +theorem contains_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty → t.contains a = false := + DTreeMap.contains_of_isEmpty + +theorem not_mem_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty → a ∉ t := + DTreeMap.not_mem_of_isEmpty + +theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] : + t.isEmpty = false ↔ ∃ a, t.contains a = true := + DTreeMap.isEmpty_eq_false_iff_exists_contains_eq_true + +theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] : + t.isEmpty = false ↔ ∃ a, a ∈ t := + DTreeMap.isEmpty_eq_false_iff_exists_mem + +theorem isEmpty_iff_forall_contains [TransCmp cmp] : + t.isEmpty = true ↔ ∀ a, t.contains a = false := + DTreeMap.isEmpty_iff_forall_contains +theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : + t.isEmpty = true ↔ ∀ a, ¬a ∈ t := + DTreeMap.isEmpty_iff_forall_not_mem + +@[simp] +theorem insert_eq_insert {p : α × β} : Insert.insert p t = t.insert p.1 p.2 := + rfl + +@[simp] +theorem singleton_eq_insert {p : α × β} : + Singleton.singleton p = (∅ : TreeMap α β cmp).insert p.1 p.2 := + rfl + +@[simp] theorem contains_insert [h : TransCmp cmp] {k a : α} {v : β} : (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := DTreeMap.contains_insert +@[simp] +theorem mem_insert [TransCmp cmp] {k a : α} {v : β} : + a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + DTreeMap.mem_insert + +theorem contains_insert_self [TransCmp cmp] {k : α} {v : β} : + (t.insert k v).contains k := + DTreeMap.contains_insert_self + +theorem mem_insert_self [TransCmp cmp] {k : α} {v : β} : + k ∈ t.insert k v := + DTreeMap.mem_insert_self + +theorem contains_of_contains_insert [TransCmp cmp] {k a : α} {v : β} : + (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + DTreeMap.contains_of_contains_insert + +theorem mem_of_mem_insert [TransCmp cmp] {k a : α} {v : β} : + a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + DTreeMap.mem_of_mem_insert + +@[simp] +theorem size_empty : (empty : TreeMap α β cmp).size = 0 := + DTreeMap.size_empty + +@[simp] +theorem size_emptyc : (∅ : TreeMap α β cmp).size = 0 := + DTreeMap.size_empty + +theorem isEmpty_eq_size_eq_zero : + t.isEmpty = (t.size == 0) := + DTreeMap.isEmpty_eq_size_eq_zero + 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 @@ -61,18 +147,39 @@ theorem size_insert_le [TransCmp cmp] {k : α} {v : β} : (t.insert k v).size ≤ t.size + 1 := DTreeMap.size_insert_le +@[simp] +theorem erase_empty {k : α} : + (empty : TreeMap α β cmp).erase k = empty := + ext <| DTreeMap.erase_empty + +@[simp] +theorem erase_emptyc {k : α} : + (∅ : TreeMap α β cmp).erase k = empty := + erase_empty + +@[simp] theorem isEmpty_erase [TransCmp cmp] {k : α} : (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := DTreeMap.isEmpty_erase +@[simp] theorem contains_erase [TransCmp cmp] {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := DTreeMap.contains_erase +@[simp] +theorem mem_erase [TransCmp cmp] {k a : α} : + a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := + DTreeMap.mem_erase + theorem contains_of_contains_erase [TransCmp cmp] {k a : α} : (t.erase k).contains a → t.contains a := DTreeMap.contains_of_contains_erase +theorem mem_of_mem_erase [TransCmp cmp] {k a : α} : + a ∈ t.erase k → a ∈ t := + DTreeMap.mem_of_mem_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 @@ -85,4 +192,60 @@ theorem size_le_size_erase [TransCmp cmp] {k : α} : t.size ≤ (t.erase k).size + 1 := DTreeMap.size_le_size_erase +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β} : + (t.insertIfNew k v).isEmpty = false := + DTreeMap.isEmpty_insertIfNew + +@[simp] +theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} : + (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := + DTreeMap.contains_insertIfNew + +@[simp] +theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} : + a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := + DTreeMap.mem_insertIfNew + +@[simp] +theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β} : + (t.insertIfNew k v).contains k := + DTreeMap.contains_insertIfNew_self + +theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β} : + k ∈ t.insertIfNew k v := + DTreeMap.mem_insertIfNew_self + +theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} : + (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := + DTreeMap.contains_of_contains_insertIfNew + +theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} : + a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := + DTreeMap.contains_of_contains_insertIfNew + +/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. -/ +theorem contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} {v : β} : + (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := + DTreeMap.contains_of_contains_insertIfNew' + +/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match +the proof obligation in the statement of `get_insertIfNew`. -/ +theorem mem_of_mem_insertIfNew' [TransCmp cmp] {k a : α} {v : β} : + a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := + DTreeMap.mem_of_mem_insertIfNew' + +theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β} : + (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := + DTreeMap.size_insertIfNew + +theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β} : + t.size ≤ (t.insertIfNew k v).size := + DTreeMap.size_le_size_insertIfNew + +theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} : + (t.insertIfNew k v).size ≤ t.size + 1 := + DTreeMap.size_insertIfNew_le + end Std.TreeMap From 33b795fbbaf75c435a5afd0ff75f0c9d86023e92 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 7 Feb 2025 09:54:34 +0100 Subject: [PATCH 05/17] treeset lemmas --- src/Std/Data/TreeSet/Lemmas.lean | 130 +++++++++++++++++++++++++--- src/Std/Data/TreeSet/RawLemmas.lean | 2 +- 2 files changed, 121 insertions(+), 11 deletions(-) diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index cd681daf126b..b28039e6fc5a 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -22,9 +22,22 @@ namespace Std.TreeSet variable {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} +private theorem ext {t t' : TreeSet α cmp} : t.inner = t'.inner → t = t' := by + cases t; cases t'; rintro rfl; rfl + +@[simp] theorem isEmpty_empty : (empty : TreeSet α cmp).isEmpty := TreeMap.isEmpty_empty +@[simp] +theorem isEmpty_emptyc : (∅ : TreeSet α cmp).isEmpty := + TreeMap.isEmpty_empty + +@[simp] +theorem isEmpty_insert [TransCmp cmp] {k : α} : + (t.insert k).isEmpty = false := + TreeMap.isEmpty_insertIfNew + theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := TreeMap.mem_iff_contains @@ -35,36 +48,133 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := TreeMap.mem_congr hab +@[simp] theorem contains_empty {k : α} : (empty : TreeSet α cmp).contains k = false := TreeMap.contains_empty -theorem mem_empty {k : α} : k ∉ (empty : TreeSet α cmp) := - TreeMap.mem_empty +@[simp] +theorem not_mem_empty {k : α} : k ∉ (empty : TreeSet α cmp) := + TreeMap.not_mem_empty -theorem isEmpty_insert [TransCmp cmp] {k : α} : - (t.insert k).isEmpty = false := - TreeMap.isEmpty_insert +@[simp] +theorem contains_emptyc {k : α} : (∅ : TreeSet α cmp).contains k = false := + TreeMap.contains_empty + +@[simp] +theorem not_mem_emptyc {k : α} : k ∉ (∅ : TreeSet α cmp) := + TreeMap.not_mem_empty + +theorem contains_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty → t.contains a = false := + DTreeMap.contains_of_isEmpty + +theorem not_mem_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty → a ∉ t := + DTreeMap.not_mem_of_isEmpty + +theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] : + t.isEmpty = false ↔ ∃ a, t.contains a = true := + DTreeMap.isEmpty_eq_false_iff_exists_contains_eq_true + +theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] : + t.isEmpty = false ↔ ∃ a, a ∈ t := + DTreeMap.isEmpty_eq_false_iff_exists_mem + +theorem isEmpty_iff_forall_contains [TransCmp cmp] : + t.isEmpty = true ↔ ∀ a, t.contains a = false := + DTreeMap.isEmpty_iff_forall_contains -theorem contains_insert [h : TransCmp cmp] (t : TreeSet α cmp) {k a : α} : +theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : + t.isEmpty = true ↔ ∀ a, ¬a ∈ t := + DTreeMap.isEmpty_iff_forall_not_mem + +@[simp] +theorem insert_eq_insert {p : α} : Insert.insert p t = t.insert p := + rfl + +@[simp] +theorem singleton_eq_insert {p : α} : + Singleton.singleton p = (∅ : TreeSet α cmp).insert p := + rfl + +@[simp] +theorem contains_insert [h : TransCmp cmp] {k a : α} : (t.insert k).contains a = (cmp k a == .eq || t.contains a) := - TreeMap.contains_insert + TreeMap.contains_insertIfNew + +@[simp] +theorem mem_insert [TransCmp cmp] {k a : α} : + a ∈ t.insert k ↔ cmp k a == .eq ∨ a ∈ t := + TreeMap.mem_insertIfNew + +theorem contains_insert_self [TransCmp cmp] {k : α} : + (t.insert k).contains k := + TreeMap.contains_insertIfNew_self + +theorem mem_insert_self [TransCmp cmp] {k : α} : + k ∈ t.insert k := + TreeMap.mem_insertIfNew_self + +theorem contains_of_contains_insert [TransCmp cmp] {k a : α} : + (t.insert k).contains a → (cmp k a == .eq) = false → t.contains a := + TreeMap.contains_of_contains_insertIfNew + +theorem mem_of_mem_insert [TransCmp cmp] {k a : α} : + a ∈ t.insert k → (cmp k a == .eq) = false → a ∈ t := + TreeMap.mem_of_mem_insertIfNew + +/-- This is a restatement of `contains_of_contains_insert` that is written to exactly match the +proof obligation in the statement of `get_insert`. -/ +theorem contains_of_contains_insert' [TransCmp cmp] {k a : α} : + (t.insert k).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := + TreeMap.contains_of_contains_insertIfNew' + +/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the +proof obligation in the statement of `get_insert`. -/ +theorem mem_of_mem_insert' [TransCmp cmp] {k a : α} : + a ∈ t.insert k → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := + TreeMap.mem_of_mem_insertIfNew' + +@[simp] +theorem size_empty : (empty : TreeSet α cmp).size = 0 := + TreeMap.size_empty + +@[simp] +theorem size_emptyc : (∅ : TreeSet α cmp).size = 0 := + TreeMap.size_empty + +theorem isEmpty_eq_size_eq_zero : + t.isEmpty = (t.size == 0) := + TreeMap.isEmpty_eq_size_eq_zero theorem size_insert [TransCmp cmp] {k : α} : (t.insert k).size = if t.contains k then t.size else t.size + 1 := - TreeMap.size_insert + TreeMap.size_insertIfNew theorem size_le_size_insert [TransCmp cmp] {k : α} : t.size ≤ (t.insert k).size := - TreeMap.size_le_size_insert + TreeMap.size_le_size_insertIfNew theorem size_insert_le [TransCmp cmp] {k : α} : (t.insert k).size ≤ t.size + 1 := - TreeMap.size_insert_le + TreeMap.size_insertIfNew_le + +@[simp] +theorem erase_empty {k : α} : + (empty : TreeSet α cmp).erase k = empty := + ext <| TreeMap.erase_empty + +@[simp] +theorem erase_emptyc {k : α} : + (empty : TreeSet α cmp).erase k = empty := + erase_empty +@[simp] theorem isEmpty_erase [TransCmp cmp] {k : α} : (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := TreeMap.isEmpty_erase +@[simp] theorem contains_erase [TransCmp cmp] {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := DTreeMap.contains_erase diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 7fb3cfcefead..6da1084988ce 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -143,7 +143,7 @@ theorem size_emptyc : (∅ : Raw α cmp).size = 0 := theorem isEmpty_eq_size_eq_zero (h : t.WF) : t.isEmpty = (t.size == 0) := - DTreeMap.Raw.isEmpty_eq_size_eq_zero h.out + TreeMap.Raw.isEmpty_eq_size_eq_zero h.out theorem size_insert [TransCmp cmp] (h : t.WF) {k : α} : (t.insert k).size = if t.contains k then t.size else t.size + 1 := From 53576495401b35c42ca0badd7d835ad0e9c0341b Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 13:21:03 +0100 Subject: [PATCH 06/17] wip --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 913cec9f9271..4d14e1f54c35 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -5,7 +5,7 @@ Authors: Markus Himmel -/ prelude import Std.Data.HashMap.Basic -import Std.Data.DTreeMap.Internal.WF +import Std.Data.DTreeMap.Internal.WF.Lemmas /-! # API lemmas for `DTreeMap.Impl` @@ -39,7 +39,7 @@ scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] open Lean private def queryNames : Array Name := - #[``apply_isEmpty, ``apply_contains, ``apply_size] + #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length] private def modifyMap : Std.HashMap Name Name := .ofList @@ -79,7 +79,7 @@ attribute [local instance] beqOfOrd attribute [local instance] equivBEq_of_transOrd theorem isEmpty_empty : isEmpty (empty : Impl α β) := by - simp [Impl.apply_isEmpty] + simp [Impl.isEmpty_eq_isEmpty] theorem isEmpty_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.insert k v h.balanced).impl.isEmpty = false := by From f7013aa524d77daaf5ba5fa309ad654dca2596c9 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 14:27:29 +0100 Subject: [PATCH 07/17] extend tests --- tests/lean/run/treemap.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/tests/lean/run/treemap.lean b/tests/lean/run/treemap.lean index 94e1a967bba2..f91b717c298a 100644 --- a/tests/lean/run/treemap.lean +++ b/tests/lean/run/treemap.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Paul Reichert -/ import Std.Data.TreeSet.Basic +import Std.Data.TreeSet.Lemmas open Std @@ -29,3 +30,12 @@ example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := (mkTreeMapSingleton a b)[a]? + +example [TransOrd α] (a : α) (b : β) : (mkTreeMapSingleton a b).contains a := by + simp [mkTreeMapSingleton, Id.run] + +example [TransOrd α] (a : α) (b : β) : (mkDTreeMapSingleton a b).contains a := by + simp [mkDTreeMapSingleton, Id.run] + +example [TransOrd α] (a : α) : (mkTreeSetSingleton a).contains a := by + simp [mkTreeSetSingleton, Id.run] From ad66d23b0c1155e8f6e5839ff22b5b33550d2980 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 14:58:02 +0100 Subject: [PATCH 08/17] wip --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 36 ++-------------------- src/Std/Data/DTreeMap/Lemmas.lean | 14 +-------- 2 files changed, 3 insertions(+), 47 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 4d14e1f54c35..42cdcef87dd0 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -138,11 +138,11 @@ theorem contains_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β k} : 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 + 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 + 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} : @@ -344,38 +344,6 @@ 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 -/-- -This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. --/ -theorem contains_of_contains_insertIfNew' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : - (t.insertIfNew k v h.balanced).impl.contains a → ¬((k == a) ∧ t.contains k = false) → t.contains a := by - simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew' - -/-- -This is a restatement of `contains_of_contains_insertIfNew!` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew!`. --/ -theorem contains_of_contains_insertIfNew!' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : - (t.insertIfNew! k v).contains a → ¬((k == a) ∧ t.contains k = false) → t.contains a := by - simp_to_model [insertIfNew!] using List.containsKey_of_containsKey_insertEntryIfNew' - -/-- -This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. --/ -theorem mem_of_mem_insertIfNew' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : - a ∈ (t.insertIfNew k v h.balanced).impl → ¬((k == a) ∧ ¬k ∈ t) → a ∈ t := by - simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h - -/-- -This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. --/ -theorem mem_of_mem_insertIfNew!' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insertIfNew! k v → ¬((k == a) ∧ ¬k ∈ t) → 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] diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 465a7d99640a..2d0ed856ac5f 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -104,7 +104,7 @@ theorem contains_insert [TransCmp cmp] {k k' : α} {v : β k} : @[simp] theorem mem_insert [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := Impl.mem_insert t.wf theorem contains_insert_self [TransCmp cmp] {k : α} {v : β k} : @@ -224,18 +224,6 @@ theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := Impl.contains_of_contains_insertIfNew t.wf -/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. -/ -theorem contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} {v : β k} : - (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := - Impl.contains_of_contains_insertIfNew' t.wf - -/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. -/ -theorem mem_of_mem_insertIfNew' [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := - Impl.mem_of_mem_insertIfNew' t.wf - theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β k} : (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := Impl.size_insertIfNew t.wf From 645e433234bd230a26f3732f229e8b856f3d4d88 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 15:59:38 +0100 Subject: [PATCH 09/17] cleanups and adaptions --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 16 +++++---- src/Std/Data/DTreeMap/Lemmas.lean | 21 +++++++----- src/Std/Data/DTreeMap/RawLemmas.lean | 31 ++++++----------- src/Std/Data/TreeMap/Lemmas.lean | 32 +++++++----------- src/Std/Data/TreeMap/RawLemmas.lean | 31 ++++++----------- src/Std/Data/TreeSet/Lemmas.lean | 39 ++++++++++------------ src/Std/Data/TreeSet/RawLemmas.lean | 25 +++++--------- 7 files changed, 81 insertions(+), 114 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 42cdcef87dd0..f3231fcf64d3 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -92,11 +92,13 @@ theorem isEmpty_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := Iff.rfl -theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : k == k') : +theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq) : t.contains k = t.contains k' := by + rw [← beq_iff_eq (b := Ordering.eq), ← beq_eq] at hab simp_to_model using List.containsKey_congr -theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : k == k') : k ∈ t ↔ k' ∈ t := by +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 @@ -162,19 +164,21 @@ theorem mem_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} : 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 → (k == a) = false → t.contains a := by + (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 → (k == a) = false → t.contains a := by + (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 → (k == a) = false → a ∈ t := by + 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 → (k == a) = false → a ∈ t := by + 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 := diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 2d0ed856ac5f..e64cd01fd67e 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -1,21 +1,24 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.DTreeMap.Internal.Lemmas import Std.Data.DTreeMap.Basic /-! -# API lemmas for `DTreeMap` +# Dependent tree map lemmas + +This file contains lemmas about `Std.Data.DTreeMap`. Most of the lemmas require +`TransCmp cmp` for the comparison function `cmp`. -/ +open Std.DTreeMap.Internal + set_option linter.missingDocs true set_option autoImplicit false -open Std.DTreeMap.Internal - universe u v namespace Std.DTreeMap @@ -41,11 +44,11 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := Impl.mem_iff_contains -theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : +theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : t.contains k = t.contains k' := Impl.contains_congr t.wf hab -theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := +theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr t.wf hab @[simp] @@ -116,11 +119,11 @@ theorem mem_insert_self [TransCmp cmp] {k : α} {v : β k} : Impl.mem_insert_self t.wf theorem contains_of_contains_insert [TransCmp cmp] {k a : α} {v : β k} : - (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := Impl.contains_of_contains_insert t.wf theorem mem_of_mem_insert [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := Impl.mem_of_mem_insert t.wf @[simp] diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index de3602047bdd..32627b6f1372 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -1,14 +1,17 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.DTreeMap.Internal.Lemmas import Std.Data.DTreeMap.Raw /-! -# API lemmas for `DTreeMap.Raw` +# Dependent tree map lemmas + +This file contains lemmas about `Std.Data.DTreeMap.Raw`. Most of the lemmas require +`TransCmp cmp` for the comparison function `cmp`. -/ set_option linter.missingDocs true @@ -41,11 +44,11 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := Impl.mem_iff_contains -theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : +theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : t.contains k = t.contains k' := Impl.contains_congr h hab -theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := +theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr h hab @[simp] @@ -104,7 +107,7 @@ theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : @[simp] theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := Impl.mem_insert! h theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : @@ -116,11 +119,11 @@ theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : Impl.mem_insert!_self h theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := Impl.contains_of_contains_insert! h theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := Impl.mem_of_mem_insert! h @[simp] @@ -223,18 +226,6 @@ theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := Impl.contains_of_contains_insertIfNew! h -/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the -proof obligation in the statement of `get_insertIfNew`. -/ -theorem contains_of_contains_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := - Impl.contains_of_contains_insertIfNew!' h - -/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the -proof obligation in the statement of `get_insertIfNew`. -/ -theorem mem_of_mem_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := - Impl.mem_of_mem_insertIfNew!' h - theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β k} : (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := Impl.size_insertIfNew! h diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 8a2d1f4927a6..3183287b7347 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -1,14 +1,17 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.DTreeMap.Lemmas import Std.Data.TreeMap.Basic /-! -# API lemmas for `TreeMap` +# Tree map lemmas + +This file contains lemmas about `Std.Data.TreeMap`. Most of the lemmas require +`TransCmp cmp` for the comparison function `cmp`. -/ set_option linter.missingDocs true @@ -41,11 +44,11 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := DTreeMap.mem_iff_contains -theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : +theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : t.contains k = t.contains k' := DTreeMap.contains_congr hab -theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := +theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.mem_congr hab @[simp] @@ -104,7 +107,7 @@ theorem contains_insert [h : TransCmp cmp] {k a : α} {v : β} : @[simp] theorem mem_insert [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := DTreeMap.mem_insert theorem contains_insert_self [TransCmp cmp] {k : α} {v : β} : @@ -116,11 +119,11 @@ theorem mem_insert_self [TransCmp cmp] {k : α} {v : β} : DTreeMap.mem_insert_self theorem contains_of_contains_insert [TransCmp cmp] {k a : α} {v : β} : - (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := DTreeMap.contains_of_contains_insert theorem mem_of_mem_insert [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := DTreeMap.mem_of_mem_insert @[simp] @@ -212,6 +215,7 @@ theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β} : (t.insertIfNew k v).contains k := DTreeMap.contains_insertIfNew_self +@[simp] theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β} : k ∈ t.insertIfNew k v := DTreeMap.mem_insertIfNew_self @@ -224,18 +228,6 @@ theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} : a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := DTreeMap.contains_of_contains_insertIfNew -/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. -/ -theorem contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} {v : β} : - (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := - DTreeMap.contains_of_contains_insertIfNew' - -/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match -the proof obligation in the statement of `get_insertIfNew`. -/ -theorem mem_of_mem_insertIfNew' [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := - DTreeMap.mem_of_mem_insertIfNew' - theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β} : (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := DTreeMap.size_insertIfNew diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 4a0ef4c5451e..5e5c910b601a 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -1,14 +1,17 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.DTreeMap.RawLemmas import Std.Data.TreeMap.Raw /-! -# API lemmas for `TreeMap.Raw` +# Tree map lemmas + +This file contains lemmas about `Std.Data.TreeMap.Raw`. Most of the lemmas require +`TransCmp cmp` for the comparison function `cmp`. -/ set_option linter.missingDocs true @@ -39,11 +42,11 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := DTreeMap.Raw.mem_iff_contains -theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : +theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : t.contains k = t.contains k' := DTreeMap.Raw.contains_congr h hab -theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := +theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.Raw.mem_congr h hab @[simp] @@ -102,7 +105,7 @@ theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β} : @[simp] theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insert k v ↔ cmp k a == .eq ∨ a ∈ t := + a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := DTreeMap.Raw.mem_insert h theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : @@ -114,11 +117,11 @@ theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : DTreeMap.Raw.mem_insert_self h theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - (t.insert k v).contains a → (cmp k a == .eq) = false → t.contains a := + (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := DTreeMap.Raw.contains_of_contains_insert h theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insert k v → (cmp k a == .eq) = false → a ∈ t := + a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := DTreeMap.Raw.mem_of_mem_insert h @[simp] @@ -221,18 +224,6 @@ theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := DTreeMap.Raw.contains_of_contains_insertIfNew h -/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the -proof obligation in the statement of `get_insertIfNew`. -/ -theorem contains_of_contains_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := - DTreeMap.Raw.contains_of_contains_insertIfNew' h - -/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the -proof obligation in the statement of `get_insertIfNew`. -/ -theorem mem_of_mem_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insertIfNew k v → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := - DTreeMap.Raw.mem_of_mem_insertIfNew' h - theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β} : (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := DTreeMap.Raw.size_insertIfNew h diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index b28039e6fc5a..80964aa92a3a 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -1,14 +1,17 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.TreeMap.Lemmas import Std.Data.TreeSet.Basic /-! -# API lemmas for `TreeMap` +# Tree set lemmas + +This file contains lemmas about `Std.Data.TreeSet`. Most of the lemmas require +`TransCmp cmp` for the comparison function `cmp`. -/ set_option linter.missingDocs true @@ -41,11 +44,11 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := TreeMap.mem_iff_contains -theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : +theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : t.contains k = t.contains k' := TreeMap.contains_congr hab -theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := +theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := TreeMap.mem_congr hab @[simp] @@ -123,18 +126,6 @@ theorem mem_of_mem_insert [TransCmp cmp] {k a : α} : a ∈ t.insert k → (cmp k a == .eq) = false → a ∈ t := TreeMap.mem_of_mem_insertIfNew -/-- This is a restatement of `contains_of_contains_insert` that is written to exactly match the -proof obligation in the statement of `get_insert`. -/ -theorem contains_of_contains_insert' [TransCmp cmp] {k a : α} : - (t.insert k).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := - TreeMap.contains_of_contains_insertIfNew' - -/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the -proof obligation in the statement of `get_insert`. -/ -theorem mem_of_mem_insert' [TransCmp cmp] {k a : α} : - a ∈ t.insert k → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := - TreeMap.mem_of_mem_insertIfNew' - @[simp] theorem size_empty : (empty : TreeSet α cmp).size = 0 := TreeMap.size_empty @@ -177,22 +168,26 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} : @[simp] theorem contains_erase [TransCmp cmp] {k a : α} : (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - DTreeMap.contains_erase + TreeMap.contains_erase theorem contains_of_contains_erase [TransCmp cmp] {k a : α} : (t.erase k).contains a → t.contains a := - DTreeMap.contains_of_contains_erase + TreeMap.contains_of_contains_erase + +theorem mem_of_mem_erase [TransCmp cmp] {k a : α} : + (t.erase k).contains a → t.contains a := + TreeMap.mem_of_mem_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 + TreeMap.size_erase theorem size_erase_le [TransCmp cmp] {k : α} : (t.erase k).size ≤ t.size := - DTreeMap.size_erase_le + TreeMap.size_erase_le theorem size_le_size_erase [TransCmp cmp] {k : α} : t.size ≤ (t.erase k).size + 1 := - DTreeMap.size_le_size_erase + TreeMap.size_le_size_erase end Std.TreeSet diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 6da1084988ce..099e9171ee7b 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -1,14 +1,17 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.TreeMap.RawLemmas import Std.Data.TreeSet.Raw /-! -# API lemmas for `TreeMap.Raw` +# Tree set lemmas + +This file contains lemmas about `Std.Data.TreeSet.Raw`. Most of the lemmas require +`TransCmp cmp` for the comparison function `cmp`. -/ set_option linter.missingDocs true @@ -39,11 +42,11 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} : theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := TreeMap.Raw.mem_iff_contains -theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : +theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : t.contains k = t.contains k' := TreeMap.Raw.contains_congr h hab -theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' == .eq) : k ∈ t ↔ k' ∈ t := +theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := TreeMap.Raw.mem_congr h hab @[simp] @@ -121,18 +124,6 @@ theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} : a ∈ t.insert k → (cmp k a == .eq) = false → a ∈ t := TreeMap.Raw.mem_of_mem_insertIfNew h -/-- This is a restatement of `contains_of_contains_insert` that is written to exactly match the -proof obligation in the statement of `get_insert`. -/ -theorem contains_of_contains_insert' [TransCmp cmp] (h : t.WF) {k a : α} : - (t.insert k).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a := - TreeMap.Raw.contains_of_contains_insertIfNew' h - -/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the -proof obligation in the statement of `get_insert`. -/ -theorem mem_of_mem_insert' [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.insert k → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t := - TreeMap.Raw.mem_of_mem_insertIfNew' h - @[simp] theorem size_empty : (empty : Raw α cmp).size = 0 := TreeMap.Raw.size_empty From 3409873c1beaa38ed95c8a7561a0b34baa6f50f3 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 16:13:44 +0100 Subject: [PATCH 10/17] shrink this PR --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 275 --------------------- src/Std/Data/DTreeMap/Lemmas.lean | 188 -------------- src/Std/Data/DTreeMap/RawLemmas.lean | 187 -------------- src/Std/Data/TreeMap/Lemmas.lean | 191 -------------- src/Std/Data/TreeMap/RawLemmas.lean | 187 -------------- src/Std/Data/TreeSet/Lemmas.lean | 141 ----------- src/Std/Data/TreeSet/RawLemmas.lean | 144 ----------- tests/lean/run/treemap.lean | 9 - 8 files changed, 1322 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index f3231fcf64d3..b14f866a1bd2 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -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 diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index e64cd01fd67e..176021656434 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -51,192 +51,4 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr t.wf hab -@[simp] -theorem contains_empty {k : α} : (empty : DTreeMap α β cmp).contains k = false := - Impl.contains_empty - -@[simp] -theorem not_mem_empty {k : α} : k ∉ (empty : DTreeMap α β cmp) := - Impl.not_mem_empty - -@[simp] -theorem contains_emptyc {k : α} : (∅ : DTreeMap α β cmp).contains k = false := - Impl.contains_empty - -@[simp] -theorem not_mem_emptyc {k : α} : k ∉ (∅ : DTreeMap α β cmp) := - Impl.not_mem_empty - -theorem contains_of_isEmpty [TransCmp cmp] {a : α} : - t.isEmpty → t.contains a = false := - Impl.contains_of_isEmpty t.wf - -theorem not_mem_of_isEmpty [TransCmp cmp] {a : α} : - t.isEmpty → a ∉ t := - Impl.not_mem_of_isEmpty t.wf - -theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] : - t.isEmpty = false ↔ ∃ a, t.contains a = true := - Impl.isEmpty_eq_false_iff_exists_contains_eq_true t.wf - -theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] : - t.isEmpty = false ↔ ∃ a, a ∈ t := - Impl.isEmpty_eq_false_iff_exists_mem t.wf - -theorem isEmpty_iff_forall_contains [TransCmp cmp] : - t.isEmpty = true ↔ ∀ a, t.contains a = false := - Impl.isEmpty_iff_forall_contains t.wf - -theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : - t.isEmpty = true ↔ ∀ a, ¬a ∈ t := - Impl.isEmpty_iff_forall_not_mem t.wf - -@[simp] -theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p t = t.insert p.1 p.2 := - rfl - -@[simp] -theorem singleton_eq_insert {p : (a : α) × β a} : - Singleton.singleton p = (∅ : DTreeMap α β cmp).insert p.1 p.2 := - rfl - -@[simp] -theorem contains_insert [TransCmp cmp] {k k' : α} {v : β k} : - (t.insert k v).contains k' = (cmp k k' == .eq || t.contains k') := - Impl.contains_insert t.wf - -@[simp] -theorem mem_insert [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := - Impl.mem_insert t.wf - -theorem contains_insert_self [TransCmp cmp] {k : α} {v : β k} : - (t.insert k v).contains k := - Impl.contains_insert_self t.wf - -theorem mem_insert_self [TransCmp cmp] {k : α} {v : β k} : - k ∈ t.insert k v := - Impl.mem_insert_self t.wf - -theorem contains_of_contains_insert [TransCmp cmp] {k a : α} {v : β k} : - (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := - Impl.contains_of_contains_insert t.wf - -theorem mem_of_mem_insert [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := - Impl.mem_of_mem_insert t.wf - -@[simp] -theorem size_empty : (empty : DTreeMap α β cmp).size = 0 := - Impl.size_empty - -@[simp] -theorem size_emptyc : (∅ : DTreeMap α β cmp).size = 0 := - Impl.size_empty - -theorem isEmpty_eq_size_eq_zero : - t.isEmpty = (t.size == 0) := - Impl.isEmpty_eq_size_eq_zero t.wf - -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 - -@[simp] -theorem erase_empty {k : α} : - (empty : DTreeMap α β cmp).erase k = empty := - ext <| Impl.erase_empty (instOrd := ⟨cmp⟩) (k := k) - -@[simp] -theorem erase_emptyc {k : α} : - (∅ : DTreeMap α β cmp).erase k = empty := - erase_empty - -@[simp] -theorem isEmpty_erase [TransCmp cmp] {k : α} : - (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := - Impl.isEmpty_erase t.wf - -@[simp] -theorem contains_erase [TransCmp cmp] {k a : α} : - (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - Impl.contains_erase t.wf - -@[simp] -theorem mem_erase [TransCmp cmp] {k a : α} : - a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := - Impl.mem_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 mem_of_mem_erase [TransCmp cmp] {k a : α} : - a ∈ t.erase k → a ∈ t := - Impl.mem_of_mem_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 - -@[simp] -theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β k} : - (t.insertIfNew k v).isEmpty = false := - Impl.isEmpty_insertIfNew t.wf - -@[simp] -theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : - (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := - Impl.contains_insertIfNew t.wf - -@[simp] -theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := - Impl.mem_insertIfNew t.wf - -@[simp] -theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} : - (t.insertIfNew k v).contains k := - Impl.contains_insertIfNew_self t.wf - -theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} : - k ∈ t.insertIfNew k v := - Impl.mem_insertIfNew_self t.wf - -theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : - (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := - Impl.contains_of_contains_insertIfNew t.wf - -theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} : - a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := - Impl.contains_of_contains_insertIfNew t.wf - -theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β k} : - (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := - Impl.size_insertIfNew t.wf - -theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β k} : - t.size ≤ (t.insertIfNew k v).size := - Impl.size_le_size_insertIfNew t.wf - -theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β k} : - (t.insertIfNew k v).size ≤ t.size + 1 := - Impl.size_insertIfNew_le t.wf - end Std.DTreeMap diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index 32627b6f1372..a08577082a05 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -51,191 +51,4 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = . theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr h hab -@[simp] -theorem contains_empty {k : α} : (empty : Raw α β cmp).contains k = false := - Impl.contains_empty - -@[simp] -theorem not_mem_empty {k : α} : k ∉ (empty : Raw α β cmp) := - Impl.not_mem_empty - -@[simp] -theorem contains_emptyc {k : α} : (∅ : Raw α β cmp).contains k = false := - Impl.contains_empty - -@[simp] -theorem not_mem_emptyc {k : α} : k ∉ (∅ : Raw α β cmp) := - Impl.not_mem_empty - -theorem contains_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : - t.isEmpty → t.contains a = false := - Impl.contains_of_isEmpty h - -theorem not_mem_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : - t.isEmpty → a ∉ t := - Impl.not_mem_of_isEmpty h - -theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] (h : t.WF) : - t.isEmpty = false ↔ ∃ a, t.contains a = true := - Impl.isEmpty_eq_false_iff_exists_contains_eq_true h - -theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) : - t.isEmpty = false ↔ ∃ a, a ∈ t := - Impl.isEmpty_eq_false_iff_exists_mem h - -theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) : - t.isEmpty = true ↔ ∀ a, t.contains a = false := - Impl.isEmpty_iff_forall_contains h - -theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : - t.isEmpty = true ↔ ∀ a, ¬a ∈ t := - Impl.isEmpty_iff_forall_not_mem h - -@[simp] -theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p t = t.insert p.1 p.2 := - rfl - -@[simp] -theorem singleton_eq_insert {p : (a : α) × β a} : - Singleton.singleton p = (∅ : Raw α β cmp).insert p.1 p.2 := - rfl - -@[simp] -theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := - Impl.contains_insert! h - -@[simp] -theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := - Impl.mem_insert! h - -theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - (t.insert k v).contains k := - Impl.contains_insert!_self h - -theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - k ∈ t.insert k v := - Impl.mem_insert!_self h - -theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := - Impl.contains_of_contains_insert! h - -theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := - Impl.mem_of_mem_insert! h - -@[simp] -theorem size_empty : (empty : Raw α β cmp).size = 0 := - Impl.size_empty - -@[simp] -theorem size_emptyc : (∅ : Raw α β cmp).size = 0 := - Impl.size_empty - -theorem isEmpty_eq_size_eq_zero (h : t.WF) : - t.isEmpty = (t.size == 0) := - Impl.isEmpty_eq_size_eq_zero h.out - -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_insert! 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_insert! h - -theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - (t.insert k v).size ≤ t.size + 1 := - Impl.size_insert!_le h - -@[simp] -theorem erase_empty {k : α} : - (empty : Raw α β cmp).erase k = empty := - ext <| Impl.erase!_empty (instOrd := ⟨cmp⟩) (k := k) - -@[simp] -theorem erase_emptyc {k : α} : - (∅ : Raw α β cmp).erase k = empty := - erase_empty - -@[simp] -theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := - Impl.isEmpty_erase! h - -@[simp] -theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : - (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - Impl.contains_erase! h - -@[simp] -theorem mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := - Impl.mem_erase! h - -theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : - (t.erase k).contains a → t.contains a := - Impl.contains_of_contains_erase! h - -theorem mem_of_mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.erase k → a ∈ t := - Impl.mem_of_mem_erase! h - -theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).size = if t.contains k then t.size - 1 else t.size := - Impl.size_erase! h - -theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).size ≤ t.size := - Impl.size_erase!_le h - -theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : - t.size ≤ (t.erase k).size + 1 := - Impl.size_le_size_erase! h - -@[simp] -theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - (t.insertIfNew k v).isEmpty = false := - Impl.isEmpty_insertIfNew! h - -@[simp] -theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := - Impl.contains_insertIfNew! h - -@[simp] -theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := - Impl.mem_insertIfNew! h - -theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - (t.insertIfNew k v).contains k := - Impl.contains_insertIfNew!_self h - -theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - k ∈ t.insertIfNew k v := - Impl.mem_insertIfNew!_self h - -theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := - Impl.contains_of_contains_insertIfNew! h - -theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} : - a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := - Impl.contains_of_contains_insertIfNew! h - -theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β k} : - (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := - Impl.size_insertIfNew! h - -theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - t.size ≤ (t.insertIfNew k v).size := - Impl.size_le_size_insertIfNew! h - -theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : - (t.insertIfNew k v).size ≤ t.size + 1 := - Impl.size_insertIfNew!_le h - end Std.DTreeMap.Raw diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 3183287b7347..b27731ba236d 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -17,8 +17,6 @@ This file contains lemmas about `Std.Data.TreeMap`. Most of the lemmas require set_option linter.missingDocs true set_option autoImplicit false -open Std.DTreeMap.Internal - universe u v namespace Std.TreeMap @@ -51,193 +49,4 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.mem_congr hab -@[simp] -theorem contains_empty {k : α} : (empty : TreeMap α β cmp).contains k = false := - DTreeMap.contains_empty - -@[simp] -theorem not_mem_empty {k : α} : k ∉ (empty : TreeMap α β cmp) := - DTreeMap.not_mem_empty - -@[simp] -theorem contains_emptyc {k : α} : (∅ : TreeMap α β cmp).contains k = false := - DTreeMap.contains_empty - -@[simp] -theorem not_mem_emptyc {k : α} : k ∉ (∅ : TreeMap α β cmp) := - DTreeMap.not_mem_empty - -theorem contains_of_isEmpty [TransCmp cmp] {a : α} : - t.isEmpty → t.contains a = false := - DTreeMap.contains_of_isEmpty - -theorem not_mem_of_isEmpty [TransCmp cmp] {a : α} : - t.isEmpty → a ∉ t := - DTreeMap.not_mem_of_isEmpty - -theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] : - t.isEmpty = false ↔ ∃ a, t.contains a = true := - DTreeMap.isEmpty_eq_false_iff_exists_contains_eq_true - -theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] : - t.isEmpty = false ↔ ∃ a, a ∈ t := - DTreeMap.isEmpty_eq_false_iff_exists_mem - -theorem isEmpty_iff_forall_contains [TransCmp cmp] : - t.isEmpty = true ↔ ∀ a, t.contains a = false := - DTreeMap.isEmpty_iff_forall_contains - -theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : - t.isEmpty = true ↔ ∀ a, ¬a ∈ t := - DTreeMap.isEmpty_iff_forall_not_mem - -@[simp] -theorem insert_eq_insert {p : α × β} : Insert.insert p t = t.insert p.1 p.2 := - rfl - -@[simp] -theorem singleton_eq_insert {p : α × β} : - Singleton.singleton p = (∅ : TreeMap α β cmp).insert p.1 p.2 := - rfl - -@[simp] -theorem contains_insert [h : TransCmp cmp] {k a : α} {v : β} : - (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := - DTreeMap.contains_insert - -@[simp] -theorem mem_insert [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := - DTreeMap.mem_insert - -theorem contains_insert_self [TransCmp cmp] {k : α} {v : β} : - (t.insert k v).contains k := - DTreeMap.contains_insert_self - -theorem mem_insert_self [TransCmp cmp] {k : α} {v : β} : - k ∈ t.insert k v := - DTreeMap.mem_insert_self - -theorem contains_of_contains_insert [TransCmp cmp] {k a : α} {v : β} : - (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := - DTreeMap.contains_of_contains_insert - -theorem mem_of_mem_insert [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := - DTreeMap.mem_of_mem_insert - -@[simp] -theorem size_empty : (empty : TreeMap α β cmp).size = 0 := - DTreeMap.size_empty - -@[simp] -theorem size_emptyc : (∅ : TreeMap α β cmp).size = 0 := - DTreeMap.size_empty - -theorem isEmpty_eq_size_eq_zero : - t.isEmpty = (t.size == 0) := - DTreeMap.isEmpty_eq_size_eq_zero - -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 - -@[simp] -theorem erase_empty {k : α} : - (empty : TreeMap α β cmp).erase k = empty := - ext <| DTreeMap.erase_empty - -@[simp] -theorem erase_emptyc {k : α} : - (∅ : TreeMap α β cmp).erase k = empty := - erase_empty - -@[simp] -theorem isEmpty_erase [TransCmp cmp] {k : α} : - (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := - DTreeMap.isEmpty_erase - -@[simp] -theorem contains_erase [TransCmp cmp] {k a : α} : - (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - DTreeMap.contains_erase - -@[simp] -theorem mem_erase [TransCmp cmp] {k a : α} : - a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := - DTreeMap.mem_erase - -theorem contains_of_contains_erase [TransCmp cmp] {k a : α} : - (t.erase k).contains a → t.contains a := - DTreeMap.contains_of_contains_erase - -theorem mem_of_mem_erase [TransCmp cmp] {k a : α} : - a ∈ t.erase k → a ∈ t := - DTreeMap.mem_of_mem_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 - -@[simp] -theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β} : - (t.insertIfNew k v).isEmpty = false := - DTreeMap.isEmpty_insertIfNew - -@[simp] -theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} : - (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := - DTreeMap.contains_insertIfNew - -@[simp] -theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := - DTreeMap.mem_insertIfNew - -@[simp] -theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β} : - (t.insertIfNew k v).contains k := - DTreeMap.contains_insertIfNew_self - -@[simp] -theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β} : - k ∈ t.insertIfNew k v := - DTreeMap.mem_insertIfNew_self - -theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} : - (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := - DTreeMap.contains_of_contains_insertIfNew - -theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} : - a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := - DTreeMap.contains_of_contains_insertIfNew - -theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β} : - (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := - DTreeMap.size_insertIfNew - -theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β} : - t.size ≤ (t.insertIfNew k v).size := - DTreeMap.size_le_size_insertIfNew - -theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} : - (t.insertIfNew k v).size ≤ t.size + 1 := - DTreeMap.size_insertIfNew_le - end Std.TreeMap diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 5e5c910b601a..6d89b178e4d9 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -49,191 +49,4 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = . theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.Raw.mem_congr h hab -@[simp] -theorem contains_empty {k : α} : (empty : Raw α β cmp).contains k = false := - DTreeMap.Raw.contains_empty - -@[simp] -theorem not_mem_empty {k : α} : k ∉ (empty : Raw α β cmp) := - DTreeMap.Raw.not_mem_empty - -@[simp] -theorem contains_emptyc {k : α} : (∅ : Raw α β cmp).contains k = false := - DTreeMap.Raw.contains_empty - -@[simp] -theorem not_mem_emptyc {k : α} : k ∉ (∅ : Raw α β cmp) := - DTreeMap.Raw.not_mem_empty - -theorem contains_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : - t.isEmpty → t.contains a = false := - DTreeMap.Raw.contains_of_isEmpty h - -theorem not_mem_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : - t.isEmpty → a ∉ t := - DTreeMap.Raw.not_mem_of_isEmpty h - -theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] (h : t.WF) : - t.isEmpty = false ↔ ∃ a, t.contains a = true := - DTreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h - -theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) : - t.isEmpty = false ↔ ∃ a, a ∈ t := - DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem h - -theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) : - t.isEmpty = true ↔ ∀ a, t.contains a = false := - DTreeMap.Raw.isEmpty_iff_forall_contains h - -theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : - t.isEmpty = true ↔ ∀ a, ¬a ∈ t := - DTreeMap.Raw.isEmpty_iff_forall_not_mem h - -@[simp] -theorem insert_eq_insert {p : α × β} : Insert.insert p t = t.insert p.1 p.2 := - rfl - -@[simp] -theorem singleton_eq_insert {p : α × β} : - Singleton.singleton p = (∅ : Raw α β cmp).insert p.1 p.2 := - rfl - -@[simp] -theorem contains_insert [h : TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - (t.insert k v).contains a = (cmp k a == .eq || t.contains a) := - DTreeMap.Raw.contains_insert h - -@[simp] -theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insert k v ↔ cmp k a = .eq ∨ a ∈ t := - DTreeMap.Raw.mem_insert h - -theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - (t.insert k v).contains k := - DTreeMap.Raw.contains_insert_self h - -theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - k ∈ t.insert k v := - DTreeMap.Raw.mem_insert_self h - -theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - (t.insert k v).contains a → ¬ cmp k a = .eq → t.contains a := - DTreeMap.Raw.contains_of_contains_insert h - -theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insert k v → ¬ cmp k a = .eq → a ∈ t := - DTreeMap.Raw.mem_of_mem_insert h - -@[simp] -theorem size_empty : (empty : Raw α β cmp).size = 0 := - DTreeMap.Raw.size_empty - -@[simp] -theorem size_emptyc : (∅ : Raw α β cmp).size = 0 := - DTreeMap.Raw.size_empty - -theorem isEmpty_eq_size_eq_zero (h : t.WF) : - t.isEmpty = (t.size == 0) := - DTreeMap.Raw.isEmpty_eq_size_eq_zero h.out - -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 - -@[simp] -theorem erase_empty {k : α} : - (empty : Raw α β cmp).erase k = empty := - ext <| DTreeMap.Raw.erase_empty - -@[simp] -theorem erase_emptyc {k : α} : - (empty : Raw α β cmp).erase k = empty := - erase_empty - -@[simp] -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 - -@[simp] -theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : - (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - DTreeMap.Raw.contains_erase h - -@[simp] -theorem mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := - DTreeMap.Raw.mem_erase h - -theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : - (t.erase k).contains a → t.contains a := - DTreeMap.Raw.contains_of_contains_erase h - -theorem mem_of_mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.erase k → a ∈ t := - DTreeMap.Raw.mem_of_mem_erase h - -theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).size = if t.contains k then t.size - 1 else t.size := - DTreeMap.Raw.size_erase h - -theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).size ≤ t.size := - DTreeMap.Raw.size_erase_le h - -theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : - t.size ≤ (t.erase k).size + 1 := - DTreeMap.Raw.size_le_size_erase h - -@[simp] -theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - (t.insertIfNew k v).isEmpty = false := - DTreeMap.Raw.isEmpty_insertIfNew h - -@[simp] -theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) := - DTreeMap.Raw.contains_insertIfNew h - -@[simp] -theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insertIfNew k v ↔ cmp k a == .eq ∨ a ∈ t := - DTreeMap.Raw.mem_insertIfNew h - -theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - (t.insertIfNew k v).contains k := - DTreeMap.Raw.contains_insertIfNew_self h - -theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - k ∈ t.insertIfNew k v := - DTreeMap.Raw.mem_insertIfNew_self h - -theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - (t.insertIfNew k v).contains a → (cmp k a == .eq) = false → t.contains a := - DTreeMap.Raw.contains_of_contains_insertIfNew h - -theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : - a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t := - DTreeMap.Raw.contains_of_contains_insertIfNew h - -theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β} : - (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 := - DTreeMap.Raw.size_insertIfNew h - -theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - t.size ≤ (t.insertIfNew k v).size := - DTreeMap.Raw.size_le_size_insertIfNew h - -theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} : - (t.insertIfNew k v).size ≤ t.size + 1 := - DTreeMap.Raw.size_insertIfNew_le h - end Std.TreeMap.Raw diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 80964aa92a3a..3dcdde0925a7 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -17,8 +17,6 @@ This file contains lemmas about `Std.Data.TreeSet`. Most of the lemmas require set_option linter.missingDocs true set_option autoImplicit false -open Std.DTreeMap.Internal - universe u v namespace Std.TreeSet @@ -51,143 +49,4 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := TreeMap.mem_congr hab -@[simp] -theorem contains_empty {k : α} : (empty : TreeSet α cmp).contains k = false := - TreeMap.contains_empty - -@[simp] -theorem not_mem_empty {k : α} : k ∉ (empty : TreeSet α cmp) := - TreeMap.not_mem_empty - -@[simp] -theorem contains_emptyc {k : α} : (∅ : TreeSet α cmp).contains k = false := - TreeMap.contains_empty - -@[simp] -theorem not_mem_emptyc {k : α} : k ∉ (∅ : TreeSet α cmp) := - TreeMap.not_mem_empty - -theorem contains_of_isEmpty [TransCmp cmp] {a : α} : - t.isEmpty → t.contains a = false := - DTreeMap.contains_of_isEmpty - -theorem not_mem_of_isEmpty [TransCmp cmp] {a : α} : - t.isEmpty → a ∉ t := - DTreeMap.not_mem_of_isEmpty - -theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] : - t.isEmpty = false ↔ ∃ a, t.contains a = true := - DTreeMap.isEmpty_eq_false_iff_exists_contains_eq_true - -theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] : - t.isEmpty = false ↔ ∃ a, a ∈ t := - DTreeMap.isEmpty_eq_false_iff_exists_mem - -theorem isEmpty_iff_forall_contains [TransCmp cmp] : - t.isEmpty = true ↔ ∀ a, t.contains a = false := - DTreeMap.isEmpty_iff_forall_contains - -theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : - t.isEmpty = true ↔ ∀ a, ¬a ∈ t := - DTreeMap.isEmpty_iff_forall_not_mem - -@[simp] -theorem insert_eq_insert {p : α} : Insert.insert p t = t.insert p := - rfl - -@[simp] -theorem singleton_eq_insert {p : α} : - Singleton.singleton p = (∅ : TreeSet α cmp).insert p := - rfl - -@[simp] -theorem contains_insert [h : TransCmp cmp] {k a : α} : - (t.insert k).contains a = (cmp k a == .eq || t.contains a) := - TreeMap.contains_insertIfNew - -@[simp] -theorem mem_insert [TransCmp cmp] {k a : α} : - a ∈ t.insert k ↔ cmp k a == .eq ∨ a ∈ t := - TreeMap.mem_insertIfNew - -theorem contains_insert_self [TransCmp cmp] {k : α} : - (t.insert k).contains k := - TreeMap.contains_insertIfNew_self - -theorem mem_insert_self [TransCmp cmp] {k : α} : - k ∈ t.insert k := - TreeMap.mem_insertIfNew_self - -theorem contains_of_contains_insert [TransCmp cmp] {k a : α} : - (t.insert k).contains a → (cmp k a == .eq) = false → t.contains a := - TreeMap.contains_of_contains_insertIfNew - -theorem mem_of_mem_insert [TransCmp cmp] {k a : α} : - a ∈ t.insert k → (cmp k a == .eq) = false → a ∈ t := - TreeMap.mem_of_mem_insertIfNew - -@[simp] -theorem size_empty : (empty : TreeSet α cmp).size = 0 := - TreeMap.size_empty - -@[simp] -theorem size_emptyc : (∅ : TreeSet α cmp).size = 0 := - TreeMap.size_empty - -theorem isEmpty_eq_size_eq_zero : - t.isEmpty = (t.size == 0) := - TreeMap.isEmpty_eq_size_eq_zero - -theorem size_insert [TransCmp cmp] {k : α} : - (t.insert k).size = if t.contains k then t.size else t.size + 1 := - TreeMap.size_insertIfNew - -theorem size_le_size_insert [TransCmp cmp] {k : α} : - t.size ≤ (t.insert k).size := - TreeMap.size_le_size_insertIfNew - -theorem size_insert_le [TransCmp cmp] {k : α} : - (t.insert k).size ≤ t.size + 1 := - TreeMap.size_insertIfNew_le - -@[simp] -theorem erase_empty {k : α} : - (empty : TreeSet α cmp).erase k = empty := - ext <| TreeMap.erase_empty - -@[simp] -theorem erase_emptyc {k : α} : - (empty : TreeSet α cmp).erase k = empty := - erase_empty - -@[simp] -theorem isEmpty_erase [TransCmp cmp] {k : α} : - (t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) := - TreeMap.isEmpty_erase - -@[simp] -theorem contains_erase [TransCmp cmp] {k a : α} : - (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - TreeMap.contains_erase - -theorem contains_of_contains_erase [TransCmp cmp] {k a : α} : - (t.erase k).contains a → t.contains a := - TreeMap.contains_of_contains_erase - -theorem mem_of_mem_erase [TransCmp cmp] {k a : α} : - (t.erase k).contains a → t.contains a := - TreeMap.mem_of_mem_erase - -theorem size_erase [TransCmp cmp] {k : α} : - (t.erase k).size = if t.contains k then t.size - 1 else t.size := - TreeMap.size_erase - -theorem size_erase_le [TransCmp cmp] {k : α} : - (t.erase k).size ≤ t.size := - TreeMap.size_erase_le - -theorem size_le_size_erase [TransCmp cmp] {k : α} : - t.size ≤ (t.erase k).size + 1 := - TreeMap.size_le_size_erase - end Std.TreeSet diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 099e9171ee7b..386a62c37363 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -49,148 +49,4 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = . theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := TreeMap.Raw.mem_congr h hab -@[simp] -theorem contains_empty {k : α} : (empty : Raw α cmp).contains k = false := - TreeMap.Raw.contains_empty - -@[simp] -theorem not_mem_empty {k : α} : k ∉ (empty : Raw α cmp) := - TreeMap.Raw.not_mem_empty - -@[simp] -theorem contains_emptyc {k : α} : (∅ : Raw α cmp).contains k = false := - TreeMap.Raw.contains_empty - -@[simp] -theorem not_mem_emptyc {k : α} : k ∉ (∅ : Raw α cmp) := - TreeMap.Raw.not_mem_empty - -theorem contains_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : - t.isEmpty → t.contains a = false := - DTreeMap.Raw.contains_of_isEmpty h - -theorem not_mem_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : - t.isEmpty → a ∉ t := - DTreeMap.Raw.not_mem_of_isEmpty h - -theorem isEmpty_eq_false_iff_exists_contains_eq_true [TransCmp cmp] (h : t.WF) : - t.isEmpty = false ↔ ∃ a, t.contains a = true := - DTreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h - -theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) : - t.isEmpty = false ↔ ∃ a, a ∈ t := - DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem h - -theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) : - t.isEmpty = true ↔ ∀ a, t.contains a = false := - DTreeMap.Raw.isEmpty_iff_forall_contains h - -theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : - t.isEmpty = true ↔ ∀ a, ¬a ∈ t := - DTreeMap.Raw.isEmpty_iff_forall_not_mem h - -@[simp] -theorem insert_eq_insert {p : α} : Insert.insert p t = t.insert p := - rfl - -@[simp] -theorem singleton_eq_insert {p : α} : - Singleton.singleton p = (∅ : Raw α cmp).insert p := - rfl - -@[simp] -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_insertIfNew h - -@[simp] -theorem mem_insert [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.insert k ↔ cmp k a == .eq ∨ a ∈ t := - TreeMap.Raw.mem_insertIfNew h - -theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} : - (t.insert k).contains k := - TreeMap.Raw.contains_insertIfNew_self h - -theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} : - k ∈ t.insert k := - TreeMap.Raw.mem_insertIfNew_self h - -theorem contains_of_contains_insert [TransCmp cmp] (h : t.WF) {k a : α} : - (t.insert k).contains a → (cmp k a == .eq) = false → t.contains a := - TreeMap.Raw.contains_of_contains_insertIfNew h - -theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.insert k → (cmp k a == .eq) = false → a ∈ t := - TreeMap.Raw.mem_of_mem_insertIfNew h - -@[simp] -theorem size_empty : (empty : Raw α cmp).size = 0 := - TreeMap.Raw.size_empty - -@[simp] -theorem size_emptyc : (∅ : Raw α cmp).size = 0 := - TreeMap.Raw.size_empty - -theorem isEmpty_eq_size_eq_zero (h : t.WF) : - t.isEmpty = (t.size == 0) := - TreeMap.Raw.isEmpty_eq_size_eq_zero h.out - -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_insertIfNew h - -theorem size_le_size_insert [TransCmp cmp] (h : t.WF) {k : α} : - t.size ≤ (t.insert k).size := - TreeMap.Raw.size_le_size_insertIfNew h - -theorem size_insert_le [TransCmp cmp] (h : t.WF) {k : α} : - (t.insert k).size ≤ t.size + 1 := - TreeMap.Raw.size_insertIfNew_le h - -@[simp] -theorem erase_empty {k : α} : - (empty : Raw α cmp).erase k = empty := - ext <| TreeMap.Raw.erase_empty - -@[simp] -theorem erase_emptyc {k : α} : - (empty : Raw α cmp).erase k = empty := - erase_empty - -@[simp] -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 - -@[simp] -theorem contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : - (t.erase k).contains a = (cmp k a != .eq && t.contains a) := - TreeMap.Raw.contains_erase h - -@[simp] -theorem mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.erase k ↔ (cmp k a == .eq) = false ∧ a ∈ t := - TreeMap.Raw.mem_erase h - -theorem contains_of_contains_erase [TransCmp cmp] (h : t.WF) {k a : α} : - (t.erase k).contains a → t.contains a := - TreeMap.Raw.contains_of_contains_erase h - -theorem mem_of_mem_erase [TransCmp cmp] (h : t.WF) {k a : α} : - a ∈ t.erase k → a ∈ t := - TreeMap.Raw.mem_of_mem_erase h - -theorem size_erase [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).size = if t.contains k then t.size - 1 else t.size := - TreeMap.Raw.size_erase h - -theorem size_erase_le [TransCmp cmp] (h : t.WF) {k : α} : - (t.erase k).size ≤ t.size := - TreeMap.Raw.size_erase_le h - -theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} : - t.size ≤ (t.erase k).size + 1 := - TreeMap.Raw.size_le_size_erase h - end Std.TreeSet.Raw diff --git a/tests/lean/run/treemap.lean b/tests/lean/run/treemap.lean index f91b717c298a..721b8badedbf 100644 --- a/tests/lean/run/treemap.lean +++ b/tests/lean/run/treemap.lean @@ -30,12 +30,3 @@ example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := (mkTreeMapSingleton a b)[a]? - -example [TransOrd α] (a : α) (b : β) : (mkTreeMapSingleton a b).contains a := by - simp [mkTreeMapSingleton, Id.run] - -example [TransOrd α] (a : α) (b : β) : (mkDTreeMapSingleton a b).contains a := by - simp [mkDTreeMapSingleton, Id.run] - -example [TransOrd α] (a : α) : (mkTreeSetSingleton a).contains a := by - simp [mkTreeSetSingleton, Id.run] From 008ce549d433ace3ad288c61f7089f14943c9c5b Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 16:25:49 +0100 Subject: [PATCH 11/17] add docstring --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index b14f866a1bd2..6da2d0b4dc7f 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -8,7 +8,10 @@ import Std.Data.HashMap.Basic import Std.Data.DTreeMap.Internal.WF.Lemmas /-! -# API lemmas for `DTreeMap.Impl` +# Internal lemmas about the tree map + +This file contains internal lemmas about `Std.DTreeMap.Internal.Impl`. Users of the hash map should +not rely on the contents of this file. -/ set_option linter.missingDocs true From 15ab685095775c0011440586e94b251e67d2bdc6 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 16:29:23 +0100 Subject: [PATCH 12/17] remove import --- tests/lean/run/treemap.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/lean/run/treemap.lean b/tests/lean/run/treemap.lean index 721b8badedbf..94e1a967bba2 100644 --- a/tests/lean/run/treemap.lean +++ b/tests/lean/run/treemap.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Paul Reichert -/ import Std.Data.TreeSet.Basic -import Std.Data.TreeSet.Lemmas open Std From b9ee72ce2e0ac1bbf926403b7d614e2889e62b6c Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 16:30:56 +0100 Subject: [PATCH 13/17] fix copyright notice --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 6da2d0b4dc7f..3660cb42b396 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Paul Reichert -/ prelude import Std.Data.HashMap.Basic From d4a062ec19f85eff86aaa5e2bc20e6af411737d4 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 16:36:16 +0100 Subject: [PATCH 14/17] remove ext lemmas --- src/Std/Data/DTreeMap/Lemmas.lean | 3 --- src/Std/Data/DTreeMap/RawLemmas.lean | 3 --- src/Std/Data/TreeMap/Lemmas.lean | 3 --- src/Std/Data/TreeMap/RawLemmas.lean | 3 --- src/Std/Data/TreeSet/Lemmas.lean | 3 --- src/Std/Data/TreeSet/RawLemmas.lean | 3 --- 6 files changed, 18 deletions(-) diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 176021656434..c8c0b85ceebe 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -25,9 +25,6 @@ namespace Std.DTreeMap variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} -private theorem ext {t t' : DTreeMap α β cmp} : t.inner = t'.inner → t = t' := by - cases t; cases t'; rintro rfl; rfl - @[simp] theorem isEmpty_empty : (empty : DTreeMap α β cmp).isEmpty := Impl.isEmpty_empty diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index a08577082a05..b3f98b2124db 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -25,9 +25,6 @@ namespace Std.DTreeMap.Raw variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp} -private theorem ext {t t' : Raw α β cmp} : t.inner = t'.inner → t = t' := by - cases t; cases t'; rintro rfl; rfl - @[simp] theorem isEmpty_empty : (empty : DTreeMap.Raw α β cmp).isEmpty := Impl.isEmpty_empty diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index b27731ba236d..b61c7f9b9bb8 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -23,9 +23,6 @@ namespace Std.TreeMap variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap α β cmp} -private theorem ext {t t' : TreeMap α β cmp} : t.inner = t'.inner → t = t' := by - cases t; cases t'; rintro rfl; rfl - @[simp] theorem isEmpty_empty : (empty : TreeMap α β cmp).isEmpty := DTreeMap.isEmpty_empty diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 6d89b178e4d9..1d9bb6ddae40 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -23,9 +23,6 @@ namespace Std.TreeMap.Raw variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap.Raw α β cmp} -private theorem ext {t t' : Raw α β cmp} : t.inner = t'.inner → t = t' := by - cases t; cases t'; rintro rfl; rfl - @[simp] theorem isEmpty_empty : (empty : TreeMap.Raw α β cmp).isEmpty := DTreeMap.Raw.isEmpty_empty diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 3dcdde0925a7..34a75d06aae8 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -23,9 +23,6 @@ namespace Std.TreeSet variable {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} -private theorem ext {t t' : TreeSet α cmp} : t.inner = t'.inner → t = t' := by - cases t; cases t'; rintro rfl; rfl - @[simp] theorem isEmpty_empty : (empty : TreeSet α cmp).isEmpty := TreeMap.isEmpty_empty diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 386a62c37363..223d05fb63a4 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -23,9 +23,6 @@ namespace Std.TreeSet.Raw variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeSet.Raw α cmp} -private theorem ext {t t' : Raw α cmp} : t.inner = t'.inner → t = t' := by - cases t; cases t'; rintro rfl; rfl - @[simp] theorem isEmpty_empty : (empty : Raw α cmp).isEmpty := TreeMap.Raw.isEmpty_empty From fb0fe33f5a25b4360ce2f6e8e06e861542f4a8ba Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 11 Feb 2025 18:10:33 +0100 Subject: [PATCH 15/17] add isEmpty_insertIfNew (needed for TreeSet) --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 8 ++++++++ src/Std/Data/DTreeMap/Lemmas.lean | 5 +++++ src/Std/Data/DTreeMap/RawLemmas.lean | 5 +++++ src/Std/Data/TreeMap/Lemmas.lean | 5 +++++ src/Std/Data/TreeMap/RawLemmas.lean | 5 +++++ 5 files changed, 28 insertions(+) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 3660cb42b396..c63de4016302 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -104,4 +104,12 @@ 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 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 + +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 + end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index c8c0b85ceebe..75deb5ab1b4e 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -48,4 +48,9 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr t.wf hab +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β k} : + (t.insertIfNew k v).isEmpty = false := + Impl.isEmpty_insertIfNew t.wf + end Std.DTreeMap diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index b3f98b2124db..8a9e8384dd77 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -48,4 +48,9 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = . theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := Impl.mem_congr h hab +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew k v).isEmpty = false := + Impl.isEmpty_insertIfNew! h + end Std.DTreeMap.Raw diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index b61c7f9b9bb8..575f601699f4 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -46,4 +46,9 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.mem_congr hab +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β} : + (t.insertIfNew k v).isEmpty = false := + DTreeMap.isEmpty_insertIfNew + end Std.TreeMap diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 1d9bb6ddae40..56c0c73db54e 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -46,4 +46,9 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = . theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t := DTreeMap.Raw.mem_congr h hab +@[simp] +theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insertIfNew k v).isEmpty = false := + DTreeMap.Raw.isEmpty_insertIfNew h + end Std.TreeMap.Raw From 37233940315cb237a12fea0053e40703b0073ae0 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 14 Feb 2025 08:59:24 +0100 Subject: [PATCH 16/17] hash -> tree --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index c63de4016302..9c3b376c5759 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -10,7 +10,7 @@ import Std.Data.DTreeMap.Internal.WF.Lemmas /-! # Internal lemmas about the tree map -This file contains internal lemmas about `Std.DTreeMap.Internal.Impl`. Users of the hash map should +This file contains internal lemmas about `Std.DTreeMap.Internal.Impl`. Users of the tree map should not rely on the contents of this file. -/ From 73d0c813f98e427532a2227a79e4bd20eba2275d Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 14 Feb 2025 09:20:45 +0100 Subject: [PATCH 17/17] apply suggestions --- src/Std/Data/DTreeMap/Lemmas.lean | 4 ---- src/Std/Data/DTreeMap/RawLemmas.lean | 4 ---- src/Std/Data/TreeMap/Lemmas.lean | 6 +----- src/Std/Data/TreeMap/RawLemmas.lean | 6 +----- src/Std/Data/TreeSet/Lemmas.lean | 6 +----- src/Std/Data/TreeSet/RawLemmas.lean | 6 +----- 6 files changed, 4 insertions(+), 28 deletions(-) diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 75deb5ab1b4e..3fa06679cc80 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -25,10 +25,6 @@ namespace Std.DTreeMap variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} -@[simp] -theorem isEmpty_empty : (empty : DTreeMap α β cmp).isEmpty := - Impl.isEmpty_empty - @[simp] theorem isEmpty_emptyc : (∅ : DTreeMap α β cmp).isEmpty := Impl.isEmpty_empty diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index 8a9e8384dd77..ec860a1fb544 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -25,10 +25,6 @@ namespace Std.DTreeMap.Raw variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp} -@[simp] -theorem isEmpty_empty : (empty : DTreeMap.Raw α β cmp).isEmpty := - Impl.isEmpty_empty - @[simp] theorem isEmpty_emptyc : (∅ : DTreeMap.Raw α β cmp).isEmpty := Impl.isEmpty_empty diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 575f601699f4..5c44e12f000e 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -23,13 +23,9 @@ namespace Std.TreeMap variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap α β cmp} -@[simp] -theorem isEmpty_empty : (empty : TreeMap α β cmp).isEmpty := - DTreeMap.isEmpty_empty - @[simp] theorem isEmpty_emptyc : (∅ : TreeMap α β cmp).isEmpty := - DTreeMap.isEmpty_empty + DTreeMap.isEmpty_emptyc @[simp] theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} : diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 56c0c73db54e..c14cfb766d86 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -23,13 +23,9 @@ namespace Std.TreeMap.Raw variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap.Raw α β cmp} -@[simp] -theorem isEmpty_empty : (empty : TreeMap.Raw α β cmp).isEmpty := - DTreeMap.Raw.isEmpty_empty - @[simp] theorem isEmpty_emptyc : (∅ : TreeMap.Raw α β cmp).isEmpty := - DTreeMap.Raw.isEmpty_empty + DTreeMap.Raw.isEmpty_emptyc @[simp] theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} : diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 34a75d06aae8..2294b92d6cc2 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -23,13 +23,9 @@ namespace Std.TreeSet variable {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} -@[simp] -theorem isEmpty_empty : (empty : TreeSet α cmp).isEmpty := - TreeMap.isEmpty_empty - @[simp] theorem isEmpty_emptyc : (∅ : TreeSet α cmp).isEmpty := - TreeMap.isEmpty_empty + TreeMap.isEmpty_emptyc @[simp] theorem isEmpty_insert [TransCmp cmp] {k : α} : diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean index 223d05fb63a4..2184fd8a5c1b 100644 --- a/src/Std/Data/TreeSet/RawLemmas.lean +++ b/src/Std/Data/TreeSet/RawLemmas.lean @@ -23,13 +23,9 @@ namespace Std.TreeSet.Raw variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeSet.Raw α cmp} -@[simp] -theorem isEmpty_empty : (empty : Raw α cmp).isEmpty := - TreeMap.Raw.isEmpty_empty - @[simp] theorem isEmpty_emptyc : (∅ : Raw α cmp).isEmpty := - TreeMap.Raw.isEmpty_empty + TreeMap.Raw.isEmpty_emptyc @[simp] theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} :