Whole unit strings, end to end (esm-spec §4.8.2)

Lean module Esm.Units.Strings, formal/Esm/Units/Strings.lean at 184aa13d35e5
Imports Esm.Units.Identities, Esm.Units.GrammarLaws

Facts about resolve on specific strings the spec names, and about the scaling-factor diagnostic text. The parse step is checked by the kernel; the table lookup and composition by rfl.

theorem resolveChars_eq proved source

theorem resolveChars_eq (cs : List Char) (h : cs ≠ []) :
    resolveChars cs = (lex (normalize cs) >>= parse) >>= UExpr.eval

Resolution of a nonempty string: normalise, lex, parse, then evaluate.

theorem percent_resolves proved source

theorem percent_resolves :
    (∃ u, resolve "%" = .ok u ∧ u.Agree (num 0.01)) ∧
    (∃ u, resolve "%/h" = .ok u ∧ u.Agree (mk (Dims.dimless - Dims.time) (1 / 360000)))

% is a symbol token (§4.8.2): "%" resolves to dimensionless scale 0.01, and "%/h" to h⁻¹ at scale 1/360000.

theorem m_per_s_pow_scaling_factor proved source

theorem m_per_s_pow_scaling_factor :
    resolve "(m/s)^-1/3" = .error (.scalingFactor "3")

"(m/s)^-1/3" reads as ((m/s)^-1)/3, and the 3 is a scaling factor.

theorem g_per_hp_hr_rejected proved source

theorem g_per_hp_hr_rejected :
    resolve "g/hp-hr" =
      .error (.syntax "'-' is not an operator in a unit string (a negative exponent is ^-n)")

MOVES’s "g/hp-hr" does not resolve: - is not an operator.

theorem scaling_factor_message proved source

theorem scaling_factor_message :
    ∀ lit : String,
      "scaling factor".toList <:+: (Err.scalingFactor lit).message.toList ∧
      "^(p/q)".toList <:+: (Err.scalingFactor lit).message.toList

The scaling-factor diagnostic, for every literal, says that the number is a scaling factor and that a rational exponent is spelled ^(p/q).