Physlib.Units.Examples

Physlib
Units
Examples

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Units.WithDim.Speed
public import Physlib.Units.FDeriv

Examples of units in Physlib

In this module we give some examples of how to use the units system in Physlib. 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.

@[expose] public section

Defining a length dependent on units

Changing that length to miles. 400 meters is very almost a quarter of a mile.

example : meters400 {SI with length := LengthUnit.miles} = ⟨1/4 - 73/50292⟩ := by⊢ ↑meters400
    (let __src := SI;
    { length := LengthUnit.miles, time := __src.time, mass := __src.mass, charge := __src.charge,
      temperature := __src.temperature }) =
  { val := 1 / 4 - 73 / 50292 }
  simp [meters400, toDimensionful_apply_apply, dimScale, LengthUnit.miles]⊢ ⟨1609.344⁻¹, ⋯⟩ • { val := 400 } = { val := 4⁻¹ - 73 / 50292 }
  ext⊢ (⟨1609.344⁻¹, ⋯⟩ • { val := 400 }).val = { val := 4⁻¹ - 73 / 50292 }.val
  show (1609.344 : ℝ)⁻¹ * 400 = _⊢ 1609.344⁻¹ * 400 = { val := 4⁻¹ - 73 / 50292 }.val
  norm_numAll goals completed! 🐙

Proving propositions are dimensionally correct

Cases with only WithDim

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

def EnergyMassWithDim' (m : WithDim M𝓭 ℝ) (E : WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ)
    (c : WithDim (L𝓭 * T𝓭⁻¹) ℝ) : Prop := E = cast (m * c * c)

