Math physics in Lean

Stream: new members

[Kevin Sullivan]

One of the main use cases for abstract math is physics. Suppose I want to do physics formally using Lean. One of the mathematical structures I'd like to work with is that of the real Euclidean space. Can you help me understand how close or far we are from being able to represent real Euclidean spaces in Lean, including objects such as points and vectors, operations such as vector-vector and point-vector addition, and transformations such as rigid body motions and affine transformations more generally? (Beneath this question lies the fact that, for me at least, without many examples, it's hard to know what I can do with the bits and snippets I find out there, e.g., reals as Cauchy sequences, etc.)

[Mario Carneiro]

right now we are fairly close, but we are still working in some ridiculous generality

[Mario Carneiro]

we have normed vector spaces, but not much about finite dimensional vector spaces and even less about R^n specifically

[Kevin Sullivan]

we have normed vector spaces, but not much about finite dimensional vector spaces and even less about R^n specifically

Mario, Thanks. Do you have any guidance on how to gain an understanding of (1) what's already done---if only what files to look at, but better yet some applications that use them, or even better yet, papers about them, (2) what would need to be done to get to the point where we could model finite Euclidean spaces, particularly over the reals, even if only as a special case?

[Kevin Buzzard]

I would just fire up a new file and start writing. All the infrastructure you need should be there, as far as I know, it's just that nobody really did $\mathbb{R}^n$ yet.

[Kevin Buzzard]

They're not keen on all these concrete examples ;-)

[Kevin Buzzard]

You might find that $\mathbb{R}^n$ automatically becomes a real vector space, so a bunch of what you're hoping to find might just magically appear.

[Kevin Buzzard]

Feel free to ask questions -- I think this is a very attainable goal.

[Kevin Buzzard]

import data.real.basic algebra.pi_instances

def ℝspace (n : ℕ) := fin n → ℝ

instance (n : ℕ): add_comm_group (ℝspace n) := by unfold ℝspace; apply_instance
noncomputable instance (n : ℕ): vector_space ℝ (ℝspace n) := by dunfold ℝspace; apply_instance

variables (n : ℕ) (v w : ℝspace n) (r : ℝ)

#check v + w -- adding vectors
#check r • v -- scalar times vector

[Johan Commelin]

@Kevin Sullivan Further tips: the search function on Github and in VScode can be really useful. If those fail, just ask about a specific concept here, and we'll be able to tell you if it's in the library. You will hit things that are missing quite soon. But it is hard to tell what they are without starting out on a Lean file.

[Kevin Buzzard]

And feel free to change the name of Rspace! I just had to write something...

[Kevin Sullivan]

And feel free to change the name of Rspace! I just had to write something...

Thank you, Kevin, Johan, Mario. I'm working through your suggestions. A question comes up. What is the conceptual difference between field and discrete_field? The latter is a term I perhaps should know but don't know from my limited studies of algebra.

[Keeley Hoek]

I think the rule is discrete_field is a maths field and we should all pretend field doesn't exist (and we'd change the name if it wasn't in core).

[Kevin Sullivan]

Ok, I see.

[Kevin Sullivan]

And feel free to change the name of Rspace! I just had to write something...

Ok, so I have started typing. The aim is to develop at least a formal sketch of a formalization of affine spaces. Here's how I started, and I immediately ran into a few questions, which I pose here.

You will recall that an affine space comprises a vector space V over a field K and a nonempty set, A, of points, with an addition operation, + : point -> vector -> point, satisfying a few axioms (e.g., \all p, p + 0 = p). My implementation strategy is to build on what's already in the libraries. So here's how I started.

class affine_space
    (P : Type)                                                  -- points
    (K: Type) [discrete_field K]               -- scalars
    (G : Type) [add_comm_group G]    -- vectors
    (V : vector_space K G) :=                     -- K vector space over G
(add : P → G → P)

I initially typed "add : P → V → P", but of course V isn't a type. On the other hand, P → G → P looks odd. Indeed, even the presence of G in my definition seems a bit weird, as mathematical texts would not mention additive groups when defining affine spaces. So, question #1: does "add : P → G → P" look right? I'd like to be sure that I start with a sound typeclass specification before building all the rest of it.

Question #2: I've chosen to use "has-a" relations rather than "is-a", (using object-oriented lexicon), to define affine_space. By this I mean that I incorporate P, K, G, and V as field values rather than by using "extends" to "inherit" these structures. The rational is that an affine space "has a" vector space but not "is a" vector space. So does the structure I've defined "look right" to those of you who design these kinds of libraries?

Thank you!
Kevin

[Mario Carneiro]

Q1: The convention would be to call G V, and call V nothing (put it in square brackets)

[Kevin Sullivan]

Q1: The convention would be to call G V, and call V nothing (put it in square brackets)

Perfect, thank you.

[Reid Barton]

And P would probably go last

[Johan Commelin]

Unfortunately we only have mul_action... so you can't use that class (in a clean way).

[Johan Commelin]

