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)
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)
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
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.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.forIn_eq_forIn_toList
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type w}
{m : Type w → Type w}
[Monad m]
[LawfulMonad m]
{f : (a : α) × β a → δ → m (ForInStep δ)}
{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.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_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k : α}
(contains : k ∈ t)
{h' : Std.DTreeMap.Internal.Impl.contains k (insertManyIfNewUnit t l ⋯).val = true}
:
theorem
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_mem_of_mem
{α : Type u}
{instOrd : Ord α}
{t : Impl α fun (x : α) => Unit}
[TransOrd α]
(h : t.WF)
{l : List α}
{k : α}
(contains : k ∈ t)
{h' : Std.DTreeMap.Internal.Impl.contains k (insertManyIfNewUnit! t l).val = true}
:
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.insertMany_empty_list_cons_eq_insertMany!
{α : Type u}
{β : α → Type v}
{instOrd : Ord α}
{k : α}
{v : β k}
{tl : List ((a : α) × β a)}
:
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.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)}
: