A framework to formalize units (such as length, time, mass, velocity, etc.) in Lean.

class UnitsSystem : Type (u_1 + 1)

• Dimensions : Type u_1
• addCommGroup : AddCommGroup Dimensions

@[reducible, inline]

abbrev UnitsSystem.Formal [UnitsSystem] : Type u_1

The two key types here are Formal and Scalar d. Scalar d is the space of scalar quantities whose units are given by d:Dimensions. Collectively, they generate a graded commutative ring Formal, which can be conveniently described using the existing Mathlib structure AddMonoidAlgebra. Algebraic manipulations of scalar quantities will be most conveniently handled by casting these quantities into the commutative ring Formal, where one can use standard Mathlib tactics such as ring.

In principle one could also develop vector-valued quantities with dimension, but for now we restrict attention to scalar quantities only.

Equations

• UnitsSystem.Formal = AddMonoidAlgebra ℝ UnitsSystem.Dimensions

structure UnitsSystem.Scalar [UnitsSystem] (d : Dimensions) : Type

The data val of a scalar quantity can be interpreted as the numerical value of that quantity with respect to some standard set of units (e.g., SI units).

• val : ℝ

theorem UnitsSystem.Scalar.ext {inst✝ : UnitsSystem} {d : Dimensions} {x y : Scalar d} (val : x.val = y.val) : x = y

theorem UnitsSystem.Scalar.ext_iff {inst✝ : UnitsSystem} {d : Dimensions} {x y : Scalar d} : x = y ↔ x.val = y.val

theorem UnitsSystem.Scalar.val_injective [UnitsSystem] (d : Dimensions) : Function.Injective val

theorem UnitsSystem.Scalar.val_inj [UnitsSystem] {d : Dimensions} (q₁ q₂ : Scalar d) : q₁.val = q₂.val ↔ q₁ = q₂

def UnitsSystem.Scalar.cast [UnitsSystem] {d d' : Dimensions} (q : Scalar d) : autoParam (d' = d) _auto✝ → Scalar d'

We will encounter a technical issue with Lean's type system, namely that the type Scalar d and Scalar d' are not identical if d' and d are merely propositionally equal (as opposed to definitionally equal); for instance, Scalar (d₁+d₂) and Scalar (d₂+d₁) are distinct types. Technically, this renders multiplication on scalar types noncommutative. To get around this, we create a casting operator, where the propositional equality is attempted to be resolved by the Lean tactic module whenever possible. Unfortunately, the casting operator from Scalar d to Scalar d' cannot be captured by standard Lean coercion classes such as Coe or CoeOut as each of the types here contain parameters not present in the other.

Equations

• q.cast x✝ = { val := q.val }

theorem UnitsSystem.Scalar.cast_eq [UnitsSystem] {d d' : Dimensions} (q : Scalar d) (q' : Scalar d') (h : d = d' := by module) : q.val = q'.val ↔ q = q'.cast h

This is a variant of Scalar.val_inj that handles casts.

theorem UnitsSystem.Scalar.cast_eq_symm [UnitsSystem] {d d' : Dimensions} (q : Scalar d) (q' : Scalar d') (h : d = d' := by module) : q = q'.cast h ↔ q' = q.cast ⋯

@[simp]

theorem UnitsSystem.Scalar.cast_val [UnitsSystem] {d d' : Dimensions} (q : Scalar d) (h : d' = d := by module) : (q.cast h).val = q.val

noncomputable def UnitsSystem.Scalar.toFormal [UnitsSystem] {d : Dimensions} (q : Scalar d) : Formal

The existing Mathlib method AddMonoidAlgebra.single is perfect for embedding each type of scalar into the formal graded ring Formal.

Equations

• ↑q = AddMonoidAlgebra.single d q.val

noncomputable instance UnitsSystem.Scalar.instCoeFormal [UnitsSystem] (d : Dimensions) : CoeOut (Scalar d) Formal

Equations

• UnitsSystem.Scalar.instCoeFormal d = { coe := UnitsSystem.Scalar.toFormal }

@[simp]

