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!

[Christian Tzurcanu]

I got time to define the identity element under addition for Quality and Measure. Also the identity element under multiplication - but that is trivial.

https://github.com/ctzurcanu/lean-measure/blob/main/LeanMeasure.lean

Practically I should be able to prove that :
(Measure , +, zero_measure) is an abelian group and also
(Measure, *, one_measure) is an abelian group
(Quality, +, zeroQ) is an abelian group and also
(Quality, *, oneQ) is an abelian group

I will see if I can learn enough Lean to perform those.

[Christian Tzurcanu]

If you find that your lib can benefit from that, let me know @Max Bobbin

[Christian Tzurcanu]

Returning to this:

I saw that the abelian group definition requires the result of the operation between an element and its inverse to be the identity element. But in the process if synthesizing the zero element (for addition), I change its type of Measure (or Quality). So the + produces the zero element just for that particular Quality. Does not conform to the Abelian Group definition. And that is even after I already forced this zero Quality in the Quality additions, and substractions.

Judging from the lack of answers to my previous messages I could guess that there is no use for having such a synthetic element. But I would love some confirmation from somebody in this field or who knows Lean proving better.

The question is: Is the existence of such an element (that is almost like identity, but not perfectly so) useful for proving (human-driven or automatic) ?

@Kevin Buzzard @Yury G. Kudryashov @Eric Wieser

[Eric Wieser]

The wording of your question is confusing me a little, but I think ultimately there are two ways to encode dimensions in Lean's dependent type theory:

• In the types, so that 1m + 1s or 1m = 1s is a type error
• Using docs#MonoidAlgebra (or something analogous), which allows 1m + 1s and is such that 0s = 0m = 0kg = ...

[Christian Tzurcanu]

Eric Wieser said:

The wording of your question is confusing me a little, but I think ultimately there are two ways to encode dimensions in Lean's dependent type theory:

• In the types, so that 1m + 1s or 1m = 1s is a type error
• Using docs#MonoidAlgebra (or something analogous), which allows 1m + 1s and is such that 0s = 0m = 0kg = ...

I could have used to show some code from my lib to be more precise, but I thought that you probably don't have the time to look at the sources, so I tried to say in English.. as well as I can

[Eric Wieser]

I think your lean code above is an incorrect implementation of this second idea, where the mistake arises from using a plain dictionary to store the dimensions. You need to also require that the dictionary contains no zero dimensions, and that a zero Quantity always has the empty dimension

[Christian Tzurcanu]

Eric Wieser said:

I think your lean code above is an incorrect implementation of this second idea, where the mistake arises from using a plain dictionary to store the dimensions. You need to also require that the dictionary contains no zero dimensions.

it does contain a zero-dim: it is the scalar

[Mario Carneiro]

Judging from the lack of answers to my previous messages

What previous messages? This seems to be your first post in this thread

[Mario Carneiro]

(If this is a continuation of another thread, you should cross link it here)

[Eric Wieser]

As I understand it, your code distinguishes {"m": 0} ($m^0$) from {} ($1$), but these are mathematically the same

[Christian Tzurcanu]

Mario Carneiro said:

Judging from the lack of answers to my previous messages

What previous messages? This seems to be your first post in this thread

my first post here was Jul 30. maybe I don't know how to use Zulip..

[Eric Wieser]

Mario, I think you must be running into a Zulip issue

[Mario Carneiro]

oh whoops

[Christian Tzurcanu]

Eric Wieser said:

As I understand it, your code distinguishes {"m": 0} ($m^0$) from {} ($1$), but these are mathematically the same

You may be right. I tried both variants: to have scalar as a Quality too. but I should probably stick with an empty dict for that

[Eric Wieser]

Thinking about it more, you're in much deeper trouble here; to Lean, {"m": 1, "s": -1} = {"s": -1, "m": 1} is false! (Equality of Batteries.HashMap is by insertion order, only == is order-independent)

[Christian Tzurcanu]

Eric Wieser said:

The wording of your question is confusing me a little, but I think ultimately there are two ways to encode dimensions in Lean's dependent type theory:

• In the types, so that 1m + 1s or 1m = 1s is a type error
• Using docs#MonoidAlgebra (or something analogous), which allows 1m + 1s and is such that 0s = 0m = 0kg = ...

Please note that I have read about Monoid Algebra and I was unable to understand how to apply.
https://leanprover.zulipchat.com/#narrow/stream/445230-Lean-for-Scientists-and-Engineers-2024/topic/Dims.20and.20Units.20for.20Physics/near/454471604

