def ABTree.access {α β : Type} (t : ABTree α β) (p : Skeleton) : Option (α ⊕ β)

Equations

• (ABTree.leaf a).access [] = some (Sum.inl a)
• (ABTree.node b bL bR).access [] = some (Sum.inr b)
• (ABTree.node i bl bR).access (SkElem.Left :: ps) = bl.access ps
• (ABTree.node i bL br).access (SkElem.Right :: ps) = br.access ps
• t.access p = none

def ABTree.iaccess {α β : Type} {n : ℕ} (t : ABTree α β) (p : ISkeleton n) : Option (α ⊕ β)

Equations

• t.iaccess p = t.access (sequence_forget p)

def ABTree.access_path_value {α β : Type} {n : ℕ} (t : ABTree α β) (p : ISkeleton n) : Option (Sequence n β × α)

Equations

• One or more equations did not get rendered due to their size.
• (ABTree.leaf v).access_path_value p_2 = some (Sequence.nil, v)
• t.access_path_value p = none

theorem access_iaccess {α β : Type} (t : ABTree α β) (p : Skeleton) : t.access p = t.iaccess (sequence_lift p)

theorem ABTree.iaccess_head_left {α β : Type} {n : ℕ} {bl br : ABTree α β} {b : β} {p : ISkeleton n.succ} {res : Option (α ⊕ β)} : Sequence.head p = SkElem.Left → (node b bl br).iaccess p = res → bl.iaccess (Sequence.tail p) = res

theorem ABTree.iaccess_head_right {α β : Type} {n : ℕ} {bl br : ABTree α β} {b : β} {p : ISkeleton n.succ} {res : Option (α ⊕ β)} : Sequence.head p = SkElem.Right → (node b bl br).iaccess p = res → br.iaccess (Sequence.tail p) = res

theorem nil_access {α β : Type} (t : ABTree α β) (a : α) : t.iaccess Sequence.nil = some (Sum.inl a) ↔ t = ABTree.leaf a

def no_dup_elements {α : Type} [DecidableEq α] (t : BTree α) : Prop

Equations

• no_dup_elements t = ∀ (p q : Skeleton) (p_v q_v : α), ¬p = q → ABTree.access t p = some (Sum.inl p_v) → ABTree.access t q = some (Sum.inl q_v) → ¬p_v = q_v

def no_dup_elements_indexed {α : Type} [DecidableEq α] (t : BTree α) : Prop

Equations

• One or more equations did not get rendered due to their size.

def no_dup_path_elems {α : Type} (t : BTree α) : Prop

Equations

• no_dup_path_elems t = t.toList.Nodup

def BTree.toPaths' {α : Type} (t : BTree α) (acc : Skeleton) : List (Skeleton × α)

Equations

• BTree.toPaths' (ABTree.leaf v) acc = [(acc, v)]
• BTree.toPaths' (ABTree.node PUnit.unit bl br) acc = bl.toPaths' (List.concat acc SkElem.Left) ++ br.toPaths' (List.concat acc SkElem.Right)

def ABTree.toPaths' {α β : Type} (t : ABTree α β) (path : Skeleton) : List (Skeleton × (α ⊕ β))

Equations

• (ABTree.leaf v).toPaths' path = [(path, Sum.inl v)]
• (ABTree.node b bl br).toPaths' path = (path, Sum.inr b) :: bl.toPaths' (List.concat path SkElem.Left) ++ br.toPaths' (List.concat path SkElem.Right)

theorem concat_prefix {α : Type} (ls et rs : List α) : ls.append et <+: rs → ls <+: rs

theorem toPaths'_lists_prefix {α β : Type} (t : ABTree α β) (p path : Skeleton) (e : α ⊕ β) : (path, e) ∈ t.toPaths' p → p <+: path

theorem toPaths_append {α β : Type} (acc_p acc_q : Skeleton) (t : ABTree α β) : t.toPaths' (acc_p ++ acc_q) = List.map (fun (x : Skeleton × (α ⊕ β)) => match x with | (ps, e) => (acc_p ++ ps, e)) (t.toPaths' acc_q)

theorem path_toPaths_wk {α β : Type} {x : SkElem} {pr pathTail : Skeleton} {t : ABTree α β} {e : α ⊕ β} (H : (pathTail, e) ∈ t.toPaths' pr) : (x :: pathTail, e) ∈ t.toPaths' (x :: pr)

theorem path_toPaths' {α β : Type} {x : SkElem} {pathTail : Skeleton} {t : ABTree α β} {e : α ⊕ β} (HR : (x :: pathTail, e) ∈ t.toPaths' [x]) : (pathTail, e) ∈ t.toPaths' []

def ABTree.toPaths {α β : Type} (t : ABTree α β) : List (Skeleton × (α ⊕ β))

Equations

• t.toPaths = t.toPaths' []

theorem toPath_are_paths' {α β : Type} (t : ABTree α β) (path : Skeleton) (e : α ⊕ β) : t.access path = some e → (path, e) ∈ t.toPaths

theorem toPath_are_paths {α β : Type} (t : ABTree α β) (path : Skeleton) (e : α ⊕ β) : (path, e) ∈ t.toPaths → t.access path = some e

def BTree.toPaths_elems {α : Type} : BTree α → List (Skeleton × α)

Equations

• BTree.toPaths_elems = (List.filterMap fun (x : Skeleton × (α ⊕ Unit)) => match x.2 with | Sum.inl v => some (x.1, v) | Sum.inr val => none) ∘ ABTree.toPaths

theorem paths_elems_are_paths {α : Type} (t : BTree α) (p : Skeleton) (a : α) : (p, Sum.inl a) ∈ ABTree.toPaths t ↔ (p, a) ∈ t.toPaths_elems

theorem paths_elems_acc_irreverent {α β : Type} (t : ABTree α β) (al bl : Skeleton) : List.map (fun (x : Skeleton × (α ⊕ β)) => x.2) (t.toPaths' al) = List.map (fun (x : Skeleton × (α ⊕ β)) => x.2) (t.toPaths' bl)

theorem toPath_elems {α : Type} (t : BTree α) : List.map (fun (x : Skeleton × α) => x.2) t.toPaths_elems = t.toList

theorem toPaths_elems_skeletons {α : Type} (t : BTree α) (a : α) (aIn : a ∈ List.map (fun (x : Skeleton × α) => x.2) t.toPaths_elems) : ∃ (sk : Skeleton), (sk, a) ∈ t.toPaths_elems

theorem proj_comp {α β γ : Type} (f : α → γ) : ((fun (x : γ × β) => x.1) ∘ fun (x : α × β) => match x with | (a, b) => (f a, b)) = fun (x : α × β) => f x.1

theorem List.Disjoint.list_cons {α : Type} (x y : α) (neq : ¬x = y) (ls rs : List (List α)) : (List.map (cons x) ls).Disjoint (List.map (cons y) rs)

theorem diff_head_nodup {α : Type} (l_1 l_2 : List (List α)) (e_1 e_2 : α) (HL : l_1.Nodup) (HR : l_2.Nodup) (hneq : ¬e_1 = e_2) : (List.map (List.cons e_1) l_1 ++ List.map (List.cons e_2) l_2).Nodup

theorem path_different {α β : Type} (t : ABTree α β) : (List.map (fun (x : Skeleton × (α ⊕ β)) => x.1) t.toPaths).Nodup

def find_first_split_acc {α : Type} (pred : α → Bool) (elems acc : List α) : Option (List α × α × List α)

Equations

• find_first_split_acc pred [] acc = none
• find_first_split_acc pred (e :: els) acc = if pred e = true then some (acc, e, els) else find_first_split_acc pred els (acc.concat e)

def find_first_split {α : Type} (P : α → Bool) (elems : List α) : Option (List α × α × List α)

Equations

• find_first_split P elems = find_first_split_acc P elems []

theorem find_first_split_none_wk {α : Type} (P : α → Bool) (els accl accr : List α) : find_first_split_acc P els (accl.append accr) = none → find_first_split_acc P els accr = none

theorem find_first_split_none_forget {α : Type} (P : α → Bool) (els acc : List α) : find_first_split_acc P els [] = none → find_first_split_acc P els acc = none

theorem find_first_split_none {α : Type} (P : α → Bool) (els acc : List α) (HAcc : ∀ e ∈ acc, ¬P e = true) : find_first_split_acc P els acc = none → ∀ e ∈ els ++ acc, ¬P e = true

theorem find_first_split_none' {α : Type} (P : α → Bool) (els acc : List α) : (∀ e ∈ els, ¬P e = true) → find_first_split_acc P els acc = none

theorem find_first_split_acc_law {α : Type} (P : α → Bool) (elems acc pred sect : List α) (e : α) : find_first_split_acc P elems acc = some (pred, e, sect) → (∀ e' ∈ acc, ¬P e' = true) → acc ++ elems = pred ++ [e] ++ sect ∧ P e = true ∧ ∀ e' ∈ pred, ¬P e' = true

def find_two_pred {α : Type} (P : α → Bool) (elems : List α) : Option (List α × α × List α × α × List α)

Equations

• One or more equations did not get rendered due to their size.

def find_dups_acc {β α : Type} [DecidableEq α] (f : β → α) (elems acc : List β) : Option (List β × β × List β × β × List β)

Equations

• One or more equations did not get rendered due to their size.
• find_dups_acc f [] acc = none

def find_dups {α β : Type} [DecidableEq α] (f : β → α) (elems : List β) : Option (List β × β × List β × β × List β)

Equations

• find_dups f elems = find_dups_acc f elems []

theorem finds_dups_law_elems_acc {α β : Type} [DecidableEq α] (f : β → α) (elems acc pred mid succs : List β) (e_1 e_2 : β) (H : find_dups_acc f elems acc = some (pred, e_1, mid, e_2, succs)) : acc ++ elems = pred ++ [e_1] ++ mid ++ [e_2] ++ succs ∧ f e_1 = f e_2

theorem finds_dups_law_elems {α β : Type} [DecidableEq α] (f : β → α) (elems pred mid succs : List β) (e_1 e_2 : β) (H : find_dups f elems = some (pred, e_1, mid, e_2, succs)) : elems = pred ++ [e_1] ++ mid ++ [e_2] ++ succs ∧ f e_1 = f e_2

theorem filtermap_nodup {α : Type} {t : BTree α} (H : (List.map (fun (x : Skeleton × (α ⊕ Unit)) => x.1) (ABTree.toPaths t)).Nodup) : (List.filterMap (fun (x : Skeleton × (α ⊕ Unit)) => match x.2 with | Sum.inl v => some (x.1, v) | Sum.inr _val => none) (ABTree.toPaths t)).Nodup

theorem finds_dups_law_elem_sk {α : Type} [DecidableEq α] (t : BTree α) {pred mid succs : List (Skeleton × α)} (e_1 e_2 : Skeleton × α) (H : find_dups (fun (x : Skeleton × α) => x.2) t.toPaths_elems = some (pred, e_1, mid, e_2, succs)) : ABTree.access t e_1.1 = some (Sum.inl e_1.2) ∧ ABTree.access t e_2.1 = some (Sum.inl e_2.2) ∧ ¬e_1.1 = e_2.1 ∧ e_1.2 = e_2.2

theorem finds_dup_wk' {α β : Type} [DecidableEq α] {f : β → α} (els accl accr : List β) : find_dups_acc f els accr = none → find_dups_acc f els (accl ++ accr) = none

theorem finds_dup_wk {α β : Type} [DecidableEq α] {f : β → α} (els accl accr : List β) : find_dups_acc f els (accl ++ accr) = none → find_dups_acc f els accr = none

theorem finds_no_dup {α β : Type} [DecidableEq β] (f : α → β) (elems : List α) (no_dups_found : find_dups f elems = none) : (List.map f elems).Nodup

theorem finds_no_dup_head_forall {α β : Type} [DecidableEq β] (f : α → β) (a : α) (elems : List α) (no_dups_found : find_dups f (a :: elems) = none) (e : α) : e ∈ elems → ¬f a = f e

theorem no_dups_no_first_head {α β : Type} [DecidableEq β] (f : α → β) (a : α) (els : List α) (h_nodups : find_dups f (a :: els) = none) : find_first_split (fun (y : α) => f a == f y) els = none

theorem no_find_dups_head {α β : Type} [DecidableEq β] (f : α → β) (a : α) (elems : List α) (h_nodups : find_dups f elems = none) (h_no_elems : ∀ e ∈ elems, ¬f a = f e) : find_dups f (a :: elems) = none

theorem no_dups_finds_none {α β : Type} [DecidableEq β] (f : α → β) (elems : List α) (h_nodups : (List.map f elems).Nodup) : find_dups f elems = none

