The canonical unit spelling

Lean module Esm.Units.Canonical, formal/Esm/Units/Canonical.lean at 184aa13d35e5
Imports Esm.Units.Factors, Esm.Units.Strings, Esm.Digits

The canonical form of a document rewrites every units string to ONE spelling built from its parsed unit (esm-spec §4.8.2), so m*h/(mi*s), m h/(mi s) and m·h/(mi·s) canonicalize alike. It is a syntactic normalization of the parsed tree, not a reduction to SI: symbols are kept (ppm stays ppm, km stays km).

From the two-sided normal form (norm2 , Esm.Units.Factors ): the numerator is the factors whose net exponent is positive, each symbol once with its exponents summed, in symbol order, joined by *; the denominator is the factors whose net exponent is negative, normalized the same way, written with the exponent’s absolute value. A symbol is NEVER cancelled across the fraction bar (ruling of 2026-11-12): mol/mol stays mol/mol, mol/mol/s is mol/(mol*s), and m m^-1 is m/m. An exponent 1 is omitted, an integer exponent is ^n, a non-integer rational is ^(p/q) in lowest terms. The spelling is num , num/den when the denominator has one factor, or num/(den1*den2*…); an empty numerator is 1, so the dimensionless unit is 1.

Choices beyond the grammar:

"", "1" and "dimensionless" are the three §4.8.1 spellings of one dimensionless entry, so all three canonicalize to "1", and a dimensionless factor inside a product is dropped like the atom 1 (UExpr.factors ).
A string that does not lex or parse is left unchanged (canon is total and is the identity there). So is a string that parses but contains a symbol run with a . in it (1.5m: the lexer reads digits.run with a non-digit in the second run as one symbol); no table key contains ., so such a string never resolves.
Because nothing cancels, a symbol of the parse is dropped from the spelling only when its exponent is 0 (m^0). A dropped symbol must still name a table unit (keepsSyms ); otherwise the string is left unchanged, so it keeps failing to resolve. Canonicalization never turns a resolving string into a non-resolving one (resolve_canon ), nor the reverse (resolve_of_canon ).

Theorems: canon_idem (idempotent), parse_canon (the spelling parses back to a tree with the same two-sided normal form), resolve_canon (and so the same unit), resolve_of_canon (a string whose spelling resolves resolves itself), canon_eq_of_factors (strings with the same two-sided normal form spell alike), and parse_spell (every two-sided normal list with admissible symbols is spelled so that it parses back to itself).

Admissible symbols and digits

def symRunB source

def symRunB (s : String) : Bool

A run of identifier characters that is not all digits: one symbol token.

def symOK source

def symOK (s : String) : Bool

A symbol the canonical spelling can write: %, or a run of identifier characters that is not all digits (so the lexer reads it back as one symbol), and not dimensionless (a spelling of 1).

def CanonFactors source

def CanonFactors (l : List Factor) : Prop

A canonical factor list: two-sided normal, every symbol admissible.

def digs source

def digs (n : ℕ) : List Char

The decimal digits of n (empty for 0; only positive numbers are written).

The spelling, as tokens

def numTok source

def numTok (n : ℕ) : Tok

The number token the lexer produces for the digits of n.

def expToks source

def expToks (q : ℚ) : List Tok

The exponent tokens for a positive exponent q.

def fToks source

def fToks (f : Factor) : List Tok

One factor, written with the absolute value of its exponent.

def joinToks source

def joinToks : List Factor → List Tok

Factors joined by *.

def spellToks source

def spellToks (l : List Factor) : List Tok

The canonical spelling of a factor list, as tokens.

def spell source

def spell (l : List Factor) : String

The canonical spelling of a factor list.

The canonicalizer

def parseChars source

def parseChars (cs : List Char) : Except Err UExpr

Parse a unit string’s characters to a tree. The empty string is the dimensionless unit 1 (§4.8.1: "" is a spelling of it).

def keepsSyms source

def keepsSyms (e : UExpr) : Bool

Every symbol of the parse either survives into the two-sided normal form or names a table unit. (A symbol is dropped only when its exponent is 0, as in m^0; spelling a string without such a symbol would hide that it does not resolve.)

def canon source

def canon (s : String) : String

The canonical spelling of a unit string; the identity on a string that does not parse, whose factors include a symbol the spelling cannot write, or that drops a symbol naming no unit (keepsSyms ).

Lexing the spelling

def OpHead source

def OpHead (rest : List Char) : Prop

What may follow an operand (a symbol run or a number): nothing, or a character that neither extends the run nor makes it a decimal.

def AnyRest source

def AnyRest (_ : List Char) : Prop

No condition on what follows.

def NoStarHead source

def NoStarHead (rest : List Char) : Prop

What may follow *: anything but a second *.

def LexP source

def LexP (toks : List Tok) (P : List Char → Prop) : Prop

toks lexes from its rendering, whatever follows that satisfies P.

theorem lexP_op proved source

theorem lexP_op (t : Tok) (c : Char) (hr : renderTok t = [c])
    (h : ∀ k cs, lexAux (k + 1) (c :: cs) = (t :: ·) <$> lexAux k cs) (P : List Char → Prop)
    (ha : c.toNat < 128) : LexP [t] P

A single-character operator other than *.

theorem symOK_head proved source

theorem symOK_head (s : String) (h : symOK s = true) : ∀ r, s.toList ≠ '*' :: r

