Defining a Type with multiple zeros

Stream: maths

[Max Bobbin]

I am working on defining a type for physical quantities in Lean. I have already finished defining a type for dimensional analysis, the code can be found here. We have a manuscript almost done on the dimensional analysis stuff. For physical quantities the idea was to define a physical quantity type as the product of a number and the dimension, ie:

def science_unit (α : Type*) := prod ℝ (dimension α)

Right now just using real numbers, but it will eventually be generalized to a vector space. For dimensional analysis, there is no zero because there is no identity element for addition. However, for physical quantities there is an identity element for addition, however there are multiple. That's because if we had 1 Length and added 0, 0 would have to have dimensions of Length too. That's because the addition of two physical quantities is only allowed if they have the same dimension.

protected noncomputable def add {α} : science_unit α → science_unit α → science_unit α
|a b := (a.fst + b.fst, a.snd + b.snd)

I wanted to get feedback on how we would go about defining zero, or even if it was possible to define a zero if a Type has multiple forms of zero.

[Yury G. Kudryashov]

You mean a.snd, not a.snd + b.snd

[Yury G. Kudryashov]

Do you want add to take a proof of a.snd = b.snd as an argument, or define it for all science_units and ask for a.snd = b.snd in proofs of properties?

[Yury G. Kudryashov]

In the first case you're sure that one can't get 0 m + 1 s by accident.

[Yury G. Kudryashov]

Another approach is to allow such sums and deal with dimension α →₀ ℝ instead.

[Yury G. Kudryashov]

(or, if you have a group structure on dimensions, then monoid_algebra ℝ (dimension α))

[Yury G. Kudryashov]

In this case you allow expressions like 0 m + 1 s

[Yury G. Kudryashov]

Unfortunately, the product type doesn't have a vector space (or even an additive group) structure.

[Yury G. Kudryashov]

(and probably you want to talk about (10 m + 20 m) / (30 s) ^ 2)

[Yury G. Kudryashov]

Are there projects that formalize computations with dimensions in Coq, Isabelle, etc?

[Yury G. Kudryashov]

If yes, what choices did they make?

[Yury G. Kudryashov]

BTW, do you want to allow 1 cm + 3 m or 5 in + 3 cm?

[Yury G. Kudryashov]

Or (1 cm).to_dim in?

[Max Bobbin]

Yury G. Kudryashov said:

You mean a.snd, not a.snd + b.snd

We defined addition already in dimensional analysis using classical choice such that it only allows to dimensions to be added if they are like dimensions. So you can have 1 m + 1 s but it won't simplify.

protected noncomputable def add {α}: dimension α → dimension α → dimension α :=
classical.epsilon $ λ f, ∀ a b, a = b → f a b = a

[Max Bobbin]

Yury G. Kudryashov said:

(or, if you have a group structure on dimensions, then monoid_algebra ℝ (dimension α))

We have already defined the multiplicative comm_group for dimensions, but no groups for addition because dimensions don't have a zero

[Max Bobbin]

Yury G. Kudryashov said:

Are there projects that formalize computations with dimensions in Coq, Isabelle, etc?

not from what I have seen, but I could have missed it

[Yury G. Kudryashov]

If you want to allow expressions like 1 m + 1 s, then I recommend using docs#monoid_algebra.

[Yury G. Kudryashov]

It explicitly allows such expressions without asking for addition on dimensions.

[Yury G. Kudryashov]

Then you can define division that makes sense only if the denominator is a non-zero single

[Max Bobbin]

Yury G. Kudryashov said:

BTW, do you want to allow 1 cm + 3 m or 5 in + 3 cm?

We want to allow this, but the addition won't simplify unless you convert the units. My idea of defining these units was:

def meter (α) [has_length α] : science_unit α := (1, dimension.length α)
noncomputable def centimeter (α) [has_length α] := 100*(meter α)
def length_meter (α) [has_length α] (value : ℝ) := value*(meter α)

Although this is the current idea, I'm not happy with it because it requires us to agree that the base SI units are the reference points. Could possibly get around this with the class strucutre

[Max Bobbin]

Yury G. Kudryashov said:

If you want to allow expressions like 1 m + 1 s, then I recommend using docs#monoid_algebra.

Let me look at the monoid_algebra. I'm not familiar with it. What is the flaw with the current way if the addition for dimensions is already defined since the addition of the dimensions checks to make sure the units are compatible to add?

[Jireh Loreaux]

Max, you definitely want docs#monoid_algebra.

[Max Bobbin]

Ok, let me play around with some stuff and see how it works. Thank you!