theorem UnitsSystem.Scalar.toFormal_inj [UnitsSystem] {d : Dimensions} (q₁ q₂ : Scalar d) : ↑q₁ = ↑q₂ ↔ q₁ = q₂

Many identities involving several types of Scalars can be dealt with by applying simp [←toFormal_inj] to move everything to Formal. A large number of further simp lemmas in this file are then designed to simplify such Formal expressions, often by pushing casting operators inward back to the Scalar types. As such, there will be significant overlap between the simp and norm_cast tags.

@[simp]

theorem UnitsSystem.Scalar.toFormal_cast [UnitsSystem] {d d' : Dimensions} (q : Scalar d) (h : d' = d := by module) : ↑(q.cast h) = ↑q

Conveniently, casts from one scalar to another will automatically disappear when moving to Formal.

instance UnitsSystem.Scalar.instZero [UnitsSystem] {d : Dimensions} : Zero (Scalar d)

Equations

• UnitsSystem.Scalar.instZero = { zero := { val := 0 } }

@[simp]

theorem UnitsSystem.Scalar.val_zero [UnitsSystem] {d : Dimensions} : val 0 = 0

theorem UnitsSystem.Scalar.neZero_iff [UnitsSystem] {d : Dimensions} (q : Scalar d) : NeZero q ↔ q.val ≠ 0

We will use the NeZero class to tag some scalars as non-zero; this becomes relevant when using such scalars as units. One could also introduce API to tag some scalars as positive, but we currently are not implementing this.

@[simp]

theorem UnitsSystem.Scalar.toFormal_zero [UnitsSystem] {d : Dimensions} : ↑0 = 0

instance UnitsSystem.Scalar.instAdd [UnitsSystem] {d : Dimensions} : Add (Scalar d)

In the next few lines of code we give Scalar d the structure of a real vector space, which is of course compatible with the real vector space structure on Formal.

Equations

• UnitsSystem.Scalar.instAdd = { add := fun (q₁ q₂ : UnitsSystem.Scalar d) => { val := q₁.val + q₂.val } }

@[simp]

theorem UnitsSystem.Scalar.val_add [UnitsSystem] {d : Dimensions} (q₁ q₂ : Scalar d) : (q₁ + q₂).val = q₁.val + q₂.val

@[simp]

theorem UnitsSystem.Scalar.toFormal_add [UnitsSystem] {d : Dimensions} (q₁ q₂ : Scalar d) : ↑(q₁ + q₂) = ↑q₁ + ↑q₂

Note how the simp lemma is in the direction of pushing casts inward.

instance UnitsSystem.Scalar.instNeg [UnitsSystem] {d : Dimensions} : Neg (Scalar d)

Equations

• UnitsSystem.Scalar.instNeg = { neg := fun (q : UnitsSystem.Scalar d) => { val := -q.val } }

@[simp]

theorem UnitsSystem.Scalar.val_neg [UnitsSystem] {d : Dimensions} (q : Scalar d) : (-q).val = -q.val

instance UnitsSystem.Scalar.instNeZero_neg [UnitsSystem] {d : Dimensions} (q : Scalar d) [h : NeZero q] : NeZero (-q)

@[simp]

theorem UnitsSystem.Scalar.toFormal_neg [UnitsSystem] {d : Dimensions} (q : Scalar d) : ↑(-q) = -↑q

instance UnitsSystem.Scalar.instSub [UnitsSystem] {d : Dimensions} : Sub (Scalar d)

Equations

• UnitsSystem.Scalar.instSub = { sub := fun (q₁ q₂ : UnitsSystem.Scalar d) => { val := q₁.val - q₂.val } }

@[simp]

theorem UnitsSystem.Scalar.val_sub [UnitsSystem] {d : Dimensions} (q₁ q₂ : Scalar d) : (q₁ - q₂).val = q₁.val - q₂.val

@[simp]

theorem UnitsSystem.Scalar.toFormal_sub [UnitsSystem] {d : Dimensions} (q₁ q₂ : Scalar d) : ↑(q₁ - q₂) = ↑q₁ - ↑q₂

