Unification of units

Type inference for units is unification modulo the equational theory of abelian groups. Kennedy showed this is decidable with principal solutions; this file is the beginning of a mechanization of that, specialized to ℚ exponents.

Why ℚ makes this linear algebra

Over ℤ the unit group is a lattice and solving requires Hermite or Smith normal form. Over ℚ it is a vector space, and the whole problem becomes linear algebra over a field.

Better, it decomposes. A unit term's variable coefficients are scalars (vars : V → ℚ), not per-base vectors, so a single system of equations gives an independent linear system for each base unit, all sharing the same coefficient matrix. One elimination serves every base unit. That structural fact is built into Term rather than proved about it, and Term.solves_iff below is where it becomes visible.

The algorithm

Gaussian elimination, with Term.reduce as the row operation. Two facts make it work, and they are the whole content:

• reducing u against a pivot equation t kills the pivot variable in u (reduce_pivot);
• reducing preserves the solution set, given that the pivot equation itself holds (solves_reduce_iff).

Termination is structural: triangulate recurses on a list of equations whose length strictly decreases, so there is no measure to invent and no well-founded argument to discharge.

Status

Proved here:

• the per-base decomposition (Term.solves_iff);
• single-equation elimination, sound (Term.solves_elim), with every ground solution fixed by elimination when its other coordinates are supplied (Term.elim_eq_of_solves);
• row reduction kills the pivot and preserves solutions (Term.reduce_pivot, Term.solves_reduce_iff);
• multi-equation systems, with reduction preserving the solution set (System.solves_reduceAll_iff) and isolating the pivot (System.reduceAll_pivot_zero);
• triangularization, terminating structurally, preserving the solution set exactly: an iff, so nothing is lost and nothing gained (System.solves_triangulate_iff);
• the rigid residual case, decided by inspection with no search (System.solves_of_no_vars, System.solves_of_pivot_none).

Not proved here: a solver constructor, a symbolic most-general substitution, or principal-type inference for Λs. Assign B V assigns ground units; a single such assignment does not represent the full family of solutions. The file has no concrete faithful pivot or composition of elimination with back-substitution. It also has no constraint generation from unannotated terms and no solver for the two-level dimension constraints introduced by conversion. Whether the full calculus admits decidable principal-type inference is open in this development; this file proves neither existence nor failure of principal types. The calculus is fully annotated. The rest of the development uses only Term, the unit expression representation (UExp abbreviates Term B (Fin k)); no result elsewhere rests on the solver.

structure LambdaS.Term (B : Type u_1) (V : Type u_2) : Type (max u_1 u_2)

A unit term over base units B with unification variables V.

base b is the exponent of base unit b; vars v is the exponent of variable v. A term denotes the formal product ∏ b^(base b) · ∏ v^(vars v).

Note the asymmetry that does all the work: vars is V → ℚ, not V → B → ℚ. A variable stands for a whole unit, so it enters every base unit's equation with the same scalar coefficient.

• base : B → ℚ
• vars : V → ℚ

@[reducible, inline]

abbrev LambdaS.Term.Assign (B : Type u_3) (V : Type u_4) : Type (max u_4 u_3)

An assignment sends each unification variable to a ground unit.

Reducible, so Function.update and the rest of the Pi API apply to it directly: the same structurality choice made for Space.

Equations

• LambdaS.Term.Assign B V = (V → LambdaS.Uom B)

def LambdaS.Term.eval {B : Type u_1} {V : Type u_2} [Fintype V] (t : Term B V) (σ : Assign B V) : Uom B

Applying an assignment: exponents combine linearly.

Equations

• t.eval σ = LambdaS.Uom.ofExp fun (b : B) => t.base b + ∑ v : V, t.vars v * (σ v).exp b

@[simp]

theorem LambdaS.Term.exp_eval {B : Type u_1} {V : Type u_2} [Fintype V] (t : Term B V) (σ : Assign B V) (b : B) : (t.eval σ).exp b = t.base b + ∑ v : V, t.vars v * (σ v).exp b

def LambdaS.Term.Solves {B : Type u_1} {V : Type u_2} [Fintype V] (σ : Assign B V) (t : Term B V) : Prop

An assignment solves a term when the term evaluates to the trivial unit, i.e. when the equation it encodes holds.

Equations

• LambdaS.Term.Solves σ t = (t.eval σ = 1)

theorem LambdaS.Term.solves_iff {B : Type u_1} {V : Type u_2} [Fintype V] (σ : Assign B V) (t : Term B V) : Solves σ t ↔ ∀ (b : B), t.base b + ∑ v : V, t.vars v * (σ v).exp b = 0

Decomposition. A single unit equation is equivalent to one independent scalar equation per base unit, all sharing the coefficient vector t.vars.

This is the statement that unification over ℚ is |B| linear systems with a common matrix, and hence one Gaussian elimination.

