1. Physlib
  2. Units
  3. WithDim
  4. Basic
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.UnitDependent

WithDim

WithDim is the type M which carrying the dimension d.

The dimension d : Dimension B may be taken over any basis B of base dimensions. The algebraic structure of WithDim d M (its additive, order, scalar-action, multiplication, division and casting instances) is available for every basis B. The unit-scaling structure (HasDim, DMul, and the scaleUnit lemmas), which routes through UnitChoices.dimScale, is provided for the standard basis LTMCTDimensionBase.

@[expose] public section

The type M carrying an instance of a dimension d.

The underlying value of M.

structure WithDim {B : Type} (d : Dimension B) (M : Type) where val : M
@[ext] lemma ext {B : Type} {d : Dimension B} {M} (x1 x2 : WithDim d M) (h : x1.val = x2.val) : x1 = x2 := B:Typed:Dimension BM:Typex1:WithDim d Mx2:WithDim d Mh:x1.val = x2.val⊢ x1 = x2 B:Typed:Dimension BM:Typex2:WithDim d Mval✝:Mh:{ val := val✝ }.val = x2.val⊢ { val := val✝ } = x2 B:Typed:Dimension BM:Typeval✝¹:Mval✝:Mh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ } All goals completed! 🐙instance (d : Dimension LTMCTDimensionBase) (M : Type) : HasDim (WithDim d M) where d := d@[simp] lemma dim_apply (d : Dimension LTMCTDimensionBase) (M : Type) : dim (WithDim d M) = d := rfl

Inherited instances