instance UnitsSystem.Scalar.instSMul [UnitsSystem] {α : Type u_2} {d : Dimensions} [SMul α ℝ] : SMul α (Scalar d)

Equations

• UnitsSystem.Scalar.instSMul = { smul := fun (c : α) (q : UnitsSystem.Scalar d) => { val := c • q.val } }

@[simp]

theorem UnitsSystem.Scalar.val_smul [UnitsSystem] {α : Type u_1} {d : Dimensions} [SMul α ℝ] (a : α) (q : Scalar d) : (a • q).val = a • q.val

instance UnitsSystem.Scalar.instAddGroup [UnitsSystem] {d : Dimensions} : AddGroup (Scalar d)

Equations

• UnitsSystem.Scalar.instAddGroup = Function.Injective.addGroup UnitsSystem.Scalar.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance UnitsSystem.Scalar.instAddCommGroup [UnitsSystem] {d : Dimensions} : AddCommGroup (Scalar d)

Equations

• UnitsSystem.Scalar.instAddCommGroup = Function.Injective.addCommGroup UnitsSystem.Scalar.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def UnitsSystem.Scalar.ofReal [UnitsSystem] (r : ℝ) : Scalar 0

The dimensionless scalars Scalar 0 can be identified with real numbers.

Equations

• ↑r = { val := r }

instance UnitsSystem.Scalar.instCoeReal [UnitsSystem] : Coe ℝ (Scalar 0)

Equations

• UnitsSystem.Scalar.instCoeReal = { coe := UnitsSystem.Scalar.ofReal }

@[simp]

theorem UnitsSystem.Scalar.coe_val [UnitsSystem] (r : ℝ) : (↑r).val = r

@[simp]

theorem UnitsSystem.Scalar.coe_zero [UnitsSystem] : ↑0 = 0

theorem UnitsSystem.Scalar.neZero_coe_iff [UnitsSystem] {r : ℝ} : NeZero ↑r ↔ r ≠ 0

@[simp]

theorem UnitsSystem.Scalar.coe_inj [UnitsSystem] {r s : ℝ} : ↑r = ↑s ↔ r = s

@[simp]

theorem UnitsSystem.Scalar.coe_add [UnitsSystem] (r s : ℝ) : ↑(r + s) = ↑r + ↑s

@[simp]

theorem UnitsSystem.Scalar.coe_neg [UnitsSystem] (r : ℝ) : ↑(-r) = -↑r

@[simp]

theorem UnitsSystem.Scalar.coe_sub [UnitsSystem] (r s : ℝ) : ↑(r - s) = ↑r - ↑s

noncomputable instance UnitsSystem.Formal.instCoeReal [UnitsSystem] : Coe ℝ Formal

It is convenient to view the real numbers as a subring of the Formal ring, thus identifying scalar multiplication with ordinary multiplication.

Equations

• UnitsSystem.Formal.instCoeReal = { coe := fun (r : ℝ) => ↑↑r }

@[simp]

theorem UnitsSystem.Formal.coe_zero [UnitsSystem] : ↑↑0 = 0

@[simp]

theorem UnitsSystem.Formal.coe_one [UnitsSystem] : ↑↑1 = 1

@[simp]

theorem UnitsSystem.Formal.coe_nat [UnitsSystem] (n : ℕ) : ↑↑↑n = ↑n

@[simp]

theorem UnitsSystem.Formal.coe_int [UnitsSystem] (n : ℤ) : ↑↑↑n = ↑n

@[simp]

theorem UnitsSystem.Scalar.toFormal_smul [UnitsSystem] {d : Dimensions} (c : ℝ) (q : Scalar d) : ↑(c • q) = ↑↑c * ↑q

@[simp]

theorem UnitsSystem.Formal.smul_eq_mul [UnitsSystem] (c : ℝ) (x : Formal) : c • x = ↑↑c * x

@[simp]

theorem UnitsSystem.Formal.smul_eq_mul' [UnitsSystem] (c : ℕ) (x : Formal) : c • x = ↑c * x

@[simp]

theorem UnitsSystem.Formal.smul_eq_mul'' [UnitsSystem] (c : ℤ) (x : Formal) : c • x = ↑c * x

@[simp]

theorem UnitsSystem.Scalar.coe_mul [UnitsSystem] (r s : ℝ) : ↑(r * s) = r • ↑s

instance UnitsSystem.Scalar.instModule [UnitsSystem] {d : Dimensions} : Module ℝ (Scalar d)

We are finally able to view Scalar as a vector space over ℝ as promised.

Equations

• UnitsSystem.Scalar.instModule = { toSMul := UnitsSystem.Scalar.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem UnitsSystem.Scalar.val_smul' [UnitsSystem] {d : Dimensions} (c : ℕ) (q : Scalar d) : (c • q).val = ↑c * q.val

@[simp]

theorem UnitsSystem.Scalar.val_smul'' [UnitsSystem] {d : Dimensions} (c : ℤ) (q : Scalar d) : (c • q).val = ↑c * q.val

@[simp]

theorem UnitsSystem.Scalar.toFormal_smul' [UnitsSystem] {d : Dimensions} (c : ℕ) (q : Scalar d) : ↑(c • q) = ↑c * ↑q

@[simp]

theorem UnitsSystem.Scalar.toFormal_smul'' [UnitsSystem] {d : Dimensions} (c : ℤ) (q : Scalar d) : ↑(c • q) = ↑c * ↑q

instance UnitsSystem.Scalar.instHMul [UnitsSystem] {d₁ d₂ : Dimensions} : HMul (Scalar d₁) (Scalar d₂) (Scalar (d₁ + d₂))

One can multiply a Scalar d₁ and Scalar d₂ quantities to obtain a Scalar (d₁+d₂) quantity, in a manner compatible with multiplication in Formal.

Equations

• UnitsSystem.Scalar.instHMul = { hMul := fun (q₁ : UnitsSystem.Scalar d₁) (q₂ : UnitsSystem.Scalar d₂) => { val := q₁.val * q₂.val } }

@[simp]

theorem UnitsSystem.Scalar.val_hMul [UnitsSystem] {d₁ d₂ : Dimensions} (q₁ : Scalar d₁) (q₂ : Scalar d₂) : (q₁ * q₂).val = q₁.val * q₂.val

@[simp]

theorem UnitsSystem.Scalar.toFormal_hMul [UnitsSystem] {d₁ d₂ : Dimensions} (q₁ : Scalar d₁) (q₂ : Scalar d₂) : ↑(q₁ * q₂) = ↑q₁ * ↑q₂

noncomputable def UnitsSystem.Scalar.pow [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℕ) : Scalar (n • d)

Similarly, one can raise a Scalar d quantity to a natural number power n to obtain a Scalar (n • d) quantity. One could also implement exponentiation to an integer, but I have elected not to do this, implementing an inversion relation instead.

Equations

• q**n = { val := q.val ^ n }

def UnitsSystem.«term_**_» : Lean.TrailingParserDescr

One cannot use the Mathlib classes Pow or HPow here because the output type Scalar (n • d) depends on the input n. As the symbol ^ is reserved for such classes, we use the symbol ** isntead.

Equations

• UnitsSystem.«term_**_» = Lean.ParserDescr.trailingNode `UnitsSystem.«term_**_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "**") (Lean.ParserDescr.cat `term 81))

@[simp]

theorem UnitsSystem.Scalar.val_pow [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℕ) : (q**n).val = q.val ^ n

@[simp]

theorem UnitsSystem.Scalar.toFormal_pow [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℕ) : ↑(q**n) = ↑q ^ n

noncomputable def UnitsSystem.Scalar.inv [UnitsSystem] {d : Dimensions} (q : Scalar d) : Scalar (-d)

We cannot use Mathlib's Inv class here or the associated ⁻¹ notation because Inv requires the output to be of the same type as the input.

Equations

• q.inv = { val := q.val⁻¹ }

@[simp]

theorem UnitsSystem.Scalar.val_inv [UnitsSystem] {d : Dimensions} (q : Scalar d) : q.inv.val = q.val⁻¹