theorem LambdaS.Term.solves_of_no_vars {B : Type u_1} {V : Type u_2} [Fintype V] (t : Term B V) (hv : t.vars = fun (x : V) => 0) (σ : Assign B V) : Solves σ t ↔ t.base = fun (x : B) => 0

Rigid mismatch. When no variable occurs, the equation is solvable exactly when it already holds on the nose. This is the error case of unification, and it is decidable pointwise.

def LambdaS.Term.elim {B : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (t : Term B V) (v₀ : V) (rest : Assign B V) : Assign B V

Elimination. Given a variable v₀ occurring with nonzero exponent, solve the equation for it, taking the other variables' values as given.

This is the single step of the unification algorithm: v₀ is determined by the rest, so each step removes one variable.

Equations

• t.elim v₀ rest = Function.update rest v₀ (LambdaS.Uom.ofExp fun (b : B) => -(t.base b + ∑ v ∈ Finset.univ.erase v₀, t.vars v * (rest v).exp b) / t.vars v₀)

theorem LambdaS.Term.solves_elim {B : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (t : Term B V) (v₀ : V) (h : t.vars v₀ ≠ 0) (rest : Assign B V) : Solves (t.elim v₀ rest) t

Soundness of elimination. The assignment it produces solves the equation.

theorem LambdaS.Term.elim_eq_of_solves {B : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (t : Term B V) (v₀ : V) (h : t.vars v₀ ≠ 0) (τ : Assign B V) (hτ : Solves τ t) : τ = t.elim v₀ τ

Single-equation solution characterization. Every ground solution is fixed by elim: its pivot value is determined by its other coordinates. Together with solves_elim, this parameterizes the solutions of one equation. It is not a theorem about principal types or symbolic most-general unifiers.

Row reduction

The single operation from which multi-equation solving is built.

def LambdaS.Term.reduce {B : Type u_1} {V : Type u_2} (u t : Term B V) (v₀ : V) : Term B V

Reduce u against pivot equation t on variable v₀: the row operation u ← u - (u[v₀]/t[v₀]) · t.

Equations

• u.reduce t v₀ = { base := fun (b : B) => u.base b - u.vars v₀ / t.vars v₀ * t.base b, vars := fun (v : V) => u.vars v - u.vars v₀ / t.vars v₀ * t.vars v }

@[simp]

theorem LambdaS.Term.reduce_base {B : Type u_1} {V : Type u_2} (u t : Term B V) (v₀ : V) (b : B) : (u.reduce t v₀).base b = u.base b - u.vars v₀ / t.vars v₀ * t.base b

@[simp]

theorem LambdaS.Term.reduce_vars {B : Type u_1} {V : Type u_2} (u t : Term B V) (v₀ v : V) : (u.reduce t v₀).vars v = u.vars v - u.vars v₀ / t.vars v₀ * t.vars v

@[simp]

theorem LambdaS.Term.reduce_pivot {B : Type u_1} {V : Type u_2} (u t : Term B V) (v₀ : V) (h : t.vars v₀ ≠ 0) : (u.reduce t v₀).vars v₀ = 0

Reduction kills the pivot. After reducing, v₀ no longer occurs in u, which is what makes the elimination make progress.

theorem LambdaS.Term.solves_reduce_iff {B : Type u_1} {V : Type u_2} [Fintype V] {σ : Assign B V} {u t : Term B V} {v₀ : V} (ht : Solves σ t) : Solves σ (u.reduce t v₀) ↔ Solves σ u

Reduction preserves solutions, given that the pivot equation holds.

This is the correctness of Gaussian elimination, and everything below is an induction over it.

Systems

@[reducible, inline]

abbrev LambdaS.System (B : Type u_1) (V : Type u_2) : Type (max u_2 u_1)

A system of unit equations, each asserted to equal the trivial unit.

Equations

• LambdaS.System B V = List (LambdaS.Term B V)

def LambdaS.System.Solves {B : Type u_1} {V : Type u_2} [Fintype V] (σ : Term.Assign B V) (sys : System B V) : Prop

An assignment solves a system when it solves every equation in it.

Equations

• LambdaS.System.Solves σ sys = ∀ t ∈ sys, LambdaS.Term.Solves σ t

@[simp]

theorem LambdaS.System.solves_nil {B : Type u_1} {V : Type u_2} [Fintype V] (σ : Term.Assign B V) : Solves σ []

@[simp]

theorem LambdaS.System.solves_cons {B : Type u_1} {V : Type u_2} [Fintype V] (σ : Term.Assign B V) (t : Term B V) (sys : System B V) : Solves σ (t :: sys) ↔ Term.Solves σ t ∧ Solves σ sys

def LambdaS.System.reduceAll {B : Type u_1} {V : Type u_2} (sys : System B V) (t : Term B V) (v₀ : V) : System B V

Reduce every equation of a system against a pivot.

Equations

• sys.reduceAll t v₀ = List.map (fun (u : LambdaS.Term B V) => u.reduce t v₀) sys

theorem LambdaS.System.solves_reduceAll_iff {B : Type u_1} {V : Type u_2} [Fintype V] {σ : Term.Assign B V} {sys : System B V} {t : Term B V} {v₀ : V} (ht : Term.Solves σ t) : Solves σ (sys.reduceAll t v₀) ↔ Solves σ sys

Reducing a whole system preserves its solution set, given the pivot holds.

theorem LambdaS.System.reduceAll_pivot_zero {B : Type u_1} {V : Type u_2} {sys : System B V} {t : Term B V} {v₀ : V} (h : t.vars v₀ ≠ 0) (u : Term B V) : u ∈ sys.reduceAll t v₀ → u.vars v₀ = 0

After reduction the pivot variable is gone from every equation.

Triangularization

Repeatedly pivot on the head equation, reducing the tail against it. Recursion is on a list whose length strictly decreases, so termination is structural: no measure to invent, no well-founded argument to discharge.

@[simp]

theorem LambdaS.System.length_reduceAll {B : Type u_1} {V : Type u_2} (sys : System B V) (t : Term B V) (v₀ : V) : List.length (sys.reduceAll t v₀) = List.length sys

Reduction preserves the number of equations: it is a row operation, not an elimination of rows. This is what makes triangulate structurally decreasing.

def LambdaS.System.Pivot (B : Type u_3) (V : Type u_4) : Type (max u_4 u_3)

Choose a pivot variable for an equation: any variable occurring with nonzero coefficient. Left abstract, since the choice affects only numerical conditioning, never the solution set.

Equations

• LambdaS.System.Pivot B V = (LambdaS.Term B V → Option V)

structure LambdaS.System.Faithful {B : Type u_1} {V : Type u_2} (p : Pivot B V) : Prop

A pivot function is faithful when it finds a variable exactly when one occurs. Correctness of elimination (solves_triangulate_iff) needs none of this: the solution set is preserved whatever the pivot does. Faithfulness is what makes elimination terminate usefully, by guaranteeing that a none answer really does mean the equation has become rigid.

• none_of (t : Term B V) : p t = none → t.vars = fun (x : V) => 0

  No pivot reported means no variable occurs.

• ne_zero (t : Term B V) (v : V) : p t = some v → t.vars v ≠ 0

  A reported pivot really has a nonzero coefficient.

@[irreducible]

def LambdaS.System.triangulate {B : Type u_1} {V : Type u_2} (p : Pivot B V) : System B V → System B V

Gaussian elimination: pivot on each equation in turn, reducing all later equations against it.

Equations

• LambdaS.System.triangulate p [] = []
• LambdaS.System.triangulate p (t :: rest) = match p t with | some v₀ => t :: LambdaS.System.triangulate p (LambdaS.System.reduceAll rest t v₀) | none => t :: LambdaS.System.triangulate p rest

theorem LambdaS.System.solves_triangulate_iff {B : Type u_1} {V : Type u_2} [Fintype V] (p : Pivot B V) {σ : Term.Assign B V} (sys : System B V) : Solves σ (triangulate p sys) ↔ Solves σ sys

Correctness of triangularization. It preserves the solution set exactly.

Together with reduceAll_pivot_zero this is Gaussian elimination: each pivot variable is isolated in a single equation, and the solution set is untouched.

The terminal case, and decidability

theorem LambdaS.System.solves_of_no_vars {B : Type u_1} {V : Type u_2} [Fintype V] {sys : System B V} (hv : ∀ t ∈ sys, t.vars = fun (x : V) => 0) (σ : Term.Assign B V) : Solves σ sys ↔ ∀ t ∈ sys, t.base = fun (x : B) => 0

A system in which no variable occurs is solvable exactly when every base exponent already vanishes.

This is the rigid-mismatch check, and it is the terminal case of elimination: once triangularization has isolated every pivot variable, what remains are the variable-free equations, and those decide solvability.

theorem LambdaS.System.no_vars_solves_iff_forall {B : Type u_1} {V : Type u_2} [Fintype V] {sys : System B V} (hv : ∀ t ∈ sys, t.vars = fun (x : V) => 0) (σ τ : Term.Assign B V) : Solves σ sys ↔ Solves τ sys

Solvability of a variable-free system does not depend on the assignment, so the check is a decision procedure, not a search.

theorem LambdaS.System.solves_of_pivot_none {B : Type u_1} {V : Type u_2} [Fintype V] {p : Pivot B V} (hp : Faithful p) {t : Term B V} (h : p t = none) (σ : Term.Assign B V) : Term.Solves σ t ↔ t.base = fun (x : B) => 0

With a faithful pivot, an equation the pivot declines is genuinely rigid, and its solvability is settled by inspecting its base exponents alone.

This is what closes the loop: elimination drives every equation either to a pivot (which determines a variable, by Term.elim_eq_of_solves) or to a rigid residual (which is decided here, with no search and no assignment).