unit-of-measurement.lean

@[derive decidable_eq] structure dim := (L M T I Θ N J : int)

def dim.one := dim.mk 0 0 0 0 0 0 0
def L := { dim.one with L := 1 }
def M := { dim.one with M := 1 }
def T := { dim.one with T := 1 }
def I := { dim.one with I := 1 }
def Θ := { dim.one with Θ := 1 }
def N := { dim.one with N := 1 }
def J := { dim.one with J := 1 }

def dim.names := [ "L", "M", "T", "I", "Θ", "N", "J" ]
def dim.units := [ "m", "kg", "s", "A", "K", "mol", "cd" ]

def dim.power_string : ℤ × string → string
| ⟨0, _⟩ := ""
| ⟨1, s⟩ := s
| ⟨x, s⟩ := sformat! "{s}^{x}"

abbreviation dim.zero_power (pair : ℤ × string) : Prop := pair.1 ≠ 0

def dim.to_string (names : list string) : dim → string |
  ⟨m, kg, s, A, K, mol, cd⟩ :=
  let powers := [ m, kg, s, A, K, mol, cd ] in
  let non_zero := list.filter dim.zero_power (list.zip powers names) in
  string.intercalate " × " (dim.power_string <$> non_zero)

namespace dim
  instance : has_to_string dim := ⟨dim.to_string dim.names⟩
  instance : has_repr dim := ⟨dim.to_string dim.names⟩
end dim

def dim.mul : dim → dim → dim |
  ⟨m₁, kg₁, s₁, A₁, K₁, mol₁, cd₁⟩
  ⟨m₂, kg₂, s₂, A₂, K₂, mol₂, cd₂⟩ :=
  ⟨m₁ + m₂, kg₁ + kg₂, s₁ + s₂, A₁ + A₂, K₁ + K₂, mol₁ + mol₂, cd₁ + cd₂⟩

def dim.inv : dim → dim |
  ⟨m, kg, s, A, K, mol, cd⟩ :=
  ⟨-m, -kg, -s, -A, -K, -mol, -cd⟩

def dim.div (x y : dim) : dim := dim.mul x (dim.inv y)

instance : has_mul dim := ⟨dim.mul⟩
instance : has_div dim := ⟨dim.div⟩
instance : has_inv dim := ⟨dim.inv⟩
instance : has_one dim := ⟨dim.one⟩

structure rich (α : Type) (d : dim) := (val : α)

namespace rich
  variables {α : Type} [has_add α] [has_mul α] [has_div α] [has_to_string α] [has_one α]

  def new {d : dim} (x : α) : rich α d := ⟨d, x⟩

  def add {d : dim} (x y : rich α d) : rich α d :=
  ⟨d, x.val + y.val⟩

  def mul {d₁ d₂ : dim} (x : rich α d₁) (y : rich α d₂) : rich α (d₁ * d₂) :=
  ⟨d₁ * d₂, x.val * y.val⟩

  def div {d₁ d₂ : dim} (x : rich α d₁) (y : rich α d₂) : rich α (d₁ / d₂) :=
  ⟨d₁ / d₂, x.val / y.val⟩

  abbreviation can : α → rich α 1 := new

  def to_string {d : dim} (x : rich α d) :=
  if d ≠ 1 then sformat! "{x.val} {dim.to_string dim.units d}"
  else to_string x.val

  instance {d : dim} : has_add (rich α d) := ⟨add⟩
  instance {d : dim} : has_to_string (rich α d) := ⟨to_string⟩
  instance {d : dim} : has_repr (rich α d) := ⟨to_string⟩

  instance {d : dim} : has_one (rich α d) := ⟨rich.new 1⟩
end rich

infixr ` * ` := rich.mul
infixr ` / ` := rich.div

abbreviation nat' := rich nat

notation x ` s`:100 := rich.mk T x
notation x ` m`:100 := rich.mk L x
notation x ` kg`:100 := rich.mk M x
notation x ` t`:100 := rich.mk M (has_mul.mul 1000 x)

#eval 23 t + 356 kg -- 23356 kg
#eval 23356 kg -- 23356 kg

def v := L / T
notation x ` m/s`:100 := rich.mk v x

def a := v / T
notation x ` m/s²`:100 := rich.mk a x

def F := M * a
notation x ` newton`:100 := rich.mk F x

def acceleration := 5 m/s²
def mass := 3 kg
def force := mass * acceleration
example : force = 15 newton := by refl

-- def fail := mass + acceleration -- fails