theorem finds_no_dup_inj {α β : Type} [DecidableEq β] (f : α → β) (elems : List α) (H_nodups : find_dups f elems = none) : elems.Nodup

def find_first_split_proj {β α : Type} [DecidableEq α] (proj : β → α) (b : β) (ll : List β) : Option (List β × β × List β)

Equations

• find_first_split_proj proj b ll = find_first_split (fun (x : β) => proj x == proj b) ll

theorem split_at_value {β α : Type} [DecidableEq α] {proj : β → α} {b b' : β} {pred ll pos : List β} : find_first_split_proj proj b ll = some (pred, b', pos) → ll = pred ++ [b'] ++ pos ∧ proj b ∉ List.map proj pred ∧ proj b' = proj b

theorem split_at_none {β α : Type} [DecidableEq α] {proj : β → α} {b : β} {ls : List β} : find_first_split_proj proj b ls = none → proj b ∉ List.map proj ls

def find_intersect' {β α : Type} [DecidableEq α] (proj : β → α) (ll rr acc : List β) : Option ((List β × β × List β) × List β × β × List β)

Equations

• find_intersect' proj [] rr acc = none
• find_intersect' proj (e :: els) rr acc = match find_first_split_proj proj e rr with | none => find_intersect' proj els rr (acc.concat e) | some inter_rr => some ((acc, e, els), inter_rr)

def split_at_first_pred' {α β : Type} (pred : α → Option β) (l acc : List α) : Option ((List α × α × List α) × β)

Equations

• split_at_first_pred' pred [] acc = none
• split_at_first_pred' pred (e :: els) acc = match pred e with | none => split_at_first_pred' pred els (acc.concat e) | some b => some ((acc, e, els), b)

theorem split_at_first_pred'_none {α β : Type} {pred : α → Option β} {l acc : List α} (H : split_at_first_pred' pred l acc = none) (a : α) : a ∈ l → pred a = none

theorem none_split_at_first_pred' {α β : Type} {pred : α → Option β} {l acc : List α} (H : ∀ a ∈ l, pred a = none) : split_at_first_pred' pred l acc = none

theorem split_eq_value {α β : Type} {pred : α → Option β} {a : α} {b : β} {l acc ls rs : List α} (HSome : split_at_first_pred' pred l acc = some ((ls, a, rs), b)) : pred a = some b

theorem split_at_first_pred'_some {α β : Type} {pred : α → Option β} {a : α} {b : β} {l acc ls rs : List α} (H : split_at_first_pred' pred l acc = some ((ls, a, rs), b)) : acc ++ l = ls ++ a :: rs

def split_at_first_pred {α β : Type} (pred : α → Option β) (l : List α) : Option ((List α × α × List α) × β)

Equations

• split_at_first_pred pred l = split_at_first_pred' pred l []

theorem splitAtFirstNone {α β : Type} {pred : α → Option β} {ls : List α} (H : split_at_first_pred pred ls = none) (a : α) : a ∈ ls → pred a = none

theorem splitAtFirstNone' {α β : Type} {pred : α → Option β} {ls : List α} (H : ∀ a ∈ ls, pred a = none) : split_at_first_pred pred ls = none

def find_intersect {β α : Type} [DecidableEq α] (proj : β → α) (ll rr : List β) : Option ((List β × β × List β) × List β × β × List β)

Equations

• find_intersect proj ll rr = split_at_first_pred (fun (x : β) => find_first_split_proj proj x rr) ll

theorem find_intersect_law {β α : Type} [DecidableEq α] {proj : β → α} (ls prels posls rs prers posrs : List β) (el er : β) (H : find_intersect proj ls rs = some ((prels, el, posls), prers, er, posrs)) : ls = prels ++ [el] ++ posls ∧ rs = prers ++ [er] ++ posrs ∧ proj el = proj er

theorem find_intersect_none {β α : Type} [DecidableEq α] {proj : β → α} {ls rs : List β} (H : find_intersect proj ls rs = none) (l : β) : l ∈ ls → ∀ r ∈ rs, ¬proj l = proj r

theorem find_intersect_none' {β α : Type} [DecidableEq α] {proj : β → α} {ls rs : List β} (H : ∀ l ∈ ls, ∀ r ∈ rs, ¬proj l = proj r) : find_intersect proj ls rs = none