Skip to content

Commit

Permalink
Style fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@jt0202
jt0202 committed Jan 14, 2025
1 parent 4a24852 commit 42ee903
Show file tree
Hide file tree
Showing 9 changed files with 190 additions and 195 deletions.
31 changes: 16 additions & 15 deletions src/Std/Data/DHashMap/Internal/List/Associative.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2493,7 +2493,7 @@ theorem containsKey_of_containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq

theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
(h : toInsert.contains k = false) (h': containsKey k l = false) :
(h': containsKey k l = false) (h : toInsert.contains k = false) :
getKey? k (insertListIfNewUnit l toInsert) = none := by
rw [getKey?_eq_getEntry?,
getEntry?_insertListIfNewUnit_of_contains_eq_false h, Option.map_eq_none', getEntry?_eq_none]
Expand All @@ -2502,8 +2502,8 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [B
theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
{k k' : α} (k_beq : k == k')
(distinct : toInsert.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ toInsert) (mem' : containsKey k l = false) :
(mem' : containsKey k l = false)
(distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert):
getKey? k' (insertListIfNewUnit l toInsert) = some k := by
simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some',
Option.or_eq_some, getEntry?_eq_none]
Expand All @@ -2528,12 +2528,12 @@ theorem getKey?_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
theorem getKey_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
{k k' : α} (k_beq : k == k')
{h} (contains_eq_false : containsKey k l = false)
(distinct : toInsert.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ toInsert)
{h} (contains_eq_false : containsKey k l = false) :
(mem : k ∈ toInsert) :
getKey k' (insertListIfNewUnit l toInsert) h = k := by
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq distinct mem contains_eq_false]
getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq contains_eq_false distinct mem]

theorem getKey_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
Expand All @@ -2545,7 +2545,8 @@ theorem getKey_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]

theorem getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α]
[Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
(contains_eq_false : toInsert.contains k = false) (contains_eq_false' : containsKey k l = false):
(contains_eq_false : containsKey k l = false)
(contains_eq_false' : toInsert.contains k = false) :
getKey! k (insertListIfNewUnit l toInsert) = default := by
rw [getKey!_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false
contains_eq_false contains_eq_false']
Expand All @@ -2554,11 +2555,11 @@ theorem getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [B
theorem getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α] [Inhabited α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
{k k' : α} (k_beq : k == k')
(distinct : toInsert.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ toInsert) (h : containsKey k l = false) :
(h : containsKey k l = false)
(distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) :
getKey! k' (insertListIfNewUnit l toInsert) = k := by
rw [getKey!_eq_getKey?,
getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq distinct mem h, Option.get!_some]
getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq h distinct mem, Option.get!_some]

theorem getKey!_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α] [Inhabited α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
Expand All @@ -2569,7 +2570,7 @@ theorem getKey!_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α] [Inhabite

theorem getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α}
(contains_eq_false : toInsert.contains k = false) (contains_eq_false' : containsKey k l = false):
(contains_eq_false : containsKey k l = false) (contains_eq_false' : toInsert.contains k = false) :
getKeyD k (insertListIfNewUnit l toInsert) fallback = fallback := by
rw [getKeyD_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false
contains_eq_false contains_eq_false']
Expand All @@ -2578,11 +2579,11 @@ theorem getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [B
theorem getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
{k k' fallback : α} (k_beq : k == k')
(distinct : toInsert.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ toInsert) (h : containsKey k l = false) :
(h : containsKey k l = false)
(distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) :
getKeyD k' (insertListIfNewUnit l toInsert) fallback = k := by
rw [getKeyD_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq distinct
mem h, Option.getD_some]
rw [getKeyD_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq h
distinct mem, Option.getD_some]

theorem getKeyD_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
{l : List ((_ : α) × Unit)} {toInsert : List α}
Expand Down
71 changes: 34 additions & 37 deletions src/Std/Data/DHashMap/Internal/RawLemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -914,7 +914,7 @@ theorem get!_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)

theorem getD_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
{l : List ((a : α) × β a)} {k : α} {fallback : β k}
(not_mem : (l.map Sigma.fst).contains k = false) :
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(m.insertMany l).1.getD k fallback = m.getD k fallback := by
simp_to_model using getValueCastD_insertList_of_contains_eq_false

Expand Down Expand Up @@ -1191,14 +1191,14 @@ theorem contains_of_contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHasha

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
[EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {l : List α} {k : α} (h' : l.contains k = false) :
m.contains k = false → getKey? (insertManyIfNewUnit m l).1 k = none := by
(h : m.1.WF) {l : List α} {k : α} :
m.contains k = false → l.contains k = false → getKey? (insertManyIfNewUnit m l).1 k = none := by
simp_to_model using getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false

theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
m.contains k = false → getKey? (insertManyIfNewUnit m l).1 k' = some k := by
(h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k') :
m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKey? (insertManyIfNewUnit m l).1 k' = some k := by
simp_to_model using getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem

theorem getKey?_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
Expand All @@ -1213,10 +1213,9 @@ theorem getKey_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashabl

theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {l : List α}
{k k' : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) {h'} :
m.contains k = false → getKey (insertManyIfNewUnit m l).1 k' h' = k := by
{k k' : α} (k_beq : k == k') {h'} :
m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKey (insertManyIfNewUnit m l).1 k' h' = k := by
simp_to_model using getKey_insertListIfNewUnit_of_contains_eq_false_of_mem

theorem getKey_insertManyIfNewUnit_list_mem_of_contains [EquivBEq α] [LawfulHashable α]
Expand All @@ -1225,16 +1224,15 @@ theorem getKey_insertManyIfNewUnit_list_mem_of_contains [EquivBEq α] [LawfulHas
simp_to_model using getKey_insertListIfNewUnit_of_contains

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {l : List α} {k : α}
(contains_eq_false : l.contains k = false) :
m.contains k = false → getKey! (insertManyIfNewUnit m l).1 k = default := by
[EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {l : List α} {k : α} :
m.contains k = false → l.contains k = false →
getKey! (insertManyIfNewUnit m l).1 k = default := by
simp_to_model using getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false

theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] (h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) :
contains m k = false → getKey! (insertManyIfNewUnit m l).1 k' = k := by
[Inhabited α] (h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k') :
contains m k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKey! (insertManyIfNewUnit m l).1 k' = k := by
simp_to_model using getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem

theorem getKey!_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
Expand All @@ -1243,16 +1241,14 @@ theorem getKey!_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashab
simp_to_model using getKey!_insertListIfNewUnit_of_contains

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List α} {k fallback : α}
(h' : l.contains k = false) :
m.contains k = false → getKeyD (insertManyIfNewUnit m l).1 k fallback = fallback := by
[EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List α} {k fallback : α} :
m.contains k = false → l.contains k = false → getKeyD (insertManyIfNewUnit m l).1 k fallback = fallback := by
simp_to_model using getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false

theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {l : List α} {k k' fallback : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) :
m.contains k = false → getKeyD (insertManyIfNewUnit m l).1 k' fallback = k := by
(h : m.1.WF) {l : List α} {k k' fallback : α} (k_beq : k == k') :
m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
getKeyD (insertManyIfNewUnit m l).1 k' fallback = k := by
simp_to_model using getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem

theorem getKeyD_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
Expand Down Expand Up @@ -1618,53 +1614,54 @@ theorem contains_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α
theorem getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
{l : List α} {k : α} (h' : l.contains k = false) :
getKey? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k = none := by
simp [getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
_ Raw.WF.empty₀ h']
exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀
contains_empty h'

theorem getKey?_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
getKey? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' = some k := by
simp [getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
distinct mem contains_empty]
exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
contains_empty distinct mem

theorem getKey_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α}
{k k' : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) {h'} :
getKey (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' h' = k := by
simp [getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
distinct mem contains_empty]
exact getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
contains_empty distinct mem

theorem getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
[Inhabited α] {l : List α} {k : α}
(h' : l.contains k = false) :
getKey! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k = default := by
simp [getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀ h']
exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀
contains_empty h'

theorem getKey!_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
[Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) :
getKey! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' = k := by
simp [getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
distinct mem contains_empty]
exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
contains_empty distinct mem

theorem getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
{l : List α} {k fallback : α}
(h' : l.contains k = false) :
getKeyD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k fallback = fallback := by
simp [getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
_ Raw.WF.empty₀ h']
exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
_ Raw.WF.empty₀ contains_empty h'

theorem getKeyD_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
{l : List α} {k k' fallback : α} (k_beq : k == k')
(distinct : l.Pairwise (fun a b => (a == b) = false))
(mem : k ∈ l) :
getKeyD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' fallback = k := by
simp [getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
distinct mem contains_empty]
exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
contains_empty distinct mem

theorem size_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α]
{l : List α}
Expand Down
Loading

0 comments on commit 42ee903

Please sign in to comment.