@[reducible, inline]

abbrev MUList.State.Key : Type

Key are nats.

Equations

• MUList.State.Key = Nat

Nodes contain some data and optionally a key and link. The link field states whats the next key in the list. Given two nodes, we can easily check if one follows from the other.

structure MUList.State.Elemt (ε α : Type) : Type

• key : Option ε
• link : Option ε
• data : α

instance MUList.State.instReprElemt {ε✝ α✝ : Type} [Repr ε✝] [Repr α✝] : Repr (Elemt ε✝ α✝)

Equations

• MUList.State.instReprElemt = { reprPrec := MUList.State.instReprElemt.repr }

def MUList.State.instReprElemt.repr {ε✝ α✝ : Type} [Repr ε✝] [Repr α✝] : Elemt ε✝ α✝ → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev MUList.State.ListToken (α : Type) : Type

Elements in a linked list are tokens containing Elemt.

Equations

• MUList.State.ListToken α = Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α)

def MUList.State.serialize_key (e : Option Key) : String

Key serialization operation.

Equations

• MUList.State.serialize_key none = "Node"
• MUList.State.serialize_key (some k) = "Node" ++ toString k

@[reducible, inline]

abbrev MUList.State.ListST (α : Type) : Type

Linked lists are defined as a tokenized linked list structure.

Equations

• MUList.State.ListST α = Tokens.State.Tokens (MUList.State.Elemt MUList.State.Key α)

def MUList.State.all_keys {α : Type} (s : ListST α) : List Key

Equations

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

def MUList.State.ListST.get_key {α : Type} (tkn : Tokens.Elem.TId) (s : ListST α) : Option Key

Equations

• MUList.State.ListST.get_key tkn s = match Tokens.State.Tokens.get tkn s with | none => none | some nd => nd.data.key

def MUList.State.ListST.get_link {α : Type} (tkn : Tokens.Elem.TId) (s : ListST α) : Option Key

Equations

• MUList.State.ListST.get_link tkn s = match Tokens.State.Tokens.get tkn s with | none => none | some nd => nd.data.link

theorem MUList.State.get_key_find {α : Type} {s : ListST α} {k : Key} {tid : Tokens.Elem.TId} : (∃ (tkn : Tokens.Elem.TokenD (Elemt Key α)), Tokens.State.Tokens.get tid s = some tkn ∧ (tkn.data.key == some k) = true) ↔ ListST.get_key tid s = some k

theorem MUList.State.get_get_key {α : Type} {s : ListST α} {tid : Tokens.Elem.TId} : Tokens.State.Tokens.get_proj tid (fun (x : Elemt Key α) => x.key) s >>= id = ListST.get_key tid s

theorem MUList.State.get_get_key_some {α : Type} {s : ListST α} {tid : Tokens.Elem.TId} {k : Key} (h : ListST.get_key tid s = some k) : Tokens.State.Tokens.get_proj tid (fun (x : Elemt Key α) => x.key) s = some (some k)

theorem MUList.State.get_get_key_some' {α : Type} {s : ListST α} {tid : Tokens.Elem.TId} {k : Key} (h : Tokens.State.Tokens.get_proj tid (fun (x : Elemt Key α) => x.key) s = some (some k)) : ListST.get_key tid s = some k

def MUList.State.ListST.get_data {α β : Type} (tid : Tokens.Elem.TId) (f : α → β) (s : ListST α) : Option β

Equations

• MUList.State.ListST.get_data tid f s = (f ∘ fun (x : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α)) => x.data.data) <$> Tokens.State.Tokens.get tid s

def MUList.State.ListST.init {α : Type} (root_d : α) : ListST α × Tokens.Elem.TId

Equations

• MUList.State.ListST.init root_d = Tokens.State.Tokens.mint' (MUList.State.serialize_key none) { key := none, link := none, data := root_d } Tokens.State.Tokens.init

theorem MUList.State.get_init {α : Type} {iv : α} {tid : Tokens.Elem.TId} {tkn : Tokens.Elem.TokenD (Elemt Key α)} (get : Tokens.State.Tokens.get tid (ListST.init iv).fst = some tkn) : tid = (ListST.init iv).snd ∧ tkn.data = { key := none, link := none, data := iv }