instance {B : Type} (d : Dimension B) (M : Type) [Inhabited M] : Inhabited (WithDim d M) where default := ⟨default⟩instance {B : Type} (d : Dimension B) (M : Type) [Zero M] : Zero (WithDim d M) where zero := ⟨0⟩@[simp] lemma val_zero {B : Type} {d : Dimension B} {M : Type} [Zero M] : (0 : WithDim d M).val = 0 := rflinstance {B : Type} (d : Dimension B) (M : Type) [Add M] : Add (WithDim d M) where add m1 m2 := ⟨m1.val + m2.val⟩@[simp] lemma val_add {B : Type} {d : Dimension B} {M : Type} [Add M] (m1 m2 : WithDim d M) : (m1 + m2).val = m1.val + m2.val := rflinstance {B : Type} (d : Dimension B) (M : Type) [Neg M] : Neg (WithDim d M) where neg m := ⟨-m.val⟩@[simp] lemma val_neg {B : Type} {d : Dimension B} {M : Type} [Neg M] (m : WithDim d M) : (-m).val = -m.val := rflinstance {B : Type} (d : Dimension B) (M : Type) [Sub M] : Sub (WithDim d M) where sub m1 m2 := ⟨m1.val - m2.val⟩@[simp] lemma val_sub {B : Type} {d : Dimension B} {M : Type} [Sub M] (m1 m2 : WithDim d M) : (m1 - m2).val = m1.val - m2.val := rflinstance {B : Type} (d : Dimension B) (M : Type) [AddSemigroup M] : AddSemigroup (WithDim d M) where add_assoc m1 m2 m3 := B:Typed:Dimension BM:Typeinst✝:AddSemigroup Mm1:WithDim d Mm2:WithDim d Mm3:WithDim d M⊢ m1 + m2 + m3 = m1 + (m2 + m3) B:Typed:Dimension BM:Typeinst✝:AddSemigroup Mm1:WithDim d Mm2:WithDim d Mm3:WithDim d M⊢ (m1 + m2 + m3).val = (m1 + (m2 + m3)).val All goals completed! 🐙instance {B : Type} (d : Dimension B) (M : Type) [AddCommSemigroup M] : AddCommSemigroup (WithDim d M) where add_comm m1 m2 := B:Typed:Dimension BM:Typeinst✝:AddCommSemigroup Mm1:WithDim d Mm2:WithDim d M⊢ m1 + m2 = m2 + m1 B:Typed:Dimension BM:Typeinst✝:AddCommSemigroup Mm1:WithDim d Mm2:WithDim d M⊢ (m1 + m2).val = (m2 + m1).val All goals completed! 🐙instance {B : Type} (d : Dimension B) (M : Type) [AddMonoid M] : AddMonoid (WithDim d M) where zero_add m := B:Typed:Dimension BM:Typeinst✝:AddMonoid Mm:WithDim d M⊢ 0 + m = m B:Typed:Dimension BM:Typeinst✝:AddMonoid Mm:WithDim d M⊢ (0 + m).val = m.val All goals completed! 🐙 add_zero m := B:Typed:Dimension BM:Typeinst✝:AddMonoid Mm:WithDim d M⊢ m + 0 = m B:Typed:Dimension BM:Typeinst✝:AddMonoid Mm:WithDim d M⊢ (m + 0).val = m.val All goals completed! 🐙 nsmul := nsmulRecinstance {B : Type} (d : Dimension B) (M : Type) [AddCommMonoid M] : AddCommMonoid (WithDim d M) where add_comm m1 m2 := B:Typed:Dimension BM:Typeinst✝:AddCommMonoid Mm1:WithDim d Mm2:WithDim d M⊢ m1 + m2 = m2 + m1 B:Typed:Dimension BM:Typeinst✝:AddCommMonoid Mm1:WithDim d Mm2:WithDim d M⊢ (m1 + m2).val = (m2 + m1).val All goals completed! 🐙instance {B : Type} (d : Dimension B) (M : Type) [AddGroup M] : AddGroup (WithDim d M) where sub_eq_add_neg m1 m2 := B:Typed:Dimension BM:Typeinst✝:AddGroup Mm1:WithDim d Mm2:WithDim d M⊢ m1 - m2 = m1 + -m2 B:Typed:Dimension BM:Typeinst✝:AddGroup Mm1:WithDim d Mm2:WithDim d M⊢ (m1 - m2).val = (m1 + -m2).val All goals completed! 🐙 neg_add_cancel m := B:Typed:Dimension BM:Typeinst✝:AddGroup Mm:WithDim d M⊢ -m + m = 0 B:Typed:Dimension BM:Typeinst✝:AddGroup Mm:WithDim d M⊢ (-m + m).val = val 0 All goals completed! 🐙 zsmul := zsmulRecinstance {B : Type} (d : Dimension B) (M : Type) [AddCommGroup M] : AddCommGroup (WithDim d M) where add_comm m1 m2 := B:Typed:Dimension BM:Typeinst✝:AddCommGroup Mm1:WithDim d Mm2:WithDim d M⊢ m1 + m2 = m2 + m1 B:Typed:Dimension BM:Typeinst✝:AddCommGroup Mm1:WithDim d Mm2:WithDim d M⊢ (m1 + m2).val = (m2 + m1).val All goals completed! 🐙instance {B : Type} (d : Dimension B) (M : Type) [LE M] : LE (WithDim d M) where le m1 m2 := m1.val ≤ m2.val@[simp] lemma le_def {B : Type} {d : Dimension B} {M : Type} [LE M] (m1 m2 : WithDim d M) : m1 ≤ m2 ↔ m1.val ≤ m2.val := Iff.rflinstance {B : Type} (d : Dimension B) (M : Type) [LT M] : LT (WithDim d M) where lt m1 m2 := m1.val < m2.val@[simp] lemma lt_def {B : Type} {d : Dimension B} {M : Type} [LT M] (m1 m2 : WithDim d M) : m1 < m2 ↔ m1.val < m2.val := Iff.rflinstance {B : Type} (d : Dimension B) (M : Type) [Preorder M] : Preorder (WithDim d M) where le_refl m := B:Typed:Dimension BM:Typeinst✝:Preorder Mm:WithDim d M⊢ m ≤ m All goals completed! 🐙 le_trans m1 m2 m3 h12 h23 := B:Typed:Dimension BM:Typeinst✝:Preorder Mm1:WithDim d Mm2:WithDim d Mm3:WithDim d Mh12:m1 ≤ m2h23:m2 ≤ m3⊢ m1 ≤ m3 B:Typed:Dimension BM:Typeinst✝:Preorder Mm1:WithDim d Mm2:WithDim d Mm3:WithDim d Mh12:m1 ≤ m2h23:m2 ≤ m3⊢ m1.val ≤ m3.val All goals completed! 🐙 lt_iff_le_not_ge m1 m2 := B:Typed:Dimension BM:Typeinst✝:Preorder Mm1:WithDim d Mm2:WithDim d M⊢ m1 < m2 ↔ m1 ≤ m2 ∧ ¬m2 ≤ m1 B:Typed:Dimension BM:Typeinst✝:Preorder Mm1:WithDim d Mm2:WithDim d M⊢ m1.val < m2.val ↔ m1.val ≤ m2.val ∧ ¬m2.val ≤ m1.val All goals completed! 🐙instance {B : Type} (d : Dimension B) (M : Type) [PartialOrder M] : PartialOrder (WithDim d M) where le_antisymm m1 m2 h12 h21 := B:Typed:Dimension BM:Typeinst✝:PartialOrder Mm1:WithDim d Mm2:WithDim d Mh12:m1 ≤ m2h21:m2 ≤ m1⊢ m1 = m2 B:Typed:Dimension BM:Typeinst✝:PartialOrder Mm1:WithDim d Mm2:WithDim d Mh12:m1 ≤ m2h21:m2 ≤ m1⊢ m1.val = m2.val All goals completed! 🐙instance {B : Type} (d : Dimension B) (M : Type) [MulAction ℝ≥0 M] : MulAction ℝ≥0 (WithDim d M) where smul a m := ⟨a • m.val⟩ one_smul m := ext _ _ (one_smul ℝ≥0 m.val) mul_smul a b m := B:Typed:Dimension BM:Typeinst✝:MulAction ℝ≥0 Ma:ℝ≥0b:ℝ≥0m:WithDim d M⊢ (a * b) • m = a • b • m B:Typed:Dimension BM:Typeinst✝:MulAction ℝ≥0 Ma:ℝ≥0b:ℝ≥0m:WithDim d M⊢ ((a * b) • m).val = (a • b • m).val All goals completed! 🐙@[simp] lemma smul_val {B : Type} {d : Dimension B} {M : Type} [MulAction ℝ≥0 M] (a : ℝ≥0) (m : WithDim d M) : (a • m).val = a • m.val := rflinstance {B : Type} {d1 d2 : Dimension B} : HMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2) ℝ) where hMul m1 m2 := ⟨m1.val * m2.val⟩lemma withDim_hMul_val {B : Type} {d1 d2 : Dimension B} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) : (m1 * m2).val = m1.val * m2.val := rflAll goals completed! 🐙@[simp] lemma val_mul_eq_mul {B : Type} {d1 d2 : Dimension B} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) : m1.val * m2.val = (m1 * m2).val := B:Typed1:Dimension Bd2:Dimension Bm1:WithDim d1 ℝm2:WithDim d2 ℝ⊢ m1.val * m2.val = (m1 * m2).val All goals completed! 🐙B:Typed1:Dimension Bm1:WithDim d1 ℝ⊢ m1.val * m1.val = (m1 * m1).val All goals completed! 🐙d:Dimension LTMCTDimensionBaseM:Typeinst✝:MulAction ℝ≥0 Mu1:UnitChoicesu2:UnitChoicesm1:WithDim d Mm2:WithDim d M⊢ scaleUnit u1 u2 m1 = scaleUnit u1 u2 m2 ↔ m1.val = m2.val d:Dimension LTMCTDimensionBaseM:Typeinst✝:MulAction ℝ≥0 Mu1:UnitChoicesu2:UnitChoicesm1:WithDim d Mm2:WithDim d M⊢ m1 = m2 ↔ m1.val = m2.val All goals completed! 🐙lemma scaleUnit_val_eq_scaleUnit_val_of_dim_eq {d1 d2 : Dimension LTMCTDimensionBase} {M : Type} [MulAction ℝ≥0 M] {u1 u2 : UnitChoices} {m1 : WithDim d1 M} {m2 : WithDim d2 M} (h : d1 = d2 := by ext <;> {simp; try ring}) : (scaleUnit u1 u2 m1).val = (scaleUnit u1 u2 m2).val ↔ m1.val = m2.val := d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseM:Typeinst✝:MulAction ℝ≥0 Mu1:UnitChoicesu2:UnitChoicesm1:WithDim d1 Mm2:WithDim d2 Mh:d1 = d2⊢ (scaleUnit u1 u2 m1).val = (scaleUnit u1 u2 m2).val ↔ m1.val = m2.val d1:Dimension LTMCTDimensionBaseM:Typeinst✝:MulAction ℝ≥0 Mu1:UnitChoicesu2:UnitChoicesm1:WithDim d1 Mm2:WithDim d1 M⊢ (scaleUnit u1 u2 m1).val = (scaleUnit u1 u2 m2).val ↔ m1.val = m2.val All goals completed! 🐙lemma scaleUnit_val {d : Dimension LTMCTDimensionBase} (M : Type) [MulAction ℝ≥0 M] (u1 u2 : UnitChoices) (m1 : WithDim d M) : (scaleUnit u1 u2 m1).val = u1.dimScale u2 d • m1.val := rfl

