Dimensional analysis

Stream: general

[Alfredo Moreira-Rosa]

Two weeks ago i started implementing a dimensional analysis library.
It's now starting to look good so i'll publish the full source code soon. I know some people where trying their own version, but i think this one is the most complete and extensible to date.

image.png

i'll not try to make merged into PhysLean because a unit system can be of help in other domains than physics (trading systems for example)

[Alfredo Moreira-Rosa]

Defining a unit system :
image.png
And defining quantities on this system of units :
image.png

[Thomas Murrills]

Ooh, intriguing! :) I’ve got a couple of questions, which will probably be answered by the source code:

1. How is e.g. Hz related to seconds above? That is, seeing as they’re defined independently, what makes one the inverse of the other? (Is one meant to use defineDerivedUnit?)
2. Can you represent dimensionful quantities without insisting on specific units (e.g. for stating a physical law)?
3. How do you handle transitioning to e.g. natural units with $c = 1$?
4. How do you manage to transport lemmas/calculations about numbers to this setting? (One thing I’ve considered is having opaque definitions to let us simply work in numbers + statements about factors, but it gets tricky to link that to a type signature that is calculationally convenient yet prevents shenanigans!)

[Alfredo Moreira-Rosa]

1. Hz is exactly 1/s , if you use defineSI, the conversion to the SI system is implicit by default. but in this setup, if you want to add two quantities , one in Hz and one in 1/s , you need to use the conversion system to mark you know what you are doing.
2. Yes you can, you just reason at dimension level instead of units level. units and dimensions form an abstract hierarchy and you can work in both.
3. the system is ready for that, (i took inspiration from mp_units library in c++) , i'll define two systems, a natural one and a SI one.
4. Not sure i understand the question. But i have taken a look at Terrence Tao implementation, and i can plug my system into his and i think this should handle Formal abtract proofs on it.

[Thomas Murrills]

Nice, looking forward to seeing how everything shakes out! :smile:

(Basically, for 4, I’m noting that we have a ton of existing infrastructure for dealing with number systems—ideally, we have a way to apply all that to dimensionful quantities out of the box, without having to duplicate and dimensionalize all of our lemmas and tactics.)

[Alfredo Moreira-Rosa]

For the point 2, here an exemple of abstract statement independent of units, all working on Dimension level:
image.png

[Alfredo Moreira-Rosa]

And obviously wrong statements are catched by the type checked that does dimensional analysis for us :
image.png

[Eric Wieser]

If you haven't already found it, PhysLean has quite a nice HasDimension predicate that is expressed in quite an abstract way.

[Alfredo Moreira-Rosa]

Yes but i don't think i can use it. Because i don't have a fixed set of Dimensions like PhysLean.
But maybe the ideas can be backported to my library. I don't know.
Maybe my framework will only be of value for engineers and not theorist.

[Alfredo Moreira-Rosa]

I did some cleanup, and code is available here :
https://github.com/ecyrbe/lean-units

Obviously more work to come to improve the formal part that is really empty for now

[Joseph Tooby-Smith]

ecyrbe said:

Yes but i don't think i can use it. Because i don't have a fixed set of Dimensions like PhysLean.
But maybe the ideas can be backported to my library. I don't know.
Maybe my framework will only be of value for engineers and not theorist.

I should say - I would be extremely glad if the implementation in PhysLean could be made extensible like your implementation @ecyrbe . In particular, the difficulty would indeed be making HasDimension work with a not-fixed set of dimensions. One thing that would for sure need to be done to make this happen is to replace e.g. TimeUnit, MassUnit with some more general Unit or something similar.
(An advantage of working with HasDimension in PhysLean is that it is very easy to prove results about dimensions of e.g. vectors, tensors etc, as well as the dimensions of derivatives - as is done in PhysLean)

[Alfredo Moreira-Rosa]

So question 1 from @Thomas Murrills made me realise that defining derived units on dimensions was confusing.
So i redesigned it to be based on Base SI units. And it makes more sence like that. Only base units should be a choice of unit .

-- base SI units
abbrev meter := defineUnit "m" Dimension.Length
abbrev second := defineUnit "s" Dimension.Time
abbrev kilogram := defineUnit "kg" Dimension.Mass
abbrev ampere := defineUnit "A" Dimension.Current
abbrev kelvin := defineUnit "K" Dimension.Temperature
abbrev mole := defineUnit "mol" Dimension.AmountOfSubstance
abbrev candela := defineUnit "cd" Dimension.LuminousIntensity
abbrev steradian := defineUnit "sr" Dimension.dimensionless

-- derived SI units
abbrev hertz := defineDerivedUnit "Hz" (-second)
abbrev newton := defineDerivedUnit "N" (kilogram + meter - 2•second)
abbrev pascal := defineDerivedUnit "Pa" (newton - 2•meter)
abbrev joule := defineDerivedUnit "J" (newton + meter)
abbrev watt := defineDerivedUnit "W" (joule - second)
abbrev coulomb := defineDerivedUnit "C" (ampere + second)
abbrev volt := defineDerivedUnit "V" (watt - ampere)
abbrev ohm := defineDerivedUnit "Ω" (volt - ampere)
abbrev farad := defineDerivedUnit "F" (coulomb - volt)
abbrev weber := defineDerivedUnit "Wb" (volt + second)
abbrev tesla := defineDerivedUnit "T" (weber - 2•meter)
abbrev henry := defineDerivedUnit "H" (ohm + second)
abbrev lumen := defineDerivedUnit "lm" (candela + steradian)
abbrev lux := defineDerivedUnit "lx" (lumen - 2•meter)
abbrev becquerel := defineDerivedUnit "Bq" (-second)
abbrev gray := defineDerivedUnit "Gy" (joule - kilogram)
abbrev sievert := defineDerivedUnit "Sv" (joule - kilogram)
abbrev katal := defineDerivedUnit "kat" (mole + second)
abbrev celsius := defineDerivedUnit "°C" kelvin (Conversion.translate (273.15))

