Multi-line equations (accepted input variants)

Lean module Esm.Document.Source.MultiLine, formal/Esm/Document/Source/MultiLine.lean at 184aa13d35e5
Imports Esm.Document.Source.Equation, Esm.Document.Math.Induct

The printer writes one equation per display. On input, one display may hold several equations, or one equation over several lines (Notation.variants):

rows separated by a top-level line break (LaTeX \\ inside aligned, Typst \);
in a row, the first top-level & splits a left cell from the rest; a row with something before its & starts a new equation, a row with an empty left cell continues the previous one (&\quad + k_{2} B), and a continuation starting with its own = is refused (an equation has one top-level =);
in split and multline, all rows are one equation;
line breaks and & nested inside a delimiter (cases, a matrix, parentheses) never split anything.

The reader works on the math tokens (Esm.Document.Math.Tok), after the lexer, so the rows and cells are found by token and depth, not by text. cookRows_layout is the normalization lemma: an equation laid out over aligned rows, the pieces of its canonical tokens separated by & and line breaks, reads back as the equation itself.

Depth and top-level cuts

def delta source

def delta : Tok → Int

How a token changes the delimiter depth.

def isKw source

def isKw (k : Kw) : Tok → Bool

The token is the keyword k.

def cut source

def cut (k : Kw) : Int → List Tok → List Tok × Option (List Tok)

Cut at the first k at depth 0: the tokens before it and, if there is one, the tokens after it. d is the depth at the start.

def noTop source

def noTop (k : Kw) : Int → List Tok → Bool

No k at depth 0, and the depth comes back to 0 at the end: a piece of a row.

def splitAll source

def splitAll (k : Kw) : Nat → List Tok → List (List Tok)

All the pieces between top-level ks.

Rows into equations

def group source

def group (one : Bool) : List (List Tok) → List (List Tok) → Option (List (List Tok))

Rows into equations’ tokens: a row with a left cell starts an equation (its & dropped), a row with an empty left cell continues the last one; split and multline (one) make all rows one equation. Refused: a continuation with no equation before it, one that starts with =, and a second top-level & in a row. acc holds the equations so far, the last first.

def cookRows source

def cookRows (sf : Sf) (S : Sym) (one : Bool) (ts : List Tok) : Option (List Eqn)

Read the rows of a multi-line display (tokens) into equations.

The normalization lemma

structure Layout source

structure Layout where
  l : List Tok
  r : List Tok
  more : List (List Tok)

An aligned layout of one equation’s tokens: the left cell, then the right parts of its first row and of each continuation row.

def Layout.toks source

def Layout.toks (L : Layout) : List Tok

The tokens the layout lays out.

def Layout.rows source

def Layout.rows (L : Layout) : List (List Tok)

The layout’s rows: l & r, then & r' for each continuation.

def Layout.OK source

def Layout.OK (L : Layout) : Prop

A layout the reader splits back: every piece is free of top-level & and line breaks, the left cell is not empty, and no continuation starts with =.

def joinRows source

def joinRows : List (List Tok) → List Tok

The tokens of rows joined by line breaks.

def rowsToks source

def rowsToks (Ls : List Layout) : List Tok

The token stream of a display laid out over aligned rows.

theorem cookRows_layout proved source

theorem cookRows_layout (sf : Sf) (S : Sym) (Ls : List Layout) (es : List Eqn)
    (hL : ∀ L ∈ Ls, L.OK) (hne : Ls ≠ [])
    (h : List.Forall₂ (fun L e => L.toks = print sf S (eqExpr e) ∧ isE e.lhs = true ∧
      isE e.rhs = true) Ls es) :
    cookRows sf S false (rowsToks Ls) = some (es.map (fun e => ⟨none, e.lhs, e.rhs⟩))

Multi-line equations read as the equations they lay out. If each equation’s canonical tokens are laid out over aligned rows (a left cell, &, the rest, then continuation rows & …), with no top-level & or line break inside a piece, the rows read back as exactly those equations.

theorem mem_rowsToks proved source

theorem mem_rowsToks {Ls : List Layout} {t : Tok} (h : t ∈ rowsToks Ls) :
    t = .kw .amp ∨ t = .kw .nl ∨ ∃ L ∈ Ls, t ∈ L.toks

Every token of a layout’s display is a token of an equation, &, or a line break.

This module also proves 9 lemmas without doc comments; they are in the source.