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).

Triangularization uses well-founded recursion on the number of equations. Row reduction preserves the tail's length, so each recursive call decreases the measure specified by termination_by.

Status

Section 2 of our paper cites this module; its main theorem is System.solves_triangulate_iff. 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 by equation-list length, 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.

The same structure at V = Fin k is the calculus's unit expression type UExp B k (in LambdaS.Syntax), where vars holds the exponents of the k unit variables in scope.

• 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 choice Space makes.

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 exactly. 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 well-founded on equation-list length: row reduction preserves the tail's length, establishing the decrease required by termination_by.

@[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 proves the length decrease required by triangulate.

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

A pivot rule: picks a variable of an equation to eliminate, or none. Faithful states the intended contract (a variable with nonzero coefficient, whenever one occurs). The rule is left abstract because, by solves_triangulate_iff, no choice changes 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, whatever the pivot rule.

Together with reduceAll_pivot_zero, which shows that a step with a nonzero pivot coefficient removes the pivot variable from every later equation, this is the forward phase of Gaussian elimination. No theorem here states that the whole output is triangular, and back-substitution is not composed with it.

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, the terminal case of elimination: after triangularization with a faithful pivot rule, each equation either has a pivot or is variable-free, and this theorem decides the variable-free ones. That the pivot equations can then always be satisfied by back-substitution is standard but not proved in this file.

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.

Elimination drives every equation either to a pivot (which determines that variable from the others, by Term.elim_eq_of_solves) or to a rigid residual, decided here with no search and no assignment. Assembling these two cases into a solver is not done in this file.