[Christian Tzurcanu]

Eric Wieser said:

Thinking about it more, you're in much deeper trouble here; to Lean, {"m": 1, "s": -1} = {"s": -1, "m": 1} is false! (Equality of Batteries.HashMap is by insertion order, only == is order-independent)

pff. that is news. I thought I had tested exactly for that case and reached my personal experience that it is not insert-dependent.

[Christian Tzurcanu]

then don't bother. Maybe tell me if there is a structure in Lean that acts like a Python dict so I can correct my code

[Eric Wieser]

You can use docs#Quotient to override the behavior of =

[Christian Tzurcanu]

Eric Wieser said:

You can use docs#Quotient to override the behavior of =

I parse this as: change the "=" for an extension of Batteries.Hashmap and use that extension and the docs for doing this should be in docs#Quotent

[Eric Wieser]

Usually docs#Foo is not making the claim "the docs for Foo will help you", but the much weaker claim of "I'm pretty sure writing Foo in your code would solve part of your problem, but the docs might not help much!"

[Christian Tzurcanu]

Eric Wieser said:

Usually docs#Foo is not making the claim "the docs for Foo will help you", but the much weaker claim of "I'm pretty sure writing Foo in your code would solve part of your problem, but the docs might not help much!"

Thank you for your time. Sorry I did not catch that problem myself. I thought I tested for it!

[Eric Wieser]

Indeed, docs#Quotient is pretty useless here, and docs#Quot (which is in the docstring of Quotient) leads to such a hugely long page that the doc browser struggles to jump to the right part of the page.

[Mario Carneiro]

docs#Quot doesn't work at all for me

[Mario Carneiro]

apparently the quotient constants (which are added by the magic init_quot command) are not supported by doc-gen

[Christian Tzurcanu]

Strange.. nobody else trying to find the Python dict equivalent in Lean? ChatGPT directed me to Batteries.HashMap.. it was not good advice

[Eric Wieser]

It was good advice (for the question you asked), the problem is that python only has == not Eq

[Christian Tzurcanu]

and there is not 1 lib of Lean that fully solved for dict as we imagine it?

[Mario Carneiro]

there is a reason HashMap does not take a quotient itself - if it did you wouldn't be able to print its elements or iterate over the keys/values

[Mario Carneiro]

If you want extensional equality of hashmaps you should be using == as eric suggests

[Eric Wieser]

Here's my toy implementation of a units library using DirectSum (which is really the same as MonoidAlgebra, but computable):

import Mathlib

set_option autoImplicit false

open scoped DirectSum

variable (R : Type*) [Ring R]

namespace Quantity

inductive BaseUnit
| meter
| second
deriving DecidableEq, Repr

abbrev PreUnit := Π₀ _ : BaseUnit, ℚ
abbrev Unit := Multiplicative PreUnit

instance : Coe BaseUnit Unit where coe u := .ofAdd <| .single u 1

abbrev Mixed (R : Type*) [AddCommMonoid R] := ⨁ u : PreUnit, R

end Quantity

def Quantity (R : Type*) (_u : Quantity.Unit) : Type _ := R

instance (u) : Ring (Quantity R u) := inferInstanceAs <| Ring R

instance (R : Type*) [Ring R] : Coe Quantity.Unit (Quantity.Mixed R) where
  coe u := DirectSum.of _ (Multiplicative.toAdd u) 1
instance (R : Type*) [Ring R] (u : Quantity.Unit) : CoeOut (Quantity R u) (Quantity.Mixed R) where
  coe q := DirectSum.of _ u q

open Quantity.BaseUnit

#eval show Quantity.Mixed ℤ from 2 + 3*↑meter + 0*second