It would probably make sense to setup a general theory of torsors... and then define an affine space to be a torsor of a vector space.

[Johan Commelin]

You would be able to reuse the general setup for things like quantities (mass, length, &c are torsors under units real). I'm far from being a (mathematical) physicist, so I have no idea if that would be useful.

[Neil Strickland]

Let's ignore for the moment the fact that you want to use additive notation. Then the natural thing would be to start with the class mul_action G X from src/group_theory/group_action.lean, and extend it to give a class principal_action involving a "division" map X → X → G such that (y / x) • x = y. You might need some other axioms, or they might follow automatically, especially in the case where G is a group. Then you could specialise to the case where G is the additive group of a vector space.

It's also possible to leave G out of the picture and axiomatize everything in terms of the subset of parallelograms in X ^ 4; then you recover G as a quotient of X ^ 2.

Ideally we should have a class for additive actions that is magically connected to the class for multiplicative actions, so we don't have to prove essentially the same results twice. We have similar things in some closely related contexts, but not this one. But it would not be hard for you to define add_action by hand, just following the example of mul_action.

[Johan Commelin]

The reason I did not define add_action is notation...

[Johan Commelin]

We can't reuse + for these, even though that would be very natural.

[Kevin Sullivan]

I'm listening. I've incorporated comments down through Reid Barton's to arrive at the following. But I'm open to reworking it entirely in light of the subsequent comments. Feedback sought on both the current formulation, as well as on the subsequent comments. My overall aim is to develop a formalization in terms of which to express mathematical physics, starting with the classical (Newtonian) case.

class affine_space
    (K: Type) [discrete_field K]
    (V : Type) [add_comm_group V] [vector_space K V] :=
    (P : Type)
(add : P → V → P)
(right_zero : ∀ (p : P), add p 0 = p)
(add_assoc : ∀ (p : P), ∀ (a b : V), add (add p a) b = add p (a + b))
(unique : ∀ (p q : P), ∃ (a : V),
            (q = add p a) ∧
            (∀ (a b : V), (q = add p a) → (q = add p b) → a = b))

[Mario Carneiro]

unique has a name clash in the variables

[Mario Carneiro]

also don't use /\ in an axiom if you can avoid it - use two axioms

[Reid Barton]

You probably want to replace unique anyways with a second operation sub : P -> P -> V and whatever axioms are necessary to characterize it uniquely

[Mario Carneiro]

^ that

[Reid Barton]

∀ (p : P), ∀ (a b : V), can be simply ∀ (p : P) (a b : V),

[Reid Barton]

but now this is getting into just style things

[Kevin Sullivan]

but now this is getting into just style things

So here's where I've gotten to.

class affine_space
    (K: Type) [discrete_field K]
    (V : Type) [add_comm_group V] [vector_space K V] :=
    (P : Type)
(add : P → V → P)
(right_zero : ∀ (p : P), add p 0 = p)
(add_assoc : ∀ (p : P) (a b : V), add (add p a) b = add p (a + b))
(sub : P → P → V)
(sub_exists : ∀ (p q : P), ∃ (a : V),  a = sub q p)
(sub_unique : (∀ (p q : P) (a b : V), (q = add p a) → (q = add p b) → a = b))

I can work the details of the axioms from here. I guess the remaining pending question is whether this is a good start on an affine space library or whether to revert to a more general theory of torsors with the affine space case as a special case. Or to go with the suggestion by Neil Strickland. The torsor direction is intriguing as our aim is to formalize aspects of physics and metrology, and, indeed, things like time, location, and voltage are torsors. I don't have a strong intuition for how hard it'd be to go in this direction given what's already in the libraries, nor what tradeoffs would be involved in eventually using such a formalization as a target for a physical denotational semantics of programming code (which is where we're headed with this work). Comments/thoughts welcome.

[Kevin Sullivan]

It would probably make sense to setup a general theory of torsors... and then define an affine space to be a torsor of a vector space.

Is something like this what you had in mind?

class torsor
    (G : Type) [add_group G]
    (X : Type) [inhabited X] :=
(add : G → X → X)
(left_zero : ∀ (x : X), add 0 x = x)
(add_assoc : ∀ (g1 g2 : G) (x : X), add (g1 + g2) x = add g1 (add g2 x))
(sub : ∀ (x1 x2 : X), ∃ d, x2 = add d x1)
(sub_unique : ∀ (g1 g2 : G) (x1 x2 : X), x2 = add g1 x1 → x2 = add g2 x1 → g1 = g2)

class affine_space
        (K: Type)  [discrete_field K]
        (V : Type) [add_comm_group V] [vector_space K V]
        (P : Type) [inhabited P]
    extends torsor V P

[Mario Carneiro]

sub still isn't a function... are you expecting to be able to define the function after the fact?

[Mario Carneiro]

that's how it's done in maths but in lean it doesn't work as well

[Reid Barton]

From a math (or a mathlib) perspective it certainly makes sense to define torsors in general and then define affine spaces as torsors over a vector space. But if you're just prototyping for now then there's no need to try to do everything in maximal generality from the start.

