Reference · Non-negative rationals
rainbow.math.rational.nnrat.ring
A verified nonnegative-rational semiring normalization tactic, up to `nnrat/equivalent`. This is the `rainbow.math.nat.ring` analogue one level up. Where nat-ring normalizes expressions over `algebra/nat-add` / `nat/multiply` and chains PROPOSITIONAL EQUALITIES, this file normalizes expressions over `nnrat/add` / `nnrat/multiply` and chains NNRAT EQUIVALENCES -- because nnrat addition and multiplication are associative, commutative and distributive only up to `~` (a sum's denominator depends on how it was bracketed), so no reassociation of an nnrat expression is ever a definitional equality. That distinction is the whole reason this exists. Hand-writing a signed or rational reassociation means chaining `add-four-reorder`, `add-associative`, `multiply-commutative` and the two congruence lemmas by hand, and the chains grow super-linearly in the number of monomials: the eight-monomial identity behind `signed/multiply-associative` is roughly two hundred error-prone lines written out. Normalizing both sides to a canonical sorted sum of canonical monomials makes it one call. Like nat-ring this is a TACTIC LIBRARY, not a spec module: it exports Clojure functions returning either a raw proof term or a proof record `{:lhs :rhs :proof}` where `:proof : lhs ~ rhs`. It operates on SURFACE terms (built with `function/const*` on the alias symbols `nnrat/add` and `nnrat/multiply`), before elaboration. PUBLIC ENTRY POINTS (prove-equiv a b) -> proof record; :proof inhabits `nnrat/equivalent a b`. Throws if the two sides are not semiring-equal, so it can never emit a false proof. (equiv a b) -> just the proof term. (prove-product-equiv a b) -> the product-only (monomial) special case. extend-environment -> chains every law provider the emitted proofs cite. LAWS CITED (all must be in the environment; `extend-environment` puts them there): `nnrat/equivalent-reflexive`, `-symmetric`, `-transitive`, `nnrat/add-respects-equivalence`, `nnrat/multiply-respects-equivalence` (these five are D63 base), `nnrat/add-associative`, `nnrat/add-commutative`, `nnrat/multiply-associative`, `nnrat/multiply-commutative`, `nnrat/multiply-distributes-add-right`. Note the distributive law available is the RIGHT one only; left distribution is derived here from it plus multiplicative commutativity, exactly as nat-ring does. The distribute-right provider is `nnrat-distribute-right` rather than `nnrat-distributive`, so that consumers of this tactic remain compatible with `nnrat-identities` (the two full modules both declare `nnrat/multiply-one-left`, and chaining both is an alias conflict).