Internal lemmas about the tree map #
This file contains internal lemmas about Std.DTreeMap.Internal.Impl. Users of the tree map should
not rely on the contents of this file.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.tacticWf_trivial = Lean.ParserDescr.node `Std.DTreeMap.Internal.Impl.tacticWf_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "wf_trivial" false)
Instances For
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.tacticEmpty = Lean.ParserDescr.node `Std.DTreeMap.Internal.Impl.tacticEmpty 1024 (Lean.ParserDescr.nonReservedSymbol "empty" false)
Instances For
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{k a : α}
{v : β k}
:
a ∈ (insertIfNew k v t ⋯).impl → compare k a ≠ Ordering.eq → a ∈ t
theorem
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{k a : α}
{v : β k}
:
a ∈ insertIfNew! k v t → compare k a ≠ Ordering.eq → a ∈ t
theorem
Std.DTreeMap.Internal.Impl.toList_insert_perm
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[BEq α]
[TransOrd α]
[LawfulBEqOrd α]
(h : t.WF)
{k : α}
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.toList_insert!_perm
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[BEq α]
[TransOrd α]
[LawfulBEqOrd α]
(h : t.WF)
{k : α}
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.Const.toList_insert_perm
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[BEq α]
[TransOrd α]
[LawfulBEqOrd α]
(h : t.WF)
{k : α}
{v : β}
:
theorem
Std.DTreeMap.Internal.Impl.Const.toList_insert!_perm
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[BEq α]
[TransOrd α]
[LawfulBEqOrd α]
(h : t.WF)
{k : α}
{v : β}
:
theorem
Std.DTreeMap.Internal.Impl.getD_empty
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[LawfulEqOrd α]
{a : α}
{fallback : β a}
:
theorem
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew'
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{k a : α}
{v : β k}
:
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
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew!'
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{k a : α}
{v : β k}
:
a ∈ insertIfNew! k v t → ¬(compare k a = Ordering.eq ∧ ¬k ∈ t) → a ∈ t
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
Std.DTreeMap.Internal.Impl.get_insertIfNew
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k a : α}
{v : β k}
{h₁ : a ∈ (insertIfNew k v t ⋯).impl}
:
theorem
Std.DTreeMap.Internal.Impl.get_insertIfNew!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k a : α}
{v : β k}
{h₁ : a ∈ insertIfNew! k v t}
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertIfNew!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k a : α}
[Inhabited (β a)]
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertIfNew
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k a : α}
{fallback : β a}
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertIfNew!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k a : α}
{fallback : β a}
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.getKey_insertIfNew!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{k a : α}
{v : β k}
{h₁ : contains a (insertIfNew! k v t) = true}
:
(insertIfNew! k v t).getKey a h₁ = if h₂ : compare k a = Ordering.eq ∧ ¬k ∈ t then k else t.getKey a ⋯
getThenInsertIfNew? #
theorem
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_fst
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_snd
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{v : β k}
:
getThenInsertIfNew?! #
theorem
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_fst
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{v : β k}
:
theorem
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_snd
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{v : β k}
:
getThenInsertIfNew? #
getThenInsertIfNew?! #
theorem
Std.DTreeMap.Internal.Impl.distinct_keys
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
:
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) t.keys
theorem
Std.DTreeMap.Internal.Impl.ordered_keys
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
:
List.Pairwise (fun (a b : α) => compare a b = Ordering.lt) t.keys
theorem
Std.DTreeMap.Internal.Impl.find?_toList_eq_some_iff_get?_eq_some
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{v : β k}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.ordered_keys_toList
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
:
List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) t.toList
theorem
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toList
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
{f : δ → (a : α) → β a → m δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_toList
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
{f : (a : α) → β a → δ → m δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_keys
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
{f : δ → α → m δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.foldl_eq_foldl_keys
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{f : δ → α → δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_keys
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
{f : α → δ → m δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.foldr_eq_foldr_keys
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{f : α → δ → δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.forIn_eq_forIn_keys
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
{f : α → δ → m (ForInStep δ)}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.Const.foldlM_eq_foldlM_toList
{α : Type u}
{δ : Type w}
{m : Type w → Type w'}
{β : Type v}
{t : Impl α fun (x : α) => β}
[Monad m]
[LawfulMonad m]
{f : δ → α → β → m δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.Const.foldrM_eq_foldrM_toList
{α : Type u}
{δ : Type w}
{m : Type w → Type w'}
{β : Type v}
{t : Impl α fun (x : α) => β}
[Monad m]
[LawfulMonad m]
{f : α → β → δ → m δ}
{init : δ}
:
theorem
Std.DTreeMap.Internal.Impl.Const.forIn_eq_forIn_toList
{α : Type u}
{δ : Type w}
{m : Type w → Type w'}
{β : Type v}
{t : Impl α fun (x : α) => β}
[Monad m]
[LawfulMonad m]
{f : α → β → δ → m (ForInStep δ)}
{init : δ}
:
@[simp]
@[simp]
theorem
Std.DTreeMap.Internal.Impl.contains_of_contains_insertMany_list
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.contains_of_contains_insertMany!_list
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.get?_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.get?_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.get_insertMany_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
(contains : (List.map Sigma.fst l).contains k = false)
{h' : k ∈ (t.insertMany l ⋯).val}
:
theorem
Std.DTreeMap.Internal.Impl.get_insertMany!_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
(contains : (List.map Sigma.fst l).contains k = false)
{h' : k ∈ (t.insertMany! l).val}
:
theorem
Std.DTreeMap.Internal.Impl.get_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
{h' : k' ∈ (t.insertMany l ⋯).val}
:
theorem
Std.DTreeMap.Internal.Impl.get_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
{h' : k' ∈ (t.insertMany! l).val}
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertMany_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
[Inhabited (β k)]
(h' : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertMany!_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
[Inhabited (β k)]
(h' : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
[Inhabited (β k')]
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
[Inhabited (β k')]
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertMany_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
{fallback : β k}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertMany!_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
{fallback : β k}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
{fallback : β k'}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
{fallback : β k'}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKey_insertMany_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
(h₁ : (List.map Sigma.fst l).contains k = false)
{h' : contains k (t.insertMany l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.getKey_insertMany!_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k : α}
(h₁ : (List.map Sigma.fst l).contains k = false)
{h' : contains k (t.insertMany! l).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.getKey_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
{h' : contains k' (t.insertMany l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.getKey_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
{h' : contains k' (t.insertMany! l).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.getKey!_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[Inhabited α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKey!_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[Inhabited α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_insertMany!_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.size_insertMany_list
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
:
theorem
Std.DTreeMap.Internal.Impl.size_insertMany!_list
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List ((a : α) × β a)}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
:
@[simp]
@[simp]
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_list_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
{k : α}
(h₁ : (List.map Prod.fst l).contains k = false)
{h' : contains k (insertMany t l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany!_list_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
{k : α}
(h₁ : (List.map Prod.fst l).contains k = false)
{h' : contains k (insertMany! t l).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
{h' : contains k' (insertMany t l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
{h' : contains k' (insertMany! t l).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany!_list_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[Inhabited α]
(h : t.WF)
{l : List (α × β)}
{k : α}
(h' : (List.map Prod.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[Inhabited α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[Inhabited α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.size_insertMany_list
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.size_insertMany!_list
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get?_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get_insertMany_list_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
{k : α}
(h₁ : (List.map Prod.fst l).contains k = false)
{h' : contains k (insertMany t l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
{k : α}
(h₁ : (List.map Prod.fst l).contains k = false)
{h' : contains k (insertMany! t l).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.get_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
{h' : contains k' (insertMany t l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
{h' : contains k' (insertMany! t l).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertMany_list'
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List (α × β)}
{k : α}
(h' : contains k (insertMany t l ⋯).val = true)
(w :
List.findSomeRev?
(fun (x : α × β) =>
match x with
| (a, b) => if compare a k = Ordering.eq then some b else none)
l = none)
:
A variant of contains_of_contains_insertMany_list used in get_insertMany_list.
theorem
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[Inhabited β]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
{v : β}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get!_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[Inhabited β]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
{v : β}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
{v fallback : β}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getD_insertMany!_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t : Impl α fun (x : α) => β}
[TransOrd α]
(h : t.WF)
{l : List (α × β)}
{k k' : α}
{v fallback : β}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List α}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List α}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKey? k' = some k
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit! t l).val.getKey? k' = some k
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{h' : contains k' (insertManyIfNewUnit t l ⋯).val = true}
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKey k' h' = k
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{h' : contains k' (insertManyIfNewUnit! t l).val = true}
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit! t l).val.getKey k' h' = k
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[Inhabited α]
(h : t.WF)
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKey! k' = k
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit!_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[Inhabited α]
(h : t.WF)
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit! t l).val.getKey! k' = k
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[BEq α]
[LawfulBEqOrd α]
[TransOrd α]
(h : t.WF)
{l : List α}
{k fallback : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[BEq α]
[LawfulBEqOrd α]
[TransOrd α]
(h : t.WF)
{l : List α}
{k fallback : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKeyD k' fallback = k
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
:
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit! t l).val.getKeyD k' fallback = k
theorem
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_list
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit!_list
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit_list
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List α}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit!_list
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
(h : t.WF)
{l : List α}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.unitOfList_eq_insertManyIfNewUnit
{α : Type u}
{instOrd : Ord α}
{l : List α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.unitOfList_eq_insertManyIfNewUnit!
{α : Type u}
{instOrd : Ord α}
{l : List α}
:
theorem
Std.DTreeMap.Internal.Impl.get?_insertMany_empty_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k : α}
(h : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.get?_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.get_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
{h : k' ∈ (empty.insertMany l ⋯).val}
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertMany_empty_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k : α}
[Inhabited (β k)]
(h : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.get!_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
[Inhabited (β k')]
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertMany_empty_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k : α}
{fallback : β k}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.getD_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[LawfulEqOrd α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β k}
{fallback : β k'}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : ⟨k, v⟩ ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKey_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
{h' : contains k' (empty.insertMany l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.getKey!_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
[Inhabited α]
{l : List ((a : α) × β a)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_insertMany_empty_list_of_mem
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
{l : List ((a : α) × β a)}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Sigma.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.size_insertMany_empty_list
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
[TransOrd α]
{l : List ((a : α) × β a)}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
{h : contains k' (insertMany empty l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v : β}
[Inhabited β]
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
{v fallback : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
{h' : contains k' (insertMany empty l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
[Inhabited α]
{l : List (α × β)}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
{β : Type v}
[TransOrd α]
{l : List (α × β)}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_singleton
{α : Type u}
{instOrd : Ord α}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_cons
{α : Type u}
{instOrd : Ord α}
{hd : α}
{tl : List α}
:
(insertManyIfNewUnit empty (hd :: tl) ⋯).val = (insertManyIfNewUnit (insertIfNew hd () empty ⋯).impl tl ⋯).val
theorem
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit!
{α : Type u}
{instOrd : Ord α}
{hd : α}
{tl : List α}
:
(insertManyIfNewUnit empty (hd :: tl) ⋯).val = (insertManyIfNewUnit! (insertIfNew! hd () empty) tl).val
theorem
Std.DTreeMap.Internal.Impl.Const.contains_insertManyIfNewUnit_empty_list
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
{l : List α}
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
(mem : k ∈ l)
{h' : contains k' (insertManyIfNewUnit empty l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
[Inhabited α]
{l : List α}
{k k' : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
[BEq α]
[LawfulBEqOrd α]
{l : List α}
{k fallback : α}
(h' : l.contains k = false)
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
{l : List α}
{k k' fallback : α}
(k_beq : compare k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_empty_list
{α : Type u}
{instOrd : Ord α}
[TransOrd α]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l)
:
@[simp]
@[simp]
theorem
Std.DTreeMap.Internal.Impl.contains_alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.contains_alter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.contains_alter_of_not_compare_eq
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : Option (β k) → Option (β k)}
(he : ¬compare k k' = Ordering.eq)
:
theorem
Std.DTreeMap.Internal.Impl.size_alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.size_alter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.get?_alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.getD_alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{fallback : β k'}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.getD_alter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{fallback : β k'}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_alter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' fallback : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_alter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' fallback : α}
{f : Option (β k) → Option (β k)}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.get?_modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : β k → β k}
:
(modify k f t).get? k' = if h : compare k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
@[simp]
theorem
Std.DTreeMap.Internal.Impl.get?_modify_self
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : β k → β k}
:
theorem
Std.DTreeMap.Internal.Impl.get_modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{f : β k → β k}
{hc : k' ∈ modify k f t}
:
theorem
Std.DTreeMap.Internal.Impl.get!_modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
[hi : Inhabited (β k')]
{f : β k → β k}
:
(modify k f t).get! k' = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
theorem
Std.DTreeMap.Internal.Impl.getD_modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' : α}
{fallback : β k'}
{f : β k → β k}
:
(modify k f t).getD k' fallback = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
else t.getD k' fallback
@[simp]
theorem
Std.DTreeMap.Internal.Impl.getD_modify_self
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{fallback : β k}
{f : β k → β k}
:
theorem
Std.DTreeMap.Internal.Impl.getKey!_modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
[Inhabited α]
{k k' : α}
{f : β k → β k}
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k k' fallback : α}
{f : β k → β k}
:
theorem
Std.DTreeMap.Internal.Impl.min?_keys
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[Min α]
[LE α]
[LawfulOrderOrd α]
[LawfulOrderMin α]
[LawfulOrderLeftLeaningMin α]
[LawfulEqOrd α]
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.head?_keys
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[Min α]
[LE α]
[LawfulOrderOrd α]
[LawfulOrderMin α]
[LawfulOrderLeftLeaningMin α]
[LawfulEqOrd α]
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.minKey?_alter_eq_self
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.minKey?_alter!_eq_self
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.maxKey?_alter_eq_self
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.maxKey?_alter!_eq_self
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t.WF)
{k : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.DTreeMap.Internal.Impl.Equiv.insert
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{v : β k}
:
(Impl.insert k v t₁ ⋯).impl.Equiv (Impl.insert k v t₂ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.insert!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{v : β k}
:
(Impl.insert! k v t₁).Equiv (Impl.insert! k v t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.erase
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
:
(Impl.erase k t₁ ⋯).impl.Equiv (Impl.erase k t₂ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.erase!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
:
(Impl.erase! k t₁).Equiv (Impl.erase! k t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.insertIfNew
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{v : β k}
:
(Impl.insertIfNew k v t₁ ⋯).impl.Equiv (Impl.insertIfNew k v t₂ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.insertIfNew!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{v : β k}
:
(Impl.insertIfNew! k v t₁).Equiv (Impl.insertIfNew! k v t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.alter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{f : Option (β k) → Option (β k)}
:
(Impl.alter k f t₁ ⋯).impl.Equiv (Impl.alter k f t₂ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.alter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{f : Option (β k) → Option (β k)}
:
(Impl.alter! k f t₁).Equiv (Impl.alter! k f t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.modify
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{f : β k → β k}
:
(Impl.modify k f t₁).Equiv (Impl.modify k f t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.filter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{f : (a : α) → β a → Bool}
:
(Impl.filter f t₁ ⋯).impl.Equiv (Impl.filter f t₂ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{f : (a : α) → β a → Bool}
:
(Impl.filter! f t₁).Equiv (Impl.filter! f t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.filterMap!
{α : Type u}
{β : α → Type v}
{γ : α → Type w}
{instOrd : Ord α}
{t₁ t₂ : Impl α β}
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{f : (a : α) → β a → Option (γ a)}
:
(Impl.filterMap! f t₁).Equiv (Impl.filterMap! f t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.mergeWith
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ t₃ t₄ : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t₁.Equiv t₂)
(h' : t₃.Equiv t₄)
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h₃ : t₃.WF)
(h₄ : t₄.WF)
{f : (a : α) → β a → β a → β a}
:
(Impl.mergeWith f t₁ t₃ ⋯).impl.Equiv (Impl.mergeWith f t₂ t₄ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.mergeWith!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ t₂ t₃ t₄ : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
(h : t₁.Equiv t₂)
(h' : t₃.Equiv t₄)
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h₃ : t₃.WF)
(h₄ : t₄.WF)
{f : (a : α) → β a → β a → β a}
:
(Impl.mergeWith! f t₁ t₃).Equiv (Impl.mergeWith! f t₂ t₄)
theorem
Std.DTreeMap.Internal.Impl.Equiv.constAlter!
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t₁ t₂ : Impl α fun (x : α) => β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{f : Option β → Option β}
:
(Const.alter! k f t₁).Equiv (Const.alter! k f t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.constModify
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t₁ t₂ : Impl α fun (x : α) => β}
[TransOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : t₁.Equiv t₂)
{k : α}
{f : β → β}
:
(Const.modify k f t₁).Equiv (Const.modify k f t₂)
theorem
Std.DTreeMap.Internal.Impl.Equiv.constMergeWith
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t₁ t₂ t₃ t₄ : Impl α fun (x : α) => β}
[TransOrd α]
(h : t₁.Equiv t₂)
(h' : t₃.Equiv t₄)
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h₃ : t₃.WF)
(h₄ : t₄.WF)
{f : α → β → β → β}
:
(Const.mergeWith f t₁ t₃ ⋯).impl.Equiv (Const.mergeWith f t₂ t₄ ⋯).impl
theorem
Std.DTreeMap.Internal.Impl.Equiv.constMergeWith!
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t₁ t₂ t₃ t₄ : Impl α fun (x : α) => β}
[TransOrd α]
(h : t₁.Equiv t₂)
(h' : t₃.Equiv t₄)
(h₁ : t₁.WF)
(h₂ : t₂.WF)
(h₃ : t₃.WF)
(h₄ : t₄.WF)
{f : α → β → β → β}
:
(Const.mergeWith! f t₁ t₃).Equiv (Const.mergeWith! f t₂ t₄)
theorem
Std.DTreeMap.Internal.Impl.Equiv.of_forall_constGet?_eq
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t₁ t₂ : Impl α fun (x : α) => β}
[TransOrd α]
[LawfulEqOrd α]
(h₁ : t₁.WF)
(h₂ : t₂.WF)
:
(∀ (k : α), Const.get? t₁ k = Const.get? t₂ k) → t₁.Equiv t₂
theorem
Std.DTreeMap.Internal.Impl.insertMany!_list_equiv_foldl
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ : Impl α β}
{l : List ((a : α) × β a)}
:
(t₁.insertMany! l).val.Equiv (List.foldl (fun (acc : Impl α β) (p : (a : α) × β a) => insert! p.fst p.snd acc) t₁ l)
theorem
Std.DTreeMap.Internal.Impl.insertManyIfNew_list_equiv_foldl
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ : Impl α β}
{l : List ((a : α) × β a)}
(h : t₁.WF)
:
(t₁.insertManyIfNew l ⋯).val.Equiv
(List.foldl (fun (acc : Impl α β) (p : (a : α) × β a) => insertIfNew! p.fst p.snd acc) t₁ l)
theorem
Std.DTreeMap.Internal.Impl.insertManyIfNew!_list_equiv_foldl
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t₁ : Impl α β}
{l : List ((a : α) × β a)}
:
(t₁.insertManyIfNew! l).val.Equiv
(List.foldl (fun (acc : Impl α β) (p : (a : α) × β a) => insertIfNew! p.fst p.snd acc) t₁ l)
theorem
Std.DTreeMap.Internal.Impl.Const.insertMany_list_equiv_foldl
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{t₁ : Impl α fun (x : α) => β}
{l : List (α × β)}
(h : t₁.WF)
:
(insertMany t₁ l ⋯).val.Equiv
(List.foldl (fun (acc : Impl α fun (x : α) => β) (p : α × β) => insert! p.fst p.snd acc) t₁ l)
theorem
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_list_equiv_foldl
{α : Type u}
{instOrd : Ord α}
{t₁ : Impl α fun (x : α) => Unit}
{l : List α}
(h : t₁.WF)
:
(insertManyIfNewUnit t₁ l ⋯).val.Equiv
(List.foldl (fun (acc : Impl α fun (a : α) => Unit) (a : α) => insertIfNew! a () acc) t₁ l)
theorem
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_list_equiv_foldl
{α : Type u}
{instOrd : Ord α}
{t₁ : Impl α fun (x : α) => Unit}
{l : List α}
:
(insertManyIfNewUnit! t₁ l).val.Equiv
(List.foldl (fun (acc : Impl α fun (a : α) => Unit) (a : α) => insertIfNew! a () acc) t₁ l)
theorem
Std.DTreeMap.Internal.Impl.toList_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
(filterMap! f t).toList = List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
theorem
Std.DTreeMap.Internal.Impl.isEmpty_filterMap_iff
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.isEmpty_filterMap!_iff
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.isEmpty_filterMap_eq_false_iff
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.isEmpty_filterMap!_eq_false_iff
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.contains_filterMap
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.contains_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.size_filterMap_eq_size_iff
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.size_filterMap!_eq_size_iff
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.isSome_apply_of_contains_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
(h : t.WF)
(h' : contains k (filterMap! f t) = true)
:
theorem
Std.DTreeMap.Internal.Impl.get_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
(h : t.WF)
{h' : k ∈ filterMap! f t}
:
theorem
Std.DTreeMap.Internal.Impl.getD_filterMap
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
{fallback : γ k}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getD_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
{fallback : γ k}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_filterMap
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_filterMap
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k fallback : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_filterMap!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Option (γ a)}
{k fallback : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.Const.toList_filterMap!
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{γ : Type w}
{t : Impl α fun (x : α) => β}
{f : α → β → Option γ}
(h : t.WF)
:
toList (filterMap! f t) = List.filterMap (fun (p : α × β) => Option.map (fun (x : γ) => (p.fst, x)) (f p.fst p.snd)) (toList t)
theorem
Std.DTreeMap.Internal.Impl.filterMap!_equiv_filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{f : (a : α) → β a → Bool}
(h : t.WF)
:
(filterMap! (fun (k : α) => Option.guard fun (v : β k) => f k v) t).Equiv (filter! f t)
theorem
Std.DTreeMap.Internal.Impl.contains_filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.get?_filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.keys_filter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.keys_filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKey?_filter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKey!_filter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
[Inhabited α]
{f : (a : α) → β a → Bool}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKey!_filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
[Inhabited α]
{f : (a : α) → β a → Bool}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_filter
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
{k fallback : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.getKeyD_filter!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → Bool}
{k fallback : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.get?_map
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{t : Impl α β}
{γ : α → Type w}
[TransOrd α]
[LawfulEqOrd α]
{f : (a : α) → β a → γ a}
{k : α}
(h : t.WF)
:
theorem
Std.DTreeMap.Internal.Impl.Const.get?_map
{α : Type u}
{instOrd : Ord α}
{β : Type v}
{γ : Type w}
{t : Impl α fun (x : α) => β}
[TransOrd α]
[LawfulEqOrd α]
{f : α → β → γ}
{k : α}
(h : t.WF)
:
def
Std.DTreeMap.Internal.Impl.decidableEquiv
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
[(k : α) → BEq (β k)]
[∀ (k : α), LawfulBEq (β k)]
(t₁ t₂ : Impl α β)
(h₁ : t₁.WF)
(h₂ : t₂.WF)
:
Internal implementation detail
Equations
- t₁.decidableEquiv t₂ h₁ h₂ = decidable_of_iff (t₁.beq t₂ = true) ⋯