[Reid Barton]

(Warning: mathematician, not a physicist)
The way I eventually learned to think about units is as independent ways in which we believe physics is scale-invariant. For example in Newtonian physics I guess there are seven independent "dimensions" (not sure what the official term is), one per SI unit: time, length, mass, charge and so on. Each of these corresponds to a separate action of units real (or what a mathematician would call G_m) on physical quantities, so that all together we have actions of units real x ... x units real. For example a length is a vector in the vector space on which the copy of units real corresponding to length acts in the tautological way ($t$ acts by multiplication by $t$), and all the other copies act trivially.

[Reid Barton]

If we call this representation $L$, then a "length squared" is a vector in $L \otimes L$, which is again one-dimensional over the reals but has the action of length scaling where $t$ acts as multiplication as $t^2$.
In this way time, length, etc. are quantities that belong to non-isomorphic representations of the big group (units real)^7, so there is no way that you can confuse them.

[Kevin Sullivan]

sub still isn't a function... are you expecting to be able to define the function after the fact?

Oops. How's this?

class torsor
    (G : Type) [add_group G]
    (X : Type) [inhabited X] :=
(add : G → X → X)
(left_zero : ∀ (x : X), add 0 x = x)
(add_assoc : ∀ (g1 g2 : G) (x : X), add (g1 + g2) x = add g1 (add g2 x))
(diff_exists : ∀ (x1 x2 : X), ∃ d, x2 = add d x1)
(diff_unique : ∀ (g1 g2 : G) (x1 x2 : X), x2 = add g1 x1 → x2 = add g2 x1 → g1 = g2)
(sub : X → X → G)
(sub_add : ∀ (x1 x2 : X), add (sub x2 x1) x1 = x2)

[Johan Commelin]

diff_exists is now redundant. And you can rephrase diff_unique using sub, I guess.

[Neil Strickland]

Here's a similar but slightly different perspective. The special relativity model says that spacetime is an affine space V. This can be formulated in terms of parallelograms, which are quadruples of events that can be characterised by certain idealised physical properties. The parallelogram structure gives an equivalence relation on V × V with quotient T say, and gives a vector space structure on T. Experimental properties characterise the light cone C ⊂ T and divide T \ C into subsets T₊, T₋ and T₀ of future, past and spacelike vectors. Let L' be the space of homogeneous quadratic functions on T that vanish on the light cone. This is one-dimensional and has a canonical half-space of forms that are positive on timelike vectors. This gives us a canonical oriented square root L with L ⊗ L = L', and measurements of time and distance naturally take values in L. (In this framework, times and distances are automatically identified via the speed of light.)

[Kevin Sullivan]

diff_exists is now redundant. And you can rephrase diff_unique using sub, I guess.

Edited as follows:

class torsor
    (G : Type) [add_group G]
    (X : Type) [inhabited X] :=
(add : G → X → X)
(left_zero : ∀ (x : X), add 0 x = x)
(add_assoc : ∀ (g1 g2 : G) (x : X), add (g1 + g2) x = add g1 (add g2 x))
(sub : X → X → G)
(add_diff : ∀ (x1 x2 : X), add (sub x2 x1) x1 = x2)
(diff_unique : ∀ (g1 g2 : G) (x1 x2 : X), g1 = sub x2 x1 → g2 = sub x2 x1 → g1 = g2)

Any comments on field names vs prevailing conventions?

[Kevin Sullivan]

Here's a similar but slightly different perspective. The special relativity model says that spacetime is an affine space V. This can be formulated in terms of parallelograms, which are quadruples of events that can be characterised by certain idealised physical properties. The parallelogram structure gives an equivalence relation on V × V with quotient T say, and gives a vector space structure on T. Experimental properties characterise the light cone C ⊂ T and divide T \ C into subsets T₊, T₋ and T₀ of future, past and spacelike vectors. Let L' be the space of homogeneous quadratic functions on T that vanish on the light cone. This is one-dimensional and has a canonical half-space of forms that are positive on timelike vectors. This gives us a canonical oriented square root L with L ⊗ L = L', and measurements of time and distance naturally take values in L. (In this framework, times and distances are automatically identified via the speed of light.)

Neil,

Thank you for your suggestion. For formalizing basic metrology (units of measure) and classical dynamics, my guess is that the formalization of the ordinary definition of torsors and affine spaces as torsors over vector spaces will suffice. However, we mean to develop a physical semantics of code for cyber-physical systems in general, eventually to include systems that are subject to relativistic effects (satellites, space missions, etc). We might well circle back around to the path you suggest. In the meantime I will try to acquaint myself with the material you highlight. Thank you.

[Mario Carneiro]

diff_unique is now just transitivity

[Mario Carneiro]

I think what you could say is add g x = y <-> sub x y = g

[Mario Carneiro]

or you could express it as the two cancellation laws add (sub x y) y = x and sub (add g x) x = g