Dims and Units for Physics

Stream: Lean for Scientists and Engineers 2024

[Christian Tzurcanu]

I was looking at https://github.com/ATOMSLab/LeanChemicalTheories/blob/main/src/dimensional_analysis/basic.lean

and was a bit unhappy with the ability to extend and write new units. Maybe I did not understand it well enough.

So I offer my own take in Lean 4:

https://github.com/ctzurcanu/lean-measure/blob/main/Measure.lean
maybe will inspire some constructive criticism @Bulhwi Cha

thank you for this course.

[Bulhwi Cha]

I don't have much to comment on your formalization of dimensional analysis, but this approach will prevent a bunch of garbage theorems like force = voltage.

[Christian Tzurcanu]

I was also curious about how to format the repo. if anybody can point me to a good repo of this nature for lean 4..

[Bulhwi Cha]

Did you try lake new <your-project-name> math?

[Christian Tzurcanu]

Bulhwi Cha said:

Did you try lake new <your-project-name> math?

no. but I believe I did that for other projects and it made 9 GB dirs. in that case: what do you recommend I gitignore?

[Bulhwi Cha]

The .lake directory?

[Kevin Buzzard]

If you make a project with lake then the .gitignore should be correct already.

[Christian Tzurcanu]

Kevin Buzzard said:

already

thanks. did not know that. I will reform the repo

[Kevin Buzzard]

It's also true that when you download a fully compiled mathlib the size of the directory will be multiple gigabytes, but most of this will be ignored by git.

[Christian Tzurcanu]

Kevin Buzzard said:

If you make a project with lake then the .gitignore should be correct already.

I hope this is the expected structure of the repo. The file is now at:
https://github.com/ctzurcanu/lean-measure/blob/main/LeanMeasure.lean

[Bulhwi Cha]

Um, the .lake directory should be ignored.

[Christian Tzurcanu]

Bulhwi Cha said:

Um, the .lake directory should be ignored.

I put it in .gitignore and it is still there
any idea what I can do?

[Christian Tzurcanu]

Bulhwi Cha said:

Um, the .lake directory should be ignored.

now I force-deleted it. seemed to work

[Bulhwi Cha]

Christian Tzurcanu said:

I was also curious about how to format the repo. if anybody can point me to a good repo of this nature for lean 4..

You can take a look at my git repository for comparison with yours: https://git.sr.ht/~chabulhwi/lean-notes/tree.

[Christian Tzurcanu]

Bulhwi Cha said:

Christian Tzurcanu said:

I was also curious about how to format the repo. if anybody can point me to a good repo of this nature for lean 4..

You can take a look at my git repository for comparison with yours: https://git.sr.ht/~chabulhwi/lean-notes/tree.

that's what I needed! thanks.

[Christian Tzurcanu]

@Tyler Josephson ⚛️ First: thank you for the course

Question: Would this library be of any use for ATOMSLab? Should I extend it with SI derived units?

If I extend it to SI, it may be able to do "canonization" that is: always find the accepted dimension and unit that fit the Measure instance after each operation.

Another way of extending it would be with "Scalar modifiers" like Decimal.mega = 10^6 represented by prefix "M" etc.

[Tyler Josephson ⚛️]

Cool! Yes, i think the community will benefit from implementation of dimensions and units in Lean. As you see in our repo, we only implemented dimensions (and proofs about them), not units.

I’m traveling for a conference now, but will look at what you’re working on soon.

Here’s another thread on Zulip discussing this:

https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/defining.20the.20force.20applied.20to.20a.20mass.20pulling.20a.20string

[Christian Tzurcanu]

Tyler Josephson ⚛️ said:

Cool! Yes, i think the community will benefit from implementation of dimensions and units in Lean. As you see in our repo, we only implemented dimensions (and proofs about them), not units.

I’m traveling for a conference now, but will look at what you’re working on soon.

Here’s another thread on Zulip discussing this:

https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/defining.20the.20force.20applied.20to.20a.20mass.20pulling.20a.20string

that is exactly what is needed: a place for each Lean concept to collaborate/chat for the benefit of that concept

[Tyler Josephson ⚛️]

@Colin Jones ⚛️ and @Max Bobbin are writing up a manuscript describing what we did before (just got sidetracked helping me put together LfSE). Hopefully have that polished up soon for sharing.

[Tyler Josephson ⚛️]

Here’s another thread:

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Defining.20a.20Type.20with.20multiple.20zeros

[Tyler Josephson ⚛️]

And maybe the oldest thread on this is here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Dimensional.20Analysis.20Community.20Input

(We started this before the Lean 4 port was finished)

[Christian Tzurcanu]

Thanks. it will take me a while to read those.
And I already have questions. I will read all and then ask there.

[Christian Tzurcanu]

Tyler Josephson ⚛️ said:

Colin Jones ⚛️ and Max Bobbin are writing up a manuscript describing what we did before (just got sidetracked helping me put together LfSE). Hopefully have that polished up soon for sharing.

I was unable to follow the discussion. Especially I tried to set my system as monoid_algebra and failed.

But today I have added the base and derived SI units and some important constants.

This system has already some nice properties: for example, it can find in the SI what other measures have the same nature as yours and return the list.

I also have trouble setting HMul and other like operations for Measure. Was successful in setting them for Quality...

Reaching the end of what I can do at my present level of knowledge.