physical units

Stream: PhysLean

[Scott N. Walck]

On the pedagogical side of things, is anyone thinking about a system of physical dimensions and units in Lean? I guess I'm thinking mainly about SI units, but I'd be interested to know about any work or ideas about physical dimensions and units.

[Joseph Tooby-Smith]

Hey, there have been a number of discussions on this in the past. See e.g.:

• #Natural sciences > physical units
• #Natural sciences > Meeting (virtual and informal) for Lean and science @ 💬

[Terence Tao]

For fun, I wrote an implementation of both abstract units in general, and SI units in particular. An example file of how the API works is at https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SIExamples.lean using the SI units defined in https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SI.lean , which are in turn a special case of "unit systems" defined in https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/UnitsSystem.lean .

Right now I have support for scalar quantities of a given dimension (e.g. length * mass / time), which can be added, multiplied, etc. in any dimensionally consistent form. There is also a larger algebra of formal combinations of scalars (basically an AddMonoidAlgebra) which one can cast into, which can be convenient for some algebraic calculations.

[Joseph Tooby-Smith]

Hi Terence,

One small comment:

Naively, I would expect dimensions to be defined independently from units. For example, the world has a manifold Time corresponding to time. A point t : Time should have dimension time. To have t : Time I need no definition of a second or units. To me what a second is, is a choice of two times t1 t2 : Time which are used to define a metric on Time, and therefore a map from Time to another type Seconds (say), terms of which correspond to differences between times in seconds.

In reality, I think in Lean one has to define t1 t2 : Time as axioms.

[Dominic Steinitz]

I just wanted to say that not everything has an SI equivalent. Maybe I am straying way off topic but the Haskell package I used made the assumption that everything was expressible in this way and this caused me problems.

Substances like erythropoietin (EPO) are measured in International Units and these cannot be converted to Moles (see Jelkmann (2009) for much more detail) so we have to pretend it really is measured in Moles as there seems to be no easy way to define what the dimensional package calls a base dimension. A typical amount for a person is 15 milli-IU / milli-litre but can reach much higher levels after loss of blood.

Jelkmann, Wolfgang. 2009. “Efficacy of Recombinant Erythropoietins: Is There Unity of International Units?” Nephrology Dialysis Transplantation 24 (5): 1366. doi:10.1093/ndt/gfp058.

[Alex Meiburg]

This is really cool! That it "just works" for type checking like this is really cool, that is that you can compare Momentum and Mass * Speed and they're actually the same time.

Another (slight) limitation: the SI definition assumes powers of units are always integers. Quantities like amplitude spectral density typically have Volts/√Hz or Watts/√Hz. Or https://en.wikipedia.org/wiki/Statcoulomb which has units cm^(3/2)⋅g^(1/2)⋅s^(−1).

Obviously not too big of a deal, and it looks like UnitsSystem supports rational powers fine

[Terence Tao]

Joseph Tooby-Smith said:

Hi Terence,

One small comment:

Naively, I would expect dimensions to be defined independently from units.

Yes, I was initially thinking in this "coordinate-free" approach, but eventually I concluded that I want to support both the "coordinate-free" way of thinking in which one does not reference units as well as the "coordinate-using" approach where one is happy to work in some artificially chosen unit system. So in the end I did not adopt a purely axiomatic approach, and instead implemented dimensions directly using an internal unit system, and supplied API for both approaches. (In particular, Scalar.val_inj is handy for manipulating scalar quantities directly through their unit representation, but one can instead use Scalar.formal_inj and work in the formal ring generated by dimensional quantities.)

[Terence Tao]

Dominic Steinitz said:

I just wanted to say that not everything has an SI equivalent. Maybe I am straying way off topic but the Haskell package I used made the assumption that everything was expressible in this way and this caused me problems.

One could set up an extended SI system in my formalism that still uses UnitsSystem but with a different Dimensions instance than the SI one. Though I haven't set up much API that would allow one to easily transfer between the SI system and an extended SI system (basically one wants a bunch of map lemmas involving homomorphisms between different Dimensions instances), but I think it can be done.

[Terence Tao]

Alex Meiburg said:

This is really cool! That it "just works" for type checking like this is really cool, that is that you can compare Momentum and Mass * Speed and they're actually the same time.

Another (slight) limitation: the SI definition assumes powers of units are always integers. Quantities like amplitude spectral density typically have Volts/√Hz or Watts/√Hz. Or https://en.wikipedia.org/wiki/Statcoulomb which has units cm^(3/2)⋅g^(1/2)⋅s^(−1).

Obviously not too big of a deal, and it looks like UnitsSystem supports rational powers fine

Actually there is a subtlety here I was trying to avoid. The reason that type checking "just works" is that my underlying Dimensions instance for SI is simple enough that things like the dimensions of Momentum and Mass * Speed are actually defeq and not just propositionally equal, ultimately due to the arithmetic of the integers being basically commutative and associative at a defeq level. I could indeed replace the dimensions instance to take rational values instead of integer ones, but then I lose the defeq and now I have to insert additional casting operators. I don't know how to enjoy the best of both worlds at this point. (Well, there are ad hoc solutions, such as taking the square root of a second as a base unit rather than a second, which would then permit introducing square roots of Hertz in a dimension system with nice defeq properties.)

[Eric Wieser]

Note that you can make them defeq:

import Mathlib

unseal Rat.add Rat.mul
example : 1 + 2*3 = (7 : ℚ) := rfl

[Joseph Tooby-Smith]

Terence Tao said:

Yes, I was initially thinking in this "coordinate-free" approach, but eventually I concluded that I want to support both the "coordinate-free" way of thinking in which one does not reference units as well as the "coordinate-using" approach where one is happy to work in some artificially chosen unit system. So in the end I did not adopt a purely axiomatic approach, and instead implemented dimensions directly using an internal unit system, and supplied API for both approaches. (In particular, Scalar.val_inj is handy for manipulating scalar quantities directly through their unit representation, but one can instead use Scalar.formal_inj and work in the formal ring generated by dimensional quantities.)

I agree and understand this approach for things like time, where I would expect the underlying manifold to be ℝ, but I'm struggling to see how this works for temperature, where the underlying manifold is ℝ≥0, and where one really wants to distinguish between temperature (living in ℝ≥0) and temperature difference in a given unit (living in ℝ).

[Terence Tao]

@Eric Wieser Thanks! I have updated the SI files to now support rational dimensions (with defeq equivalence in any namespace in which Rat arithmetic is unsealed), and it works smoothly:

abbrev half_frequency_unit := (1/2:ℚ) • frequency_unit
abbrev SqrtFrequency := Scalar half_frequency_unit
abbrev sqrt_hertz:SqrtFrequency := StandardUnit _

example : sqrt_hertz**2 = hertz := by
  simp [←Scalar.val_inj, half_frequency_unit, frequency_unit, sqrt_hertz]

example {w : SqrtFrequency} (hw : w = 2 • sqrt_hertz) : hertz.in (w**2) = 4 := by
  simp [←Scalar.val_inj, half_frequency_unit, frequency_unit, hw]
  norm_num

