Executable completeness of unit declarations

Consistency (LambdaS.Declare) says some valuation satisfies the declarations. Running a program needs more: every conversion between two units of the same dimension must have a factor the declarations fix. By Decl.determined_iff_mem_span (LambdaS.Determinacy), a consistent set fixes a factor exactly when its ratio lies in the ℚ-span of the declared ratios. The ratios of same-dimension pairs are exactly the dimensionless unit vectors, the kernel of the dimension map, so completeness is the condition that the declared ratios span that kernel.

check decides this without computing a kernel basis. It appends one row per base dimension (dimensionRows) to the declared ratio vectors (combined) and asks whether the result spans all of B → ℚ; checkSpan answers by solving one rational system per standard basis vector with RationalSolver.solve. For sound declarations the two spanning conditions agree (Decl.combined_span_eq_top_iff).

The theorems, from the linear-algebra form to the one the checker uses:

• check_iff_span_dimensionless: for sound declarations, check holds exactly when every dimensionless ratio lies in Decl.ratioSpan.
• check_iff_determined: if the set is also consistent, exactly when every dimensionless ratio is Decl.Determined.
• check_iff_all_conversions_determined: the same, stated for every same-dimension pair; Section 3 of our paper cites it, and DeclSolver.check relies on it.

Consistency itself is checked separately, by DeclSolver.solve.

def LambdaS.DeclarationComplete.checkSpan {B : Type} {m k : ℕ} (enum : Fin m ≃ B) (vectors : Fin k → B → ℚ) : Bool

Check that the supplied vectors span by solving for every standard basis vector.

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaS.DeclarationComplete.checkSpan_iff {B : Type} [Fintype B] [DecidableEq B] {m k : ℕ} (enum : Fin m ≃ B) (vectors : Fin k → B → ℚ) : checkSpan enum vectors = true ↔ Submodule.span ℚ (Set.range vectors) = ⊤

The executable span check is sound and complete.

def LambdaS.DeclarationComplete.dimensionRows {B D : Type} [UnitSys B D] : D → B → ℚ

One row per dimension, over the base-unit coordinates.

Equations

• LambdaS.DeclarationComplete.dimensionRows e b = (LambdaS.UnitSys.dim b).base e

def LambdaS.DeclarationComplete.combined {B D : Type} [DecidableEq B] [UnitSys B D] {d n : ℕ} (dims : Fin d ≃ D) (ds : Fin n → Decl B) : Fin (n + d) → B → ℚ

Declaration vectors followed by dimension rows, explicitly enumerated.

Equations

• LambdaS.DeclarationComplete.combined dims ds i = Sum.elim (fun (j : Fin n) => (ds j).ratio.base) (fun (e : Fin d) => LambdaS.DeclarationComplete.dimensionRows (dims e)) (finSumFinEquiv.symm i)

def LambdaS.DeclarationComplete.check {B D : Type} [DecidableEq B] [UnitSys B D] {m d n : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) : Bool

True when the declaration vectors and dimension rows span all unit coordinates.

Equations

• LambdaS.DeclarationComplete.check enum dims ds = LambdaS.DeclarationComplete.checkSpan enum (LambdaS.DeclarationComplete.combined dims ds)

theorem LambdaS.DeclarationComplete.check_iff_span_dimensionless {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {m d n : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) (hsound : ∀ (i : Fin n), (ds i).Sound) : check enum dims ds = true ↔ ∀ (r : UExp B 0), dimOf (DCtx.nil D) r = 1 → r.base ∈ Decl.ratioSpan ds

Sound declarations make the executable combined-span check equivalent to covering the full kernel of the dimension map.

theorem LambdaS.DeclarationComplete.check_iff_determined {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {m d n : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) (hsound : ∀ (i : Fin n), (ds i).Sound) (hconsistent : ∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)) : check enum dims ds = true ↔ ∀ (r : UExp B 0), dimOf (DCtx.nil D) r = 1 → Decl.Determined ds r

For consistent sound declarations, completeness means every dimensionless ratio has the same factor in every satisfying valuation.

theorem LambdaS.DeclarationComplete.check_iff_all_conversions_determined {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {m d n : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) (hsound : ∀ (i : Fin n), (ds i).Sound) (hconsistent : ∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)) : check enum dims ds = true ↔ ∀ (u v : UExp B 0), SameDim (DCtx.nil D) u v → Decl.Determined ds (Term.div u v)

Global completeness, decided. For sound and consistent declarations, check returns true exactly when every legal conversion (every pair u, v of the same dimension) has a factor fixed by the declarations. Section 3 of our paper cites this form; DeclSolver.check relies on it.

Executable boundary checks for the standard-basis solving loop.

@[instance_reducible]

def LambdaS.DeclarationComplete.instUnitSysFinOfNatNat : UnitSys (Fin 2) (Fin 1)

Equations

• LambdaS.DeclarationComplete.instUnitSysFinOfNatNat = { dim := fun (x : Fin 2) => LambdaS.Term.ofBase 0 }