lemma energyMassWithDim'_isDimensionallyCorrect :
    IsDimensionallyCorrect EnergyMassWithDim' := by⊢ IsDimensionallyCorrect EnergyMassWithDim' simp [funext_iff, EnergyMassWithDim']All goals completed! 🐙

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

def NewtonsSecondWithDim' (m : WithDim M𝓭 ℝ) (F : WithDim (M𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ)
    (a : WithDim (L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ) : Prop :=
    F = cast (m * a)

lemma newtonsSecondWithDim'_isDimensionallyCorrect :
    IsDimensionallyCorrect NewtonsSecondWithDim' := by⊢ IsDimensionallyCorrect NewtonsSecondWithDim' simp [funext_iff, NewtonsSecondWithDim']All goals completed! 🐙

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

def SpeedEq (s : WithDim (L𝓭 * T𝓭⁻¹) ℝ) (d : WithDim L𝓭 ℝ) (t : WithDim T𝓭 ℝ) : Prop :=
  s = cast (d / t)

lemma speedEq_isDimensionallyCorrect : IsDimensionallyCorrect SpeedEq := by⊢ IsDimensionallyCorrect SpeedEq
  simp [funext_iff, SpeedEq]All goals completed! 🐙

An example with complicated dimensions.

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

lemma oddDimensions_isDimensionallyCorrect : IsDimensionallyCorrect OddDimensions := by⊢ IsDimensionallyCorrect OddDimensions
  simp [funext_iff, OddDimensions]All goals completed! 🐙

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

def EnergyMassWithDim (m : WithDim M𝓭 ℝ) (E : WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ)
    (c : WithDim (L𝓭 * T𝓭⁻¹) ℝ) : Prop :=
  E.1 = m.1 * c.1 ^ 2



lemma energyMassWithDim_isDimensionallyCorrect : IsDimensionallyCorrect EnergyMassWithDim := by⊢ IsDimensionallyCorrect EnergyMassWithDim
  simp [funext_iff, EnergyMassWithDim]⊢ ∀ (u1 u2 : UnitChoices) (m : WithDim M𝓭 ℝ) (x : WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ) (x_1 : WithDim (L𝓭 * T𝓭⁻¹) ℝ),
  (scaleUnit u2 u1 x).val = (scaleUnit u2 u1 (m * (x_1 * x_1))).val ↔ x.val = (m * (x_1 * x_1)).val
  introsu1✝:UnitChoicesu2✝:UnitChoicesm✝:WithDim M𝓭 ℝx✝¹:WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝx✝:WithDim (L𝓭 * T𝓭⁻¹) ℝ⊢ (scaleUnit u2✝ u1✝ x✝¹).val = (scaleUnit u2✝ u1✝ (m✝ * (x✝ * x✝))).val ↔ x✝¹.val = (m✝ * (x✝ * x✝)).val
  rw [WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_equ1✝:UnitChoicesu2✝:UnitChoicesm✝:WithDim M𝓭 ℝx✝¹:WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝx✝:WithDim (L𝓭 * T𝓭⁻¹) ℝ⊢ x✝¹.val = (m✝ * (x✝ * x✝)).val ↔ x✝¹.val = (m✝ * (x✝ * x✝)).valAll goals completed! 🐙]All goals completed! 🐙

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

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



lemma newtonsSecondWithDim_isDimensionallyCorrect :
    IsDimensionallyCorrect NewtonsSecondWithDim := by⊢ IsDimensionallyCorrect NewtonsSecondWithDim
  simp [funext_iff, NewtonsSecondWithDim]⊢ ∀ (u1 u2 : UnitChoices) (m : WithDim M𝓭 ℝ) (x : WithDim (M𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ) (x_1 : WithDim (L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ),
  (scaleUnit u2 u1 x).val = (scaleUnit u2 u1 (m * x_1)).val ↔ x.val = (m * x_1).val
  introsu1✝:UnitChoicesu2✝:UnitChoicesm✝:WithDim M𝓭 ℝx✝¹:WithDim (M𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝx✝:WithDim (L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ⊢ (scaleUnit u2✝ u1✝ x✝¹).val = (scaleUnit u2✝ u1✝ (m✝ * x✝)).val ↔ x✝¹.val = (m✝ * x✝).val
  rw [WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_equ1✝:UnitChoicesu2✝:UnitChoicesm✝:WithDim M𝓭 ℝx✝¹:WithDim (M𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝx✝:WithDim (L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ⊢ x✝¹.val = (m✝ * x✝).val ↔ x✝¹.val = (m✝ * x✝).valAll goals completed! 🐙]All goals completed! 🐙

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

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

set_option backward.isDefEq.respectTransparency false in
lemma energyMassWithDimNot_not_isDimensionallyCorrect :
    ¬ IsDimensionallyCorrect EnergyMassWithDimNot := by⊢ ¬IsDimensionallyCorrect EnergyMassWithDimNot
  simp only [isDimensionallyCorrect_fun_iff, not_forall, funext_iff, scaleUnit_apply_fun]⊢ ∃ x x_1 x_2 x_3 x_4,
  ¬scaleUnit x x_1 (EnergyMassWithDimNot (scaleUnit x_1 x x_2) (scaleUnit x_1 x x_3)) x_4 =
      EnergyMassWithDimNot x_2 x_3 x_4
  /- We show that `EnergyMassWithDimNot` is not dimensionally correct by
    changing from `SI` to `SIPrimed` with values of `E`, `m` and `c` all equal to `1`. -/
  use SI, SIPrimed, ⟨1⟩, ⟨1⟩, ⟨1⟩h⊢ ¬scaleUnit SI SIPrimed (EnergyMassWithDimNot (scaleUnit SIPrimed SI { val := 1 }) (scaleUnit SIPrimed SI { val := 1 }))
      { val := 1 } =
    EnergyMassWithDimNot { val := 1 } { val := 1 } { val := 1 }
  unfold EnergyMassWithDimNoth⊢ ¬scaleUnit SI SIPrimed
      (fun c => (scaleUnit SIPrimed SI { val := 1 }).val = (scaleUnit SIPrimed SI { val := 1 }).val * c.val)
      { val := 1 } =
    ({ val := 1 }.val = { val := 1 }.val * { val := 1 }.val)
  norm_num [WithDim.scaleUnit_val, M𝓭, NNReal.smul_def]All goals completed! 🐙

Cases with Dimensionful

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.

def EnergyMass (m : WithDim M𝓭 ℝ) (E : WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ)
    (u : UnitChoices) : Prop :=
    E.1 = m.1 * (speedOfLight u).1 ^ 2

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

def EnergyMass' (m : Dimensionful (WithDim M𝓭 ℝ))
    (E : Dimensionful (WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ))
    (u : UnitChoices) : Prop :=
    (E.1 u).1 = (m.1 u).1 * (speedOfLight u).1 ^ 2

The lemma that the proposition EnergyMass is dimensionally correct

lemma energyMass_isDimensionallyCorrect :
    IsDimensionallyCorrect EnergyMass := by⊢ IsDimensionallyCorrect EnergyMass
  /- Scale such that the unit u1 is taken to u2. -/
  intro u1 u2u1:UnitChoicesu2:UnitChoices⊢ scaleUnit u1 u2 EnergyMass = EnergyMass
  /- Let `m` be the mass, `E` be the energy and `u` be the actual units we start with. -/
  funext m E uu1:UnitChoicesu2:UnitChoicesm:WithDim M𝓭 ℝE:WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝu:UnitChoices⊢ scaleUnit u1 u2 EnergyMass m E u = EnergyMass m E u
  unfold EnergyMassu1:UnitChoicesu2:UnitChoicesm:WithDim M𝓭 ℝE:WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝu:UnitChoices⊢ scaleUnit u1 u2 (fun m E u => E.val = m.val * (↑speedOfLight u).val ^ 2) m E u =
  (E.val = m.val * (↑speedOfLight u).val ^ 2)
  simp only [eq_iff_iff, UnitDependent.scaleUnit_apply_fun_left,
    UnitDependent.scaleUnit_apply_fun, Dimensionful.of_scaleUnit, dim_apply,
    WithDim.scaleUnit_val, WithDim.smul_val, map_mul, mul_pow, NNReal.smul_def, smul_eq_mul,
    NNReal.coe_mul]u1:UnitChoicesu2:UnitChoicesm:WithDim M𝓭 ℝE:WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝu:UnitChoices⊢ ↑((u2.dimScale u1) M𝓭) * ↑((u2.dimScale u1) L𝓭) * ↑((u2.dimScale u1) L𝓭) * ↑((u2.dimScale u1) T𝓭⁻¹) *
        ↑((u2.dimScale u1) T𝓭⁻¹) *
      E.val =
    ↑((u2.dimScale u1) M𝓭) * m.val *
      (↑((u2.dimScale u1) L𝓭) ^ 2 * ↑((u2.dimScale u1) T𝓭⁻¹) ^ 2 * (↑speedOfLight u).val ^ 2) ↔
  E.val = m.val * (↑speedOfLight u).val ^ 2
  ring_nfu1:UnitChoicesu2:UnitChoicesm:WithDim M𝓭 ℝE:WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝu:UnitChoices⊢ ↑((u2.dimScale u1) M𝓭) * ↑((u2.dimScale u1) L𝓭) ^ 2 * ↑((u2.dimScale u1) T𝓭⁻¹) ^ 2 * E.val =
    ↑((u2.dimScale u1) M𝓭) * ↑((u2.dimScale u1) L𝓭) ^ 2 * ↑((u2.dimScale u1) T𝓭⁻¹) ^ 2 * m.val *
      (↑speedOfLight u).val ^ 2 ↔
  E.val = m.val * (↑speedOfLight u).val ^ 2
  simp [mul_assoc, mul_eq_mul_left_iff, dimScale_ne_zero]All goals completed! 🐙

Examples of using `isDimensionallyCorrect`

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

lemma example1_energyMass : EnergyMass ⟨2⟩ ⟨2 * 299792458 ^ 2⟩ SI := by⊢ EnergyMass { val := 2 } { val := 2 * 299792458 ^ 2 } SI
  simp [EnergyMass, speedOfLight, toDimensionful_apply_apply, dimScale, SI]All goals completed! 🐙



/- The lemma `energyMass_isDimensionallyCorrect` allows us to scale the units
  of `example1_energyMass`, that is - we proved it in one set of units, but we get the result
  in any set of units. -/
lemma example2_energyMass (u : UnitChoices) :
    EnergyMass (scaleUnit SI u ⟨2⟩) (scaleUnit SI u ⟨2 * 299792458 ^ 2⟩) u := byu:UnitChoices⊢ EnergyMass (scaleUnit SI u { val := 2 }) (scaleUnit SI u { val := 2 * 299792458 ^ 2 }) u
  conv_rhs => rw [← UnitChoices.scaleUnit_apply_fst SI u]u:UnitChoices| scaleUnit SI u SI
  rw [← energyMass_isDimensionallyCorrect SI uu:UnitChoices⊢ scaleUnit SI u EnergyMass (scaleUnit SI u { val := 2 }) (scaleUnit SI u { val := 2 * 299792458 ^ 2 })
  (scaleUnit SI u SI)u:UnitChoices⊢ scaleUnit SI u EnergyMass (scaleUnit SI u { val := 2 }) (scaleUnit SI u { val := 2 * 299792458 ^ 2 })
  (scaleUnit SI u SI)]u:UnitChoices⊢ scaleUnit SI u EnergyMass (scaleUnit SI u { val := 2 }) (scaleUnit SI u { val := 2 * 299792458 ^ 2 })
  (scaleUnit SI u SI)
  simp only [scaleUnit_apply_fst, scaleUnit_apply_fun, scaleUnit_symm_apply,
    scaleUnit_apply_fun_left]u:UnitChoices⊢ EnergyMass { val := 2 } { val := 2 * 299792458 ^ 2 } SI
  exact example1_energyMassAll goals completed! 🐙

## Examples with other functions

An example of a dimensionally correct result using functions.

def CosDim (t : WithDim T𝓭 ℝ) (ω : WithDim T𝓭⁻¹ ℝ) (a : ℝ) : Prop :=
  Real.cos (ω.1 * t.1) = a

lemma cosDim_isDimensionallyCorrect : IsDimensionallyCorrect CosDim := by⊢ IsDimensionallyCorrect CosDim
  simp [funext_iff, CosDim]All goals completed! 🐙

## An example involving derivatives

example {M1 M2 : Type} [NormedAddCommGroup M1] [NormedSpace ℝ M1]
    [ContinuousConstSMul ℝ M1] [HasDim M1]
    [NormedAddCommGroup M2] [NormedSpace ℝ M2] [SMulCommClass ℝ ℝ M2]
    [ContinuousConstSMul ℝ M2] [HasDim M2] (f : M1 → M2)
    (hf : IsDimensionallyCorrect f) (f_diff : Differentiable ℝ f) :
    IsDimensionallyCorrect (fderiv ℝ f) :=
  fderiv_isDimensionallyCorrect f hf f_diff

example {M1 M2 : Type} [NormedAddCommGroup M1] [NormedSpace ℝ M1]
    [ContinuousConstSMul ℝ M1] [HasDim M1]
    [NormedAddCommGroup M2] [NormedSpace ℝ M2] [SMulCommClass ℝ ℝ M2]
    [ContinuousConstSMul ℝ M2] [HasDim M2] (dm : M1) (f : M1 → M2)
    (hf : IsDimensionallyCorrect f) (f_diff : Differentiable ℝ f) :
    IsDimensionallyCorrect (fun x (v : WithDim (dim M2 * (dim M1)⁻¹) M2) =>
      fderiv ℝ f x dm = v.1) :=
  fderiv_dimension_const_direction dm f hf f_diff