(I've still limited my ** operation to natural number exponentation, though, so any square roots have to be done by hand, as above, though it would not be difficult to define some qpow operation with rudimentary API.)

@Joseph Tooby-Smith : I've now given each Scalar d type an instance of an ordered vector space, so one can create subtypes such as {T:Temperature // T ≥ 0 } if desired.

[Joseph Tooby-Smith]

I had a go at modifying @Terence Tao 's approach to do two things:

1. Include more concretely the physical origin and meaning of dimensions and units into the story. That is, e.g. something has dimensions time if it scales in a certain way under a choice of metric on the Time manifold (aka a choice of time unit).
2. Allow any quantity M which depends on a choice of units to carry a dimension.

In short, this amounts to replacing Terence's Scalar definition with:

def Dimensionful (M : Type) [SMul ℝ M] (d : Dimension) : Type :=
  {f : UnitChoice → M // HasDimensions d f}

where the condition HasDimensions d f is related to how f scales on changing units.

Obviously I haven't built nearly as much API around things (but think all the features of Terence's code could be reproduced in this framework). Below is the code. I'm naturally not claiming mine is better, it just starts from a different place.

One thing I couldn't get to work is casting from dimensionless quantities to e.g. the reals (see the last example).

Code

import Mathlib

/-- Metric's on e.g. `Time` are specified
  (via some choice of reference metric) by a positive real number. -/
def UnitMetric : Type := {x : ℝ | 0 < x}

@[simp]
lemma UnitMetric.val_neq_zero (x : UnitMetric) : x.val ≠ 0 := by
  exact Ne.symm (ne_of_lt x.property)

lemma UnitMetric.val_pos (x : UnitMetric) : 0 < x.val := x.property

/-- The difference in scale between two Unit metrics. -/
noncomputable instance : HDiv UnitMetric UnitMetric ℝ where
  hDiv := fun x y => x.val / y.val

lemma UnitMetric.hDiv_eq (x y : UnitMetric) :
    (x / y : ℝ) = x.val / y.val := rfl

/-!

## Defining dimensions

-/

structure Dimension where
  length : ℚ
  time : ℚ
  mass : ℚ
  -- more to be added.

namespace Dimension

instance : Zero Dimension where
  zero := { length := 0, time := 0, mass := 0 }

lemma zero_eq : (0 : Dimension) = { length := 0, time := 0, mass := 0 } := rfl

instance : Add Dimension where
  add d1 d2 := ⟨d1.length + d2.length, d1.time + d2.time, d1.mass + d2.mass⟩

@[simp]
lemma time_add (d1 d2 : Dimension) :
    (d1 + d2).time = d1.time + d2.time := rfl

@[simp]
lemma length_add (d1 d2 : Dimension) :
    (d1 + d2).length = d1.length + d2.length := rfl

@[simp]
lemma mass_add (d1 d2 : Dimension) :
    (d1 + d2).mass = d1.mass + d2.mass := rfl

instance : Neg Dimension where
  neg d := ⟨-d.length, -d.time, -d.mass⟩

end Dimension


/-!

## Choice of units (aka metrics)

-/

/-- Choices of units for each physical quantity. -/
structure UnitChoice where
  length : UnitMetric
  time : UnitMetric
  mass : UnitMetric
  -- more to be added.

namespace UnitChoice

noncomputable def dimScale (u1 u2 : UnitChoice) (dim : Dimension):  ℝ  :=
  (u1.length / u2.length ) ^ (dim.length : ℝ) *
  (u1.time / u2.time) ^ (dim.time : ℝ) *
  (u1.mass / u2.mass) ^ (dim.mass : ℝ)

instance : Inhabited UnitChoice where
  default := { length := ⟨1, by norm_num⟩, time := ⟨1, by norm_num⟩, mass := ⟨1, by norm_num⟩ }

end UnitChoice

/-!

## Quantities of a given dimension

-/

def HasDimensions {M : Type} [SMul ℝ M] (d : Dimension) (f : UnitChoice → M) :
    Prop := ∀ u1 u2 : UnitChoice, f u2 = (UnitChoice.dimScale u1 u2 d) • f u1

def Dimensionful (M : Type) [SMul ℝ M] (d : Dimension) : Type :=
  {f : UnitChoice → M // HasDimensions d f}

@[coe]
def Dimensionful.toVal (M : Type) [SMul ℝ M] (f : Dimensionful M 0) : M := f.1 default

abbrev ScalarTime := Dimensionful ℝ {length := 0, time := 1, mass := 0}

abbrev ScalarFrequency := Dimensionful ℝ {length := 0, time := -1, mass := 0}

abbrev Dimensionless (M : Type) [SMul ℝ M]  := Dimensionful M 0

/-- Multiplication of two dimensionful real numbers. This has natural generalizations. -/
instance {d1 d2 : Dimension} : HMul (Dimensionful ℝ d1) (Dimensionful ℝ d2)
    (Dimensionful ℝ (d1 + d2)) where
  hMul := fun f1 f2 => ⟨fun u => f1.1 u * f2.1 u, by
    intro u1 u2
    dsimp
    rw [f1.2 u1 u2, f2.2 u1 u2]
    simp [UnitChoice.dimScale, UnitMetric.hDiv_eq]
    rw [Real.rpow_add, Real.rpow_add, Real.rpow_add]
    ring
    · have h1 : 0 < u1.mass.val := UnitMetric.val_pos u1.mass
      have h2 : 0 < u2.mass.val := UnitMetric.val_pos u2.mass
      positivity
    · have h1 : 0 < u1.time.val := UnitMetric.val_pos u1.time
      have h2 : 0 < u2.time.val := UnitMetric.val_pos u2.time
      positivity
    · have h1 : 0 < u1.length.val := UnitMetric.val_pos u1.length
      have h2 : 0 < u2.length.val := UnitMetric.val_pos u2.length
      positivity⟩
/-!

## Examples

-/

noncomputable def Time.distM (t1 t2 : ℝ) -- `ℝ` here should be `Time`.
     : ScalarTime :=
    ⟨fun u => (t2 - t1) / u.time.val, by
      intro u1 u2
      simp [UnitChoice.dimScale, UnitMetric.hDiv_eq]⟩

unseal Rat.add Rat.mul

example (x : ScalarTime) (f : ScalarFrequency) : Dimensionless ℝ := (f * x)

example (x : ScalarTime) (f : ScalarFrequency) : Dimensionless ℝ := x * f

-- can't get casting to work :(.
example (x : ScalarTime) (f : ScalarFrequency) :  ℝ := (x * f).toVal

[Terence Tao]

Nice. One can probably create some casting operators between your Dimensionful ℝ d and my Scalar d that render them functionally equivalent, but your framework also allows for vector-valued dimensionful quantities, such as velocity and (vector-valued) momentum, which is of course useful (in my framework one would have to take the tensor product of Speed with Space or something).

For your final coercion problem, perhaps one has to replace Coe with CoeOut? I had a similar issue in a separate project.

One question is what the use cases would be for dimensionful units. My API was mostly intended for a situation in which one selects a single unit system (such as SI) to work with, and the main purpose of the API was to ensure that all of one's manipulations remain dimensionally consistent. Your framework looks like it would be more useful in situations in which one wants to consider multiple unit systems at once (e.g. SI and Planck), and the conversions between them.

[Joseph Tooby-Smith]

One can probably create some casting operators between your Dimensionful ℝ d and my Scalar d that render them functionally equivalent,

Agreed, although I don't think there will be a canonical way to cast - I think there will be one for each set of units.

For your final coercion problem, perhaps one has to replace Coe with CoeOut? I had a similar issue in a separate project.

I'll have a play around with this - a naive implementation didn't seem to work.

One question is what the use cases would be for dimensionful units. My API was mostly intended for a situation in which one selects a single unit system (such as SI) to work with, and the main purpose of the API was to ensure that all of one's manipulations remain dimensionally consistent. Your framework looks like it would be more useful in situations in which one wants to consider multiple unit systems at once (e.g. SI and Planck), and the conversions between them.

I would say that another difference between the two frameworks is the following:

• In yours the multiplication of a quantity a1 with dimension d1 with a quantity b2 with dimension d2 is defined to have dimension d1 + d2, whilst in mine, it is proved to have dimension d1 + d2.

But I don't think this affects the use of it.

With a bias towards PhysLean, I see three main use cases (in addition to the obvious calculation and conversion use cases):

1. I think the main one, which both our frameworks do in the same way, is being able to keep track of the dimensions, as you say. Notably, you don't need to create a new API every time you want a quantity with a dimension you've never used before - I can see this being very useful.
2. Another use case is being able to define constants, for example the speed of light or Planck's constant, and relate them to their numerical value.
3. On the more theoretical side, and using the time manifold as an example, let me call it TimeMan. One day (based on previous conversations), it would be nice to have the structure of an AddTorsor on TimeMan, allowing you to take an abstract point in time t1 and add e.g. 2 seconds to it, or 1 hour etc to it.

[Joseph Tooby-Smith]

With regard to the third application in my list, I've made this PR to PhysLean, with the TimeTransMan.lean file being the relevant one.

The idea of this PR is to relate the UnitChoice in my framework above for time (called TimeMetric in the PR) explicitly to the different versions of Time present in PhysLean. I think probably the docstring of this file explains things better:

Docstring

The time manifold with a transitive action of ℝ

In this module we define the type TimeTransMan. This type physically corresponds to the manifold of time (diffeomorphic to ℝ) with the following additional structure:

1. a transitive action of ℝ,
2. a choice of orientation.

The manifold TimeTransMan is not equipped with a translationally-invariant metric. Such metrics are in one-to-one correspondence (to be shown) with positive reals, and as such we define the type TimeMetric (equivalent to the positive reals) to represent the choice of metric on TimeTransMan.

From the point of view of physics, this choice of metric corresponds to a choice of units, and we will use the phrase 'units of time' interchangeably 'term of TimeMetric'.

Given a x : TimeMetric, and the structure above, we can define the following operations on TimeTransMan:

• diff x t1 t2, for t1 t2 : TimeTransMan gives the signed difference between two points in time in the units x.

• addTime x r t, for r : ℝ and t : TimeTransMan, gives the point in TimeTransMan that seperated from t, by r in the unit x. For example, if x is the unit of seconds, then addTime x 1 t gives the point in TimeTransMan that is one second after t.

Recall that the type Time corresponds to the manifold of time with a
given (but arbitrary) choice of units and origin (and therefore has a structure
of a module over ℝ). Here we define the map:

• toTime zero x from TimeTransMan to Time where zero : TimeTransMan is the choice of origin and x : TimeMetric is the choice of units.

This map is a diffeomorphism (to be shown).

[Joseph Tooby-Smith]

For reference for people who end up reading this thread: I asked this question:

• #general > A general proposition for group invariance

on the general channel of this Zulip. It is framed in terms of group invariance but the principal should carry over to the notion of being dimensionally correct.

[Alfredo Moreira-Rosa]

I'm toying around with a simple extensible dimensional analysis framework, i'll keep you updated if i can make it fully work :
image.png
image.png

[Joseph Tooby-Smith]

Nice @ecyrbe! There is also an implementation (based on the conversation above) of units and dimensions now in PhysLean, see here.

[Alfredo Moreira-Rosa]

Joseph Tooby-Smith said:

Nice ecyrbe! There is also an implementation (based on the conversation above) of units and dimensions now in PhysLean, see here.

Yes, i took a look at all the solutions. one minor issue, is that adding new dimensions to all of them require to change the libraries. Not big of a deal, but that's why i'm trying this new approach based on Strings.

[Joseph Tooby-Smith]

Ah, I see. Could you give me an example of a dimension you would like to add, which would require a change?

[Kenny Lau]

isn't there only 7 dimensions?

[Joseph Tooby-Smith]

In otherwords (as I think Kenny is refering to), I expect the only fundamental dimensions you would ever need are:
length, time, mass, charge, and temperature. (Maybe also moles but I personal find that one a bit dubious - but would be happy to implement it if a strong case was made)

[Alfredo Moreira-Rosa]

I'm thinking bigger, not Just for physics. Dimensional analysis is used in other fields. Like Finantial systems, Computer science, etc

One big inspiration comes from the most complete implementation out there (mp_units)

[Joseph Tooby-Smith]

So another example would be something like currency?

[Joseph Tooby-Smith]

Not a comment on any particular implementation, but something I being thinking about for a while so thought it is worth writing down:

I think one thing to bear in mind with any implementation of dimensions and units, is the following definitions:

Definition 1:
A dimensional quantity is one whose value depends on the choice of units. Such a quantity is said to have a given dimension, if it scales under a change in units in a specific way.

Definition 2:
An expression is dimensionally correct if its validity does not depend on the choice of units.

In programming languages other than interactive theorem provers (ITP), to work with units it is sufficient to:

• Come up with a system which keeps track of dimensions, and ensure you have dimensional consistency.

But within an ITP I advocate that one needs more: each dimensionally correct expression should give you a theorem which you can use. This theorem should correspond to that expression being dimensionally correct and say "I can use any choice of units in this expression and it will work".

[Alfredo Moreira-Rosa]

Joseph Tooby-Smith said:

So another example would be something like currency?

yes, and in stock market, shares would be another one. in such systems, proving your stock market algorithms can be of value and so dimensional analysis also

[ZhiKai Pong]

Random idea: I think it will be nice to have a proof that units multiply (divide) under integration (differentiation). The handwavy way that I know would be to write a Riemann sum for the integral and use first principles for differentiation, but I'm curious what would a more rigorous proof look like.

[Joseph Tooby-Smith]

For the derivative, multiplication and division there are proofs (naturally set up dependent) here. But having integration, and sums in general, would be good.

[Izan Beltran]

Hello everyone! I've been learning Lean recently and got interested into applications outside of pure math. I was thinking about physical problems and units, and I found PhysLean has some units defined and some theorems. However, I didn't find any simple example and I'm struggling a bit understanding how it is supposed to be used. Maybe I've missed the example, but I would be thankful of being pointed to it, or otherwise maybe someone can provide me with a bit of insight. Thanks!

[Joseph Tooby-Smith]

Hi Izan! There is a precisely a single example here:

• ClassicalMechanics/HarmonicOscillator/Solution

Units are very new to PhysLean and @Daniel Morrison is working on it improving the API. But in general we are still working out the best way to use it. Any help or ideas , example cases would be very much appreciated :). (Note we are trying to make an API that 'proofs' units and dimensions, not only tracks them - if this makes sense).

[Izan Beltran]

Thanks Joseph! Will take a look at it :)

[Izan Beltran]

Hi, I have a question about units in PhysLean, when you define

structure LengthUnit where
  /-- The underlying scale of the unit. -/
  val : ℝ
  property : 0 < val

and then
axiom meters : LengthUnit

Could you just have defined meters as ⟨1, by norm_num⟩?

I guess it is a decision to avoid meters being just a wrapper of some numbers but an actual "concept"? Like you always need to work in terms of meters (or some function of meters)?

I'd like to hear from the authors :)

[Eric Wieser]

Arguably that should be opaque not axiom

[Izan Beltran]

That makes sense from my little understanding of it, it will have the same effect without having extra assumptions, right?

[Joseph Tooby-Smith]

So here is my philosophy.