[Max Bobbin]

Do you have any recommendations for resources to learn about monoid algebra and how I would apply it here?

[Jireh Loreaux]

You would use monoid_algebra ℝ (dimension α). This is a synonym for dimension α →₀ ℝ, the collection of finitely supported functions on dimension α. You should think of these as finite formal sums of scalar multiples of dimensions. (e.g., like 2 d + π d', where d d' : dimension α). This structure forms an ℝ-algebra. The multiplication is defined in the way you want (as a convolution using the comm_group structure you have on dimensions).

[Jireh Loreaux]

So, suppose d₁ d₂ d₃ d₄ : dimension α, r₁ r₂ r₃ r₃ : ℝ and r₁ d₁ + r₂ d₂ and r₃ d₃ + r₄ d₄ : monoid_algebra ℝ (dimension α) (these last two are not valid syntax), then

(r₁ d₁ + r₂ d₂) * (r₃ d₃ + r₄ d₄) = (r₁ * r₃) (d₁ * d₃) + (r₁ * r₄) (d₁ * d₄) + (r₂ * r₃) (d₂ * d₃) + (r₂ * r₄) (d₂ * d₄)

And, supposing for the sake of example that d₁ * d₃ = d₂ * d₄ and d₁ * d₄ = d₂ * d₃, then the above is equal to: (r₁ * r₃ + r₂ * r₄) (d₁ * d₃) + (r₁ * r₄ + r₂ * r₃) (d₁ * d₄)

[Jireh Loreaux]

The classic example of a monoid_algebra is the group ring of a group G (which is monoid_algebra ℤ G)

[Eric Wieser]

Max Bobbin said:

Yury G. Kudryashov said:

If you want to allow expressions like 1 m + 1 s, then I recommend using docs#monoid_algebra.

Let me look at the monoid_algebra. I'm not familiar with it.

@Max Bobbin, can you confirm whether you actually do want to allow 1 m + 1 s?

[Jireh Loreaux]

(If not then (d : dimension α) should be a parameter to science_unit, and then science_unit is just a fancy type synonym for ℝ and it will be hard to combine units)

[Kevin Buzzard]

That weird auxiliary sigma type which we use in grading theory has lots of zeros

[Max Bobbin]

Eric Wieser said:

Max Bobbin said:

Yury G. Kudryashov said:

If you want to allow expressions like 1 m + 1 s, then I recommend using docs#monoid_algebra.

Let me look at the monoid_algebra. I'm not familiar with it.

Max Bobbin, can you confirm whether you actually do want to allow 1 m + 1 s?

We don't want 1 m + 1 s to be a valid form, but I was thinking we would have to allow it to at least be possible to write so we can write complex equations like 1 m / 1 s + 1 m/s The second equation is a valid equation to reduce to 2 m/s where as 1 m + 1 s can't be reduced. Not sure if that answers the question though, I may be misunderstanding what you are asking.

[Yury G. Kudryashov]

Another way to do it is to use Lean 4 docs4#HMul and docs4#HAdd

[Yury G. Kudryashov]

You can say that ScienceUnit (d : Dimension α) := ℝ, then define AddCommGroup instance for each ScienceUnit d and HMul instances for ScienceUnit d1 -> ScienceUnit d2 -> ScienceUnit (d1 * d2).

[Yury G. Kudryashov]

This way you will be able to write a + b only if a and b have definitionally equal dimensions.

[Yury G. Kudryashov]

(so, you need computable dimensions)

[Jireh Loreaux]

I think requiring defeq dimensions would be miserable. However, using monoid_algebra with an is_valid_form predicate saying that an element is equal to some finsupp.single would make sense.

[Jireh Loreaux]

That way you avoid computability requirements.

[Yury G. Kudryashov]

As you can see, you can get at least n + 1 opinions from n experienced users. ;-)

[Jireh Loreaux]

1 m / 1 s + 1 m/s is exactly the kind of thing you could do with monoid_algebra (or more precisely, 1 m * 1 s⁻¹ + 1 (m * s⁻¹)) and have it make sense easily. Admittedly, Yury's heterogeneous suggestion should also work, but I would be concerned you would run into unification headaches (maybe that's an unfounded concern).

[Max Bobbin]

I see, I'll work on implementing this. The other thing I've been mulling over is scale. I'm curious to see what others think, but my guess is using monoid_algebra we could define meter := monoid_algebra 1 dimension.length and then centimeter := meter/100. I worry that this definition is limiting, but I could be wrong.

[Yury G. Kudryashov]

You can define centimeter := 100⁻¹ • meter