[Alok Singh]

ecyrbe said:

So question 1 from Thomas Murrills made me realise that defining derived units on dimensions was confusing.
So i redesigned it to be based on Base SI units. And it makes more sence like that. Only base units should be a choice of unit .

-- base SI units
abbrev meter := defineUnit "m" Dimension.Length
abbrev second := defineUnit "s" Dimension.Time
abbrev kilogram := defineUnit "kg" Dimension.Mass
abbrev ampere := defineUnit "A" Dimension.Current
abbrev kelvin := defineUnit "K" Dimension.Temperature
abbrev mole := defineUnit "mol" Dimension.AmountOfSubstance
abbrev candela := defineUnit "cd" Dimension.LuminousIntensity
abbrev steradian := defineUnit "sr" Dimension.dimensionless

-- derived SI units
abbrev hertz := defineDerivedUnit "Hz" (-second)
abbrev newton := defineDerivedUnit "N" (kilogram + meter - 2•second)
abbrev pascal := defineDerivedUnit "Pa" (newton - 2•meter)
abbrev joule := defineDerivedUnit "J" (newton + meter)
abbrev watt := defineDerivedUnit "W" (joule - second)
abbrev coulomb := defineDerivedUnit "C" (ampere + second)
abbrev volt := defineDerivedUnit "V" (watt - ampere)
abbrev ohm := defineDerivedUnit "Ω" (volt - ampere)
abbrev farad := defineDerivedUnit "F" (coulomb - volt)
abbrev weber := defineDerivedUnit "Wb" (volt + second)
abbrev tesla := defineDerivedUnit "T" (weber - 2•meter)
abbrev henry := defineDerivedUnit "H" (ohm + second)
abbrev lumen := defineDerivedUnit "lm" (candela + steradian)
abbrev lux := defineDerivedUnit "lx" (lumen - 2•meter)
abbrev becquerel := defineDerivedUnit "Bq" (-second)
abbrev gray := defineDerivedUnit "Gy" (joule - kilogram)
abbrev sievert := defineDerivedUnit "Sv" (joule - kilogram)
abbrev katal := defineDerivedUnit "kat" (mole + second)
abbrev celsius := defineDerivedUnit "°C" kelvin (Conversion.translate (273.15))

Why not use the inversion symbol instead of negation for Hz ? Your operator overloading is confusing to me

[Alfredo Moreira-Rosa]

I needed the operations on dimensional analysis to be on Addition to have a AddCommGroup.
This allows to have automatic casting using (by module).

But you are right that i can also define the multiplicative ones as an alias for the additive ones.
So i just pushed it at the moment. Now it looks like this :

-- base SI units
abbrev meter := defineUnit "m" Dimension.Length
abbrev second := defineUnit "s" Dimension.Time
abbrev kilogram := defineUnit "kg" Dimension.Mass
abbrev ampere := defineUnit "A" Dimension.Current
abbrev kelvin := defineUnit "K" Dimension.Temperature
abbrev mole := defineUnit "mol" Dimension.AmountOfSubstance
abbrev candela := defineUnit "cd" Dimension.LuminousIntensity
abbrev steradian := defineUnit "sr" Dimension.dimensionless

-- derived SI units
abbrev hertz := defineDerivedUnit "Hz" (second⁻¹)
abbrev newton := defineDerivedUnit "N" (kilogram * meter / second^2)
abbrev pascal := defineDerivedUnit "Pa" (newton / meter^2)
abbrev joule := defineDerivedUnit "J" (newton * meter)
abbrev watt := defineDerivedUnit "W" (joule / second)
abbrev coulomb := defineDerivedUnit "C" (ampere * second)
abbrev volt := defineDerivedUnit "V" (watt / ampere)
abbrev ohm := defineDerivedUnit "Ω" (volt / ampere)
abbrev farad := defineDerivedUnit "F" (coulomb / volt)
abbrev weber := defineDerivedUnit "Wb" (volt * second)
abbrev tesla := defineDerivedUnit "T" (weber / meter^2)
abbrev henry := defineDerivedUnit "H" (ohm * second)
abbrev lumen := defineDerivedUnit "lm" (candela * steradian)
abbrev lux := defineDerivedUnit "lx" (lumen / meter^2)
abbrev becquerel := defineDerivedUnit "Bq" (second⁻¹)
abbrev gray := defineDerivedUnit "Gy" (joule / kilogram)
abbrev sievert := defineDerivedUnit "Sv" (joule / kilogram)
abbrev katal := defineDerivedUnit "kat" (mole * second)
abbrev celsius := defineDerivedUnit "°C" kelvin (Conversion.translate (273.15))

Thanks for the feeback.

[Alfredo Moreira-Rosa]

And to clarify, the additive operations come directly from DFinsupp that is used under the hood to define Dimensions and Units. So they are native to how they are internally defined.