Skip to content

Commit

Permalink
Replace 'm.contains k = false' by '¬ k ∈ m' in statements for insertI…
Browse files Browse the repository at this point in the history 
…fNewUnit
  • Loading branch information
@jt0202
jt0202 committed Jan 14, 2025
1 parent 97f9854 commit aea42fb
Show file tree
Hide file tree
Showing 6 changed files with 176 additions and 162 deletions.
79 changes: 43 additions & 36 deletions src/Std/Data/DHashMap/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -990,7 +990,7 @@ theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
simp [mem_iff_contains]

theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
{l : List ((a : α) × β a)} {k : α} (mem : k ∈ (m.insertMany l))
{l : List ((a : α) × β a)} {k : α} (mem : k ∈ m.insertMany l)
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
k ∈ m :=
Raw₀.contains_of_contains_insertMany_list ⟨m.1, _⟩ m.2 mem contains_eq_false
Expand Down Expand Up @@ -1335,74 +1335,81 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
k ∈ insertManyIfNewUnit m l → k ∈ m :=
Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list ⟨m.1, _⟩ m.2 contains_eq_false

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
(contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
getKey? (insertManyIfNewUnit m l) k = none :=
Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
⟨m.1, _⟩ m.2 contains_eq_false contains_eq_false'
(not_mem : ¬ k ∈ m) (contains_eq_false' : l.contains k = false) :
getKey? (insertManyIfNewUnit m l) k = none := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
⟨m.1, _⟩ m.2 not_mem contains_eq_false'

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' : α} (k_beq : k == k')
(contains_eq_false : m.contains k = false)
(not_mem : ¬ k ∈ m)
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
getKey? (insertManyIfNewUnit m l) k' = some k :=
Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩
m.2 k_beq contains_eq_false distinct mem
getKey? (insertManyIfNewUnit m l) k' = some k := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩
m.2 k_beq not_mem distinct mem

theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} (h' : k ∈ m) :
getKey? (insertManyIfNewUnit m l) k = getKey? m k :=
Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains ⟨m.1, _⟩ m.2 h'

theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α}
{k k' : α} (k_beq : k == k')
(contains_eq_false : m.contains k = false) (distinct : l.Pairwise (fun a b => (a == b) = false))
(not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) {h} :
getKey (insertManyIfNewUnit m l) k' h = k :=
Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
contains_eq_false distinct mem
getKey (insertManyIfNewUnit m l) k' h = k := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
not_mem distinct mem

theorem getKey_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} (mem : k ∈ m) {h} :
getKey (insertManyIfNewUnit m l) k h = getKey m k mem :=
Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains ⟨m.1, _⟩ m.2 _

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α}
(contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
getKey! (insertManyIfNewUnit m l) k = default :=
Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
⟨m.1, _⟩ m.2 contains_eq_false contains_eq_false'
(not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
getKey! (insertManyIfNewUnit m l) k = default := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
⟨m.1, _⟩ m.2 not_mem contains_eq_false

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
(contains_eq_false: m.contains k = false) (distinct : l.Pairwise (fun a b => (a == b) = false))
(not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) :
getKey! (insertManyIfNewUnit m l) k' = k :=
Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
contains_eq_false distinct mem
getKey! (insertManyIfNewUnit m l) k' = k := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
not_mem distinct mem

theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] {l : List α} {k : α} (mem : k ∈ m) :
getKey! (insertManyIfNewUnit m l) k = getKey! m k :=
Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains ⟨m.1, _⟩ m.2 mem

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α}
(contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
getKeyD (insertManyIfNewUnit m l) k fallback = fallback :=
Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
⟨m.1, _⟩ m.2 contains_eq_false contains_eq_false'
(not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
getKeyD (insertManyIfNewUnit m l) k fallback = fallback := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
⟨m.1, _⟩ m.2 not_mem contains_eq_false

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' fallback : α} (k_beq : k == k')
(contains_eq_false : m.contains k = false)
(not_mem : ¬ k ∈ m)
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
getKeyD (insertManyIfNewUnit m l) k' fallback = k :=
Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
contains_eq_false distinct mem
getKeyD (insertManyIfNewUnit m l) k' fallback = k := by
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
exact Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
not_mem distinct mem

theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k fallback : α} (mem : k ∈ m) :
Expand Down
35 changes: 21 additions & 14 deletions src/Std/Data/DHashMap/RawLemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1435,16 +1435,18 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :
m.contains k = false → l.contains k = false →
¬ k ∈ m → l.contains k = false →
getKey? (insertManyIfNewUnit m l) k = none := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
(h : m.WF) {l : List α} {k k' : α} (k_beq : k == k') :
m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKey? (insertManyIfNewUnit m l) k' = some k := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
Expand All @@ -1458,23 +1460,26 @@ theorem getKey_insertManyIfNewUnit_list_of_mem
getKey (insertManyIfNewUnit m l) k h' = getKey m k mem := by
simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains

theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
(h : m.WF) {l : List α}
{k k' : α} (k_beq : k == k') {h'} :
m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKey (insertManyIfNewUnit m l) k' h' = k := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α} :
m.contains k = false → l.contains k = false → getKey! (insertManyIfNewUnit m l) k = default := by
¬ k ∈ m → l.contains k = false → getKey! (insertManyIfNewUnit m l) k = default := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using
Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k') :
contains m k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKey! (insertManyIfNewUnit m l) k' = k := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
Expand All @@ -1483,17 +1488,19 @@ theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α
simp only [mem_iff_contains]
simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α} :
m.contains k = false → l.contains k = false →
¬ k ∈ m → l.contains k = false →
getKeyD (insertManyIfNewUnit m l) k fallback = fallback := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using
Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
(h : m.WF) {l : List α} {k k' fallback : α} (k_beq : k == k') :
m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKeyD (insertManyIfNewUnit m l) k' fallback = k := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
Expand Down
56 changes: 28 additions & 28 deletions src/Std/Data/HashMap/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -915,71 +915,71 @@ theorem getD_insertManyIfNewUnit_list
getD (insertManyIfNewUnit m l) k fallback = () := by
simp

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
(contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
(not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
getKey? (insertManyIfNewUnit m l) k = none :=
DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
contains_eq_false contains_eq_false'
DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' : α} (k_beq : k == k') (contains_eq_false : m.contains k = false)
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' : α} (k_beq : k == k') (not_mem : ¬ k ∈ m)
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
getKey? (insertManyIfNewUnit m l) k' = some k :=
DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
k_beq contains_eq_false distinct mem
DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
k_beq not_mem distinct mem

theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} (mem : k ∈ m) :
getKey? (insertManyIfNewUnit m l) k = getKey? m k :=
DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_mem mem

theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' : α} (k_beq : k == k') (contains_eq_false : m.contains k = false)
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' : α} (k_beq : k == k') (not_mem : ¬ k ∈ m)
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h} :
getKey (insertManyIfNewUnit m l) k' h = k :=
DHashMap.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
k_beq contains_eq_false distinct mem
DHashMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
k_beq not_mem distinct mem

theorem getKey_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} (mem : k ∈ m) {h} :
getKey (insertManyIfNewUnit m l) k h = getKey m k mem :=
DHashMap.Const.getKey_insertManyIfNewUnit_list_of_mem mem

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α}
(contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
(not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
getKey! (insertManyIfNewUnit m l) k = default :=
DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
contains_eq_false contains_eq_false'
DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
(contains_eq_false : m.contains k = false)
(not_mem : ¬ k ∈ m)
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
getKey! (insertManyIfNewUnit m l) k' = k :=
DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
k_beq contains_eq_false distinct mem
DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
k_beq not_mem distinct mem

theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] {l : List α} {k : α} (mem : k ∈ m) :
getKey! (insertManyIfNewUnit m l) k = getKey! m k :=
DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_mem mem

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α}
(contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
(not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
getKeyD (insertManyIfNewUnit m l) k fallback = fallback :=
DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
contains_eq_false contains_eq_false'
DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' fallback : α} (k_beq : k == k')
(contains_eq_false : m.contains k = false)
(not_mem : ¬ k ∈ m)
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l ) :
getKeyD (insertManyIfNewUnit m l) k' fallback = k :=
DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
k_beq contains_eq_false distinct mem
DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
k_beq not_mem distinct mem

theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k fallback : α} (mem : k ∈ m) :
Expand Down
Loading

0 comments on commit aea42fb

Please sign in to comment.