Division

@[simp] lemma val_div_val {B : Type} {d1 d2 : Dimension B} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) : (m1.val / m2.val) = (m1 / m2).val := rfld1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBasem1:WithDim d1 ℝm2:WithDim d2 ℝu1:UnitChoicesu2:UnitChoices⊢ ↑((u1.dimScale u2) d1) / ↑((u1.dimScale u2) d2) * (m1.val / m2.val) = ↑((u1.dimScale u2) d1) * m1.val / (↑((u1.dimScale u2) d2) * m2.val) All goals completed! 🐙u1:UnitChoicesu2:UnitChoicesm:WithDim 1 ℝ⊢ (u1.dimScale u2) 1 • m.val = m.val All goals completed! 🐙

Casting

The casting from WithDim d M to WithDim d2 M when d = d2.

set_option linter.unusedVariables false in@[nolint unusedArguments] def cast {B : Type} {d d2 : Dimension B} {M : Type} (m : WithDim d M) (h : d = d2 := by ext <;> {simp; try ring}) : WithDim d2 M := ⟨m.val⟩
@[simp] lemma cast_refl {B : Type} {d : Dimension B} {M : Type} (m : WithDim d M) : cast m rfl = m := rfl@[simp] lemma cast_scaleUnit {d d2 : Dimension LTMCTDimensionBase} {M : Type} [MulAction ℝ≥0 M] (m : WithDim d M) (h : d = d2) (u1 u2 : UnitChoices) : cast (scaleUnit u1 u2 m) h = scaleUnit u1 u2 (cast m h) := d:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseM:Typeinst✝:MulAction ℝ≥0 Mm:WithDim d Mh:d = d2u1:UnitChoicesu2:UnitChoices⊢ (scaleUnit u1 u2 m).cast h = scaleUnit u1 u2 (m.cast h) d:Dimension LTMCTDimensionBaseM:Typeinst✝:MulAction ℝ≥0 Mm:WithDim d Mu1:UnitChoicesu2:UnitChoices⊢ (scaleUnit u1 u2 m).cast ⋯ = scaleUnit u1 u2 (m.cast ⋯) All goals completed! 🐙TODO "Induce further non-additive algebraic, additional order, and topological instances on `WithDim d M` from instances on `M`."