DefEq types

Stream: Is there code for X?

[Max Bobbin]

I've been on a year break from Lean and am returning to formalizing dimensional analysis and physical variables. I'm running into a problem where I have definitionally equal types (ie. I can show through a theorem that both types are the same) however I get a type error when I try to write a theorem about elements of the types.

import Mathlib.Tactic
universe u

class HasBaseLength (α : Type u) where
  [dec : DecidableEq α]
  length : α
attribute [instance] HasBaseLength.dec

def dimension (α : Type u) := α → ℚ

protected def dimension.mul {α} : dimension α → dimension α → dimension α
| a, b => fun i => a i + b i
protected def dimension.pow {α} : dimension α → ℚ → dimension α
| a, n => fun i => n * (a i)
instance {α} : Mul (dimension α) := ⟨dimension.mul⟩
instance {α} : Pow (dimension α) ℕ := ⟨fun d n => dimension.pow d n⟩


def dimension.length (α) [HasBaseLength α] : dimension α := Pi.single HasBaseLength.length 1
def dimension.area (α) [HasBaseLength α] := dimension.length α^2
def dimension.volume (α) [HasBaseLength α] := dimension.length α^3

structure measurement (V) {α : Type*} (dim : dimension α) where
(value : V)

def measurement.Mul {V1 V2 V3} [HMul V1 V2 V3] {α} {dim1 dim2 : dimension α} : measurement V1 dim1 → measurement V2 dim2 → measurement V3 (dim1*dim2)
| a,b => ⟨a.value*b.value⟩

instance {α : Type*} {V1 V2 V3} [HMul V1 V2 V3] {dim1 dim2: dimension α} :
  HMul (measurement V1 dim1) (measurement V2 dim2) (measurement V3 (dim1*dim2)) := ⟨measurement.Mul⟩

variable (β) [HasBaseLength β] (a : measurement ℝ (dimension.length β)) (b : measurement ℝ (dimension.area β)) (c : measurement ℝ (dimension.volume β))
#check a*b=c

I get an error in the check statement because c : measurement ℝ (dimension.volume β) and is expected to have type measurement ℝ (dimension.length β * dimension.area β) My first thought was to have an instance showing that measurement ℝ (dimension.volume β) = measurement ℝ (dimension.length β * dimension.area β) but that didn't fix the issue and would be annoying to do for every combination. My other thought was casting one variable but I ran into a problem with Coe because i don't have a type to satisfy outParams. Looking for any advice on this Type problem.

[Max Bobbin]

Let me know if the MWE doesn't work. I'm pretty sure it will work, but am pulling from multiple files.

[Edward van de Meent]

Instance synthesis cannot see through defs by default. Either make them abbrevs or mark them as @[reducible]

[Max Bobbin]

Replacing def with abbrev still gives the same problem. I also ran into a synthesization order issue if I tried defining multiplication like this:

class dimension.Eq {α} (dim1 dim1 : dimension α) where
(eq : dim1 = dim2)

def measurement.Mul {V1 V2 V3} [HMul V1 V2 V3] {α} {dim1 dim2 dim3 : dimension α} [dimension.Eq (dim1*dim2) dim3]: measurement V1 dim1 → measurement V2 dim2 → measurement V3 dim3
| a,b => ⟨a.value*b.value⟩

instance {α : Type*} {V1 V2 V3} [HMul V1 V2 V3] {dim1 dim2 dim3: dimension α} [dimension.Eq (dim1*dim2) dim3]:
  HMul (measurement V1 dim1) (measurement V2 dim2) (measurement V3 dim3) := ⟨measurement.Mul⟩

[Edward van de Meent]

ah, right, because at that point it still has to realise that dimension.lenght α * dimension.lenght α ^ 2 = dimension.lenght α ^ 3... you'd need to mark area,volume and pow as reducible for this, i think.

[Edward van de Meent]

unless then you still need mul_assoc...

[Mitchell Lee]

You are using the words "definitionally equal" incorrectly. It is not the case that measurement ℝ (dimension.volume β) is definitionally equal to measurement ℝ (dimension.length β * dimension.area β), because proving that they are equal requires performing some computation rather than merely unfolding definitions.

[Mitchell Lee]

Another user, wuyoli, ran into a similar issue when trying to formalize dimensional analysis in Lean (#new members > Help with simple proof). I think Lean's type system is not designed for something like this.

[Matt Diamond]

I think I found a way to do this

[Matt Diamond]

import Mathlib.Tactic
universe u

class HasBaseLength (α : Type u) where
  [dec : DecidableEq α]
  length : α
attribute [instance] HasBaseLength.dec

def dimension (α : Type u) := α → ℚ

protected def dimension.mul {α} : dimension α → dimension α → dimension α
| a, b => fun i => a i + b i
protected def dimension.pow {α} : dimension α → ℚ → dimension α
| a, n => fun i => n * (a i)
instance {α} : Mul (dimension α) := ⟨dimension.mul⟩
instance {α} : Pow (dimension α) ℕ := ⟨fun d n => dimension.pow d n⟩


def dimension.length (α) [HasBaseLength α] : dimension α := Pi.single HasBaseLength.length 1
def dimension.area (α) [HasBaseLength α] := dimension.length α^2
def dimension.volume (α) [HasBaseLength α] := dimension.length α^3

structure measurement (V) {α : Type*} (dim : dimension α) where
(value : V)

class DimProd (dim1 dim2 : dimension α) (dim3 : outParam (dimension α))

instance (β) [HasBaseLength β] : DimProd (dimension.length β) (dimension.area β) (dimension.volume β) where

def measurement.Mul {V1 V2 V3} [HMul V1 V2 V3] {α} {dim1 dim2 dim3 : dimension α} : measurement V1 dim1 → measurement V2 dim2 → measurement V3 dim3
| a,b => ⟨a.value*b.value⟩

instance {α : Type*} {V1 V2 V3} [HMul V1 V2 V3] {dim1 dim2 dim3: dimension α} [DimProd dim1 dim2 dim3] :
  HMul (measurement V1 dim1) (measurement V2 dim2) (measurement V3 dim3) := ⟨measurement.Mul⟩

variable (β) [HasBaseLength β] (a : measurement ℝ (dimension.length β)) (b : measurement ℝ (dimension.area β)) (c : measurement ℝ (dimension.volume β))
#check a*b=c

[Matt Diamond]

of course this requires that your notion of dimensional products is a finite list of combinations

[Matt Diamond]

actually never mind, this is very limited and doesn't really help (you would have to write out instances for length * length = area, length * area = volume, area * length = volume and it wouldn't scale past that)

[Yaël Dillies]

Every time someone wants to do dimensional analysis on Zulip, we tell them "Don't do that, or do it in a way that lets length + area make sense" (namely by using multivariate Laurent series with the base dimensions as indeterminates)