The LaTeX lexer lemma
Every list of LaTeX tokens (tokOK
) reads back from its rendering: lex (render ts) = some ts. The proof goes token by token: each token reads back from its spelling
whatever follows it, as long as what follows does not extend it (Sep
), and the
renderer writes a space exactly where a following token would extend the previous
one.
Characters
Balanced raw text
JSON strings
Numbers
def spOK : List Char → Bool
A spelling skipSp
stops at: its first character is not white space and not \,
or it is \ followed by something other than a spacing command.
def clash : List Char → List Char → Bool
Two spellings differ within the first one’s length.
theorem sciExp_pre (P Y : List Char) (h1 : spOK P = true) (h2 : clash "\\times".toList P = true) :
sciExp (P ++ Y) = none
No scientific tail after a spelling that skipSp
stops at and that is not \times.
theorem sciExp_none {Z : List Char} (h : dropP "\\times".toList (skipSp Z) = none) : sciExp Z = none
No scientific tail where \times does not come first.
theorem sciExp_tail (e : Int) (X : List Char) :
sciExp (timesTen ++ (Number.printInt e ++ '}' :: X)) = some (e, X)
The printed scientific tail reads back as its exponent.
def NumSep (X : List Char) : Prop
What may follow a number: nothing that extends it, and not a scientific tail.
theorem lexSigned_num (n : JNum) (hn : n.WF) (X : List Char)
(h : lexNum sciExp (numChars n ++ X) = some (.num n, X)) :
lexSigned sciExp (numChars n ++ X) = some (.num n, X)
A number token reads back with its sign: a printed - starts a negative number.
Character classes
theorem letter_facts {c : Char} (h : isLetter c = true) :
isDig c = false ∧ c ≠ '\\' ∧ c ≠ '"' ∧ c ≠ '-' ∧ c ≠ ' ' ∧ c ≠ '\n' ∧ c ≠ '\t' ∧ c ≠ '\r' ∧
c ≠ ';' ∧ c ≠ ':' ∧ c ≠ '!'
A letter is none of the characters the lexer dispatches on.
Greek names
Tokens
def kwOK : Kw → Bool
LaTeX keywords: the ones with a LaTeX spelling, except \times, which the printer
never writes (it would run into the \times 10^{…} of a scientific number).
def Sep (t : Tok) (X : List Char) : Prop
What may follow the spelling of t: nothing that extends it.
Spaces
One token
Token lists
theorem lex_render (ts : List Tok) (h : ∀ t ∈ ts, tokOK t) : lex (render ts) = some ts
The LaTeX lexer lemma: a list of LaTeX tokens reads back from its rendering.