instance UnitsSystem.Scalar.instNeg_inv [UnitsSystem] {d : Dimensions} (q : Scalar d) [h : NeZero q] : NeZero q.inv

@[simp]

theorem UnitsSystem.Scalar.mul_inv_self [UnitsSystem] {d : Dimensions} (q : Scalar d) [h : NeZero q] : ↑q * ↑q.inv = 1

@[simp]

theorem UnitsSystem.Scalar.inv_mul_self [UnitsSystem] {d : Dimensions} (q : Scalar d) [h : NeZero q] : ↑q.inv * ↑q = 1

@[simp]

theorem UnitsSystem.Scalar.inv_coe [UnitsSystem] (r : ℝ) : ↑(↑r).inv = ↑↑r⁻¹

@[simp]

theorem UnitsSystem.Scalar.mul_inv [UnitsSystem] {d₁ d₂ : Dimensions} (q₁ : Scalar d₁) (q₂ : Scalar d₂) : (q₁ * q₂).inv = (q₁.inv * q₂.inv).cast ⋯

@[simp]

theorem UnitsSystem.Scalar.pow_inv [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℕ) : (q**n).inv = (q.inv**n).cast ⋯

noncomputable instance UnitsSystem.Scalar.instHDiv [UnitsSystem] {d₁ d₂ : Dimensions} : HDiv (Scalar d₁) (Scalar d₂) (Scalar (d₁ - d₂))

Multiplication and inversion combine to give division in the usual fashion.

Equations

• UnitsSystem.Scalar.instHDiv = { hDiv := fun (q₁ : UnitsSystem.Scalar d₁) (q₂ : UnitsSystem.Scalar d₂) => { val := q₁.val / q₂.val } }

@[simp]

theorem UnitsSystem.Scalar.val_hDiv [UnitsSystem] {d₁ d₂ : Dimensions} (q₁ : Scalar d₁) (q₂ : Scalar d₂) : (q₁ / q₂).val = q₁.val / q₂.val

@[simp]

theorem UnitsSystem.Scalar.toFormal_hDiv [UnitsSystem] {d₁ d₂ : Dimensions} (q₁ : Scalar d₁) (q₂ : Scalar d₂) : ↑(q₁ / q₂) = ↑q₁ * ↑q₂.inv

noncomputable instance UnitsSystem.Scalar.instHDiv' [UnitsSystem] {d : Dimensions} : HDiv (Scalar d) ℝ (Scalar d)

Equations

• UnitsSystem.Scalar.instHDiv' = { hDiv := fun (q : UnitsSystem.Scalar d) (r : ℝ) => { val := q.val / r } }

noncomputable instance UnitsSystem.Scalar.instHDiv'' [UnitsSystem] {d : Dimensions} : HDiv (Scalar d) ℕ (Scalar d)

Equations

• UnitsSystem.Scalar.instHDiv'' = { hDiv := fun (q : UnitsSystem.Scalar d) (n : ℕ) => q / ↑n }

noncomputable instance UnitsSystem.Scalar.instHDiv''' [UnitsSystem] {d : Dimensions} : HDiv (Scalar d) ℤ (Scalar d)

Equations

• UnitsSystem.Scalar.instHDiv''' = { hDiv := fun (q : UnitsSystem.Scalar d) (n : ℤ) => q / ↑n }

@[simp]

theorem UnitsSystem.Scalar.val_hDiv' [UnitsSystem] {d : Dimensions} (q : Scalar d) (r : ℝ) : (q / r).val = q.val / r

@[simp]

theorem UnitsSystem.Scalar.val_hDiv'' [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℕ) : (q / n).val = q.val / ↑n

@[simp]

theorem UnitsSystem.Scalar.val_hDiv''' [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℤ) : (q / n).val = q.val / ↑n

@[simp]

theorem UnitsSystem.Scalar.toFormal_hDiv' [UnitsSystem] {d : Dimensions} (q : Scalar d) (r : ℝ) : ↑(q / r) = ↑q * ↑↑r⁻¹

@[simp]

theorem UnitsSystem.Scalar.toFormal_hDiv'' [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℕ) : ↑(q / n) = ↑q * ↑↑(↑n)⁻¹

@[simp]

theorem UnitsSystem.Scalar.toFormal_hDiv''' [UnitsSystem] {d : Dimensions} (q : Scalar d) (n : ℤ) : ↑(q / n) = ↑q * ↑↑(↑n)⁻¹