The first character of an admissible symbol is not *.

def numToks source

def numToks (l : List Factor) : List Tok

The numerator tokens.

theorem lex_spell proved source

theorem lex_spell (l : List Factor) (hl : CanonFactors l) :
    lex (normalize (renderToks (spellToks l))) = .ok (spellToks l)

The spelling’s characters lex to the spelling’s tokens.

The parse of the spelling

def term source

def term (f : Factor) : UExpr

The tree one factor parses to: its symbol, raised to the exponent’s absolute value unless that is 1.

def foldTerms source

def foldTerms (acc : UExpr) (fs : List Factor) : UExpr

acc * t₁ * t₂ * …, folded left.

def numTree source

def numTree (l : List Factor) : UExpr

The numerator’s tree.

def spellTree source

def spellTree (l : List Factor) : UExpr

The tree the spelling parses to.

theorem parse_spellToks proved source

theorem parse_spellToks (l : List Factor) (hl : ∀ f ∈ l, f.2 ≠ 0) :
    parse (spellToks l) = .ok (spellTree l)

The spelling’s tokens parse to spellTree .

The spelling’s factors

def absF source

def absF (f : Factor) : Factor

A factor with its exponent’s absolute value.

theorem parse_spell proved source

theorem parse_spell :
    ∀ l : List Factor, CanonFactors l →
      ∃ e, parseChars (spell l).toList = .ok e ∧ e.factors = l ∧ norm2 e.factors = l

The spelling parses back. Every canonical factor list is spelled so that it parses (§4.8.2) to a tree whose factor list is a permutation of it, and whose normalized factor list is it exactly.

theorem canon_cases proved source

theorem canon_cases (s : String) :
    canon s = s ∨ ∃ e, parseChars s.toList = .ok e ∧ CanonFactors (norm2 e.factors) ∧
      keepsSyms e = true ∧ canon s = spell (norm2 e.factors)

canon either leaves a string alone or spells a canonical factor list — the normalized factor list of the string’s parse.

theorem keepsSyms_of_normal proved source

theorem keepsSyms_of_normal (e : UExpr) (h : norm2 e.factors = e.factors) :
    keepsSyms e = true

A tree whose factors are exactly its normal form keeps its symbols.

theorem canon_spell proved source

theorem canon_spell (l : List Factor) (hl : CanonFactors l) : canon (spell l) = spell l

The canonical spelling of a canonical factor list is a fixed point.

theorem canon_idem proved source

theorem canon_idem : ∀ s : String, canon (canon s) = canon s

Idempotence. Canonicalizing a canonical spelling returns it unchanged.

theorem parse_canon proved source

theorem parse_canon :
    ∀ (s : String) (e : UExpr), parseChars s.toList = .ok e →
      ∃ e', parseChars (canon s).toList = .ok e' ∧ norm2 e'.factors = norm2 e.factors

The canonical spelling keeps the factors. If a unit string parses, its canonical spelling parses too, to a tree with the same normalized factor list.

theorem canon_eq_of_factors proved source

theorem canon_eq_of_factors :
    ∀ (s t : String) (e e' : UExpr), parseChars s.toList = .ok e → parseChars t.toList = .ok e' →
      norm2 e.factors = norm2 e'.factors → (norm2 e.factors).all (fun f => symOK f.1) = true →
      keepsSyms e = true → keepsSyms e' = true → canon s = canon t

Two strings whose parses have the same normalized factor list, all of whose symbols the spelling can write, and neither of which drops a symbol naming no unit, have the same canonical spelling. (Strings that resolve never drop such a symbol: keepsSyms_of_eval .)

The canonical spelling denotes the same unit

def vsym source

def vsym (s : String) : Dim × (Base → ℚ)

What a symbol denotes, as a vector (dimension, scale exponents).

theorem eval_factors proved source

theorem eval_factors :
    ∀ (e : UExpr) (u : U), e.eval = .ok u →
      (∀ f ∈ e.factors, f.1 ∈ keys) ∧ u.val = wsum vsym e.factors

A tree that evaluates names only table keys, and its unit is the weighted sum of its factors.

theorem eval_of_keys proved source

theorem eval_of_keys :
    ∀ e : UExpr, (∀ f ∈ e.factors, f.1 ∈ keys) →
      ∃ u, e.eval = .ok u ∧ u.val = wsum vsym e.factors

A tree whose factors are all table keys evaluates, to the weighted sum.

theorem resolve_canon proved source

theorem resolve_canon :
    ∀ (s : String) (u : U), resolve s = .ok u → ∃ u', resolve (canon s) = .ok u' ∧ u'.Agree u

The canonical spelling denotes the same unit. If a unit string resolves (§4.8.1, §4.8.2), its canonical spelling resolves to a unit that agrees with it: same dimension, same exact scale.

theorem keepsSyms_of_eval proved source

theorem keepsSyms_of_eval (e : UExpr) (u : U) (h : e.eval = .ok u) : keepsSyms e = true

A tree that evaluates drops no symbol naming no unit.

theorem resolve_of_canon proved source

theorem resolve_of_canon :
    ∀ (s : String) (u' : U), resolve (canon s) = .ok u' → ∃ u, resolve s = .ok u ∧ u'.Agree u

Canonicalization does not hide an unresolvable unit. If the canonical spelling of a string resolves, the string itself resolves, to a unit that agrees with it.

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