Examples of units in PhysLean

In this module we give some examples of how to use the units system in PhysLean. This module should not be imported into any other module, and the results here should not be used in the proofs of any other results other then those in this file.

Defining a length dependent on units

noncomputable def UnitExamples.meters400 : Dimensionful (WithDim Dimension.L𝓭 ℝ)

The length corresponding to 400 meters.

Equations

• UnitExamples.meters400 = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 400 }

Proving propositions are dimensionally correct

Cases with only WithDim

def UnitExamples.EnergyMassWithDim' (m : WithDim Dimension.M𝓭 ℝ) (E : WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) (c : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹) ℝ) : Prop

An example of dimensions corresponding to E = m c^2 using WithDim.

Equations

• UnitExamples.EnergyMassWithDim' m E c = (E = (m * c * c).cast UnitExamples.EnergyMassWithDim'._proof_1)

theorem UnitExamples.energyMassWithDim'_isDimensionallyCorrect : IsDimensionallyCorrect EnergyMassWithDim'

def UnitExamples.NewtonsSecondWithDim' (m : WithDim Dimension.M𝓭 ℝ) (F : WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) (a : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) : Prop

An example of dimensions corresponding to F = m a using WithDim.

Equations

• UnitExamples.NewtonsSecondWithDim' m F a = (F = (m * a).cast UnitExamples.NewtonsSecondWithDim'._proof_1)

theorem UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect : IsDimensionallyCorrect NewtonsSecondWithDim'

def UnitExamples.SpeedEq (s : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹) ℝ) (d : WithDim Dimension.L𝓭 ℝ) (t : WithDim Dimension.T𝓭 ℝ) : Prop

An example of dimensions corresponding to s = d/t using WithDim.

Equations

• UnitExamples.SpeedEq s d t = (s = (d / t).cast UnitExamples.SpeedEq._proof_1)

theorem UnitExamples.speedEq_isDimensionallyCorrect : IsDimensionallyCorrect SpeedEq

def UnitExamples.OddDimensions (m1 m2 : WithDim Dimension.M𝓭 ℝ) (θ : WithDim Dimension.Θ𝓭 ℝ) (I1 I2 : WithDim (Dimension.C𝓭 / Dimension.T𝓭) ℝ) (d : WithDim Dimension.L𝓭 ℝ) (t : WithDim Dimension.T𝓭 ℝ) (X : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹ ^ 3 * Dimension.Θ𝓭⁻¹ * Dimension.C𝓭 ^ 2) ℝ) : Prop

An example with complicated dimensions.

Equations

• UnitExamples.OddDimensions m1 m2 θ I1 I2 d t X = (X = (m1 * (d / t) / (m2 * θ) * I2 * I1).cast UnitExamples.OddDimensions._proof_1)

theorem UnitExamples.oddDimensions_isDimensionallyCorrect : IsDimensionallyCorrect OddDimensions

def UnitExamples.EnergyMassWithDim (m : WithDim Dimension.M𝓭 ℝ) (E : WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) (c : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹) ℝ) : Prop

An example of dimensions corresponding to E = m c^2 using WithDim with .val.

Equations

• UnitExamples.EnergyMassWithDim m E c = (E.val = m.val * c.val ^ 2)

theorem UnitExamples.energyMassWithDim_isDimensionallyCorrect : IsDimensionallyCorrect EnergyMassWithDim

def UnitExamples.NewtonsSecondWithDim (m : WithDim Dimension.M𝓭 ℝ) (F : WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) (a : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) : Prop

An example of dimensions corresponding to F = m a using WithDim with .val.

Equations

• UnitExamples.NewtonsSecondWithDim m F a = (F.val = m.val * a.val)

theorem UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect : IsDimensionallyCorrect NewtonsSecondWithDim

def UnitExamples.EnergyMassWithDimNot (m : WithDim Dimension.M𝓭 ℝ) (E : WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) (c : WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹) ℝ) : Prop

An example of dimensions corresponding to E = m c using WithDim with .val, which is not dimensionally correct.

Equations

• UnitExamples.EnergyMassWithDimNot m E c = (E.val = m.val * c.val)

theorem UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect : ¬IsDimensionallyCorrect EnergyMassWithDimNot

Cases with Dimensionful

def UnitExamples.EnergyMass (m : WithDim Dimension.M𝓭 ℝ) (E : WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ) (u : UnitChoices) : Prop

The equation E = m c^2, in this equation we E and m are implicitly in the units u, while the speed of light is explicitly written in those units.

Equations

• UnitExamples.EnergyMass m E u = (E.val = m.val * (↑DimSpeed.speedOfLight u).val ^ 2)

def UnitExamples.EnergyMass' (m : Dimensionful (WithDim Dimension.M𝓭 ℝ)) (E : Dimensionful (WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ)) (u : UnitChoices) : Prop

The equation E = m c^2, in this version everything is written explicitly in terms of a choice of units.

Equations

• UnitExamples.EnergyMass' m E u = ((↑E u).val = (↑m u).val * (↑DimSpeed.speedOfLight u).val ^ 2)

theorem UnitExamples.energyMass_isDimensionallyCorrect : IsDimensionallyCorrect EnergyMass

The lemma that the proposition EnergyMass is dimensionally correct

Examples of using isDimensionallyCorrect

We now explore the consequences of energyMass_isDimensionallyCorrect and how we can use it.

theorem UnitExamples.example1_energyMass : EnergyMass { val := 2 } { val := 2 * 299792458 ^ 2 } UnitChoices.SI

theorem UnitExamples.example2_energyMass (u : UnitChoices) : EnergyMass (UnitDependent.scaleUnit UnitChoices.SI u { val := 2 }) (UnitDependent.scaleUnit UnitChoices.SI u { val := 2 * 299792458 ^ 2 }) u

## Examples with other functions

def UnitExamples.CosDim (t : WithDim Dimension.T𝓭 ℝ) (ω : WithDim Dimension.T𝓭⁻¹ ℝ) (a : ℝ) : Prop

An example of a dimensionafully correct result using functions.

Equations

• UnitExamples.CosDim t ω a = (Real.cos (ω.val * t.val) = a)

theorem UnitExamples.cosDim_isDimensionallyCorrect : IsDimensionallyCorrect CosDim

## An example involving derivatives