(this raises that there is a parenthesization bug in docs#DFinsupp.instRepr)

[Eric Wieser]

The output is

fun₀ | fun₀ | Quantity.BaseUnit.meter => 1 => 3 | 0 => 2

which should really be

fun₀ | (fun₀ | Quantity.BaseUnit.meter => 1) => 3 | 0 => 2

which reads as 3m^1 + 2

[Christian Tzurcanu]

Mario Carneiro said:

If you want extensional equality of hashmaps you should be using == as eric suggests

I understand that: if I change all places in my code where I used "=" with "==" about HashMaps, the problem should be solved.

[Christian Tzurcanu]

Eric Wieser said:

Here's my toy implementation of a units library using DirectSum (which is really the same as MonoidAlgebra, but computable):

import Mathlib

set_option autoImplicit false

open scoped DirectSum

variable (R : Type*) [Ring R]

namespace Quantity

inductive BaseUnit
| meter
| second
deriving DecidableEq, Repr

abbrev PreUnit := Π₀ _ : BaseUnit, ℚ
abbrev Unit := Multiplicative PreUnit

instance : Coe BaseUnit Unit where coe u := .ofAdd <| .single u 1

abbrev Mixed (R : Type*) [AddCommMonoid R] := ⨁ u : PreUnit, R

end Quantity

def Quantity (R : Type*) (_u : Quantity.Unit) : Type _ := R

instance (u) : Ring (Quantity R u) := inferInstanceAs <| Ring R

instance (R : Type*) [Ring R] : Coe Quantity.Unit (Quantity.Mixed R) where
  coe u := DirectSum.of _ (Multiplicative.toAdd u) 1
instance (R : Type*) [Ring R] (u : Quantity.Unit) : CoeOut (Quantity R u) (Quantity.Mixed R) where
  coe q := DirectSum.of _ u q

open Quantity.BaseUnit

#eval show Quantity.Mixed ℤ from 2 + 3*↑meter + 0*second

(this raises that there is a parenthesization bug in docs#DFinsupp.instRepr)

all is well. But I can't understand your Leans source... I need more training.

[Eric Wieser]

Christian Tzurcanu said:

I understand that: if I change all places in my code where I used "=" with "==" about HashMaps, the problem should be solved.

The issue with that plan is that AddGroup is about = not ==

[Eric Wieser]

But I can't understand your Leans source... I need more training.

This is partly my fault for writing it quickly without documentation. Perhaps I should just publish a library out of this one day...

[Christian Tzurcanu]

Eric Wieser said:

Christian Tzurcanu said:

I understand that: if I change all places in my code where I used "=" with "==" about HashMaps, the problem should be solved.

The issue with that plan is that AddGroup is about = not ==

so I have to force a new type of = over the old one with a technique that is documented on a very long web page

[Christian Tzurcanu]

I will try my luck with ChatGPT tomorrow with this change form the old = to new = for HashMap. My eyes already hurt.. Thank you both for your time.

[Eric Wieser]

@Mario Carneiro, am I right in saying that RBMap has order-independent semantics?

[Mario Carneiro]

yes

[Mario Carneiro]

RBMap also doesn't have extensional = though, because = can observe the tree balance

[Eric Wieser]

Is there a proposition that states an RBMap is in normal form?

[Christian Tzurcanu]

Eric Wieser said:

Mario Carneiro, am I right in saying that RBMap has order-independent semantics?

just to be clear: I tried first with RBMap. I was unable to imagine how it can be used as dict.

[Mario Carneiro]

there is no such thing

[Mario Carneiro]

RBMaps are always balanced, but there are multiple ways to be balanced

[Mario Carneiro]

it does not enforce strict balance because that is too expensive to maintain as an invariant

[Mario Carneiro]

Christian Tzurcanu said:

Eric Wieser said:

Mario Carneiro, am I right in saying that RBMap has order-independent semantics?

just to be clear: I tried first with RBMap. I was unable to imagine how it can be used as dict.

RBMap and HashMap have almost identical API when used as a dict

[Mario Carneiro]

the main user-level difference is that HashMap expects the keys to be hashable while RBMap expects the keys to be ordered

[Eric Wieser]

Here's how to use Quotient to make hash maps order-invariant:

open Batteries (HashMap)

/-- Hash maps with extensional equality. -/
def Batteries.HashMapQuotient  {α β} [DecidableEq α] [Hashable α] [DecidableEq β] :=
  Quotient (Setoid.ker HashMap.find? : Setoid (HashMap α β))

[Christian Tzurcanu]

Mario Carneiro said:

Christian Tzurcanu said:

Eric Wieser said:

Mario Carneiro, am I right in saying that RBMap has order-independent semantics?

just to be clear: I tried first with RBMap. I was unable to imagine how it can be used as dict.

RBMap and HashMap have almost identical API when used as a dict

I was in such beginner stages of using Lean that I did not know even how to import RBMap! I tried some things but they were form Lean 3 docs..

[Eric Wieser]

(note that docs#Lean.RBMap and docs#Batteries.RBMap are different things)

[Christian Tzurcanu]

Eric Wieser said:

(note that docs#Lean.RBMap and docs#Batteries.RBMap are different things)

maybe I was confused between..

[Christian Tzurcanu]

Eric Wieser said:

Here's how to use Quotient to make hash maps order-invariant:

open Batteries (HashMap)

/-- Hash maps with extensional equality. -/
def Batteries.HashMapQuotient  {α β} [DecidableEq α] [Hashable α] [DecidableEq β] :=
  Quotient (Setoid.ker HashMap.find? : Setoid (HashMap α β))

I will do this tomorrow (read later today). I'm on Paris time.. 0:30 am here..

[Christian Tzurcanu]

Eric Wieser said:

Here's how to use Quotient to make hash maps order-invariant:

open Batteries (HashMap)

/-- Hash maps with extensional equality. -/
def Batteries.HashMapQuotient  {α β} [DecidableEq α] [Hashable α] [DecidableEq β] :=
  Quotient (Setoid.ker HashMap.find? : Setoid (HashMap α β))

using this and defining Decideable I was able to:

def accel1 := length/ time / time
def accel2 := oneQ / time / time * length

#eval QtoString accel1
#eval QtoString accel2

#eval accel1 == accel2 -- this is true
#eval accel1 = accel2 -- this is true too!

[Christian Tzurcanu]

also: I think I'm able to imagine correctly the measurable space (geometrically). So now I see that a zeroQ (identity element for + on Quality/Dimension) is not needed, is not elegant, worse: it produces bad effects: it forces existence of inverse of Quality under +. And that may change that nature of the Quality.
Not good: Quality is an essence, semantically. Therefore there needs to be at least one operation that does not change its value.

What I imagined was a cylinder:

Screenshot-2024-08-04-at-17.35.04.png

section at plane scalar = 0:

Screenshot-2024-08-04-at-17.36.05.png

[Christian Tzurcanu]

in the center is the scalar Quality and radiates qualities with and increasing and decreasing powers. So the inverses are on the diameter

[Christian Tzurcanu]

the central axis of the cylinder is \R

[Christian Tzurcanu]

I wonder what rational or even irrational powers of the Qualities may mean. They certainly have where to be placed in this space..

[Eric Wieser]

I don't really understand what you're using the word "quality" to mean, or what you intend to show with those diagrams. If you mean something like "compound base unit", then the visualization of meters and seconds is just the 2D plane, where $m^2$ is at (2, 0) and $m/s$ is at (1, -1), and multiplication of these base units is just addition in the plane. Fractional powers are just fractional points in this plane.

[Christian Tzurcanu]

Quality = Dimension.

The cylinder is the measurement: quality x quantity. the set of points that are at the intersection of the plane specific for a \R number is the quantity and the points where it intersects the axes of each quality define the combination that is the resultant Quality.

It is not important that ppl understand this imagination, but I used it to understand that + is not supposed to change the composed Quality, but * will (unless with a scalar).
So using a combination of those operations one can visit the whole length of the parallel axes.

[Christian Tzurcanu]

Imagining this I could see the usefulness of grouping dimensions as has_length for all those that have positive and negative values of the powers of L. @Max Bobbin

[Christian Tzurcanu]

Now I would like very much to understand and obtain all that was described by @Eric Wieser in his namespace Quantity with the eventual benefit that additional base units can be added.

[Christian Tzurcanu]

Eric Wieser said:

I don't really understand what you're using the word "quality" to mean, or what you intend to show with those diagrams. If you mean something like "compound base unit", then the visualization of meters and seconds is just the 2D plane, where $m^2$ is at (2, 0) and $m/s$ is at (1, -1), and multiplication of these base units is just addition in the plane. Fractional powers are just fractional points in this plane.

yes, I can see the space where these have room. I cannot imagine what $m^(1/2)$ or $$m^\PI$$ means, physically

[Mario Carneiro]

Units of $\sqrt{\mathrm{kg}}$ are not that unusual, e.g. https://en.wikipedia.org/wiki/Harmonic_oscillator#Simple_harmonic_oscillator

[Yakov Pechersky]

According to this answer, there are irrational dimensions https://physics.stackexchange.com/a/14268

[Mario Carneiro]

my favorite counterexample to formal unit analysis systems is $\ln(\mathrm{kg})$

[Eric Wieser]

Can you elaborate on that? It's not immediately obvious to me where the $\ln(\mathrm{kg})$ is hiding on that page

[Eric Wieser]

Is the issue somehow related to expanding $\ln{\frac{m_1}{m_2}}$ as $\ln{m_1} - \ln{m_2}$? Can you just not do that expansion?

[Eric Wieser]

This seems related to how you can't just average $n$ points in an affine space in the usual way, because you're not allowed to add them together without moving to a vector space and back.

[Tyler Josephson ⚛️]

Christian Tzurcanu said:

Judging from the lack of answers to my previous messages I could guess that there is no use for having such a synthetic element. But I would love some confirmation from somebody in this field or who knows Lean proving better.

Sorry for the slow response. I know this is related to my group’s work; I was at a conference all week, and Max Bobbin graduated and isn’t working much with Lean anymore. But we’re really interested in this!

It’s also been tough to respond when y’all can’t look at the latest version of dimensional analysis that we built. I’m still waiting for past group members to transfer the latest version of the code so I can make it public. The public version of our code is really old (still Lean 3; we have a Lean 4 version now).

[Tyler Josephson ⚛️]

Christian Tzurcanu said:

Strange.. nobody else trying to find the Python dict equivalent in Lean? ChatGPT directed me to Batteries.HashMap.. it was not good advice

I would be interested in this. Lots of scientists and engineers learn to code in Python, and having an idea of “this is how you translate a ____ in Python to Lean” would be nice. Dictionaries, classes, lists, tuples, etc. It could make for a nice cheat sheet. But maybe worth discussing in a separate thread.

[Josha Dekker]

Or a lean cheat sheet that also has proofs that those translations behave as you would expect them to…

[Tyler Josephson ⚛️]

Yakov Pechersky said:

According to this answer, there are irrational dimensions https://physics.stackexchange.com/a/14268

Oh! Interesting cases. I was only aware of cases that need rational powers, those seem to cover most cases. We built our dimension object assuming powers could be rational, but not irrational. Hmmm.

[Tyler Josephson ⚛️]

Mario Carneiro said:

my favorite counterexample to formal unit analysis systems is $\ln(\mathrm{kg})$

In the rocket equation, ln is applied to a unitless ratio of masses, so still okay. Formally, I don’t know of many “proper” uses of ln or exp in which the argument has dimensions.

Nonetheless, the docs for this unit system in Python points out a few useful cases, like when you want to plot a dimensional quantity on a log scale.
https://unyt.readthedocs.io/en/stable/usage.html#powers-logarithms-exponentials-and-trigonometric-functions

[Tyler Josephson ⚛️]

Here’s a real case of an equation with log applied to something with units:
https://en.m.wikipedia.org/wiki/Antoine_equation

It’s recognized as a semi-empirical relationship, so it’s not properly derivable from other equations. Furthermore, because it has log (p) (and not log (p/p_reference) or something like that, which would make it dimensionless), the constants A, B, and C are weirdly dependent on the units of P and T. In a normal equation, you can just say “k_B is 1.380649×10−23 J/K” and “the density of water at this temperature and pressure is 1 g/cm^3” - these other things in the equation can be expressed in any kinds of units and it will all be sensible once conversions are finished.

But in Antoine’s equation, you need to report your data like “A, B, and C are _____ when T is in K and p is in Pa” or “A, B, and C are ____ when T is in degrees C and p is in atm.” Ensuring these are correct is likely harder to do in a principled way.

[Eric Wieser]

It seems like this can be fixed by adding a $10^A$ to the LHS in a suitable way?

[Eric Wieser]

That is, this just seems like the sort of type-sloppy nonsense that would be rephrased before writing down in lean, and the rephrasing would make the problem go away

[Patrick Massot]

Tyler Josephson ⚛️ said:

Christian Tzurcanu said:

Strange.. nobody else trying to find the Python dict equivalent in Lean? ChatGPT directed me to Batteries.HashMap.. it was not good advice

I would be interested in this. Lots of scientists and engineers learn to code in Python, and having an idea of “this is how you translate a ____ in Python to Lean” would be nice. Dictionaries, classes, lists, tuples, etc. It could make for a nice cheat sheet. But maybe worth discussing in a separate thread.

This is tempting but also very dangerous. Those are extremely different programming languages, and we really want to train people in writing idiomatic Lean code, not python code in Lean. This is not specific to Lean and python, this apply to any pair of very different programming languages.

[Tyler Josephson ⚛️]

Eric Wieser said:

That is, this just seems like the sort of type-sloppy nonsense that would be rephrased before writing down in lean, and the rephrasing would make the problem go away

Right. It’s awkward. I think it’s better to just disallow this and enforce that ln and exp operate on dimensionless quantities, and maybe a flag to optionally allow some behavior along the convention that unyt uses and return no dimensions. Antoine’s Equation is the 1% exception among the 99% of cases in which we want type checking to enforce the rules.

[Christian Tzurcanu]

I knew only about the irrational length, area, and volume for fractals. Not sure if related, but it could be to $m$, $m^2$, $m^3$ if we refer to shoreline geography for example or porosity.
It would be fascinating for the library to link to such examples for other basic or combined dimensions.

[Christian Tzurcanu]

So I have an interest in making or using a library for measurement that has dimensional analysis as a side-offer, but where the user can add his own dimensions.
If I make it: I want it to be maximally flexible. That means exponents in $\R$. At least.

Now the new question: is there any case where exponents in $\Complex$ or other more complex type are needed?

[Christian Tzurcanu]

(Should I open another subject for this? How is the norm?)

[Mario Carneiro]

Eric Wieser said:

Is the issue somehow related to expanding $\ln{\frac{m_1}{m_2}}$ as $\ln{m_1} - \ln{m_2}$? Can you just not do that expansion?

Yes of course you can do so, but this is generally the case for any unitful quantity, you always need to combine it with other things to make it unitless before you can do anything mathematically nontrivial with it. But actually it is sensible to perform the separation $\ln{m_1} - \ln{m_2}$, since $m_2$ just plays the role of a reference mass and can be viewed in a similar spirit as the zero point of potential energy - the physics is invariant under shifting everything additively, so you can pick the zero point corresponding to some mass as your "unit", and when translating to another unit you need to perform a shift instead of a multiplication by a factor

[Mario Carneiro]

the point of a unit system is so that you can make sense of the individual components of physical equations without having to say that certain pieces can't be separated until they are unitless-ized

[Mario Carneiro]

Eric Wieser said:

This seems related to how you can't just average $n$ points in an affine space in the usual way, because you're not allowed to add them together without moving to a vector space and back.

Yes, affine spaces are another example where this shifting operation comes up. There is no designated zero point in real physical space, and picking your zero point has some of the characteristics of choosing a unit

[Mario Carneiro]

Somehow I sense Noether's theorem hiding behind these observations...

[Joachim Breitner]

In the rocket equation, though, $m_2$ isn't an arbitrary reference point that can be chosen without changing the physics, but something concrete about the rocket in question, is it?

[Christian Tzurcanu]

Patrick Massot said:

Tyler Josephson ⚛️ said:

Christian Tzurcanu said:

Strange.. nobody else trying to find the Python dict equivalent in Lean? ChatGPT directed me to Batteries.HashMap.. it was not good advice

I would be interested in this. Lots of scientists and engineers learn to code in Python, and having an idea of “this is how you translate a ____ in Python to Lean” would be nice. Dictionaries, classes, lists, tuples, etc. It could make for a nice cheat sheet. But maybe worth discussing in a separate thread.

This is tempting but also very dangerous. Those are extremely different programming languages, and we really want to train people in writing idiomatic Lean code, not python code in Lean. This is not specific to Lean and python, this apply to any pair of very different programming languages.

It is tempting for good reason: like in a proving system, in the mind of the programmer, he has to root new knowledge in the old. So we can preface the code with an explanation of the differences and have both benefits: of having a new paradigm and welcoming people who know of old ones.

[Tyler Josephson ⚛️]

I guess a cheat sheet isn’t the right idea, because one does not simply translate across these very different languages. But, in my class tomorrow, I am introducing recursion, and I’m showing examples in both Python and Lean. Part of the idea, is that Python programmers would use loops for lots of programming tasks, but these need to be recursive functions if we’re going to implement them in Lean and prove things like termination. So I’ll have for loop in Python, recursive function in Python, and recursive function in Lean. But all the context around this means it can work as a slide deck / long-form explanation, but a cheat sheet wouldn’t make sense. FPIL brings in other languages every once in a while, but definitely not as if there’s a one-to-one mapping between such things.

[Eric Wieser]

Arguably lean also uses for loops for some programming tasks, but the resulting function is currently tricky to prove things about (due to missing API lemmas around for loops)

[Notification Bot]

6 messages were moved from this topic to #new members > Ordering strings by Eric Wieser.