From 9bb3511e6cd0b30f565f5c02b093528c44135137 Mon Sep 17 00:00:00 2001 From: monsterkrampe Date: Tue, 3 Dec 2024 16:34:00 +0100 Subject: [PATCH] Shorten List.pairwise statements --- .../DHashMap/Internal/List/Associative.lean | 24 +++++++++---------- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 24 +++++++++---------- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index 217cabfc61ab..9cf1beab8b9f 100644 --- a/src/Std/Data/DHashMap/Internal/List/Associative.lean +++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean @@ -175,7 +175,7 @@ theorem getValueCast?_cons_self [BEq α] [LawfulBEq α] {l : List ((a : α) × theorem getValueCast?_of_mem [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (k' : α ) (v : β k) (k_beq : k == k') (mem : ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : getValueCast? k' l = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by induction l with | nil => simp at mem @@ -928,7 +928,7 @@ theorem DistinctKeys.nil [BEq α] : DistinctKeys ([] : List ((a : α) × β a)) ⟨by simp⟩ theorem DistinctKeys.def [BEq α] {l : List ((a : α) × β a)} : - DistinctKeys l ↔ List.Pairwise (fun a b => (a.1 == b.1) = false) l := + DistinctKeys l ↔ l.Pairwise (fun a b => (a.1 == b.1) = false) := ⟨fun h => by simpa [keys_eq_map, List.pairwise_map] using h.distinct, fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩ @@ -2218,7 +2218,7 @@ theorem getKeyD_insertList_of_mem [BEq α] [EquivBEq α] theorem perm_insertList [BEq α] [ReflBEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) - (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) + (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ containsKey a toInsert)) : Perm (insertList l toInsert) (l ++ toInsert) := by rw [← DistinctKeys.def] at distinct_toInsert @@ -2263,7 +2263,7 @@ theorem perm_insertList [BEq α] [ReflBEq α] [PartialEquivBEq α] theorem length_insertList [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) - (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) + (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ (toInsert.map Sigma.fst).contains a)) : (insertList l toInsert).length = l.length + toInsert.length := by rw [← DistinctKeys.def] at distinct_toInsert @@ -2350,7 +2350,7 @@ theorem getValue?_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α] theorem getValue?_insertList_of_mem [BEq α] [PartialEquivBEq α] {l toInsert : List ((_ : α) × β )} {k k' : α} (k_beq : k == k') {v : β} - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) + (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert) : getValue? k' (insertList l toInsert) = v := by induction toInsert generalizing l with @@ -2394,7 +2394,7 @@ theorem getValue!_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α] theorem getValue!_insertList_of_mem [BEq α] [PartialEquivBEq α] [Inhabited β] {l toInsert : List ((_ : α) × β)} {k k' : α} {v: β} (k_beq : k == k') - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert): + (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert): getValue! k' (insertList l toInsert) = v := by simp only [getValue!_eq_getValue?] rw [getValue?_insertList_of_mem (mem:= mem)] @@ -2412,7 +2412,7 @@ theorem getValueD_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α] theorem getValueD_insertList_of_mem [BEq α] [PartialEquivBEq α] {l toInsert : List ((_ : α) × β)} {k k' : α} {v fallback: β} (k_beq : k == k') - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert): + (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert): getValueD k' (insertList l toInsert) fallback= v := by simp only [getValueD_eq_getValue?] rw [getValue?_insertList_of_mem (mem:= mem)] @@ -2627,7 +2627,7 @@ theorem getKeyD_insertListConst_of_mem [BEq α] [EquivBEq α] theorem length_insertListConst [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) - (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) + (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ (toInsert.map Prod.fst).contains a)) : (insertListConst l toInsert).length = l.length + toInsert.length := by rw [insertListConst_eq_insertList] @@ -2677,7 +2677,7 @@ theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq theorem getValue?_insertListConst_of_mem [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) + (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert) : getValue? k' (insertListConst l toInsert) = v := by rw [insertListConst_eq_insertList] @@ -2698,7 +2698,7 @@ theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq theorem getValue!_insertListConst_of_mem [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k') - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert): + (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert): getValue! k' (insertListConst l toInsert) = v := by rw [insertListConst_eq_insertList, getValue!_insertList_of_mem (k_beq:=k_beq)] · apply pairwise_list_conversion_insertListConst distinct @@ -2716,7 +2716,7 @@ theorem getValueD_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq theorem getValueD_insertListConst_of_mem [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k') - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert): + (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert): getValueD k' (insertListConst l toInsert) fallback= v := by rw [insertListConst_eq_insertList, getValueD_insertList_of_mem (k_beq:= k_beq)] · apply pairwise_list_conversion_insertListConst distinct @@ -3034,7 +3034,7 @@ theorem getKeyD_insertListIfNewUnit_of_mem_of_contains [BEq α] [EquivBEq α] theorem length_insertListIfNewUnit [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} (distinct_l : DistinctKeys l) - (distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) toInsert) + (distinct_toInsert : toInsert.Pairwise (fun a b => (a == b) = false)) (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ toInsert.contains a)) : (insertListIfNewUnit l toInsert).length = l.length + toInsert.length := by induction toInsert generalizing l with diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index d12cb9d954ad..474cf4c8aa96 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -1009,7 +1009,7 @@ theorem get?_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas theorem get?_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) : Const.get? (m.insertMany l).1 k' = v := by simp_to_model using getValue?_insertList_of_mem @@ -1022,7 +1022,7 @@ theorem get_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHash theorem get_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) {h'}: + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) {h'}: Const.get (m.insertMany l).1 k' h' = v := by simp_to_model using getValue_insertList_of_mem @@ -1034,7 +1034,7 @@ theorem get!_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas theorem get!_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) : Const.get! (m.insertMany l).1 k' = v := by simp_to_model using getValue!_insertList_of_mem @@ -1046,7 +1046,7 @@ theorem getD_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas theorem getD_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v fallback: β} (mem: ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) : Const.getD (m.insertMany l).1 k' fallback = v := by simp_to_model using getValueD_insertList_of_mem @@ -1139,14 +1139,14 @@ theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m. theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List (α × β)} - {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l} : + {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)} : (∀ (a : α), ¬ (m.contains a ∧ (l.map Prod.fst).contains a)) → (insertMany m l).1.1.size = m.1.size + l.length := by simp_to_model using length_insertListConst theorem isEmpty_insertMany_list_eq_false_of_isEmpty_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List (α × β)} : - (m.1.isEmpty = false) → (insertMany m l).1.1.isEmpty = false := by + (m.1.isEmpty = false) → (insertMany m l).1.1.isEmpty = false := by simp_to_model using isEmpty_insertListConst_eq_false_of_isEmpty_eq_false theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) @@ -1162,7 +1162,7 @@ theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable theorem get?_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) : get? (insertMany m l).1 k' = v := by simp_to_model using getValue?_insertListConst_of_mem @@ -1175,7 +1175,7 @@ theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable theorem get_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) {h'}: + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) {h'}: get (insertMany m l).1 k' h' = v := by simp_to_model using getValue_insertListConst_of_mem @@ -1187,7 +1187,7 @@ theorem get!_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas theorem get!_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) : get! (insertMany m l).1 k' = v := by simp_to_model using getValue!_insertListConst_of_mem @@ -1199,7 +1199,7 @@ theorem getD_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas theorem getD_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List (α × β)} {k k' : α} (k_beq : k == k') {v fallback: β} (mem: ⟨k, v⟩ ∈ l) - (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) : + (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) : getD (insertMany m l).1 k' fallback = v := by simp_to_model using getValueD_insertListConst_of_mem @@ -1261,7 +1261,7 @@ theorem getKey_insertManyIfNewUnit_list_of_mem_of_contains_eq_false [EquivBEq α {k k' : α} (k_beq : k == k') (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h'} : - m.contains k = false → + m.contains k = false → getKey (insertManyIfNewUnit m l).1 k' h' = k := by simp_to_model using getKey_insertListIfNewUnit_of_mem_of_contains_eq_false @@ -1314,7 +1314,7 @@ theorem getKeyD_insertManyIfNewUnit_list_of_mem_of_contains [EquivBEq α] [Lawfu theorem size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List α} - (distinct : List.Pairwise (fun a b => (a == b) = false) l): + (distinct : l.Pairwise (fun a b => (a == b) = false)): (∀ (a : α), ¬ (m.contains a ∧ l.contains a)) → (insertManyIfNewUnit m l).1.1.size = m.1.size + l.length := by simp_to_model using length_insertListIfNewUnit