@[reducible, inline]

abbrev Units.UnitChoice : Type

Choosing a metric involves choosing

• a power factor (it's one for base and derived units)
• an affine conversion (to convert between units of the same dimension)
• a dimension (to ensure dimensional correctness)

Note that all these 3 choices form a AddCommGroup, so we can combine them easily.

Equations

• Units.UnitChoice = (ℚ × Units.Conversion × Units.Dimension)

structure Units.Unit : Type

A unit is a product of base units raised to rational powers. For example, the unit of force in the SI system is kg•m/s² can be represented as :

• force₁ = {"kg" ↦ (1,0,Mass), "m" ↦ (1,0,Length), "s" ↦ (-2,0,Time⁻²)}

or when using derived units:

• force₂={"N" ↦ (1,0,Mass•Length•Time⁻²)}

Converting between these two representations is possible because their dimensions are the same under product:

• Π 𝒟(force₁) = Mass•Length•Time⁻² = Π 𝒟(force₂)

• _impl : Π₀ (x : String), UnitChoice

def Units.instDecidableEqUnit.decEq (x✝ x✝¹ : Unit) : Decidable (x✝ = x✝¹)

Equations

• Units.instDecidableEqUnit.decEq { _impl := a } { _impl := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Units.instDecidableEqUnit : DecidableEq Unit

Equations

• Units.instDecidableEqUnit = Units.instDecidableEqUnit.decEq

def Units.instBEqUnit.beq : Unit → Unit → Bool

Equations

• Units.instBEqUnit.beq { _impl := a } { _impl := b } = (a == b)
• Units.instBEqUnit.beq x✝¹ x✝ = false

instance Units.instBEqUnit : BEq Unit

Equations

• Units.instBEqUnit = { beq := Units.instBEqUnit.beq }

instance Units.Unit.instAddCommGroup : AddCommGroup Unit

Equations

• Units.Unit.instAddCommGroup = Units.Unit.instEquiv.addCommGroup

instance Units.Unit.instOne : One Unit

Equations

• Units.Unit.instOne = { one := 0 }

instance Units.Unit.instMul : Mul Unit

Equations

• Units.Unit.instMul = { mul := fun (u1 u2 : Units.Unit) => u1 + u2 }

instance Units.Unit.instInv : Inv Unit

Equations

• Units.Unit.instInv = { inv := fun (u : Units.Unit) => -u }

instance Units.Unit.instDiv : Div Unit

Equations

• Units.Unit.instDiv = { div := fun (u1 u2 : Units.Unit) => u1 - u2 }

instance Units.Unit.instPowNat : Pow Unit ℕ

Equations

• Units.Unit.instPowNat = { pow := fun (u : Units.Unit) (q : ℕ) => q • u }

instance Units.Unit.instPowInt : Pow Unit ℤ

Equations

• Units.Unit.instPowInt = { pow := fun (u : Units.Unit) (n : ℤ) => n • u }

def Units.Unit.dimension (u : Unit) : Dimension

Equations

• u.dimension = u._impl.sum fun (x : String) (qd : Units.UnitChoice) => qd.2.2

def Units.Unit.conversion (u : Unit) : Conversion

Equations

• u.conversion = u._impl.sum fun (x : String) (qd : Units.UnitChoice) => qd.2.1

instance Units.Unit.instHasDimension : HasDimension Unit

Equations

• Units.Unit.instHasDimension = { dimension := Units.Unit.dimension }

instance Units.Unit.instHasConversion : HasConversion Unit

Equations

• Units.Unit.instHasConversion = { conversion := Units.Unit.conversion }

instance Units.Unit.instSetoidUnit : Setoid Unit

Two units are considered equal if they have the same dimension and conversion, regardless of their representation.

For example, N and kg•m/s² are considered equivalent

Equations

• Units.Unit.instSetoidUnit = { r := fun (u₁ u₂ : Units.Unit) => u₁.dimension = u₂.dimension ∧ u₁.conversion = u₂.conversion, iseqv := Units.Unit.instSetoidUnit._proof_1 }

instance Units.Unit.instDecidableEquivUnit (u1 u2 : Unit) : Decidable (u1 ≈ u2)

Equations

• u1.instDecidableEquivUnit u2 = id inferInstance

def Units.Unit.defineUnit (s : String) (d : Dimension) : Unit

Define a base unit with a given name and dimension.

Example:

• meter = defineUnit "m" Dimension.Length

Equations

• Units.Unit.defineUnit s d = { _impl := fun₀ | s => (1, 0, d) }

def Units.Unit.defineDerivedUnit (s : String) (u : Unit) (conv : Conversion := 0) : Unit

Define a derived unit with a given name, unit and optional conversion. Example:

• newton = defineDerivedUnit "N" (kilogram * meter / second^2)
• celsius = defineDerivedUnit "°C" kelvin (Conversion.translate (27315/100))

Equations

• Units.Unit.defineDerivedUnit s u conv = { _impl := fun₀ | s => (1, conv.div u.conversion, u.dimension) }

instance Units.Unit.instRepr : Repr Unit

Equations

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