def MUList.State.ListST.gen_root_init {α β : Type} (root_data : α) : ListST (α ⊕ β) × Tokens.Elem.TId

Equations

• MUList.State.ListST.gen_root_init root_data = Tokens.State.Tokens.mint' (MUList.State.serialize_key none) { key := none, link := none, data := Sum.inl root_data } Tokens.State.Tokens.init

def MUList.State.ListST.upd_link {α : Type} (tkn : Tokens.Elem.TId) (nl : Option Key) (s : ListST α) : Option (ListST α)

Equations

• MUList.State.ListST.upd_link tkn nl s = Tokens.State.Tokens.update_data tkn (fun (t : MUList.State.Elemt MUList.State.Key α) => { key := t.key, link := nl, data := t.data }) s

theorem MUList.State.upd_link_find {α : Type} {tkn : Tokens.Elem.TId} {s : ListST α} {t : Tokens.Elem.TokenD (Elemt Key α)} (HF : Tokens.State.Tokens.get tkn s = some t) (mk : Option Key) : ∃ (s' : ListST α), ListST.upd_link tkn mk s = some s'

theorem MUList.State.find_upd_link_find_others {α : Type} {tkn otkn : Tokens.Elem.TId} {mk : Option Key} {s s' : ListST α} {t : Tokens.Elem.TokenD (Elemt Key α)} (neq : ¬tkn = otkn) (HF : Tokens.State.Tokens.get otkn s = some t) (Upd : ListST.upd_link tkn mk s = some s') : Tokens.State.Tokens.get otkn s' = some t

theorem MUList.State.find_upd_link_find {α : Type} {tkn : Tokens.Elem.TId} {mk : Option Key} {s s' : ListST α} {t : Tokens.Elem.TokenD (Elemt Key α)} (HF : Tokens.State.Tokens.get tkn s = some t) (Upd : ListST.upd_link tkn mk s = some s') : Tokens.State.Tokens.get tkn s' = some { name := t.name, data := have __src := t.data; { key := __src.key, link := mk, data := __src.data }, id := t.id }

theorem MUList.State.burn_find_some {α : Type} {s : ListST α} {tid : Tokens.Elem.TId} (HF : (Tokens.State.Tokens.get tid s).isSome = true) : ∃ (s' : Tokens.State.Tokens (Elemt Key α)), Tokens.State.Tokens.burn tid s = some s'

theorem MUList.State.get_key_mem_key_all_keys {α : Type} {s : ListST α} {tid : Tokens.Elem.TId} {key : Key} (HM : Tokens.State.Tokens.get_proj tid (fun (x : Elemt Key α) => x.key) s = some (some key)) : key ∈ all_keys s

def MUList.State.midgard_is_root_node {α : Type} (nd : ListToken α) : Bool

Equations

• MUList.State.midgard_is_root_node nd = nd.data.key.isNone

def MUList.State.ListST.is_root_node {α : Type} (nid : Tokens.Elem.TId) (s : ListST α) : Bool

Equations

• MUList.State.ListST.is_root_node nid s = match Tokens.State.Tokens.get nid s with | none => false | some b => MUList.State.midgard_is_root_node b

theorem MUList.State.root_find_and_root {α : Type} {id : Tokens.Elem.TId} {s : ListST α} (H : ListST.is_root_node id s = true) : ∃ (nd : Tokens.Elem.TokenD (Elemt Key α)), Tokens.State.Tokens.get id s = some nd ∧ midgard_is_root_node nd = true

def MUList.State.midgard_is_last_node {α : Type} (nd : ListToken α) : Bool

Equations

• MUList.State.midgard_is_last_node nd = nd.data.link.isNone

def MUList.State.ListST.is_last_node {α : Type} (nid : Tokens.Elem.TId) (s : ListST α) : Bool

Equations

• MUList.State.ListST.is_last_node nid s = match Tokens.State.Tokens.get nid s with | none => false | some b => MUList.State.midgard_is_last_node b

theorem MUList.State.last_find_and_last {α : Type} {id : Tokens.Elem.TId} {s : ListST α} (H : ListST.is_last_node id s = true) : ∃ (nd : Tokens.Elem.TokenD (Elemt Key α)), Tokens.State.Tokens.get id s = some nd ∧ midgard_is_last_node nd = true

def MUList.State.midgard_is_empty {α : Type} (nd : ListToken α) : Bool

Equations

• MUList.State.midgard_is_empty nd = (MUList.State.midgard_is_root_node nd && MUList.State.midgard_is_last_node nd)

def MUList.State.ListST.is_empty {α : Type} (nid : Tokens.Elem.TId) (s : ListST α) : Bool

Equations

• MUList.State.ListST.is_empty nid s = match Tokens.State.Tokens.get nid s with | none => false | some b => MUList.State.midgard_is_empty b

def MUList.State.midgard_is_member {α : Type} (key : Key) (nd : ListToken α) : Bool

Equations

• MUList.State.midgard_is_member key nd = (some key == nd.data.key)

def MUList.State.ListST.is_member {α : Type} (key : Key) (nd : Tokens.Elem.TId) (s : ListST α) : Bool

Equations

• MUList.State.ListST.is_member key nd s = match Tokens.State.Tokens.get nd s with | none => false | some nd => MUList.State.midgard_is_member key nd

theorem MUList.State.is_member_find {α : Type} {k : Key} {nd : Tokens.Elem.TId} {s : ListST α} (H : ListST.is_member k nd s = true) : (Tokens.State.Tokens.get nd s).isSome = true

theorem MUList.State.is_member_get_key {α : Type} {s : ListST α} {k : Key} {t : Tokens.Elem.TId} : ListST.is_member k t s = true ↔ ListST.get_key t s = some k

theorem MUList.State.is_member_and_key {α : Type} {s : ListST α} {k : Key} {t : Tokens.Elem.TId} {tkn : Tokens.Elem.TokenD (Elemt Key α)} (hm : ListST.is_member k t s = true) (htkn : Tokens.State.Tokens.get t s = some tkn) : tkn.data.key = some k

theorem MUList.State.is_member_exists_tkn {α : Type} {s : ListST α} {k : Key} {t : Tokens.Elem.TId} (hm : ListST.is_member k t s = true) : ∃ (tkn : Tokens.Elem.TokenD (Elemt Key α)), Tokens.State.Tokens.get t s = some tkn ∧ tkn.data.key = some k

def MUList.State.ListST.is_anchor {α : Type} (key : Key) (anchor : Tokens.Elem.TId) (s : ListST α) : Bool

Equations

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

theorem MUList.State.is_anchor_get_link {α : Type} {key : Key} {tid : Tokens.Elem.TId} {s : ListST α} : ListST.is_anchor key tid s = true ↔ ListST.get_link tid s = some key

def MUList.State.ListST.is_anchor_tokens {α : Type} (tkn anch : Tokens.Elem.TId) (s : ListST α) : Bool

Equations

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

theorem MUList.State.is_anchor_tokens_get_key_and_token {α : Type} {tkn anch : Tokens.Elem.TId} {s : ListST α} (st : ListST.is_anchor_tokens tkn anch s = true) : ∃ (key : Key), ListST.get_key tkn s = some key ∧ ListST.is_anchor key anch s = true

inductive MUList.State.Actions (α : Type) : Type

• ModifyData {α : Type} : Tokens.Elem.TId → α → Actions α
• UnsafeAppend {α : Type} (key : Key) (data : α) (last : Tokens.Elem.TId) : Actions α
• UnsafePrepend {α : Type} (key : Key) (data : α) (root : Tokens.Elem.TId) : Actions α
• Remove {α : Type} (removed_node anchor_node : Tokens.Elem.TId) : Actions α

instance MUList.State.instReprActions {α✝ : Type} [Repr α✝] : Repr (Actions α✝)

Equations

• MUList.State.instReprActions = { reprPrec := MUList.State.instReprActions.repr }

def MUList.State.instReprActions.repr {α✝ : Type} [Repr α✝] : Actions α✝ → Nat → Std.Format

Equations

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

def MUList.State.Actions.isRemove {α : Type} : Actions α → Prop

Equations

• (MUList.State.Actions.Remove removed_node anchor_node).isRemove = True
• x✝.isRemove = False

def MUList.State.ListST.singleton {α : Type} (iv : α) (key : Key) (d : α) : ListST α × Tokens.Elem.TId × Tokens.Elem.TId

Equations

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