Let LengthMetric represent translationally and rotationally invariant metrics on $\mathbb{R}^n$.
A choice of an element in LengthMetric is what really represents a unit of length, but there is no canonical choice. In the real world we historically choose it by using some reference stick. Mathematically I would see no other way here than by using an axiom, either the axiom of choice or another custom axiom (as we have done).
The type LengthMetric is not yet in PhysLean (it's open if anyone wants to do this!).

Currently LengthUnit can be seen as a place-holder for LengthMetric. Here is where it gets a bit tricky.
The equivalence between LengthUnit and LengthMetric depends on a choice of metric (or unit).

Until LengthMetric is defined, which I beleive will remove all ambiguity here, there are two choices:

1. Assume the equivalence from LengthUnit and LengthMetric to be defined through meters. In which case meters in LengthUnit should be defined through ⟨1, by norm_num⟩. In this case, once LengthMetric is defined, an axiom would then need to be introduced for meters in LengthMetric. I.e. it moves the use of an axiom (either the axiom of choice or something else) to a latter date.
2. Consider the equivalence from LengthUnit and LengthMetric to be define through some arbitrary choice of unit, and for now axiomize meters in LengthUnit.

These are two different design decisions, which I believe will converge in the end. With good documentation it shouldn't matter which is chosen. (I am not claiming that the documentation there is good - I wrote it :))

[Joseph Tooby-Smith]

(If someone has the time, and they agree with what I have written above, it would help to create a TODO item (see this) in this file regarding the definition of LengthMetric).

[Eric Wieser]

The advantage of opaque over axiom is that it doesn't raise any soundness questions, and #print axioms doesn't track it

[Joseph Tooby-Smith]

@Eric Wieser I actually like the fact that #print axioms tracks it - because it is in a sense tracking what things from the real-world are used. But your point about soundness outweighs any positive I can think of. A solution that might work for LengthMetric in the end, is to just use Classical.choose, and maybe this is the way we should go for LengthUnit, for the time-being, or just swap to ⟨1, by norm_num⟩ with the appropriate modification of the docs.

[Eric Wieser]

I think "used" is a strong term here though; if I define def radians := meters / meters did I "use" meters?

[Joseph Tooby-Smith]

Yeah, ok, there is probably some better way to phrase it

[Izan Beltran]

I see, thanks Joseph and Eric!

I have also been looking at the example solution of the Harmonic Oscillator. So as you mentioned before, "API that 'proofs' units and dimensions, not only tracks them". So we would be separately proving theorems with no units about the equations, etc, and then prove some facts about the units?
I see right now solDim is defined, and there is a future lemma solDim_eq_sol to be formalized and proven.

In contrast, I've seen Terence Tao's posts about units, and he has examples like
example (first_law : F = m * a) (hm : m = 2 • kilogram) (ha : a = 3 • meter / second**2) : F = 6 • newton

Are you expecting to provide such capabilities in the future, also working with vectors etc?

[Joseph Tooby-Smith]

So we would be separately proving theorems with no units about the equations, etc, and then prove some facts about the units?

Ideally the API should be good enough that you essentially get the theorems about units for free or very easily, without having to do much extra work. Ideally in that example we wouldn't need solDim and sol itself would contain the dimensions - just not sure how to make this all work yet - in a nice way that gives you usable theorems :).

Concerning Tao's examples, one can do e.g.:

import PhysLean.Units.Mass

open Dimension
open Dimensionful
open UnitChoices
open NNReal


noncomputable def newtons : Dimensionful (M𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ := ofUnit _ 1 SI

noncomputable def kilograms : Dimensionful M𝓭  ℝ := ofUnit _ 1 SI

noncomputable def mPerSecond : Dimensionful (L𝓭 * T𝓭⁻¹ * T𝓭⁻¹)  ℝ := ofUnit _ 1 SI

variable (F : Dimensionful (M𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ) (m : Dimensionful M𝓭  ℝ)
    (a : Dimensionful (L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) ℝ)

unseal Rat.add Rat.mul
example (first_law : F = m * a)
    (hm : m = 2 • kilograms) (ha : a = 3 • mPerSecond) :
    F = 6 • newtons := by
  sorry

among other things - so yes we expect this sort of capabilities. Note in this example, the dimensions are indeed being tracked correctly by Lean.

One would already be able to define Dimensionful with vectors and work with them in a similar way to the above.

[Daniel Morrison]

What I'm trying to do with units is similar to Tao's example where units can be added to calculations via the scalar multiplication notation. As Joseph mentioned these kinds of things are technically possible at the moment but are a little cumbersome to use because you need to use several different types. My goal is to move stuff to classes so it can be used implicitly without much thought from the user, how exactly that happens is something to be figured out.

[Max Bobbin]

We've finished a draft of our manuscript on defining dimensions and physical variables in Lean, which may be of interest for this thread. We wanted to post it here to gather feedback from the community and solicit thoughts on its applicability. It's great to see all the researchers interested in Lean!
Formalizing_dimensional_analysis.pdf

[Max Bobbin]

We explored implementing PhysicalVariables as a graded algebra over dimensions, but found the code to be unusable since each physical variable (such as velocity or force) is its own type and requires a large amount of coercion instances to use together in equations.

[Alfredo Moreira-Rosa]

Max Bobbin said:

We explored implementing PhysicalVariables as a graded algebra over dimensions, but found the code to be unusable since each physical variable (such as velocity or force) is its own type and requires a large amount of coercion instances to use together in equations.

hello, can you elaborate on this part ? does it mean afftecting s^-1 * (m * s) / s to m/s don't work ?

[Eric Wieser]

Some quick feedback on the manuscript:

• could you remark on why you chose not use Multiplicative to define Dimension, which give you the group structure for free and eliminates 2.5 pages of work
• Why do you define addition on dimensions at all?
• Could you remark on how you define addition of PhysicalVariable, and what happens if the units mismatch?

[Joseph Tooby-Smith]

Hey @Max Bobbin , just wanted to say well done getting this draft done! I know this is something you all started a fair while ago, and I'm sure it's going to act as a useful reference point in the future, so congrats!

[Max Bobbin]

ecyrbe said:

Max Bobbin said:

We explored implementing PhysicalVariables as a graded algebra over dimensions, but found the code to be unusable since each physical variable (such as velocity or force) is its own type and requires a large amount of coercion instances to use together in equations.

hello, can you elaborate on this part ? does it mean afftecting s^-1 * (m * s) / s to m/s don't work ?

We tried defining physical variable as a structure that took in a dimension instead of having a dimension as a field (we have this saved on github to check out. We defined the graded structure as a subtype of PhysicalVariable). A major problem is that the PhysicalVariable (length/time) is a different type than PhysicalVariable (velocity). This made it very difficult to write a statement like v = x/t . To write such a statement required Coe (PhysicalVariable (length/time)) (PhysicalVariable velocity). We couldn't write general Coe instances because we ran into a problem with Lean not having a definite output for the Type.

[Max Bobbin]

Eric Wieser said:

Some quick feedback on the manuscript:

• could you remark on why you chose not use Multiplicative to define Dimension, which give you the group structure for free and eliminates 2.5 pages of work
• Why do you define addition on dimensions at all?
• Could you remark on how you define addition of PhysicalVariable, and what happens if the units mismatch?

After you said that, I remember this suggestion from before. There is no reason we chose not to use Multiplicative, and I think the code would be nicely golfed with Multiplicative. One thing we liked about showing that definition of dimension is offering an example to scientists about defining Types in a similar way the way the Natural numbers are built. We hoped it would give an easily accessible example for scientist to understand how to build these mathematical objects.

We define addition for dimensions, mainly, so we can define addition for Physical Variables. We define their addition as:

protected noncomputable def Add {B : Type u} {V : Type v} [Field V] :
PhysicalVariable B V →  PhysicalVariable B V → PhysicalVariable B V
| a,b => PhysicalVariable.mk (a.value+b.value) (a.dim+b.dim)

The other way we found to define addition is to use the graded structure which prevents the dimensions from being different, but we found that formulation to be unuseable for theorems. This definition uses our definition of addition for dimensions. So, if we correctly understand how the Epsilon function works, you could write an equation of velocity + time = force but you wouldn't be able to show the dimensional homogeneity because the addition for dimensions requires it to be the same dimension.

[Alfredo Moreira-Rosa]

Max Bobbin said:
We tried defining physical variable as a structure that took in a dimension instead of having a dimension as a field (we have this saved on github to check out. We defined the graded structure as a subtype of PhysicalVariable). A major problem is that the PhysicalVariable (length/time) is a different type than PhysicalVariable (velocity). This made it very difficult to write a statement like v = x/t . To write such a statement required Coe (PhysicalVariable (length/time)) (PhysicalVariable velocity). We couldn't write general Coe instances because we ran into a problem with Lean not having a definite output for the Type.

So does this mean that in your new implementation, we can add two incompatible dimensions and not have an error catched at compile time ?

[Eric Wieser]

Yes. It also means that you can't add quantities at runtime any more, as + is noncomputable

[Eric Wieser]

(it's also non-commutative, so there is no Ring structure on quantities)

[Alfredo Moreira-Rosa]

@Eric Wieser do you think a custom elaborator could solve the issue ? i think i saw someone try that path in one implementation to do the checks and proven coe generated at compile time

[Eric Wieser]

I think we already found the solution, it's unseal Rat.* in

[Eric Wieser]

But also, velocity = length/time should be rfl anyway, so I think there is something else going wrong here

[Alfredo Moreira-Rosa]

Eric Wieser said:

But also, velocity = length/time should be rfl anyway, so I think there is something else going wrong here

yes, in my own implementation, this works, definitely something else going on.

[Izan Beltran]

Terence Tao said:

Nice. One can probably create some casting operators between your Dimensionful ℝ d and my Scalar d that render them functionally equivalent, but your framework also allows for vector-valued dimensionful quantities, such as velocity and (vector-valued) momentum, which is of course useful (in my framework one would have to take the tensor product of Speed with Space or something).

For your final coercion problem, perhaps one has to replace Coe with CoeOut? I had a similar issue in a separate project.

One question is what the use cases would be for dimensionful units. My API was mostly intended for a situation in which one selects a single unit system (such as SI) to work with, and the main purpose of the API was to ensure that all of one's manipulations remain dimensionally consistent. Your framework looks like it would be more useful in situations in which one wants to consider multiple unit systems at once (e.g. SI and Planck), and the conversions between them.

Hi Terence, is there a convenient way to work with vectors and dimensions with your units approach? Also, since it is inside your "Analysis" project in the "Misc" section, do you plan to keep improving it? Or is it just an exercise on formalizing units? Thanks!

[Terence Tao]

Given all the other efforts now to formalize units in Lean, I do not have plans to significantly expand my current code, which I was indeed viewing as an exercise.

As for vector valued dimensional quantities, one could simply create an API for Vector X := Fin 3 → X that might be good for creating, e.g., Vector Length, Vector Momentum, etc. (and then develop further API for covectors (axial vectors), etc. perhaps) with typechecking that "just works", but I haven't put much thought into this. One could also try to use the TensorProduct API already in Mathlib, but the lack of defeq, e.g., between X ⊗ Y and Y ⊗ X, would be annoying.

[Alfredo Moreira-Rosa]

Happy to announce some progress on my compile time checked dimensional analysis framework library.
took inspiration from @Terence Tao ideas.
All formal proofs have been done making my Dimension implementation a AddCommGroup. Allowing to use module tactic to cast seemlessly if it's provable.
Here an exemple :

image.png

If cast fails, you are sure it's incompatible :
image.png

[Alfredo Moreira-Rosa]

And you can define new dimensions on the fly, and mix them with previously defined ones, and it works without touching the base framework :

image.png

[Alfredo Moreira-Rosa]

next step, i'll define properly ISO-80000 for system of quantities and hierarchical quantities (meaning, even if dimensions are equal, they may not be of the same kind and you don't want to mix them, like altitude and width should not be mixed together even if they have the same dimension)

[Alfredo Moreira-Rosa]

To make this possible, under the hood, Dimensions are a normalized list of Bases that are pretty much just string and non null exponents :
image.png
image.png
image.png

[Alfredo Moreira-Rosa]

hardest part, was proving that this form a AddCommGroup

[Eric Wieser]

I think you could save yourself some effort by defining Dimension := DFinsupp String (fun _ => Rat)

[Eric Wieser]

(deleted)

[Alfredo Moreira-Rosa]

Thanks Eric, i'm not familiar with DFinsupp, i'll take a look. if it can make the proofs easier, i'm all for it;

[Eric Wieser]

Notably you get the AddCommGroup structure for free

[Eric Wieser]

Yours is probably computationally faster though

[Alfredo Moreira-Rosa]

@Eric Wieser i created a new Dimension based on DFinsupp, works like a charm.
image.png

no more proofs needed, like you said all free, just one thing is that i had to make an unsafe Repr (like DFinsupp does) while mine was not.

[Alfredo Moreira-Rosa]

image.png

[Eric Wieser]

You should be able to make a safe one with .support.sort

[Eric Wieser]

But also, because you're using abbrev you shouldn't define that instance

[Eric Wieser]

Probably you should make a one-field structure instead

[Eric Wieser]

Then you can use docs#Equiv.addCommGroup to pull across that structure, and be free to define your own repr

[Eric Wieser]

(also, consider posting with #backticks rather than screenshots)

[Alfredo Moreira-Rosa]

All this make sence; thanks for the kind advices

[Eric Wieser]

I'll remind you that your initial implementation is probably faster; though I think @Kim Morrison has a (D)Finsupp alternative for hashable types that might be even faster here

[Alfredo Moreira-Rosa]

Yes, mine is certainly faster, i'll measure for sure. i may provide both implementations if it's that bad.
They have the same user surface level API and are compatible. So i don't worry too much.

[Alfredo Moreira-Rosa]

I think i'll keep DFinsupp, it's kind of magical to compose Dimensions into higher Opaque Hierachical Unit system.
I can now define a unit as :

instance : AddCommGroup (ℚ × Dimension) := inferInstance

structure Unit where
  _impl : DFinsupp (fun _ : String => ℚ × Dimension)

def defineUnit (s : String) (d : Dimension) : Unit := ⟨DFinsupp.single s (1,d)⟩

instance instEquiv : Unit ≃ DFinsupp (fun _ : String => ℚ × Dimension) :=
  ⟨Unit._impl, Unit.mk, by intro x; cases x; rfl, by intro y; rfl⟩

instance instAddCommGroup : AddCommGroup Unit :=
  Unit.instEquiv.addCommGroup

def dimension (u : Unit) : Dimension :=
  u._impl.sum (fun _ qd => qd.2)

Here a starting preview or units definition :
image.png

[Alfredo Moreira-Rosa]

i may rename Unit into QuantityRef to say that it's a ISQ reference from a unit of choice into a dimension.
it's the name used in c++ mp_units

[Alfredo Moreira-Rosa]

You then build quantities on top of it, since it works like dimension themselves

[Alfredo Moreira-Rosa]

One cool thing is that now, with this system, we can prevent adding Becquerel and Frequency quantities, because even if they have the same dimension, we can define them as opaque different units.

abbrev Hz := defineUnit "Hz" (-Dimension.Time)
abbrev Bq := defineUnit "Bq" (-Dimension.Time)

same dimension, but not addable by default. i'll try to come up with an escape hatch to allow it (maybe something like strong cast)

[Eric Wieser]

I don't understand the intent of your Unit type, what does 2*m +s mean?

[Alfredo Moreira-Rosa]

it's a reference, they form a hierarchy in ISO 80000
So it's just an abstraction over dimensions to say you have chosen a metric for a dimension.
Seconds for Time, Kilograms for Mass, etc
The confusion may come because we have chosen to represent Dimension and Quantities Reference as a AddCommGroup instead of a CommGroup (because there is no good tactic that work on CommGroup only, so it was better to represent them like that to leverage on Mathlib power)
So here we are not dealing with quantities, yet. Just Dimension Abstractions.

Here a less confusing application once we work on quantities with proper operators :
image.png

[Alfredo Moreira-Rosa]

And i encourage anyone interrested in how to properly implement Physical Units to take a look at the most advanced implementation out there that will be standardized by C++ ISO commity.
They explain pretty well what are System of Quantities in their docs, and why they are needed:
https://mpusz.github.io/mp-units/latest/users_guide/framework_basics/systems_of_quantities/

[Alfredo Moreira-Rosa]

New exemple, you want to work on electron volts. it's another system of metric. and don't want to have implicit conversion between eV and Joules (that could be bad if not taken care of)
Having this hierarchy in place allows to force some kind of explicit conversion if someone want to work with both at the ame time.
image.png

[Alfredo Moreira-Rosa]

Conversion system is now in place. This is starting to look very good. i'll publish the full source code soon :
image.png

[Tyler Josephson ⚛️]

A high-level question I wanted to ask about: in PhysLean, time is semantically distinct from distance, and their implementations are rather different (according to this topic). But in dimensional analysis, there is no distinction. I wonder how these might ultimately be stitched together.

[Joseph Tooby-Smith]

Would you mind providing more detail about what you mean by:

But in dimensional analysis, there is no distinction.

Are you thinking about natural units where time and space are treated the same due to the speed of light being set to 1, or something else?

[Joseph Tooby-Smith]

(I should also add a note that we are refactoring Space to make it more like the implementation of Time, this is taking place here)

[Tyler Josephson ⚛️]

Interesting! I'm not referring to natural units - mainly about dimensions on this, not units. I feel like time and space are rather different in their internal structure / their semantics, but one treats them the same when doing dimensional analysis math (or handling any of the ISQ dimensions, FWIW). We might first be dealing with this in time and space, but I anticipate it will come up more often. For instance, electric current is the ISQ dimension, but I wonder if you'd rather define what an electron is, first (alongside the other fundamental particles, their relationships to one another, etc.), define what its charge is, then link it to time to derive the ISQ dimension. I also wonder about temperature, too.

[Tyler Josephson ⚛️]

Indeed, Space d abstracting over `EuclideanSpace has no parallel of Time d abstracting over EuclideanTime. SpaceStruct d representing d dimensional Euclidean space seems cleaner, indeed. Nice!

[Joseph Tooby-Smith]

I wonder if you'd rather define what an electron is, first (alongside the other fundamental particles, their relationships to one another, etc.), define what its charge is, then link it to time to derive the ISQ dimension.

This is certainly the way I would like things to be done in PhysLean, i.e. dimensions should be defined and connected to the actual physical choices they correspond to, and this is currently the set up of dimensions within PhysLean (although much of the nitty-gritty detail is left as a TODO, and there is much to be refined). This is somewhat related to this message of mine above:

#PhysLean > physical units @ 💬

For what it's worth I view dimensions and units as a two sided problem:

1. Define/derive the physical origin and meaning of the notion of a dimension.
2. Come with a system to effectively and efficiently track dimensions and convert between units.

Much of the conversation here has focused on (2) - which is great because this is perhaps the most useful part. Long term in PhysLean we need both (1) and (2) and them connected well.

[Alfredo Moreira-Rosa]

You can't define and link Dimensions based on theories that are underlying it.
Because there is no one true theory in physics. Dimensional Analysis is an abtraction and i think it should be kept like that. It helps state and prove theorems based on some theories axioms. So we should keep them appart. This way you'll be able to build different theories, state some truth about them if you consider the theory axioms true. An if needed, at the proper hierachy level use dimensional analysis to cheack your statements are at least sound.

[Tyler Josephson ⚛️]

Joseph Tooby-Smith said:

For what it's worth I view dimensions and units as a two sided problem:

1. Define/derive the physical origin and meaning of the notion of a dimension.
2. Come with a system to effectively and efficiently track dimensions and convert between units.

Much of the conversation here has focused on (2) - which is great because this is perhaps the most useful part. Long term in PhysLean we need both (1) and (2) and them connected well.

Nice! I like the way you're framing this. This more cleanly divides the syntax and semantics. I was trying to articulate a question like (1) here, what will this look like? The closest thing I've seen in the various implementations is to essentially: someone builds an implementation of (2) (aka syntax), and then says "now let's define the ISQ dimensions" (making the jump to semantics).

[Tyler Josephson ⚛️]

ecyrbe said:

You can't define and link Dimensions based on theories that are underlying it.
Because there is no one true theory in physics. Dimensional Analysis is an abtraction and i think it should be kept like that. It helps state and prove theorems based on some theories axioms. So we should keep them appart. This way you'll be able to build different theories, state some truth about them if you consider the theory axioms true. An if needed, at the proper hierachy level use dimensional analysis to cheack your statements are at least sound.

Agreed! What's clearer to me, now, is that even defining ISQ (without any deeper connections) is already breaking away from that abstraction, and linking this to semantics. Eventually, we'll want the broader physical theories to be "linkable" to the dimensional analysis syntax, but they wouldn't be used to derive the math of dimensional analysis. A deeper theory might be used to derive the ISQ base dimensions, though. But different theories might implement that differently, for instance, depending on how fundamental that theory considers temperature to be.

[Joseph Tooby-Smith]

I was trying to articulate a question like (1) here, what will this look like?

To me it looks like a file like:

• https://github.com/HEPLean/PhysLean/blob/master/PhysLean/SpaceAndTime/Time/TimeUnit.lean

for each unit, which is the origin of the non-canonical choice that one has to make, and which corresponds to the units. This is what covers (1), and then a file like:

• https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Units/Basic.lean

which defines the notion of a dimension formally based on quantities which whose values depend on those non-canonical choices. This can then be fed into an implementation like (2), ideally it should be possible to go back from (2) to (1) though, and make consequential lemmas about the choices made.

Again all of this in PhysLean is very much open to improvement, and is more a framework of how things could look, then set-in-stone.

[Alfredo Moreira-Rosa]

I'm in the process of cleaning my take on Dimensional Analysis and publish the source code. I took inspiration from Terrence Tao implementation.
You can just work on Dimensional system (without ISQ) and have an abtract Formal Quantity system based on AddMonoidAlgebra. All decorelated from the practical Unit system.

[Alfredo Moreira-Rosa]

Hello i just published the source code of Lean-Units framework :
https://github.com/ecyrbe/lean-units

[Alfredo Moreira-Rosa]

@Joseph Tooby-Smith what's a good (simple) lemma you proved using physlean dimensional analysis that i can check also against my library ? So that i can have a basic idea if it can be of any help for formal physics.

[Joseph Tooby-Smith]

Hi @ecyrbe , I don't have any simple examples, mainly because we are trying to tie things (as implicitly as possible) into the more core definitions within PhysLean, and as @Daniel Morrison pointed out above that will probably involve going over to a type-class approach. I.e. we haven't worked out the best way to do (2) (in my list above) within PhysLean, which makes it hard to give examples which could be compared with your implementation.

[Joseph Tooby-Smith]

(By a type-class approach I mean something along the lines of terms of type M is assigned a dimension through an instance of a type-class on M, rather then making a special types which are explicitly defined to carry dimensions (e.g. SI T say). )

[Alfredo Moreira-Rosa]

Thank you very much.
So, i'll try to do some basic things then that i have in my old grad books

[Tyler Josephson ⚛️]

ecyrbe said:

Joseph Tooby-Smith what's a good (simple) lemma you proved using physlean dimensional analysis that i can check also against my library ? So that i can have a basic idea if it can be of any help for formal physics.

Conceptually, I think your simple E = m*c^2 idea is a good place to start. https://github.com/ecyrbe/lean-units/blob/9fb70fb0a7a1e6ad74274cd02be94803438d1c37/Examples/formal.lean#L17

FWIW, while @Max Bobbin was working on his implementation, we had a version we were pretty happy with. I then suggested he try, as a stretch goal, the Lennard-Jones potential, since we implemented that here. My original ask was "can you literally take our Real-valued function (without the if and else complication), somehow attribute dimensions to the variables on the right-hand-side, and write a theorem about the dimensions of the LJ function." That turned out to be too hard. But we settled for something less elegant - can we define a new version of the LJ function, in which we specify the dimensions of the RHS variables in the function, and then do that? While tackling this, he realized some issues with his old implementation (I forget exactly, it might have been related to handling energy - energy [=] energy), and refactored the code into its current state. We're in the process of one more refactor of that section, but the simplest theorem in that area is here - essentially that, for the function LJ whose RHS has dimensional variables, prove that when $r$ = $\sigma$, LJ = 0 (with dimensions of energy).

[Joseph Tooby-Smith]

As an example of the sort of thing I think PhysLean would end up needing

(This assumes some contents from this file)

Code

/-!

## CarrysDimension

-/

class CarriesDimension (M : Type) extends SMul ℝ≥0 M where
  d : Dimension


def HasDimension' {M : Type} [CarriesDimension M] (f : UnitChoices → M) : Prop :=
  ∀ u1 u2 : UnitChoices, f u2 = UnitChoices.dimScale u1 u2 (CarriesDimension.d M) • f u1

def Dimensionful' (M : Type) [CarriesDimension M] :=
  {f : UnitChoices → M // HasDimension' f}

class DMul (M1 M2 M3 : Type) [CarriesDimension M1] [CarriesDimension M2] [CarriesDimension M3]
    extends HMul M1 M2 M3 where
  mul_dim : ∀ (m1  : Dimensionful' M1) (m2 : Dimensionful' M2),
    HasDimension' (fun u => hMul (m1.1 u) (m2.1 u))


/-!

## WithDim

WithDim is the type `M` which carrying the dimension `d`.  But one could assign
the instance `CarriesDimension` to any type.

-/

structure WithDim (d : Dimension) (M : Type) [SMul ℝ≥0 M] where
  val : M

namespace WithDim

@[ext]
lemma ext {d M}  [SMul ℝ≥0 M] (x1 x2 : WithDim d M) (h : x1.val = x2.val) : x1 = x2 := by
  cases x1
  cases x2
  simp_all

instance (d : Dimension) (M : Type) [SMul ℝ≥0 M] : SMul ℝ≥0 (WithDim d M) where
  smul a m := ⟨a • m.val⟩

@[simp]
lemma smul_val {d : Dimension} {M : Type} [SMul ℝ≥0 M] (a : ℝ≥0) (m : WithDim d M) :
    (a • m).val = a • m.val := rfl

instance (d : Dimension) (M : Type) [inst : SMul ℝ≥0 M] : CarriesDimension (WithDim d M) where
  d := d

@[simp]
lemma carriesDimension_d (d : Dimension) (M : Type) [SMul ℝ≥0 M] :
    CarriesDimension.d (WithDim d M) = d := rfl

instance {d1 d2 : Dimension} :
    HMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2) ℝ) where
  hMul m1 m2 := ⟨m1.val * m2.val⟩

@[simp]
lemma withDim_hMul_val {d1 d2 : Dimension} (m1 : WithDim d1 ℝ) (m2 : WithDim d2 ℝ) :
    (m1 * m2).val = m1.val * m2.val := rfl


instance {d1 d2 : Dimension} :
    DMul (WithDim d1 ℝ) (WithDim d2 ℝ) (WithDim (d1 * d2)  ℝ) where
  mul_dim m1 m2 := by
    intro u1 u2
    ext
    simp
    rw [m1.2 u1, m2.2 u1]
    simp
    rw [smul_smul]
    congr 1
    rw [mul_comm]

open Dimension
example (m1 : WithDim L𝓭 ℝ) (m2 : WithDim T𝓭 ℝ) : WithDim (L𝓭 * T𝓭) ℝ := m1 * m2

end WithDim

One would have to more manually build the API then other implementations, but everything is done by actual proofs (e.g. in DMul), and otherwise tracked by typeclasses.

[Joseph Tooby-Smith]

See I cleaned up the PhysLean version of units based on the above in PhysLean#718.

But also, @ecyrbe , I think it may be possible to combine your implementation with the one in PhysLean, and get the best of both worlds.

For example, your type Dimension is defined as

structure Dimension where
  _impl : DFinsupp (fun _ : String => ℚ)

While PhysLean's is:

structure Dimension where
  /-- The length dimension. -/
  length : ℚ
  /-- The time dimension. -/
  time : ℚ
  /-- The mass dimension. -/
  mass : ℚ
  /-- The charge dimension. -/
  charge : ℚ
  /-- The temperature dimension. -/
  temperature : ℚ

So we could just combine and do:

structure Dimension where
  /-- The length dimension. -/
  length : ℚ
  /-- The time dimension. -/
  time : ℚ
  /-- The mass dimension. -/
  mass : ℚ
  /-- The charge dimension. -/
  charge : ℚ
  /-- The temperature dimension. -/
  temperature : ℚ
  /-- Other dimensions based on strings.  -/
  other : DFinsupp (fun _ : String => ℚ)

Similarly your type Quantity is the same as PhysLean's type WithDim. Let me know what you think? (Not so say I think this is going to be easy - but I think it could be possible).

[Alfredo Moreira-Rosa]

i'm not sure how to transpose HasDimension for others . When working formally, would this mean that you would need to reason differently for others dimensions and length ?

[Joseph Tooby-Smith]

I was thinking making a type like OtherUnit defined isomorphic to ℝ≥0, similar to how TemperatureUnit etc are defined. Then one could define e.g.

/-- The choice of units. -/
structure UnitChoices where
  /-- The length unit. -/
  length : LengthUnit
  /-- The time unit. -/
  time : TimeUnit
  /-- The mass unit. -/
  mass : MassUnit
  /-- The charge unit. -/
  charge : ChargeUnit
  /-- The temperature unit. -/
  temperature : TemperatureUnit
  /-- The other units -/
  other : String -> OtherUnit

Then given you have restricted to finite support, we could add to dimScale a factor which depends on these other units. Then (I think) everything else should follow in exactly the same way for others and lengthetc. i.e they wouldn't have to be reasoned about differently. (I agree that if they did then this would defeat the point).

[Alfredo Moreira-Rosa]

In my lib, i can implement as many systems (a system is a choice of dimensions and units) as needed.
I have of course setup the standard SI system, but for natural unit systems i know it's kind of a complex.

from the wikipedia page, i see 6 different natural unit systems. is it exhaustive ? are there more ?
should i just not pre-define them and let the users implement their own, or would it be convenient if i pre-defined those 6 ? or less ?

[Alfredo Moreira-Rosa]

the wikipedia page : https://en.wikipedia.org/wiki/Natural_units

[Alfredo Moreira-Rosa]

As an engineer i only work with SI, so i'm kind of lost when it comes to natural units :)

[Joseph Tooby-Smith]

I think some of them are probably never used. The one I would recognize as "natural units" is the one labelled "Particle and atomic physics" in that list.

BTW is there a specific type for 'a system' (as you describe above) in your implementation? I guess this is something easier in PhysLean's current implementation where the dimension are fixed and one can define a system by just specifying a unit for each dimension (e.g. here).

[Alfredo Moreira-Rosa]

Your right to point that out, i have not yet attached anything to the concept of coherent system of units. And i think i should, because if i do, we could create morphisms between them (some would be isomorphic, others not)

[Joseph Tooby-Smith]

ZhiKai Pong said:

Random idea: I think it will be nice to have a proof that units multiply (divide) under integration (differentiation). The handwavy way that I know would be to write a Riemann sum for the integral and use first principles for differentiation, but I'm curious what would a more rigorous proof look like.

All a bit of a mess, but here is a proof that integrals behave as one would expect with regard to dimensions.

[Alfredo Moreira-Rosa]

@Terence Tao is it Ok for you if i use the lemmas you defined here ? :
https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/UnitsSystem.lean

into my library ? i can give credit in the header of the file where i'd use it and in de Readme.md so that nobody thinks i'm the author.

[Alfredo Moreira-Rosa]

The License of my Library is MIT in case this matter

[Terence Tao]

Sure, this is fine with me.

[Joseph Tooby-Smith]

Was thinking of putting the following comment in the Units file of PhysLean:

Other implementations of units

There are other implementations of units in Lean, in particular:

1. https://github.com/ATOMSLab/LeanDimensionalAnalysis/tree/main
2. https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SI.lean
3. https://github.com/ecyrbe/lean-units

Each of these have their own advantages and specific use-cases.
For example both (1) and (3) allow for or work in Floats, allowing computability and the use of #eval. This is currently not possible with the more theoretical implementation here in PhysLean which is based exclusively on Reals.

Do people think this is fair/have anything that could be added?

[Alfredo Moreira-Rosa]

Yes, good note. i'll do the same on mine.

[Terence Tao]

I've updated my own file with these links. I've decided to stop maintaining my own code for units and let it be used freely in other projects of this nature.

[Alfredo Moreira-Rosa]

@Joseph Tooby-Smith i took some time to check your new examples in physlean, and i see the DimensionInvariant concept and i'm a bit puzzled.
You could have just made the equations computed directly on quantities and by the magic of type checking this would have been by definition. Am i missing something ?

[Alfredo Moreira-Rosa]

As an exemple, in my lib :

theorem e_equal_mc2 (E : SI Dimension.Energy) (m : SI Dimension.Mass) :
    E =  ↑(m * c²) := sorry

is typechecked and so is dimensionally invariant by definition.
and this one :

theorem e_equal_mc (E : SI Dimension.Energy) (m : SI Dimension.Mass) :
    E =  ↑(m * c) := by -- statement is wrong and is directly catched by the type checker
    sorry

Don't type check, you can't compile it. And so is not DimensionalInvariant by definition.

[Alfredo Moreira-Rosa]

And using Terence Tao Abstraction, you could have exactly the same for your WithDim quantity abstraction

[Joseph Tooby-Smith]

The reason is that in your lib,

theorem e_equal_mc' (E : SI Dimension.Energy) (m : SI Dimension.Mass) :
    E.val =  (m.val * c.val) := by
    sorry

does type check, so why is it not 'dimensionally invariant' in your library?

With PhysLean's implementation you would be able to prove that e_equal_mc2 is dimensionally invariant and e_equal_mc and e_equal_mc' are not.
This is because dimensions are defined by how quantities scale under a change in units.
It works no matter what tricks the user plays with types or casting, and you get from it a bona-fide theorem which you can apply in proving other theorems.

This means that with something like IsDimensionalInvariant you can prove derivatives and integrals have certain dimensions, whilst this would be impossible in the sort of implementation you have (as far as I am aware), where it would just have to be defined.

It is certainly true that type checking and the sort of implementation you have is extremely useful, and with a good API would be able to help prove e.g. IsDiemsionallyInvariant for e_equal_mc2 based on the fact it type checks.

[Joseph Tooby-Smith]

And using Terence Tao Abstraction, you could have exactly the same for your WithDim quantity abstraction

I agree, and this is what we would want, we would want that implementation connected to IsDimensionallyInvariant as well though.

[Joseph Tooby-Smith]

...does type check, so why is it not 'dimensionally invariant' in your library?

To answer this, in your library the definition of 'dimensionally invariant' really has two parts to it:

1. It type checks.
2. You have only used a set of allowed operations which have specially been defined to track and account for dimensions.

Lean knows about 1, but it does not know about or check for 2, a human has to do this. Both for e_equal_mc2 and e_equal_mc', the first of these hold, but for e_equal_mc' the second does not hold. You could write a theorem for 2 - and then you are already heading in the direction of the sort of implementation PhysLean has.

[Alfredo Moreira-Rosa]

Joseph Tooby-Smith said:

The reason is that in your lib,

theorem e_equal_mc' (E : SI Dimension.Energy) (m : SI Dimension.Mass) :
    E.val =  (m.val * c.val) := by
    sorry

does type check, so why is it not 'dimensionally invariant' in your library?

But here you are working on values that are not typed checked, so it's normal.
It's the whole point of a unit system (in my point of view) to compute everything using quantities and not values.
Writing proofs for Dimensional invariance is cumbersome when you can just work with Quantities and have it for free.

[Joseph Tooby-Smith]

It's the whole point of a unit system (in my point of view) to compute everything using quantities and not values.

But this is not something you can tell or encode into Lean.

[Joseph Tooby-Smith]

Writing proofs for Dimensional invariance is cumbersome when you can just work with Quantities and have it for free.

I will be the first to admit that writing proofs for dimensional invariance is currently very cumbersome, but this is more a case of building the API I think, and part of that API should be about working with Quantities.

[Alfredo Moreira-Rosa]

Joseph Tooby-Smith said:

To answer this, in your library the definition of 'dimensionally invariant' really has two parts to it:

1. It type checks.
2. You have only used a set of allowed operations which have specially been defined to track and account for dimensions.

Lean knows about 1, but it does not know about or check for 2, a human has to do this. Both for e_equal_mc2 and e_equal_mc', the first of these hold, but for e_equal_mc' the second does not hold. You could write a theorem for 2 - and then you are already heading in the direction of the sort of implementation PhysLean has.

I don't agree, type checking is not based on allowed computations. It's using an automated proof tactic to prove the dimensions are equal (by using module tactic). And lean can perfectly do it.

[Alfredo Moreira-Rosa]

That's what cast do. automatically prove that the dimensions are equal

[Alfredo Moreira-Rosa]

But for that to work you need to make your Dimensions AddCommGroup instead of CommGroup, like Terence did

[Joseph Tooby-Smith]

I agree with this, but I don't think this is what I am saying.

You, as a human, had to tell me that e_equal_mc' wasn't dimensionally invariant, because it depended on values and not quantities. Lean would have let me write down this equation without any problem.

Let me rephrase this: How would you tell Lean that e_equal_mc' is not dimensionally invariant?

[Alfredo Moreira-Rosa]

You don't, you work on Quantities all the time ?

[Alfredo Moreira-Rosa]

My point is, why would you write your physics equations using values, when you can just use the Quantities?
Even your examples use quantities abstractions to write the equations and provide a proof manually.
And so why not write the equation directly using the quantities. If it don't type check, it's a proof. That's what Lean does. A proof is just a type checked code. It it don't type check you don't have a proof

[Alfredo Moreira-Rosa]

And sorry, it's the other way around, if it type checks, you have a proof. absence of type checking is not a proof it could not type check.

[Alfredo Moreira-Rosa]

Maybe that's your point ? But even so, failing to writing a proof manually is not a proof of absence of dimensional invariance

[Joseph Tooby-Smith]

My point is, why would you write your physics equations using values, when you can just use the Quantities?

But one could say: Why would you write physics equations that are dimensionally incorrect anyway, just write dimensionally correct equations?

You are trusting the user here to work just with Quantities, which is fine, but this is not something you can encode into Lean.

if it type checks, you have a proof

A proof of what theorem?

But even so, failing to writing a proof manually is not a proof of absence of dimensional invariance

Agreed, but I'm all for automated ways to prove dimensionally invariance too

[Alfredo Moreira-Rosa]

You are trusting the user here to work just with Quantities, which is fine, but this is not something you can

I don't get it, to write Dimensional Invariance like you did in physlean, you have to attach dimensions to your values. hence the .1 everywhere.

> if it type checks, you have a proof

A proof of what theorem?

A proof that it that the dimension on the left side is equal to the one on the right side. On Terence Tao, it's even better, you get a proof at each casting operation. So you can have multiple proofs.

[Alfredo Moreira-Rosa]

An the proof is just by module

[Alfredo Moreira-Rosa]

And if they are the same, you get dimensional invariance

[Joseph Tooby-Smith]

I don't get it, to write Dimensional Invariance like you did in physlean, you have to attach dimensions to your values. hence the .1 everywhere.

Those .1 could be got rid of by defining multiplication between WithDim _ _s, in the same way that you have defined it. This is just a case of bad API.

Let me add another equation into the mix:

theorem e_equal_mc2' (E : SI Dimension.Energy) (m : SI Dimension.Mass) :
    E.val =  (m.val * c.val²) := sorry

To me, the following is ture

1. Both e_equal_mc2 and e_equal_mc2' are both dimensionally valid statements. In that, on changing units the expressions still hold.
2. Both e_equal_mc and e_equal_mc' are both dimensionally invalid statements. In particular e_equal_mc does not type-check.

Thus to me there should be a theorem which is true for e_equal_mc2 and e_equal_mc2' and false for e_equal_mc' (let's ignore e_equal_mc as you won't even be able to write it down). That theorem is IsDimensionallyInvariant in PhysLean.

Now, given your implementation, which is something that could be mapped to WithDim _ _ in PhysLean, then IsDimensionallyInvariant e_equal_mc2 should manifestly be true and the proof should ideally be a one-liner.
But IsDimensionallyInvariant e_equal_mc2' should also be true, but since now dimensions aren't being tracked it may be harder to prove this, but it is still possible.

I also reiterate a point I made earlier, I do not see a way to give derivatives or integrals a notion of dimension in your implementation, without just defining it to be true.

[Joseph Tooby-Smith]

BTW if you want to hash this out over Zoom at some point - it may be easier. But no worries if not, also happy to continue here.

[Alfredo Moreira-Rosa]

Yes, i'll try to be there for the next Cafe if i can be available. (i'm in Paris time zone)

[Joseph Tooby-Smith]

Will DM you.

(Edit - cafe organized to discuss this here: #PhysLean > The PhysLean café @ 💬 )

[Alfredo Moreira-Rosa]

edit: sorry i wrote some nonsense. we'll discuss on friday

[Alfredo Moreira-Rosa]

(deleted)

[Joseph Tooby-Smith]

[I fixed a mathematical bias of mine in PhysLean#727 and have renamed IsDimensionallyInvariant to IsDimensionallyCorrect. Also added more examples based on WithDim, with one-line proofs of IsDimensionallyCorrect]

[Alfredo Moreira-Rosa]

So here an example of derivative on quantities, one with proof with an abstraction on quantities and one using mathlib :

-- proof using Quantities lemmas
theorem simp_over_time (t : WithDim Time) (v0 : WithDim Speed) (angle : ℝ) :
    Quantity.deriv (fun t => Real.cos angle • v0 * t) t = ↑(Real.cos angle•v0) := by
  rw [Quantity.deriv_qconst_mul_real]
  · rw [Quantity.deriv_id, Quantity.mul_one]; rfl
  · exact Quantity.differentiable_fun_id

-- proof using only mathlib lemmas
theorem simp_over_time' (t : WithDim Time) (v0 : WithDim Speed) (angle : ℝ) :
    Quantity.deriv (fun t => Real.cos angle • v0 * t) t = ↑(Real.cos angle•v0) := by
  simp [Quantity.deriv, Quantity.cast]
  change deriv (fun t : ℝ => Real.cos angle • v0.val * t) t.val = Real.cos angle * v0.val
  rw [deriv_const_mul]
  · rw [_root_.smul_eq_mul, deriv_id'', mul_one]
  · exact differentiableAt_fun_id

And i defined derivative as this (that i think is correct for single base dimensions or units) :

-- derivative
noncomputable def deriv [NontriviallyNormedField α]
  (f : Quantity d₁ α → Quantity d₂ α) (x : Quantity d₁ α) : Quantity (d₂-d₁) α :=
  ⟨_root_.deriv (fun_to_val f) x.val⟩

[Alfredo Moreira-Rosa]

I think i have another way to prove dimensional inviance that feels more natural to write. The idea is to extract dimension information from the Quantities we want to extract.
Maybe not as powerfull as PhysLean current definition, but feals simpler to me to understand :
image.png

[Alfredo Moreira-Rosa]

You can think of the 𝒟 symbol as dimension of

[Alfredo Moreira-Rosa]

So we just compare dimensions of both sides of the equation.

[Alfredo Moreira-Rosa]

This works on any quantities (units choosen or not)

[Alfredo Moreira-Rosa]

We can still have both defined, since i think mine is less powerful

[Joseph Tooby-Smith]

How is it defined? is it something like :

def 𝒟 {d : Dimension} (a : SI d) : Dimension := d

[Alfredo Moreira-Rosa]

No, it uses a typeclass, but in the end it derives into something like this transitively

[Alfredo Moreira-Rosa]

The typeclass allows to abstract the notion of dimension, so many stacked layers (in my definition, quantities compute dimension, units compute dimensions and dimensions on dimensions are just identity)

[Alfredo Moreira-Rosa]

that's why there is a simp_dim in there, to apply some rules on computing the dimensions and simplifying them.

[Joseph Tooby-Smith]

Ok, this makes sense, thanks for explaining.

Would the following be provable:?

def wrongMul (a : SI Dimension.Time) (b : SI Dimension.Length) :
     SI Dimension.Mass := ⟨a.val * b.val⟩

example (m : SI Dimension.Mass)
    (a : SI Dimension.Time) (b : SI Dimension.Length) :
    𝓓 m = 𝓓 (wrongMul a b) := by sorry

(just trying to understand how things work, and whether or not 𝓓 cares about what makes up the quantity, or just the type of the final quantity itself).

[Alfredo Moreira-Rosa]

No this would not work. Leaving Quantity universe to build a wronful quantity can't be detected with this. That's why i think we should keep yours also.

[Joseph Tooby-Smith]

Ok, good, I understand and I think this is a nice way of phrasing it :).

Though now I am slightly confused why not defining 𝒟 as I did above wouldn't work in exactly the same way as you have defined it?

[Alfredo Moreira-Rosa]

I'm explaining further then.
You see, you can also want to proove things on units and in my library dimensions on units is a computed property :

abbrev UnitChoice := ℚ × Conversion × Dimension

structure Unit where
  _impl : DFinsupp (fun _ : String =>  UnitChoice)
  deriving DecidableEq, BEq

def dimension (u : Unit) : Dimension :=
  u._impl.sum (fun _ qd => qd.2.2)

instance : HasDimension Unit where
  dimension := Unit.dimension

but if you work on dimensions (without units, like in my formal example), the dimensions are not computed :

instance : HasDimension Dimension where
  dimension u := u

is it clearer ?

[Joseph Tooby-Smith]

Ok, I think this is clearer. Thank you for taking the time to explain!

[Alfredo Moreira-Rosa]

Ok, so i made it simpler to proove, now it's just :

theorem kepler_third_law
    (T : SI Dimension.Time) (a : SI Dimension.Length) (M m : SI Dimension.Mass) :
    𝒟 T² = 𝒟 ((4•π^2) • (a³/ (G *(M + m))))  := by
    simp_dim
    module

after simp_dim the goal becomes :

G : SI (Dimension.Length ^ 3 / (Dimension.Mass * Dimension.Time ^ 2))
T : SI Dimension.Time
a : SI Dimension.Length
M m : SI Dimension.Mass
⊢ 2 • Dimension.Time =
  3 • Dimension.Length - (3 • Dimension.Length - (Dimension.Mass + 2 • Dimension.Time) + Dimension.Mass)

by then, module solves the goal directly

[Alfredo Moreira-Rosa]

After some cleanup, i'll be able to have both working :

theorem kepler_third_law_dim_check
    (T : WithDim Dimension.Time) (a : WithDim Dimension.Length) (M m : WithDim Dimension.Mass) :
    𝒟 T² = 𝒟 ((4•π^2) • (a³/ (G *(M + m))))  := by
    simp_dim
    module

theorem kepler_third_law_si_check
    (T : SI Unit.second) (a : SI Unit.meter) (M m : SI Unit.kilogram) :
    𝒟 T² = 𝒟 ((4•π^2) • (a³/ (G *(M + m))))  := by
    simp_dim
    module

[Alfredo Moreira-Rosa]

And by cleanup, i mean, having SI system not be relying upon Float, but be generic on the value (Real, Float, Complex, ...)

[Alfredo Moreira-Rosa]

Didn't need cleanup actually, working like a charm !
https://github.com/ecyrbe/lean-units/blob/main/Examples/formal.lean

[Alfredo Moreira-Rosa]

@Joseph Tooby-Smith so, i'm trying to adapt my lib to physlean, but i got a first issue. You defined change of units only using scales, not affine transformations (so Celsius conversion, Fahrenheit won't work)
Do you think it's possible to come up with a dimension check that would work with affine transformations or you think it's impossible ?
From first analysis, i can't find a way (because affine transformations are not transitive, nor commutative, while scaling only is). But Maybe you have an idea ?

[Joseph Tooby-Smith]

No, I don't know how to do affine transformations. I'm not sure even sure how to make sense of them on pen-and-paper.

For example, something like $E/(Tk_B)$ has no dimensions, which means that it's value does not change if you change the unit of temperature from absolute Celsius (aka kelvin) to absolute Fahrenheit (where 0 absolute Fahrenheit is absolute zero), but its value absolutely does change when you go from ordinary Celsius to ordinary Fahrenheit.

I think maybe when doing dimensional analysis quantities should be thought of as secretly differences in quantities between your chosen value and a given fixed chosen value of zero - which for temperature is usually absolute zero.

[Alfredo Moreira-Rosa]

Ok, good.
I'll try to define an alternative conversion system that only handle scaling and keep the affine one only for computable side of units.

[Tyler Josephson ⚛️]

Joseph Tooby-Smith said:

For example, something like $E/(Tk_B)$ has no dimensions, which means that it's value does not change if you change the unit of temperature from absolute Celsius (aka kelvin) to absolute Fahrenheit (where 0 absolute Fahrenheit is absolute zero), but its value absolutely does change when you go from ordinary Celsius to ordinary Fahrenheit.

The only equation I know of where this matters is Antoine’s Equation. All other cases that I’ve come across use absolute temperature (it’s wrong to use C or F, only use K or R) or use a temperature difference (C and F are okay, but the offset from absolute zero cancels out). https://en.m.wikipedia.org/wiki/Antoine_equation

Antoine is semi empirical; it has weird unit properties, like “all parameters A B and C jointly depend on the choice of units for psat and T.” Unit conversions are possible, but they don’t end up being simple proportions like usual.

[Alfredo Moreira-Rosa]

So, a little feeback on trying to integrate with what Physlean has already done, without taking away key ideas, but trying to generalize them.
So one of the features on lean-units is that there is no fixed set of dimensions, and also no fixed set of units.
this allows for extensibiity, but that maybe not that important to physlean.
Another feature is computability, and i think this one is of use for physicist when exploring a problem. because you can always try to #eval your ideas.

So for the no fixed dimension set feature, when integrating with phylean, two different ideas came to me :

• instead of setting in stone the dimension at the core, fix them at the abstract level. this way, the core stays generic, and only when you want to work with a system of dimensions that you fix them. I have named this, Building a Dimensional System and Unit System.
• the other approach is : instead of trying to fix dimension at any level, don't fix them at all and try to find a generic way to handle scaling, UnitDependent and DimensionallyCorrect.

I'm convinced that the second one is more powerful. So i'm trying to expand on this one. Maybe it will be a failure, i don't know yet. But i have an idea of how to do it.

So one of the nice tricks of PhysLean on DimensionallyCorrect is that you can use Prime Numbers Scales to define another UnitChoices and disprove DimensionallyCorrect.
But i think it can also be used to prove it. Indeed, if you define a One Unit and Prime Unit, you can generate all Unitchoices from them. So maybe just Proving a Scale between One and Prime is sufficient. (maybe i'm wrong, just a conjecture i have). If i'm wrong, i think a counter example should be easilly found.

So if true, i can automate building such a prime scale. Indeed, on lean-units, each dimension is defined by a String, and you can map uniquely a String to a natural number. And for each natural number you can get the nth Prime Number and automate building a Prime UnitChoice for an undefined number of dimensions. And build a generic DimensionallyCorrect system.

So that's the idea, maybe it will prove unfruitful. But it's fun to try.

[Alfredo Moreira-Rosa]

To elaborate the idea, we can build this :

def string_to_nat (s : String) : Nat :=
  (s.toList).foldl (fun h c => h * (UInt32.size+1) + (c.val.toNat + 1)) 0

theorem string_to_nat_inj (s1 s2 : String) :
  s1 = s2 ↔ string_to_nat s1 = string_to_nat s2 := by proof_to_big_to_show_here

noncomputable def prime_from_str (s : String) : Nat :=
  Nat.nth Nat.Prime (string_to_nat s)

theorem prime_from_str_prime (s : String) : (prime_from_str s).Prime := by
  simp only [prime_from_str, Nat.prime_nth_prime]

theorem prime_from_str_inj (s1 s2 : String) :
  s1 = s2 ↔ prime_from_str s1 = prime_from_str s2 := by
  constructor
  · intro h; rw [h]
  · intro h
    have h_enc : string_to_nat s1 = string_to_nat s2 := Nat.nth_injective Nat.infinite_setOf_prime h
    exact (string_to_nat_inj s1 s2).mpr h_enc

[Joseph Tooby-Smith]

Nice! Yeah, I had also thought whether this other side to the prime number thing could be done, and I think it would be possible. It would be awesome if you could make this 'automated'!

Concerning computability. I did have a go making the stuff in PhysLean computable. It involved having a special subset of scalings which are rationals rather than reals, which allows you to define dimensions on floats in addition to reals. I didn't get very far but I think something along these lines should be possible.

[Alfredo Moreira-Rosa]

yes, one of the key proofs will be to show (or disprove) that :
(∀ u1 u2 : UnitChoices, scaleUnit u1 u2 m = m) ↔ (u_one u_prime: UnitChoices, scaleUnit u_one u_prime m = m)
i think i will need help on this one.

[Alfredo Moreira-Rosa]

Finished the PrimeScale automation and created some proofs.

https://github.com/ecyrbe/lean-units/blob/main/LeanUnits/Framework/Dimensions/PrimeScale.lean
https://github.com/ecyrbe/lean-units/blob/main/LeanUnits/Framework/Dimensions/Lemmas.lean

Thank to DFinsupp, It's then just defined as :

noncomputable def PrimeScale (d : Dimension) : ℝ := d._impl.prod PrimeScale.prime_pow

Now the hardest part, defining UnitDependent and DimensionCheck on top of this. Need to think how to do this :)

[Joseph Tooby-Smith]

Awesome! Shouldn't this somehow be a result built upon/from UnitDependent, not the other way around?

[Alfredo Moreira-Rosa]

You may be right. I'll didn't think yet about how to link unitDependent to this yet. I may indeed need to refactor things in the end.

[Alfredo Moreira-Rosa]

One of the nice things i discovered with my previous simple dimension check is that you can disprove also using kernel decidability, making such proofs really small :

theorem not_e_equal_mc_dim_check (E : WithDim Dimension.Energy) (m : WithDim Dimension.Mass) :
   ¬ 𝒟 E =  𝒟 (m * c) := by
    simp_dim
    decide +kernel

[Alfredo Moreira-Rosa]

Some news, i have defined DimentionallyCorrect, not yet tried to use it (to see if it works).
So i have simplified a lot UnitDependant, and renamed it to Scaler with this definition :

class Scaler (M : Type) where
  scale : M → M
  scale_inv: M → M
  scale_inv_scale_cancel : ∀ m, scale_inv (scale m) = m
  scale_inj : Function.Injective scale
  scale_inv_inj : Function.Injective scale_inv

class MulScaler (M : Type) [MulAction α M] extends Scaler M where
  scale_smul : ∀ (r : α) m, scale (r • m) = r • scale m

Indeed, we now only apply scales using a PrimeScale. So u1 and u2 disapear.
Example instance for Quantities based on Dimensions (WithDim) :

noncomputable instance [HasDimension δ] : MulScaler (α:=ℝ) (Quantity d ℝ)  where
  scale q := ⟨(𝒟 q).PrimeScale * q.val⟩
  scale_inv q := ⟨q.val/ (𝒟 q).PrimeScale⟩
  scale_inj := by
    intro q1 q2 h
    simp only [dim_eq_dim, ← val_inj, mul_eq_mul_left_iff] at h
    cases h with
    | inl h1 => apply (val_inj q1 q2).mp h1
    | inr h2 => exfalso; exact Dimension.PrimeScale.scaler_ne_zero h2
  scale_inv_inj := by
    intro q1 q2 h
    simp only [dim_eq_dim, ← val_inj] at h
    apply congrArg ((𝒟 d).PrimeScale * ·) at h
    simp only [div_eq_mul_inv, ← _root_.mul_assoc, _root_.mul_comm, mul_eq_mul_right_iff, val_inj,
      inv_eq_zero, or_self_right] at h
    cases h with
    | inl h1 => exact h1
    | inr h2 => exfalso; exact Dimension.PrimeScale.scaler_ne_zero h2
  scale_inv_scale_cancel q := by
    simp only [dim_eq_dim, ← val_inj]
    rw [_root_.mul_comm,←_root_.mul_div, _root_.div_self,_root_.mul_one]
    exact Dimension.PrimeScale.scaler_ne_zero
  scale_smul := by
    intros r q
    simp only [smul_def, _root_.smul_eq_mul, dim_eq_dim, ← val_inj]
    ring

And dimensionally correct is just :

def IsDimensionallyCorrect {M : Type} [Scaler M] (m : M) : Prop :=
  Scaler.scale m = m

Now crossing fingers this works. i'll have some time this week end to test this. But not that much.

[Joseph Tooby-Smith]

I understand why this definition is simpler to use and computationally would be a lot quicker than UnitDependent. My one unease about this is that it looses the physical meaning behind the class. In UnitDependent the function scaleUnit allowed you to see what happens when you change units from u1 to u2 and therefore had a precise physical meaning.

Really IMHO, it would be better to have your definition of a Scaler as a constructor for a UnitDependent and your IsDimensionallyCorrect as a if and only if statement related to the existing IsDimensionallyCorrect statement. I do not know if this latter one is possible, because it relies on the instances.

[Alfredo Moreira-Rosa]

The issue is, at the moment i can't build a UnitDependent class, i would first need to proove my conjecture to allow a relation between all units and PrimeScales.
I don't know where to start for this one. I would need help from a mathematician.
One other thing is that, i have no UnitChoice really, because, choosing a Unit on my implementation is a deliberate abstracted type, unlike UnitChoice.
Even more so, i can't define a UnitChoice. Because it would mean fixing a set of dimensions to do so.
Defining UnitChoice is the Approach 1 i exposed earlier, where i could define a Dimension System and Unit System on top of my library. Something i tried to evoid for Approach 2.
Let me try this Approach 2, if it prooves unfruitful, i'll go back to Approach 1.

[Alfredo Moreira-Rosa]

So here, Scaler is just a mean to define IsDimensionallyCorrectfor now and test if it works. We'll see after that if we can define another kind of UnitChoice, not the same as yours (can't define an undefined number of axioms for undefined number of units), on top of my Units type

[Tyler Josephson ⚛️]

FYI - we updated our manuscript and posted it here: https://arxiv.org/abs/2509.13142

[Alfredo Moreira-Rosa]

A quick feedback, if you want to have a (somewhat) ok notation for powers with a custom typeclass :

/--
Dependent power operator, allows to have the output type depend on the exponent.
`q ^ᵈ n`:
Examples:
- `q ^ᵈ 2`   -- power with ℕ exponent
- `q ^ᵈ (-2 : ℤ)`   -- power with ℤ exponent
- `q ^ᵈ (1/3 : ℚ)`  -- power with ℚ exponent
-/
class DPow (α : Type u) (β : Type v) (γ : outParam (β → Type w)) where
  pow : α → (n : β) → γ n

infixr:80 " ^ᵈ " => DPow.pow

Example of instanciation :

instance [Pow α ℚ] [SMul ℚ δ] : DPow (Quantity d α) ℚ (fun n => Quantity (n • d) α) where
  pow := ⟨ q.val ^ n ⟩

It may make some of the example equations feel a litle more natural.

[Alfredo Moreira-Rosa]

Hello,

Another week, another quick report of how it's going to try integrating lean-units into PhysLean.
So the definition above of IsDimensionallyCorrect works.
But, proving it is harder than in PhysLean for now. I need to add simp annotations to my PrimeScale lemmas and see if it makes things simpler to prove (like what i did with simp_dim tactic).
I'm also in the process to prove PrimeScale function is injective, thats a way to say that two different Dimensions have two different PrimeScale and vice-versa, making my conjecture a proved theorem.
I proved it on paper (with some holes i'm confident with), so now i need to formalize it (and fill the holes)

:warning: A litle warning, because i'm not sure i explained it very well. My integration means that choosing a unit will no more be an axiom and Space and Time Unit (that are defined like a quantity) will need to be derived from Quantity, not the other way around.
This means certainly some refactoring in Physlean, not sure how big it will be, because i did not look if this API is used all over PhysLean or not.

[Joseph Tooby-Smith]

Space and Time are used all over PhysLean so this would be a big refactor if you mean this, but their units are not currently used very much.

Seeing injectivity of PrimeScale would be very nice.

[Alfredo Moreira-Rosa]

Hello,

Some news to say that i almost finished formalizing injectivity of Primescale, it required proving ℚ-linear indépendance of logarithmic primes. This is something that is missing in mathlib, so i tacled this proof.
This proof is formalized and done (it's bit Big, so i'll eventually refactor it).
I'm now just missing some plumbing to finish Primescale injectivity.
Next, i'll work on a series of PR to merge. And will be able to discuss how to do that.
Maybe a PhysLean café would be nice to discuss this.

[Joseph Tooby-Smith]

Nice! Yeah let's discuss at a PhysLean café - I will organize one now

[Alfredo Moreira-Rosa]

Finished the plumbing of primescale injectivity proof. I'm not a mathlib expert, so the proof looks nice at the higher level, but the lower levels looks kind of messy.
Anyway, here the interresting files :
lemmas about primescale
https://github.com/ecyrbe/lean-units/blob/main/LeanUnits/Framework/Dimensions/Lemmas.lean#L330
lemmas and definitions to build primescale
https://github.com/ecyrbe/lean-units/blob/main/LeanUnits/Framework/Dimensions/PrimeScale.lean
lemmas for ℚ-linear independance of logarithmic primes (rephased to use product instead of logarithmic directly, so that the proof can be used directly)
https://github.com/ecyrbe/lean-units/blob/main/LeanUnits/Framework/Dimensions/Prime.lean

[Alfredo Moreira-Rosa]

So after our discussion, i found a way to make a computable version of nth_prime and have the associated proofs i needed. They are suficienlty simple by using monotonicity and deriving it by a special implementation of next_prime using Nat.find helper lemmas:

Computable nth_prime with proofs

def next_prime (n : ℕ) : Nat.Primes :=
  let prime := Nat.find (Nat.exists_infinite_primes n)
  have hprime : Nat.Prime prime := (Nat.find_spec (Nat.exists_infinite_primes n)).2
  ⟨prime, hprime⟩

theorem next_prime_gt (n : ℕ) : n ≤ (next_prime n).1 := by
  exact (Nat.find_spec (Nat.exists_infinite_primes n)).1

def nth_prime (n : ℕ) (nth : Nat.Primes := ⟨2, Nat.prime_two⟩) : Nat.Primes :=
  if n == 0 then
    nth
  else
    nth_prime (n - 1) (next_prime (nth+1))
termination_by n
decreasing_by
  refine Nat.sub_one_lt ?_
  rename_i h
  rw [beq_iff_eq] at h
  assumption

def nth_prime_nat (n : ℕ) : ℕ := nth_prime n

theorem nth_prime_nat_prime (n : ℕ) : (nth_prime_nat n).Prime := by
  exact (nth_prime n).2

theorem nth_prime_strictmono : StrictMono nth_prime_nat := by
  apply strictMono_nat_of_lt_succ
  intro n
  have hstep : ∀ k (p : Nat.Primes), (nth_prime k p).1 < (nth_prime (k+1) p).1 := by
    intro k p
    induction k generalizing p with
    | zero =>
        simpa [nth_prime] using next_prime_gt (p + 1)
    | succ k ih =>
        rw (occs:=[2]) [nth_prime]
        rw [nth_prime]
        exact ih (next_prime (p + 1))
  exact hstep n ⟨2, Nat.prime_two⟩

theorem nth_prime_nat_inj : Function.Injective nth_prime_nat :=
  nth_prime_strictmono.injective

def prime_from_str (s : String) : Nat :=
  nth_prime_nat (string_to_nat s)

#eval prime_from_str "L" -- 397
#eval prime_from_str "T" -- 443
#eval prime_from_str "M" -- 401
#eval prime_from_str "I" -- 379
#eval prime_from_str "K" -- 389
#eval prime_from_str "N" -- 409
#eval prime_from_str "J" -- 383

[Joseph Tooby-Smith]

Nice! These primes are lower than I was expecting :). Do you know if "in theory" your computable version gives the same numbers as the non-computable one?

[Alfredo Moreira-Rosa]

yes they are exactly the same.

[Ronan Lamy]

Hello! I'm interested in improving units in PhysLean and, in particular, in generalising the framework using typeclasses for dimension systems and/or unit systems, ... so that each application only needs to care about the relevant dimensions. I'm not sure about the status of the integration of lean-units with PhysLean, but hopefully that should make it easier.

Anyway, for now I'm looking at refactoring some of the code in PhysLean.Units. I've found a way to get rid of ModuleCarriesDimension, I'll send a PR soon if that's considered useful.

[Joseph Tooby-Smith]

Hey Ronan, I think anything to simplify the units in PhysLean will in the end make it easier to integrate with lean-units! So I am all for this.

I am curious how you removed ModuleCarriesDimension, the reason I added it (if I recall correctly) was to prevent a typeclass diamond happening. But am happy to wait for a PR to see :).

[Alfredo Moreira-Rosa]

In my impl, i also did not use ModuleCarriesDimension, but because i did not need DimensionFul since Quantity is already generic. I have a HasDimension that looks like CarriesDimension.

[Ronan Lamy]

Alfredo Moreira-Rosa said:

In my impl, i also did not use ModuleCarriesDimension, but because i did not need DimensionFul since Quantity is already generic. I have a HasDimension that looks like CarriesDimension.

Yes, I basically copied that idea - I have:

class HasDim (M : Type) where
  d : Dimension

[Ronan Lamy]

I sent the PR.

[Alfredo Moreira-Rosa]

@Joseph Tooby-Smith does physlean have a notion of experimental measure with an measurement error ?
If so/or not is it something that could be interresting for Quantities to have a Measured Quantity with error threshold ?

[Joseph Tooby-Smith]

No PhysLean doesn't currently have anything along these lines! I would be extremely interested to see something like this.

[Alfredo Moreira-Rosa]

Thanks, i'll do a check of what is the state of the art on this subject and try to bring these ideas to discussion.

[Tyler Josephson ⚛️]

Woukd this be related to regular statistics topics like mean, standard deviation, standard error of the mean, 95% confidence interval, and uncertainty propagation? Much of that would have a home in Mathlib, I would guess.

[Joseph Tooby-Smith]

I guess it would be a combination of both, no? The underlying theory in Mathlib, but the actual quantities of interest in PhysLean or something similar.