instance UnitsSystem.Scalar.instLE [UnitsSystem] (d : Dimensions) : LE (Scalar d)

Equations

• UnitsSystem.Scalar.instLE d = { le := fun (x y : UnitsSystem.Scalar d) => x.val ≤ y.val }

theorem UnitsSystem.Scalar.val_le [UnitsSystem] {d : Dimensions} (x y : Scalar d) : x ≤ y ↔ x.val ≤ y.val

noncomputable instance UnitsSystem.Scalar.instLinearOrder [UnitsSystem] (d : Dimensions) : LinearOrder (Scalar d)

Equations

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

theorem UnitsSystem.Scalar.val_lt [UnitsSystem] {d : Dimensions} (x y : Scalar d) : x < y ↔ x.val < y.val

instance UnitsSystem.Scalar.instOrderedSMul [UnitsSystem] (d : Dimensions) : OrderedSMul ℝ (Scalar d)

def UnitsSystem.StandardUnit [UnitsSystem] (d : Dimensions) : Scalar d

The standard unit of Scalar d is the quantity whose data val is equal to 1.

Equations

• UnitsSystem.StandardUnit d = { val := 1 }

@[simp]

theorem UnitsSystem.StandardUnit.val_eq [UnitsSystem] (d : Dimensions) : (StandardUnit d).val = 1

instance UnitsSystem.StandardUnit.inst_NeZero [UnitsSystem] (d : Dimensions) : NeZero (StandardUnit d)

@[simp]

theorem UnitsSystem.StandardUnit.mul [UnitsSystem] (d₁ d₂ : Dimensions) : StandardUnit d₁ * StandardUnit d₂ = StandardUnit (d₁ + d₂)

@[simp]

theorem UnitsSystem.StandardUnit.mul' [UnitsSystem] (d₁ d₂ : Dimensions) : ↑(StandardUnit d₁) * ↑(StandardUnit d₂) = ↑(StandardUnit (d₁ + d₂))

@[simp]

theorem UnitsSystem.StandardUnit.pow [UnitsSystem] (d : Dimensions) (n : ℕ) : StandardUnit d**n = StandardUnit (n • d)

@[simp]

theorem UnitsSystem.StandardUnit.pow' [UnitsSystem] (d : Dimensions) (n : ℕ) : ↑(StandardUnit d) ^ n = ↑(StandardUnit (n • d))

@[simp]

theorem UnitsSystem.StandardUnit.inv [UnitsSystem] (d : Dimensions) : (StandardUnit d).inv = StandardUnit (-d)

@[simp]

theorem UnitsSystem.StandardUnit.div [UnitsSystem] (d₁ d₂ : Dimensions) : StandardUnit d₁ / StandardUnit d₂ = StandardUnit (d₁ - d₂)

noncomputable def UnitsSystem.Scalar.in [UnitsSystem] {d : Dimensions} (unit q : Scalar d) : ℝ

unit.in q is q:Scalar d measured in terms of unit:Scalar d.

Equations

• unit.in q = q.val / unit.val

@[simp]

theorem UnitsSystem.Scalar.val_in [UnitsSystem] (d : Dimensions) (unit q : Scalar d) : unit.in q = q.val / unit.val

theorem UnitsSystem.Scalar.in_def [UnitsSystem] {d : Dimensions} (unit q : Scalar d) [h : NeZero unit] : q = unit.in q • unit

@[simp]

theorem UnitsSystem.Scalar.in_smul [UnitsSystem] {d : Dimensions} (c : ℝ) (unit q : Scalar d) : unit.in (c • q) = c * unit.in q

theorem UnitsSystem.Scalar.in_inj [UnitsSystem] {d : Dimensions} (unit q₁ q₂ : Scalar d) [h : NeZero unit] : unit.in q₁ = unit.in q₂ ↔ q₁ = q₂