Internal Theorems #
Theorems with access to the internal representation of tokens.
Ideally, theorems outside this file should not use them.
We can guarantee that are not used by usign the private command, but I will
leave this as a TODO for now.
theorem
Tokens.Internal.get_succ_hd
{α : Type}
{n : Elem.TId}
{hd : Option (Elem.TokenD α)}
{tl : State.Tokens α}
:
theorem
Tokens.Internal.get_ext_concat
{α : Type}
{n : Elem.TId}
{v : Elem.TokenD α}
{s : State.Tokens α}
(H : State.Tokens.get n s = some v)
(ext : State.Tokens α)
:
theorem
Tokens.Internal.get_length
{α : Type}
{n : Elem.TId}
{s : State.Tokens α}
{t : Elem.TokenD α}
(HG : State.Tokens.get n s = some t)
:
theorem
Tokens.Internal.get_none
{α : Type}
{n : Elem.TId}
{s : State.Tokens α}
(gt : List.length s ≤ n)
:
theorem
Tokens.Internal.get_at
{α : Type}
{tid : Elem.TId}
{pre pos : State.Tokens α}
{v : Option (Elem.TokenD α)}
(pre_cond : tid = List.length pre)
:
theorem
Tokens.Internal.get_concat_left
{α : Type}
{tid : Elem.TId}
{l r : State.Tokens α}
(pre : tid < List.length l)
:
theorem
Tokens.Internal.get_concat_right
{α : Type}
{tid : Elem.TId}
{l r : State.Tokens α}
(pre : List.length l ≤ tid)
:
theorem
Tokens.Internal.get_concat_cons_right
{α : Type}
{tid : Elem.TId}
{l r : State.Tokens α}
{v : Option (Elem.TokenD α)}
(pre : List.length l < tid)
:
theorem
Tokens.Internal.get_split_pos
{α : Type}
{tid : Elem.TId}
{pre pos : State.Tokens α}
{v : Option (Elem.TokenD α)}
(pos_cond : List.length pre ≤ tid)
:
theorem
Tokens.Internal.same_len_update_data
{α : Type}
{t : Elem.TId}
{f : α → α}
{s s' : State.Tokens α}
(H : State.Tokens.update_data t f s = some s')
:
theorem
Tokens.Internal.update_data_list
{α : Type}
{t : Elem.TId}
{s s' : State.Tokens α}
{f : α → α}
(H : some s' = State.Tokens.update_data t f s)
:
theorem
Tokens.Internal.update_data_list'
{α : Type}
{t : Elem.TId}
{s s' : State.Tokens α}
{f : α → α}
(H : State.Tokens.update_data t f s = some s')
:
theorem
Tokens.Internal.get_last_id
{α : Type}
{s : State.Tokens α}
{last : Option (Elem.TokenD α)}
:
theorem
Tokens.Internal.get_last_id'
{α : Type}
{s : State.Tokens α}
{last : Option (Elem.TokenD α)}
:
theorem
Tokens.Properties.get_empty
{α : Type}
{tid : Elem.TId}
{s : State.Tokens α}
(se : s = [])
:
theorem
Tokens.Properties.get_elem_mem
{α : Type}
{tid : Elem.TId}
{s : State.Tokens α}
{tkn : Elem.TokenD α}
(get : State.Tokens.get tid s = some tkn)
:
theorem
Tokens.Properties.mem_elem_list_get
{α : Type}
{s : State.Tokens α}
{tkn : Option (Elem.TokenD α)}
(n : Fin (List.length s))
(get : List.get s n = tkn)
:
theorem
Tokens.Properties.mem_elem_list_get'
{α : Type}
{s : State.Tokens α}
{tkn : Option (Elem.TokenD α)}
(min : List.Mem tkn s)
:
theorem
Tokens.Properties.mem_elem_get
{α : Type}
{s : State.Tokens α}
{tkn : Elem.TokenD α}
(HB : ∀ (t : Elem.TId) (nt : Elem.TokenD α), State.Tokens.get t s = some nt → nt.id = t)
(mem : List.Mem (some tkn) s)
:
theorem
Tokens.Properties.mem_get
{α : Type}
{tid : Elem.TId}
{s : State.Tokens α}
(Hmem : tid ∈ s)
:
theorem
Tokens.Properties.update_none
{α : Type}
{tid : Elem.TId}
{f : Elem.TokenD α → Option (Elem.TokenD α)}
{s : State.Tokens α}
(HG : State.Tokens.get tid s = none)
:
theorem
Tokens.Properties.get_update
{α : Type}
{tid : Elem.TId}
{v : Elem.TokenD α}
{s : State.Tokens α}
(f : Elem.TokenD α → Option (Elem.TokenD α))
(Hget : State.Tokens.get tid s = some v)
:
theorem
Tokens.Properties.get_update_neq
{α : Type}
{i j : Elem.TId}
{f : Elem.TokenD α → Option (Elem.TokenD α)}
{s s' : State.Tokens α}
(neq : ¬i = j)
(HS : State.Tokens.update j f s = some s')
:
theorem
Tokens.Properties.get_update_eq
{α : Type}
{i : Elem.TId}
{f : Elem.TokenD α → Elem.TokenD α}
{s s' : State.Tokens α}
(HS : State.Tokens.update i (some ∘ f) s = some s')
:
theorem
Tokens.Properties.no_get_no_update_data
{α : Type}
{s : State.Tokens α}
{t : Elem.TId}
(f : α → α)
(H : State.Tokens.get t s = none)
:
theorem
Tokens.Properties.update_data_some
{α : Type}
{t : Elem.TId}
{s s' : State.Tokens α}
{f : α → α}
(H : State.Tokens.update_data t f s = some s')
:
theorem
Tokens.Properties.get_update_data
{α : Type}
{tid : Elem.TId}
{v : Elem.TokenD α}
{s : State.Tokens α}
(f : α → α)
(Hget : State.Tokens.get tid s = some v)
:
theorem
Tokens.Properties.get_update_data_res
{α : Type}
{tid : Elem.TId}
{v : Elem.TokenD α}
{s : State.Tokens α}
(f : α → α)
(Hget : State.Tokens.get tid s = some v)
:
theorem
Tokens.Properties.update_data_res
{α : Type}
{s s' : State.Tokens α}
{tid : Elem.TId}
{f : α → α}
(HB : ∀ (t : Elem.TId) (nt : Elem.TokenD α), State.Tokens.get t s = some nt → nt.id = t)
(H : State.Tokens.update_data tid f s = some s')
(t : Elem.TId)
(nt : Elem.TokenD α)
:
State.Tokens.get t s' = some nt → nt.id = t
theorem
Tokens.Properties.get_update_data_eq
{α : Type}
{i : Elem.TId}
{v : Elem.TokenD α}
{f : α → α}
{s s' : State.Tokens α}
(Ha : State.Tokens.get i s = some v)
(H : State.Tokens.update_data i f s = some s')
:
theorem
Tokens.Properties.get_update_data_eq'
{α : Type}
{i : Elem.TId}
{v : Elem.TokenD α}
{f : α → α}
{s s' : State.Tokens α}
(Ha : State.Tokens.get i s' = some v)
(H : State.Tokens.update_data i f s = some s')
:
theorem
Tokens.Properties.get_update_data_neq
{α : Type}
{i j : Elem.TId}
{f : α → α}
{s s' : State.Tokens α}
(neq : ¬i = j)
(H : State.Tokens.update_data j f s = some s')
:
theorem
Tokens.Properties.update_data_get_eq
{α : Type}
{i : Elem.TId}
{f : α → α}
{s s' : State.Tokens α}
{v : Elem.TokenD α}
(Hget : State.Tokens.get i s' = some v)
(Hupd : State.Tokens.update_data i f s = some s')
:
theorem
Tokens.Properties.get_mint
{α : Type}
{n : Elem.TId}
{v : Elem.TokenD α}
{s : State.Tokens α}
(H : State.Tokens.get n s = some v)
(nm : String)
(d : α)
:
theorem
Tokens.Properties.get_mint'
{α : Type}
{n : Elem.TId}
{v : Elem.TokenD α}
{s : State.Tokens α}
(H : State.Tokens.get n s = some v)
(nm : String)
(d : α)
:
theorem
Tokens.Properties.get_mint_neq
{α : Type}
{n : Elem.TId}
{s : State.Tokens α}
{nm : String}
{d : α}
(nlt : n < List.length s)
:
theorem
Tokens.Properties.get_mint_neq_last
{α : Type}
{n : Elem.TId}
{s : State.Tokens α}
{nm : String}
{d : α}
(nlt : ¬n = (State.Tokens.mint nm d s).last_id)
:
theorem
Tokens.Properties.last_id_update_same
{α : Type}
{f : α → α}
{tid : Elem.TId}
{s s' : State.Tokens α}
(upd : State.Tokens.update_data tid f s = some s')
:
theorem
Tokens.Properties.get_last_id_mint
{α : Type}
{s : State.Tokens α}
{nm : String}
{d : α}
:
State.Tokens.get (State.Tokens.mint nm d s).last_id (State.Tokens.mint nm d s) = some { name := (), data := d, id := (State.Tokens.mint nm d s).last_id }
theorem
Tokens.Properties.get_pre_mint
{α : Type}
{s : State.Tokens α}
{tid : Elem.TId}
{tkn : Elem.TokenD α}
{nm : String}
{d : α}
(get : State.Tokens.get tid s = some tkn)
:
theorem
Tokens.Properties.get_mint_neq'
{α : Type}
{n : Elem.TId}
{s : State.Tokens α}
{nm : String}
{d : α}
(Hnz : 0 < List.length s)
(nlt : ¬n = Nat.succ s.last_id)
:
theorem
Tokens.Properties.burn_after_get
{α : Type}
{tid : Elem.TId}
{tkn : Elem.TokenD α}
{s : State.Tokens α}
(hget : State.Tokens.get tid s = some tkn)
:
theorem
Tokens.Properties.burn_prop_after_no_get
{α : Type}
{rem : Elem.TId}
{s burnt : State.Tokens α}
(hb : State.Tokens.burn rem s = some burnt)
:
State.Tokens.get rem burnt = none ∧ ∀ (i : Elem.TId), ¬i = rem → State.Tokens.get i s = State.Tokens.get i burnt
theorem
Tokens.Properties.get_after_burn_none
{α : Type}
{rem : Elem.TId}
{s burnt : State.Tokens α}
(hb : State.Tokens.burn rem s = some burnt)
:
theorem
Tokens.Properties.burn_prop_after_same_get
{α : Type}
{rem : Elem.TId}
{s burnt : State.Tokens α}
(hb : State.Tokens.burn rem s = some burnt)
(i : Elem.TId)
:
¬i = rem → State.Tokens.get i s = State.Tokens.get i burnt
theorem
Tokens.Properties.burn_dec_size
{α : Type}
{t : Elem.TId}
{s s' : State.Tokens α}
(Hs : State.Tokens.burn t s = some s')
:
After burning, size decreases
theorem
Tokens.Mathlib.get_zipIdx_eq
{α : Type}
{ls : State.Tokens α}
{a : Option (Elem.TokenD α)}
{t : Elem.TId}
:
theorem
Tokens.Mathlib.get_zipIdx_eq_some
{α : Type}
{ls : State.Tokens α}
{a : Elem.TokenD α}
{t : Elem.TId}
: