@[irreducible]

def Trie.Raw.Equiv {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t₁ t₂ : Raw α β) : Prop

Equations

• t₁.Equiv t₂ = (t₁.val = t₂.val ∧ (∀ (k : α) (a : Trie.Raw α β), t₁.get1? k = some a → ∃ (b : Trie.Raw α β) (_ : t₂.get1? k = some b), a.Equiv b) ∧ ∀ (k : α) (b : Trie.Raw α β), t₂.get1? k = some b → ∃ (a : Trie.Raw α β) (_ : t₁.get1? k = some a), a.Equiv b)

@[simp]

theorem Trie.Raw.Equiv.refl {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} : t.Equiv t

theorem Trie.Raw.Equiv.symm {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (h : t₁.Equiv t₂) : t₂.Equiv t₁

theorem Trie.Raw.Equiv.comm {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} : t₁.Equiv t₂ ↔ t₂.Equiv t₁

theorem Trie.Raw.Equiv.trans {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ t₃ : Raw α β} (h₁ : t₁.Equiv t₂) (h₂ : t₂.Equiv t₃) : t₁.Equiv t₃

theorem Trie.Raw.Equiv.iseqv {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : Equivalence Equiv

@[instance_reducible]

instance Trie.Raw.Setoid {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : _root_.Setoid (Raw α β)

Equations

• Trie.Raw.Setoid = { r := Trie.Raw.Equiv, iseqv := ⋯ }

theorem Trie.Raw.Equiv.depth_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) : t₁.depth = t₂.depth

theorem Trie.Raw.Equiv.get1? {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) {k : α} {t : Raw α β} (h : t₁.get1? k = some t) : ∃ (t' : Raw α β), t₂.get1? k = some t' ∧ t'.Equiv t

theorem Trie.Raw.Equiv.get1?' {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) {k : α} {t : Raw α β} (h : t₂.get1? k = some t) : ∃ (t' : Raw α β), t₁.get1? k = some t' ∧ t'.Equiv t

theorem Trie.Raw.Equiv.mem {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) {k : α} : k ∈ t₁.mp ↔ k ∈ t₂.mp

theorem Trie.Raw.Equiv.size_mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) : t₁.mp.size = t₂.mp.size

theorem Trie.Raw.Equiv.iff_alt' {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} : t₁.Equiv t₂ ↔ t₁.val = t₂.val ∧ t₁.mp.size = t₂.mp.size ∧ ∀ (k : α) (x : Raw α β), t₁.get1? k = some x → ∃ (y : Raw α β), t₂.get1? k = some y ∧ x.Equiv y

@[irreducible]

def Trie.Raw.Equiv.Alt {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t₁ t₂ : Raw α β) : Prop

Equations

• Trie.Raw.Equiv.Alt t₁ t₂ = (t₁.val = t₂.val ∧ t₁.mp.size = t₂.mp.size ∧ ∀ (k : α) (a : Trie.Raw α β), t₁.get1? k = some a → ∃ (b : Trie.Raw α β) (_ : t₂.get1? k = some b), Trie.Raw.Equiv.Alt a b)

theorem Trie.Raw.Equiv.iff_alt {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} : t₁.Equiv t₂ ↔ Alt t₁ t₂

@[irreducible]

def Trie.Raw.equivComp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb : DecidableEq β] (t₁ t₂ : Raw α β) : Bool

Equations

• t₁.equivComp t₂ = (t₁.val == t₂.val && t₁.mp.size == t₂.mp.size && t₁.mp.foldWith ⋯ (fun (acc : Bool) (k : α) (t₀' : Trie.Raw₀ α β) (h : t₁.mp.get? k = some t₀') => acc && have t₁' := { inner := t₀', wf := ⋯ }; match h : t₂.get1? k with | none => false | some t₂' => t₁'.equivComp t₂') true)

theorem Trie.Raw.equivComp_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} [hb : DecidableEq β] : t₁.equivComp t₂ = (t₁.val == t₂.val && t₁.mp.size == t₂.mp.size && t₁.mp.foldWith ⋯ (fun (acc : Bool) (k : α) (t₀' : Raw₀ α β) (h : t₁.mp.get? k = some t₀') => acc && (t₂.get1? k).elim false { inner := t₀', wf := ⋯ }.equivComp) true)

theorem Trie.Raw.equiv_iff_equivComp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} [hb : DecidableEq β] : t₁.Equiv t₂ ↔ t₁.equivComp t₂ = true

@[instance_reducible]

instance Trie.Raw.instDecidableEquiv {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} [hb : DecidableEq β] : Decidable (t₁.Equiv t₂)

Equations

• Trie.Raw.instDecidableEquiv = decidable_of_bool (t₁.equivComp t₂) ⋯

@[simp]

theorem Trie.Raw.equivComp_eq_decide_equiv {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} [hb : DecidableEq β] : t₁.equivComp t₂ = decide (t₁.Equiv t₂)

theorem Trie.Raw.equivComp_eq_of_equiv2 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb : DecidableEq β] {a₁ b₁ a₂ b₂ : Raw α β} (h₁ : a₁.Equiv a₂) (h₂ : b₁.Equiv b₂) : a₁.equivComp b₁ = a₂.equivComp b₂

theorem Trie.Raw.equivComp_eq_of_equiv2_expl {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb : DecidableEq β] (a₁ b₁ a₂ b₂ : Raw α β) (h₁ : a₁.Equiv a₂) (h₂ : b₁.Equiv b₂) : a₁.equivComp b₁ = a₂.equivComp b₂

theorem Trie.Raw.Equiv.val_eq {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) : t₁.val = t₂.val

theorem Trie.Raw.Equiv.setVal {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Raw α β} (H : t₁.Equiv t₂) {val : Option β} : (t₁.setVal val).Equiv (t₂.setVal val)