The token-level round trip: generic pieces
PL c e: the printed tokens of e for any level read back to e at that level,
before anything that does not continue it, with enough fuel (need
). The main
theorem (Esm.Document.Math.Main
) proves it for every well-formed expression by
strong induction; this file holds the steps that do not depend on the notation.
def startA (t : Tok) : Bool
A token a printed expression can start with: one that starts an operand, but not a call parenthesis or a bracket (those only follow something).
def HeadOK (c : Ctx) : List Tok → Prop
What a printed expression starts with, as far as the variant readings care.
theorem lift_step {c : Ctx} {L f : Nat} {ts r : List Tok} {x : Json} (hL : 1 ≤ L) (hL' : L < 10)
(h : pLvl c f (L + 1) ts = some (x, r)) (hr : Fol c.sf L r) :
pLvl c (f + 1) L ts = some (x, r)
One level looser.
theorem lift {c : Ctx} {ts r : List Tok} {x : Json} {N : Nat} :
∀ (d L : Nat), 1 ≤ L → L + d ≤ 10 → (∀ f, N ≤ f → pLvl c f (L + d) ts = some (x, r)) →
Fol c.sf L r → ∀ f, N + d ≤ f → pLvl c f L ts = some (x, r)
Several levels looser.
theorem pPrim_grp (c : Ctx) (e : Json) (toks : List Tok) (hh : HeadOK c toks)
(h1 : ∀ rest, Fol c.sf 1 rest → ∀ f, need 1 toks.length ≤ f → pOr c f (toks ++ rest) = some (e, rest))
(rest : List Tok) (f : Nat) (hf : need 1 toks.length + 1 ≤ f) :
pPrim c f (grp c.sf toks ++ rest) = some (e, rest)
A primary read in parentheses.