[Max Bobbin]

Yury G. Kudryashov said:

You can define centimeter := 100⁻¹ • meter

What I meant was, I think there should be a better way then hoping that everyone agrees that the reference unit for length is 1 meter and everything is defined off the meter. The worry is someone comes along and defines the foot and they define it as 1, then you have 1 meter = 1 foot. Wanted to know if people had thoughts on this if its avoidable

[Kevin Buzzard]

You can either (a) use nonnegative reals and label your axes with the unit being used (meter, foot,...), (b) use no labelling and make your axes homogeneous spaces (so there is no "1" but you can still add, and multiply by a natural) or (c) use the nonnegative reals, not label your axes, and then have the ambiguity.

[Mario Carneiro]

Just call the type structure Length := (meters : Real), now if someone does the same definition for feet there is a clash

[Max Bobbin]

What do you mean by labeling your axes? The second option sounds like what I could be looking for, but I'm not familiar with homogeneous spaces

[Mario Carneiro]

the idea being that when you define def meter : Length := { meters := 1 }, in order to get unit confusion you would need to also define def foot : Length := { meters := 1 } which is obviously suspicious

[Mario Carneiro]

This is basically the argument for newtypes in the setting of lean

[Yury G. Kudryashov]

@Mario Carneiro This doesn't help with 1 m / 1 s

[Kevin Buzzard]

Max Bobbin said:

What do you mean by labeling your axes? The second option sounds like what I could be looking for, but I'm not familiar with homogeneous spaces

Labeling your axes: I mean what Mario is suggesting, with the constructor names saying which units you'er using. The homogeneous space idea: I'm suggesting not using the real numbers but a 1-dimensional vector space with no fixed choice of basis. This would be the "correct" abstract unitless way to do it. So you just have some 1-d space V and then a non-zero element of V represents a measurement, and given two nonzero elements $v,w$ of V there's a unique real number $r$ such that $rv=w$, but it doesn't make sense to say "v=1" or "v=37" or anything, until you choose the unit, i.e. pick a basis. The moment you pick a basis $e$ for $V$ (e.g. 1 metre or 1 foot) then every $v\in V$ is of the form $re$ for $r$ a real number and now you can call $v$ "r metres" or "r feet" or whatever, although of course the value of $r$ changes depending on which basis you pick.

[Eric Wieser]

Max Bobbin said:

I have already finished defining a type for dimensional analysis, the code can be found here.

This code looks a bit weird to me:

class has_time (α : Type u) :=
[dec : decidable_eq α]
(time [] : α)
(h : [time].nodup)

What was your intention with [time].nodup? [x].nodup is always true, docs#list.nodup_singleton

[Yury G. Kudryashov]

@Kevin Buzzard How do you suggest to implement a 1-dimensional vector space with no fixed choice of basis?

[Yury G. Kudryashov]

What is the type definition?

[Mario Carneiro]

Yury G. Kudryashov said:

Mario Carneiro This doesn't help with 1 m / 1 s

What I described was just the 1D space for lengths. If you want to have all your units in a pot you need some monoid_algebra thing

[Eric Wieser]

The "all the units in a pot" thing feels like the wrong design to me

[Mario Carneiro]

but you can build that on top of Length as one of the coordinates

[Eric Wieser]

If you're working in any real physical problem all your dimensions are known down to constructors anyway, so you have no defeq problems

[Mario Carneiro]

you might have an n-dimensional problem?

[Mario Carneiro]

granted that's probably not too common in physics, unless you are talking about e.g. the lagrangian in n-dimensional phase space

[Eric Wieser]

These are dimensions in the sense of metrology not space

[Eric Wieser]

Ah, I guess your lagrangian remark covers that

[Eric Wieser]

I think it's rare enough that dealing with a dimension.cast of some form very rarely is much less bad than having to constantly persuade lean you haven't mixed incompatible dimensions

[Eric Wieser]

I'd probably go for something like

class has_time (α : Type u) := (time [] : α)
class has_length (α : Type u) := (length [] : α)
class has_mass (α : Type u) := (mass [] : α)

@[reducible] def dimension (α : Type u) : Type := α → multiplicative ℚ
@[reducible] def dimension.of {α : Type u} (a : α) : dimension α := pi.single a (multiplicative.of_add 1)

def length (α) [has_length α] [decidable_eq α] : dimension α := dimension.of $ has_length.length α
def time (α) [has_time α] [decidable_eq α] : dimension α := dimension.of $ has_time.time α
def mass (α) [has_mass α] [decidable_eq α] : dimension α := dimension.of $ has_mass.mass α

@[nolint unused_arguments]
structure measurement (V) {α : Type*} (dim : α) :=of :: (value : V)

[Eric Wieser]

And then use it as

@[derive decidable_eq]
inductive system1
| second | meter

instance : has_time system1 := {  time := system1.second }
instance : has_length system1 := { length := system1.meters }

-- `measurement real (time system1)` is a real-valued duration

[Kevin Buzzard]

@Yury G. Kudryashov just ask findim V = 1 (or whatever the nat version of dimension is called)

[Yury G. Kudryashov]

I meant "how to define types", not "how to define a typeclass".

[Yury G. Kudryashov]

BTW, not a formalization but a good C++ library for units: https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.html

[Max Bobbin]

Eric Wieser said:

I'd probably go for something like

class has_time (α : Type u) := (time [] : α)
class has_length (α : Type u) := (length [] : α)
class has_mass (α : Type u) := (mass [] : α)

@[reducible] def dimension (α : Type u) : Type := α → multiplicative ℚ
@[reducible] def dimension.of {α : Type u} (a : α) : dimension α := pi.single a (multiplicative.of_add 1)

def length (α) [has_length α] [decidable_eq α] : dimension α := dimension.of $ has_length.length α
def time (α) [has_time α] [decidable_eq α] : dimension α := dimension.of $ has_time.time α
def mass (α) [has_mass α] [decidable_eq α] : dimension α := dimension.of $ has_mass.mass α

@[nolint unused_arguments]
structure measurement (V) {α : Type*} (dim : α) :=of :: (value : V)

I remember being recommended something like this in the past, but I couldn't find information that explained what multiplicative was. Could someone explain how multiplicative works?

[Max Bobbin]

I guess my big confusion is how multiplicative and additive structures relate.

[Max Bobbin]

I notice that when I use this definition: @[reducible] def dimension (α : Type u) := multiplicative (α → ℚ) The abelian group comes automatically, however, addition doesn't come (as to be expected). If I do .to_additive does this convert multiplication operations to addition? My guess was the .to_additive makes the dimensions act like we were manipulating a vector of exponent values, which are done under the operations of addition. If so, how does this work with the need to define the addition of dimensions to be idempotent? My other concern with this way is I'm not sure if the exponents are being added correctly. While I can say area := length^2 I want the underlying code to have an area of 2 when indexed by the Length base dimension class. This is important when we try to implement the Buckingham pi theorem.

[Max Bobbin]

Kevin Buzzard said:

Max Bobbin said:

What do you mean by labeling your axes? The second option sounds like what I could be looking for, but I'm not familiar with homogeneous spaces

Labeling your axes: I mean what Mario is suggesting, with the constructor names saying which units you'er using. The homogeneous space idea: I'm suggesting not using the real numbers but a 1-dimensional vector space with no fixed choice of basis. This would be the "correct" abstract unitless way to do it. So you just have some 1-d space V and then a non-zero element of V represents a measurement, and given two nonzero elements $v,w$ of V there's a unique real number $r$ such that $rv=w$, but it doesn't make sense to say "v=1" or "v=37" or anything, until you choose the unit, i.e. pick a basis. The moment you pick a basis $e$ for $V$ (e.g. 1 metre or 1 foot) then every $v\in V$ is of the form $re$ for $r$ a real number and now you can call $v$ "r metres" or "r feet" or whatever, although of course the value of $r$ changes depending on which basis you pick.

Unless I'm misunderstanding, the only problem I have with implementing this is I can't make dimensions into a module because they don't form an add_comm_monoid. The exponents of dimensions form one, I believe.

[Max Bobbin]

or wait, the vector space isn't over the dimensions, is it?

[Yury G. Kudryashov]

multiplicative G is a type synonym for G; for each additive structure on G (has_add, add_comm_monoid etc), it defines the corresponding multiplicative structure which is mathematically the same structure with different notation.

[Eric Wieser]

The abelian group comes automatically, however, addition doesn't come (as to be expected).

I'd go as far as saying that you don't want the additive structure in the first place. Leave that to monoid_algebra to generate if you really want it.

[Eric Wieser]

If so, how does this work with the need to define the addition of dimensions to be idempotent?

If you replace this with "addition of (mixed) measurements", then monoid_algebra handles this for you; 1 * of R meters + 2 * of R meters = 3 * of R meters

[Eric Wieser]

If you restrict yourself to well-typed measurements then the question does't even make sense

[Eric Wieser]

My other concern with this way is I'm not sure if the exponents are being added correctly.

Write a theorem to prove that they are!