Projects.Util.Data.LeafTrie.Raw0

source

inductive LeafTrie.Raw₀ (α : Type u_1) (β : Type u_2) [DecidableEq α] [Hashable α] :

Type (max u_1 u_2)

leaf {α : Type u_1} {β : Type u_2} [DecidableEq α] [Hashable α] : β → Raw₀ α β
node {α : Type u_1} {β : Type u_2} [DecidableEq α] [Hashable α] : (Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Raw₀ α β

Instances For

source

def LeafTrie.Raw₀.isLeaf {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) :

Bool

Equations

(LeafTrie.Raw₀.leaf a).isLeaf = true
t.isLeaf = false

Instances For

source

def LeafTrie.Raw₀.isNode {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) :

Bool

Equations

(LeafTrie.Raw₀.node a).isNode = true
t.isNode = false

Instances For

source

class inductive LeafTrie.Raw₀.WF {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Raw₀ α β → Prop

leaf {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : β} : (Raw₀.leaf x).WF
node {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (k : α) => Raw₀ α β} : mp.WF → (∀ (k : α) (t₁ : Raw₀ α β), mp.get? k = some t₁ → t₁.WF) → (Raw₀.node mp).WF

Instances

source

theorem LeafTrie.Raw₀.rec_3_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)} {M₁ : Raw₀ α β → Sort u_3} {M₂ : (Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Sort u_3} {M₃ : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₄ : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₅ : (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {H₁ : (a : β) → M₁ (leaf a)} {H₂ : (a : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → M₂ a → M₁ (node a)} {H₃ : (size : ℕ) → (buckets : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₃ buckets → M₂ { size := size, buckets := buckets }} {H₄ : (toList : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₄ toList → M₃ { toList := toList }} {H₅ : M₄ []} {H₆ : (head : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → (tail : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₅ head → M₄ tail → M₄ (head :: tail)} {H₇ : M₅ Std.DHashMap.Internal.AssocList.nil} {H₈ : (key : α) → (value : (fun (x : α) => Raw₀ α β) key) → (tail : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → M₁ value → M₅ tail → M₅ (Std.DHashMap.Internal.AssocList.cons key value tail)} :

rec_3 H₁ H₂ H₃ H₄ H₅ H₆ H₇ H₈ xs = List.rec H₅ (fun (x : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) (xs : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) (acc : M₄ xs) => H₆ x xs (rec_4 H₁ H₂ H₃ H₄ H₅ H₆ H₇ H₈ x) acc) xs

source

theorem LeafTrie.Raw₀.rec_4_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β} {M₁ : Raw₀ α β → Sort u_3} {M₂ : (Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → Sort u_3} {M₃ : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₄ : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → Sort u_3} {M₅ : Sort u_3} {H₁ : (a : β) → M₁ (leaf a)} {H₂ : (a : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → M₂ a → M₁ (node a)} {H₃ : (size : ℕ) → (buckets : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₃ buckets → M₂ { size := size, buckets := buckets }} {H₄ : (toList : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₄ toList → M₃ { toList := toList }} {H₅ : M₄ []} {H₆ : (head : Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → (tail : List (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β)) → M₅ → M₄ tail → M₄ (head :: tail)} {H₇ : M₅} {H₈ : (key : α) → (value : (fun (x : α) => Raw₀ α β) key) → (Std.DHashMap.Internal.AssocList α fun (x : α) => Raw₀ α β) → M₁ value → M₅ → M₅} :

rec_4 H₁ H₂ H₃ H₄ H₅ H₆ H₇ H₈ xs = List.rec H₇ (fun (x : (_ : α) × Raw₀ α β) (xs : List ((_ : α) × Raw₀ α β)) (acc : M₅) => H₈ x.fst x.snd (Std.DHashMap.Internal.AssocList.ofList xs) (rec H₁ H₂ H₃ H₄ H₅ H₆ H₇ H₈ x.snd) acc) xs.toList

source

noncomputable def LeafTrie.Raw₀.depthAux {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) :

ℕ

Equations

t.depthAux = (fun (motive_1 : LeafTrie.Raw₀ α β → Type) (motive_2 : (Std.DHashMap.Raw α fun (x : α) => LeafTrie.Raw₀ α β) → Type) (motive_3 : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) → Type) (motive_4 : List (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) → Type) (motive_5 : (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) → Type) (leaf : (a : β) → motive_1 (LeafTrie.Raw₀.leaf a)) (node : (a : Std.DHashMap.Raw α fun (x : α) => LeafTrie.Raw₀ α β) → motive_2 a → motive_1 (LeafTrie.Raw₀.node a)) (mk : (size : ℕ) → (buckets : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) → motive_3 buckets → motive_2 { size := size, buckets := buckets }) (mk_1 : (toList : List (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) → motive_4 toList → motive_3 { toList := toList }) (nil : motive_4 []) (cons : (head : Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) → (tail : List (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) → motive_5 head → motive_4 tail → motive_4 (head :: tail)) (nil_1 : motive_5 Std.DHashMap.Internal.AssocList.nil) (cons_1 : (key : α) → (value : LeafTrie.Raw₀ α β) → (tail : Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) → motive_1 value → motive_5 tail → motive_5 (Std.DHashMap.Internal.AssocList.cons key value tail)) => LeafTrie.Raw₀.rec leaf node mk mk_1 nil cons nil_1 cons_1 t) (fun (x : LeafTrie.Raw₀ α β) => ℕ) (fun (x : Std.DHashMap.Raw α fun (x : α) => LeafTrie.Raw₀ α β) => ℕ) (fun (x : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) => ℕ) (fun (x : List (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) => ℕ) (fun (x : Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) => ℕ) (fun (x : β) => 0) (fun (x : Std.DHashMap.Raw α fun (x : α) => LeafTrie.Raw₀ α β) (n : ℕ) => n + 1) (fun (x : ℕ) (x_1 : Array (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) (n : ℕ) => n) (fun (x : List (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) (n : ℕ) => n) 0 (fun (x : Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) (x_1 : List (Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β)) (n m : ℕ) => max n m) 0 fun (x : α) (x_1 : LeafTrie.Raw₀ α β) (x_2 : Std.DHashMap.Internal.AssocList α fun (x : α) => LeafTrie.Raw₀ α β) (n m : ℕ) => max n m

Instances For

source

@[simp]

theorem LeafTrie.Raw₀.depthAux_leaf {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : β} :

(leaf x).depthAux = 0

source

theorem LeafTrie.Raw₀.depthAux_lt_of_mem {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {i : α} {t : Raw₀ α β} (h : mp.get? i = some t) :

t.depthAux < (node mp).depthAux

source

def LeafTrie.Raw₀.get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) (k : α) :

Option (Raw₀ α β)

Equations

(LeafTrie.Raw₀.leaf a).get? k = none
(LeafTrie.Raw₀.node mp).get? k = mp.get? k

Instances For

source

theorem LeafTrie.Raw₀.WF.mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp₁ : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} [H : (Raw₀.node mp₁).WF] :

mp₁.WF

source

theorem LeafTrie.Raw₀.WF.mp_get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp₁ : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {k : α} {t : Raw₀ α β} [H : (Raw₀.node mp₁).WF] (h : mp₁.get? k = some t) :

t.WF

source

theorem LeafTrie.Raw₀.WF.get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp₁ : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {k : α} {t : Raw₀ α β} [H : (Raw₀.node mp₁).WF] (h : (Raw₀.node mp₁).get? k = some t) :

t.WF

source

@[irreducible]

def LeafTrie.Raw₀.recAux {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw₀ α β → Sort u_3} (t : Raw₀ α β) (wf : t.WF) (motive₁ : (val : β) → γ (leaf val)) (motive₂ : (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (node mp)) :

γ t

Equations

(LeafTrie.Raw₀.leaf val).recAux wf_2 motive₁ motive₂ = motive₁ val
(LeafTrie.Raw₀.node mp).recAux wf_2 motive₁ motive₂ = motive₂ mp ⋯ fun (i : α) (t : LeafTrie.Raw₀ α β) (h : mp.get? i = some t) => t.recAux ⋯ motive₁ motive₂

Instances For

source

def LeafTrie.Raw₀.rec' {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw₀ α β → Sort u_3} (t : Raw₀ α β) [wf : t.WF] (motive₁ : (val : β) → γ (leaf val)) (motive₂ : (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (node mp)) :

γ t

Equations

t.rec' motive₁ motive₂ = t.recAux wf motive₁ motive₂

Instances For

source

def LeafTrie.Raw₀.depth {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw₀ α β) [wf : t.WF] :

ℕ

Equations

t.depth = t.rec' (fun (x : β) => 0) fun (mp : Std.DHashMap.Raw α fun (x : α) => LeafTrie.Raw₀ α β) (wf : mp.WF) (f : (i : α) → (t : LeafTrie.Raw₀ α β) → mp.get? i = some t → ℕ) => 1 + mp.foldWith wf (fun (acc : ℕ) (k : α) (t : LeafTrie.Raw₀ α β) (h : mp.get? k = some t) => max acc (f k t h)) 0

Instances For

source

def LeafTrie.Raw₀.empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Raw₀ α β

Equations

LeafTrie.Raw₀.empty = LeafTrie.Raw₀.node ∅

Instances For

source

@[instance_reducible]

instance LeafTrie.Raw₀.instEmptyCollection {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

EmptyCollection (Raw₀ α β)

Equations

LeafTrie.Raw₀.instEmptyCollection = { emptyCollection := LeafTrie.Raw₀.empty }

source

theorem LeafTrie.Raw₀.empty_def {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅ = node ∅

source

instance LeafTrie.Raw₀.WF.empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.WF

source

@[simp]

theorem LeafTrie.Raw₀.rec'_leaf {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : β} {γ : Raw₀ α β → Sort u_3} {motive₁ : (val : β) → γ (leaf val)} {motive₂ : (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (node mp)} :

(leaf val).rec' motive₁ motive₂ = motive₁ val

source

@[simp]

theorem LeafTrie.Raw₀.rec'_node {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp₁ : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {γ : Raw₀ α β → Sort u_3} [wf : (node mp₁).WF] {motive₁ : (val : β) → γ (leaf val)} {motive₂ : (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → mp.WF → ((i : α) → (t : Raw₀ α β) → mp.get? i = some t → γ t) → γ (node mp)} :

(node mp₁).rec' motive₁ motive₂ = motive₂ mp₁ ⋯ fun (x : α) (t : Raw₀ α β) (h : mp₁.get? x = some t) => t.recAux ⋯ motive₁ motive₂

source

@[simp]

theorem LeafTrie.Raw₀.depth_leaf {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {val : β} :

(leaf val).depth = 0

source

@[simp]

theorem LeafTrie.Raw₀.get?_leaf {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : β} {k : α} :

(leaf x).get? k = none

source

@[simp]

theorem LeafTrie.Raw₀.get?_node {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {k : α} :

(node mp).get? k = mp.get? k

source

theorem LeafTrie.Raw₀.get?_eq_some_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw₀ α β} {k : α} :

t.get? k = some t₁ ↔ ∃ (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β), node mp = t ∧ mp.get? k = some t₁

source

theorem LeafTrie.Raw₀.WF.of_mp_get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {mp₁ : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {k : α} [wf : (Raw₀.node mp₁).WF] (h : mp₁.get? k = some t) :

t.WF

source

theorem LeafTrie.Raw₀.WF.of_get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw₀ α β} {k : α} [wf : t.WF] (h : t.get? k = some t₁) :

t₁.WF

source

theorem LeafTrie.Raw₀.depth_node {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} [wf : (node mp).WF] :

(node mp).depth = 1 + mp.foldWith ⋯ (fun (acc : ℕ) (x : α) (t : Raw₀ α β) (h : mp.get? x = some t) => max acc t.depth) 0

source

@[simp]

theorem LeafTrie.Raw₀.depth_empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.depth = 1

source

theorem LeafTrie.Raw₀.depth_lt_of_mp_get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} {mp₁ : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {k : α} [wf : (node mp₁).WF] (h : mp₁.get? k = some t) :

t.depth < (node mp₁).depth

source

theorem LeafTrie.Raw₀.depth_lt_of_get? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw₀ α β} {k : α} [wf : t.WF] (h : t.get? k = some t₁) :

t₁.depth < t.depth

source

theorem LeafTrie.Raw₀.WF.of_mem_toList {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {p : (_ : α) × Raw₀ α β} [wf : (Raw₀.node mp).WF] (h : p ∈ mp.toList) :

p.snd.WF

source

theorem LeafTrie.Raw₀.wf_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} :

t.WF ↔ (∃ (x : β), leaf x = t) ∨ ∃ (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β), node mp = t ∧ mp.WF ∧ ∀ (k : α) (t₁ : Raw₀ α β), mp.get? k = some t₁ → t₁.WF

source

theorem LeafTrie.Raw₀.wf_node_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} :

(node mp).WF ↔ mp.WF ∧ ∀ (k : α) (t₁ : Raw₀ α β), mp.get? k = some t₁ → t₁.WF

source

theorem LeafTrie.Raw₀.depthAux_node {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} :

(node mp).depthAux = 1 + List.foldl (fun (acc : ℕ) (x : (_ : α) × Raw₀ α β) => max acc x.snd.depthAux) 0 mp.toList

source

theorem LeafTrie.Raw₀.depthAux_node' {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} (wf : (node mp).WF) :

(node mp).depthAux = 1 + mp.foldWith ⋯ (fun (acc : ℕ) (x : α) (t : Raw₀ α β) (x_1 : mp.get? x = some t) => max acc t.depthAux) 0

source

theorem LeafTrie.Raw₀.depthAux_eq_depth {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw₀ α β} [wf : t.WF] :

t.depthAux = t.depth