diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index f91c766688..d848449cca 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -334,6 +334,10 @@ theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.1.WF) {a : α} : m.contains a = (m.get? a).isSome := by simp_to_model [contains, get?] using List.containsKey_eq_isSome_getValueCast? +theorem get?_eq_some_iff [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} : + m.get? k = some v ↔ ∃ h : m.contains k, m.get k h = v := by + simp_to_model [contains, get?, get] using List.getValueCast?_eq_some_iff + theorem get?_eq_none [LawfulBEq α] (h : m.1.WF) {a : α} : m.contains a = false → m.get? a = none := by simp_to_model [contains, get?] using List.getValueCast?_eq_none @@ -373,6 +377,10 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) { m.contains a = (get? m a).isSome := by simp_to_model [contains, Const.get?] using List.containsKey_eq_isSome_getValue? +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} : + get? m k = some v ↔ ∃ h : m.contains k, get m k h = v := by + simp_to_model [contains, Const.get?, Const.get] using List.getValue?_eq_some_iff + theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} : m.contains a = false → get? m a = none := by simp_to_model [contains, Const.get?] using List.getValue?_eq_none.2 @@ -701,6 +709,10 @@ theorem getKey?_eq_some [LawfulBEq α] (h : m.1.WF) {a : α} : m.contains a → m.getKey? a = some a := by simp_to_model [getKey?, contains] using List.getKey?_eq_some +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} : + m.getKey? k = some k' ↔ ∃ h : m.contains k, m.getKey k h = k' := by + simp_to_model [contains, getKey?, getKey] using List.getKey?_eq_some_iff' + theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} (h : k == k') : m.getKey? k = m.getKey? k' := by diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 1dc9e832f9..0ac2b60096 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -272,6 +272,10 @@ theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isS theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [LawfulBEq α] {k : α} {v : β k} : + m.get? k = some v ↔ ∃ h : k ∈ m, m.get k h = v := + Raw₀.get?_eq_some_iff ⟨m.1, _⟩ m.2 + theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} : m.contains a = false → m.get? a = none := Raw₀.get?_eq_none ⟨m.1, _⟩ m.2 @@ -332,6 +336,10 @@ theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (get? m a).isSome ↔ a ∈ m := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : + get? m k = some v ↔ ∃ h : k ∈ m, get m k h = v := + Raw₀.Const.get?_eq_some_iff ⟨m.1, _⟩ m.2 + theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → get? m a = none := Raw₀.Const.get?_eq_none ⟨m.1, _⟩ m.2 @@ -748,6 +756,10 @@ theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.getKey? k = some k') : k' ∈ m := Raw₀.contains_of_getKey?_eq_some ⟨m.1, _⟩ m.2 h +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} : + m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := + Raw₀.getKey?_eq_some_iff ⟨m.1, _⟩ m.2 + theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m.getKey? a = none := Raw₀.getKey?_eq_none ⟨m.1, _⟩ m.2 diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index b9f5515346..65fe8754bf 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -322,6 +322,11 @@ theorem mem_iff_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} : theorem isSome_get?_iff_mem [LawfulBEq α] (h : m.WF) {a : α} : (m.get? a).isSome ↔ a ∈ m := (mem_iff_isSome_get? h).symm +theorem get?_eq_some_iff [LawfulBEq α] (h : m.WF) {k : α} {v : β k} : + m.get? k = some v ↔ ∃ h : k ∈ m, m.get k h = v := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.get?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} : m.contains a = false → m.get? a = none := by simp_to_raw using Raw₀.get?_eq_none @@ -385,6 +390,11 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α (get? m a).isSome ↔ a ∈ m := (mem_iff_isSome_get? h).symm +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} : + get? m k = some v ↔ ∃ h : k ∈ m, get m k h = v := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.get?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.contains a = false → get? m a = none := by simp_to_raw using Raw₀.Const.get?_eq_none @@ -800,12 +810,16 @@ theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : (m.getKey? a).isSome ↔ a ∈ m := (mem_iff_isSome_getKey? h).symm -theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] - {a a' : α} (h : m.WF) : +theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {a a' : α} (h : m.WF) : m.getKey? a = some a' → a' ∈ m := by simp [← contains_iff_mem] simp_to_raw using Raw₀.contains_of_getKey?_eq_some +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.WF) : + m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := by + simp [← contains_iff_mem] + simp_to_raw using Raw₀.getKey?_eq_some_iff + theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.contains a = false → m.getKey? a = none := by simp_to_raw using Raw₀.getKey?_eq_none diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 938615d21d..98ad00628b 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -535,6 +535,10 @@ theorem mem_iff_isSome_get? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : a ∈ t ↔ (t.get? a).isSome := by simpa [mem_iff_contains] using contains_eq_isSome_get? h +theorem get?_eq_some_iff [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} : + t.get? k = some v ↔ ∃ h, t.get k h = v := by + simp_to_model [contains, get?, get] using List.getValueCast?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : t.contains a = false → t.get? a = none := by simp_to_model [contains, get?] using List.getValueCast?_eq_none @@ -596,6 +600,10 @@ theorem mem_iff_isSome_get? [TransOrd α] (h : t.WF) {a : α} : a ∈ t ↔ (get? t a).isSome := by simpa [mem_iff_contains] using contains_eq_isSome_get? h +theorem get?_eq_some_iff [TransOrd α] (h : t.WF) {k : α} {v : β} : + get? t k = some v ↔ ∃ h, get t k h = v := by + simp_to_model [contains, Const.get?, Const.get] using List.getValue?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} : t.contains a = false → get? t a = none := by simp_to_model [Const.get?, contains] using List.getValue?_eq_none.mpr @@ -1051,6 +1059,10 @@ theorem mem_of_getKey?_eq_some [TransOrd α] {a a' : α} (h : t.WF) : t.getKey? a = some a' → a' ∈ t := by simp_to_model [getKey?, contains] using List.containsKey_of_getKey?_eq_some +theorem getKey?_eq_some_iff [TransOrd α] {k k' : α} (h : t.WF) : + t.getKey? k = some k' ↔ ∃ h, t.getKey k h = k' := by + simp_to_model [getKey?, contains, getKey] using List.getKey?_eq_some_iff' + theorem getKey?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} : t.contains a = false → t.getKey? a = none := by simp_to_model [contains, getKey?] using List.getKey?_eq_none diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 08d78fbbfc..d283c52195 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -254,6 +254,10 @@ theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : (t.get? a).isSome ↔ a ∈ t := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + t.get? k = some v ↔ ∃ h, t.get k h = v := + Impl.get?_eq_some_iff t.wf + theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : t.contains a = false → t.get? a = none := Impl.get?_eq_none_of_contains_eq_false t.wf @@ -307,6 +311,10 @@ theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} : a ∈ t ↔ (get? t a).isSome := Impl.Const.mem_iff_isSome_get? t.wf +theorem get?_eq_some_iff [TransCmp cmp] {k : α} {v : β} : + get? t k = some v ↔ ∃ h, get t k h = v := + Impl.Const.get?_eq_some_iff t.wf + @[simp] theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} : (get? t a).isSome ↔ a ∈ t := @@ -694,6 +702,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} : t.getKey? k = some k' → k' ∈ t := Impl.mem_of_getKey?_eq_some t.wf +theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} : + getKey? t k = some k' ↔ ∃ h, getKey t k h = k' := + Impl.getKey?_eq_some_iff t.wf + theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t.getKey? a = none := Impl.getKey?_eq_none_of_contains_eq_false t.wf diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index 777ef17c3a..8793e4fc86 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -255,6 +255,10 @@ theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} (t.get? a).isSome ↔ a ∈ t := (mem_iff_isSome_get? h).symm +theorem get?_eq_some_iff [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} : + t.get? k = some v ↔ ∃ h, t.get k h = v := + Impl.get?_eq_some_iff h + theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t.get? a = none := Impl.get?_eq_none_of_contains_eq_false h @@ -308,6 +312,10 @@ theorem mem_iff_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} : a ∈ t ↔ (get? t a).isSome := Impl.Const.mem_iff_isSome_get? h +theorem get?_eq_some_iff [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + get? t k = some v ↔ ∃ h, get t k h = v := + Impl.Const.get?_eq_some_iff h + @[simp] theorem isSome_get?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} : (get? t a).isSome ↔ a ∈ t := @@ -697,6 +705,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] (h : t.WF) {k k' : α} : t.getKey? k = some k' → k' ∈ t := Impl.mem_of_getKey?_eq_some h +theorem getKey?_eq_some_iff [TransCmp cmp] (h : t.WF) {k k' : α} : + getKey? t k = some k' ↔ ∃ h, getKey t k h = k' := + Impl.getKey?_eq_some_iff h + theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t.getKey? a = none := Impl.getKey?_eq_none_of_contains_eq_false h diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean index 01431e398d..058f9b0f4c 100644 --- a/src/Std/Data/ExtDHashMap/Lemmas.lean +++ b/src/Std/Data/ExtDHashMap/Lemmas.lean @@ -214,6 +214,10 @@ theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isS theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [LawfulBEq α] {k : α} {v : β k} : + m.get? k = some v ↔ ∃ h : k ∈ m, m.get k h = v := + m.inductionOn fun _ => DHashMap.get?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} : m.contains a = false → m.get? a = none := m.inductionOn fun _ => DHashMap.get?_eq_none_of_contains_eq_false @@ -263,6 +267,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (get? m a).isSome ↔ a ∈ m := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : + get? m k = some v ↔ ∃ h : k ∈ m, get m k h = v := + m.inductionOn fun _ => DHashMap.Const.get?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → get? m a = none := m.inductionOn fun _ => DHashMap.Const.get?_eq_none_of_contains_eq_false @@ -611,6 +619,10 @@ theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (m.getKey? a).isSome ↔ a ∈ m := mem_iff_isSome_getKey?.symm +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} : + m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := + m.inductionOn fun _ => DHashMap.getKey?_eq_some_iff + theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.getKey? k = some k') : k' ∈ m := m.inductionOn (fun _ h => DHashMap.mem_of_getKey?_eq_some h) h diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean index a6324634a5..0ef6e0e105 100644 --- a/src/Std/Data/ExtDTreeMap/Lemmas.lean +++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean @@ -234,6 +234,10 @@ theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : (t.get? a).isSome ↔ a ∈ t := t.inductionOn fun _ => DTreeMap.isSome_get?_iff_mem +theorem get?_eq_some_iff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + t.get? k = some v ↔ ∃ h, t.get k h = v := + t.inductionOn fun _ => DTreeMap.get?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : t.contains a = false → t.get? a = none := t.inductionOn fun _ => DTreeMap.get?_eq_none_of_contains_eq_false @@ -283,6 +287,10 @@ theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} : a ∈ t ↔ (get? t a).isSome := t.inductionOn fun _ => DTreeMap.Const.mem_iff_isSome_get? +theorem get?_eq_some_iff [TransCmp cmp] {k : α} {v : β} : + get? t k = some v ↔ ∃ h, get t k h = v := + t.inductionOn fun _ => DTreeMap.Const.get?_eq_some_iff + @[simp] theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} : (get? t a).isSome ↔ a ∈ t := @@ -650,6 +658,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} : t.getKey? k = some k' → k' ∈ t := t.inductionOn fun _ => DTreeMap.mem_of_getKey?_eq_some +theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} : + getKey? t k = some k' ↔ ∃ h, getKey t k h = k' := + t.inductionOn fun _ => DTreeMap.getKey?_eq_some_iff + theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t.getKey? a = none := t.inductionOn fun _ => DTreeMap.getKey?_eq_none_of_contains_eq_false diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean index 425176c08c..875adf85cc 100644 --- a/src/Std/Data/ExtHashMap/Lemmas.lean +++ b/src/Std/Data/ExtHashMap/Lemmas.lean @@ -229,6 +229,10 @@ theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m[a]?.isSome ↔ a ∈ m := mem_iff_isSome_getElem?.symm +theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : + m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v := + ExtDHashMap.Const.get?_eq_some_iff + theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m[a]? = none := ExtDHashMap.Const.get?_eq_none_of_contains_eq_false @@ -421,6 +425,10 @@ theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.getKey? k = some k') : k' ∈ m := ExtDHashMap.mem_of_getKey?_eq_some h +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} : + m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := + ExtDHashMap.getKey?_eq_some_iff + theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m.getKey? a = none := ExtDHashMap.getKey?_eq_none_of_contains_eq_false diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean index 3380676c57..93670d1ffb 100644 --- a/src/Std/Data/ExtHashSet/Lemmas.lean +++ b/src/Std/Data/ExtHashSet/Lemmas.lean @@ -209,6 +209,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (m.get? a).isSome ↔ a ∈ m := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} : + m.get? k = some k' ↔ ∃ h : k ∈ m, m.get k h = k' := + ExtHashMap.getKey?_eq_some_iff + theorem mem_of_get?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.get? k = some k') : k' ∈ m := ExtHashMap.mem_of_getKey?_eq_some h diff --git a/src/Std/Data/ExtTreeMap/Lemmas.lean b/src/Std/Data/ExtTreeMap/Lemmas.lean index 512a7e475b..5430683905 100644 --- a/src/Std/Data/ExtTreeMap/Lemmas.lean +++ b/src/Std/Data/ExtTreeMap/Lemmas.lean @@ -243,6 +243,10 @@ theorem isSome_getElem?_iff_mem [TransCmp cmp] {a : α} : t[a]?.isSome ↔ a ∈ t := mem_iff_isSome_getElem?.symm +theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} : + t[k]? = some v ↔ ∃ h, t[k] = v := + ExtDTreeMap.Const.get?_eq_some_iff + theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t[a]? = none := ExtDTreeMap.Const.get?_eq_none_of_contains_eq_false @@ -445,6 +449,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} : t.getKey? k = some k' → k' ∈ t := ExtDTreeMap.mem_of_getKey?_eq_some +theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} : + getKey? t k = some k' ↔ ∃ h, getKey t k h = k' := + ExtDTreeMap.getKey?_eq_some_iff + theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t.getKey? a = none := ExtDTreeMap.getKey?_eq_none_of_contains_eq_false @@ -757,10 +765,6 @@ instance [TransCmp cmp] : LawfulGetElem (ExtTreeMap α β cmp) α β (fun m a => rw [getElem!_eq_get!_getElem?] split <;> simp_all -theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} : - t[k]? = some v ↔ ∃ h : k ∈ t, t[k] = v := - _root_.getElem?_eq_some_iff - @[simp, grind =] theorem length_keys [TransCmp cmp] : t.keys.length = t.size := diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean index 78c506165d..a380c452b4 100644 --- a/src/Std/Data/ExtTreeSet/Lemmas.lean +++ b/src/Std/Data/ExtTreeSet/Lemmas.lean @@ -225,6 +225,10 @@ theorem mem_of_get?_eq_some [TransCmp cmp] {k k' : α} (h : t.get? k = some k') : k' ∈ t := ExtTreeMap.mem_of_getKey?_eq_some h +theorem get?_eq_some_iff [TransCmp cmp] {k k' : α} : + t.get? k = some k' ↔ ∃ h, t.get k h = k' := + ExtTreeMap.getKey?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t.get? a = none := ExtTreeMap.getKey?_eq_none_of_contains_eq_false diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 1bd1ff7a14..033b62df18 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -284,6 +284,10 @@ theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m[a]?.isSome ↔ a ∈ m := mem_iff_isSome_getElem?.symm +theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : + m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v := + DHashMap.Const.get?_eq_some_iff + theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m[a]? = none := DHashMap.Const.get?_eq_none_of_contains_eq_false @@ -509,6 +513,10 @@ theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.getKey? k = some k') : k' ∈ m := DHashMap.mem_of_getKey?_eq_some h +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} : + m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := + DHashMap.getKey?_eq_some_iff + theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m.getKey? a = none := DHashMap.getKey?_eq_none_of_contains_eq_false @@ -828,10 +836,6 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β rw [getElem!_eq_get!_getElem?] split <;> simp_all -theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : - m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v := - _root_.getElem?_eq_some_iff - @[simp, grind =] theorem length_keys [EquivBEq α] [LawfulHashable α] : m.keys.length = m.size := diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 9ef6a775e0..2dc175116f 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -298,6 +298,10 @@ theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a (m[a]?).isSome ↔ a ∈ m := (mem_iff_isSome_getElem? h).symm +theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} : + m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v := + DHashMap.Raw.Const.get?_eq_some_iff h.out + theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.contains a = false → m[a]? = none := DHashMap.Raw.Const.get?_eq_none_of_contains_eq_false h.out @@ -563,11 +567,14 @@ theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : (m.getKey? a).isSome ↔ a ∈ m := (mem_iff_isSome_getKey? h).symm -theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] - {a a' : α} (h : m.WF) : +theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {a a' : α} (h : m.WF) : m.getKey? a = some a' → a' ∈ m := DHashMap.Raw.mem_of_getKey?_eq_some h.out +theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.WF) : + m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := + DHashMap.Raw.getKey?_eq_some_iff h.out + @[simp, grind =] theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} : (m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h h') := diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index ca464f9655..01bf95f31a 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -257,6 +257,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (m.get? a).isSome ↔ a ∈ m := mem_iff_isSome_get?.symm +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} : + m.get? k = some k' ↔ ∃ h : k ∈ m, m.get k h = k' := + HashMap.getKey?_eq_some_iff + theorem mem_of_get?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.get? k = some k') : k' ∈ m := HashMap.mem_of_getKey?_eq_some h diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 889e8ad1be..60cf450f2d 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -269,6 +269,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α (m.get? a).isSome ↔ a ∈ m := (mem_iff_isSome_get? h).symm +theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} : + m.get? k = some k' ↔ ∃ h : k ∈ m, m.get k h = k' := + HashMap.Raw.getKey?_eq_some_iff h.out + theorem mem_of_get?_eq_some [EquivBEq α] [LawfulHashable α] (h : m.WF) {a a' : α} : m.get? a = some a' → a' ∈ m := HashMap.Raw.mem_of_getKey?_eq_some h.out @@ -784,6 +788,12 @@ theorem ofList_cons {hd : α} {tl : List α} : ofList (hd :: tl) = insertMany ((∅ : Raw α).insert hd) tl := ext HashMap.Raw.unitOfList_cons +theorem ofList_eq_insertMany_empty {l : List α} : + ofList l = insertMany (∅ : Raw α) l := + match l with + | [] => by simp [insertMany_nil .empty] + | hd :: tl => by simp [ofList_cons, insertMany_cons .empty] + @[simp, grind =] theorem contains_ofList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 12e5f52332..8778fc2f22 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -547,6 +547,12 @@ theorem getValue?_eq_some_getValue [BEq α] {l : List ((_ : α) × β)} {a : α} getValue? a l = some (getValue a l h) := by simp [getValue] +theorem getValue?_eq_some_iff [BEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : + getValue? k l = some v ↔ ∃ h : containsKey k l, getValue k l h = v := by + by_cases h : containsKey k l + · simp [h, getValue?_eq_some_getValue] + · simp [getValue?_eq_none.mpr (Bool.not_eq_true _ ▸ h), h] + theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) : getValue a (⟨k, v⟩ :: l) (containsKey_cons_of_beq h) = v := by simp [getValue, getValue?_cons_of_true h] @@ -603,6 +609,12 @@ theorem getValueCast?_eq_some_getValueCast [BEq α] [LawfulBEq α] {l : List ((a (h : containsKey a l) : getValueCast? a l = some (getValueCast a l h) := by simp [getValueCast] +theorem getValueCast?_eq_some_iff [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : + getValueCast? k l = some v ↔ ∃ h : containsKey k l, getValueCast k l h = v := by + by_cases h : containsKey k l + · simp [h, getValueCast?_eq_some_getValueCast] + · simp [getValueCast?_eq_none (Bool.not_eq_true _ ▸ h), h] + theorem getValueCast_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : containsKey a (⟨k, v⟩ :: l)) : getValueCast a (⟨k, v⟩ :: l) h = @@ -884,6 +896,15 @@ theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} · rfl · exact getKey?_eq_some_getKey _ +theorem getKey?_eq_some_iff' [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k'} : + getKey? k l = some k' ↔ ∃ h, getKey k l h = k' := by + by_cases h : containsKey k l + · simp [h, getKey?_eq_some_getKey] + · simp only [h] + simp only [containsKey_eq_isSome_getKey?, Bool.not_eq_true, Option.isSome_eq_false_iff, + Option.isNone_iff_eq_none] at h + simp [h] + theorem getKey_beq [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) : getKey a l h == a := by simpa only [getKey?_eq_some_getKey h] using getKey?_beq (l := l) (a := a) diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 908adc99dc..d57a750bc5 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -255,10 +255,18 @@ theorem isSome_getElem?_iff_mem [TransCmp cmp] {a : α} : t[a]?.isSome ↔ a ∈ t := mem_iff_isSome_getElem?.symm +theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} : + t[k]? = some v ↔ ∃ h, t[k] = v := + DTreeMap.Const.get?_eq_some_iff + theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} (h : t.getKey? k = some k') : k' ∈ t := DTreeMap.mem_of_getKey?_eq_some h +theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} : + getKey? t k = some k' ↔ ∃ h, getKey t k h = k' := + DTreeMap.getKey?_eq_some_iff + theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t[a]? = none := DTreeMap.Const.get?_eq_none_of_contains_eq_false @@ -789,10 +797,6 @@ instance [TransCmp cmp] : LawfulGetElem (TreeMap α β cmp) α β (fun m a => a rw [getElem!_eq_get!_getElem?] split <;> simp_all -theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} : - t[k]? = some v ↔ ∃ h : k ∈ t, t[k] = v := - _root_.getElem?_eq_some_iff - @[simp, grind =] theorem length_keys [TransCmp cmp] : t.keys.length = t.size := diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 0f98c2277c..b8083602c9 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -255,6 +255,10 @@ theorem isSome_getElem?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} : t[a]?.isSome ↔ a ∈ t := (mem_iff_isSome_getElem? h).symm +theorem getElem?_eq_some_iff [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + t[k]? = some v ↔ ∃ h, t[k] = v := + DTreeMap.Raw.Const.get?_eq_some_iff h + theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t[a]? = none := DTreeMap.Raw.Const.get?_eq_none_of_contains_eq_false h @@ -465,10 +469,14 @@ theorem isSome_getKey?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} : (t.getKey? a).isSome ↔ a ∈ t := (mem_iff_isSome_getKey? h).symm -theorem mem_of_getKey?_eq_some [TransCmp cmp] {a a' : α} (h : t.WF) : +theorem mem_of_getKey?_eq_some [TransCmp cmp] (h : t.WF) {a a' : α} : t.getKey? a = some a' → a' ∈ t := DTreeMap.Raw.mem_of_getKey?_eq_some h +theorem getKey?_eq_some_iff [TransCmp cmp] (h : t.WF) {k k' : α} : + getKey? t k = some k' ↔ ∃ h, getKey t k h = k' := + DTreeMap.Raw.getKey?_eq_some_iff h + theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t.getKey? a = none := DTreeMap.Raw.getKey?_eq_none_of_contains_eq_false h diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index b0351ede08..ab59f5e773 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -238,6 +238,10 @@ theorem mem_of_get?_eq_some [TransCmp cmp] {k k' : α} (h : t.get? k = some k') : k' ∈ t := TreeMap.mem_of_getKey?_eq_some h +theorem get?_eq_some_iff [TransCmp cmp] {k k' : α} : + t.get? k = some k' ↔ ∃ h, t.get k h = k' := + TreeMap.getKey?_eq_some_iff + theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : t.contains a = false → t.get? a = none := TreeMap.getKey?_eq_none_of_contains_eq_false diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 9bfae375be..9d7a192b2e 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -236,6 +236,10 @@ theorem mem_of_get?_eq_some [TransCmp cmp] (h : t.WF) {a a' : α} : t.get? a = some a' → a' ∈ t := TreeMap.Raw.mem_of_getKey?_eq_some h +theorem get?_eq_some_iff [TransCmp cmp] (h : t.WF) {k k' : α} : + t.get? k = some k' ↔ ∃ h, t.get k h = k' := + TreeMap.Raw.getKey?_eq_some_iff h + theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t.get? a = none := TreeMap.Raw.getKey?_eq_none_of_contains_eq_false h