Zulip Chat Archive

Stream: new members

Topic: Some olympiad formalisations


view this post on Zulip Joseph Myers (Apr 18 2020 at 18:30):

As a first exercise in formalisation after Kevin's natural number game and Lean maths challenges, I tried formalising solutions to some problems from this year's British Mathematical Olympiad round 2. A couple of questions that arose from this. (a) In the course of those formalisations I found I wanted various trivial lemmas that I couldn't locate in mathlib, but that seemed of more general relevance than just those particular olympiad problems; see p1_lemmas.lean, p3_lemmas.lean and p4_lemmas.lean at the link. Are some of those actually in mathlib in a different form, or do any of them belong there? (b) The proof of problem 3 (p3.lean) got very bogged down proving trivialities. Are there key Lean tricks I'm missing that could make it, say, five times shorter (which would still be longer than either of the other proofs there)?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 19:08):

Thanks for mentioning this stuff here Joseph, I know you told me about it weeks ago but I've been focusing on other things.

view this post on Zulip Scott Morrison (Apr 18 2020 at 23:20):

I only briefly skimmed your lemmas, but mostly these look useful and appropriate for mathlib.

view this post on Zulip Scott Morrison (Apr 18 2020 at 23:20):

I'd double check on some of the simpler ones that library_search doesn't find any matches.

view this post on Zulip Scott Morrison (Apr 18 2020 at 23:21):

and then start PR'ing them. It's probably best to do them in small chunks, as it makes it more likely that the relevant reviewer who knows the file the lemmas belong in will have time to check them.

view this post on Zulip Scott Morrison (Apr 18 2020 at 23:22):

(But my first impression is that everything was written nicely, and had good mathlib-style names, so PRing should be pretty straightforward, beyond looking for existing matches.)

view this post on Zulip Joseph Myers (Apr 19 2020 at 15:47):

OK, I've filed PR #2460 for some of the modular arithmetic lemmas after checking with library_search. Though as library_search is very sensitive to the exact form in which a lemma is stated, it's quite possible something very similar is already present. (E.g. at one point in doing these formalisations I wanted the name of the lemma that turns out to be nat.add_mul_div_right, but because I had the additions the other way round, library_search didn't find it.) I left out one of the modular arithmetic lemmas from this PR, both because it's more complicated and because I got a mysterious timeout after updating to the latest Lean and mathlib. Why does this code timeout on use (but not if existsi is used instead, or with different imports)? This is with Lean 3.9.0, mathlib commit 99245b33741b6b3adc6832858c88e7b0ce2de519, and didn't appear with Lean 3.8.0, mathlib commit d2db3e831a8f8e20564e7c702409bd3bdda691f5.

-- This import is needed; the timeout does not appear with "import tactic" instead.
import data.int.basic

lemma mod_mul_eq_cases (n : ) (a : ) (b : ) (c : ) (hbpos : 0 < b) (hcpos : 0 < c)
  (hmod : n % b = a) :
   d : , 0  d  d < c  n % (c * b) = a + d * b :=
begin
  use ((n % (c * b)) / b), -- Times out (works with "existsi")
  sorry
end

view this post on Zulip Joseph Myers (Apr 28 2020 at 20:15):

Having got a first few batches of lemmas intro mathlib, a couple of followup questions.

  1. One of the lemmas I have is one where the statement seems reasonable for mathlib, but the proof I have surely isn't.
import data.real.cardinality

/-- Any open interval of reals is uncountable. -/
lemma not_countable_real_Ioo {k1 k2 : } (h : k1 < k2) :
  ¬ set.countable (set.Ioo k1 k2) :=
begin
  sorry
end

The proof I have (in p4_lemmas.lean) deducing this from not_countable_real is about as long as the whole of data.real.cardinality once you include the auxiliary lemmas. Maybe someone can see a much simpler proof of this and can PR that to mathlib instead?

  1. I only formalised solutions to three of the four problems on the paper because the other one is geometry and mathlib doesn't have any Euclidean geometry. I know there have been various attempts at Euclidean geometry in Lean, are there any plans to add it (at least basic definitions) to mathlib? (I tend to think the natural starting point is the definition of a Euclidean space as an affine space whose associated vector space is a finite-dimensional real inner product space. mathlib has real inner product spaces, but not affine spaces.)

view this post on Zulip Reid Barton (Apr 28 2020 at 20:27):

For 1, it would be nice to know that an open interval is homeomorphic to ℝ anyways, from which the uncountability follows. (Maybe @Sebastien Gouezel knows whether we have this already?)

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:28):

For 2, I don't know of any plans to add Euclidean geometry to mathlib. But PRs are welcome!

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:29):

Not having affine spaces is really really sad, especially now calculus is very advanced in the wrong direction (using linear spaces everywhere instead of affine spaces)

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:29):

For 1. I would guess that it is not too hard to show that the interval Ioo a b is uncountable if the unit interval Ioo 0 1 is.

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:30):

I tried to define affine spaces a very very long time ago, but I never managed to get elaboration to cooperate.

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:30):

And we know that exp is injective. So R injects into the positive reals. That's also only a couple of lines.

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:31):

Then you apply negation, and another exp.

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:31):

We know that exp is monotone as well, I htink.

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:34):

Library-wise I don't think we should look for a tricky proof. We need to make sure we have an bijection from R to any nonempty open interval

view this post on Zulip Reid Barton (Apr 28 2020 at 20:35):

The library should have (a) (0,1)(a,b)(0, 1) \cong (a, b) for any a<ba < b, (b) https://en.wikipedia.org/wiki/Sigmoid_function or similar.

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:36):

Hmmm, didn't @Sebastien Gouezel do the sigmoid function, or something similar?

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:36):

Assuming of course \cong means diffemorphism.

view this post on Zulip Reid Barton (Apr 28 2020 at 20:36):

Oh I guess I always thought that the sigmoid function specifically meant what that page calls the logistic function, but the point is we should have at least one such function which also has some other utility.

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:38):

Oooh, I was thinking of

src/analysis/calculus/specific_functions.lean:
The real function `exp_neg_inv_glue` given by `x ↦ exp (-1/x)` for `x > 0` and `0`

view this post on Zulip Reid Barton (Apr 28 2020 at 20:38):

There is exp_neg_inv_glue, but this is a bit different (and more difficult)

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:40):

But exp_neg_inv_glue would also do the trick, right?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:40):

For 2, one has to think about how to formalise a general Euclidean geometry question. If it says something like "Let ABC be a triangle, now construct D,E,F,G,H and prove that ABDH all lie on a circle" then you can either use a coordinate approach or a synthetic approach. There has been a lot of work towards getting the synthetic approach to work in a theorem prover, including some serious stuff done in Coq (some links here). I had a student formalise a load of stuff in Lean here but they didn't document what they did so the code is impenetrable.

view this post on Zulip Sebastien Gouezel (Apr 28 2020 at 20:41):

I don't think we have the sigmoid (and I just learned this name). But it would be very easy to do.

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:41):

And then we can claim Lean does AI

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:41):

Sébastien, this fancy sigmoid name is AI

view this post on Zulip Alastair Horn (Apr 28 2020 at 21:47):

I'm interested in formalising (e.g. olympiad) Euclidean geometry in Lean and I would love to learn from/contribute to any project related to this, something like Geocoq perhaps?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:58):

Geocoq is synthetic, right?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:58):

I was going to have a student look at this this summer but my plans are now a bit up in the air.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:59):

It's one thing formalising the theorems, it's another to make the tactics which prove them automatically

view this post on Zulip Alastair Horn (Apr 28 2020 at 22:10):

Assuming I understand what synthetic is, then yes I believe it is since it's based off Tarski's axioms

view this post on Zulip Reid Barton (Apr 28 2020 at 22:10):

Johan Commelin said:

But exp_neg_inv_glue would also do the trick, right?

It does one trick (via Cantor-Schroeder-Bernstein) but not all tricks.

view this post on Zulip Alastair Horn (Apr 28 2020 at 22:22):

I suppose a synthetic approach wouldn't be appropriate for mathlib, since nothing else would really depend on it. Though synthetic would presumably be the logical choice for a formalisation of Olympiad geometry.

view this post on Zulip Joseph Myers (Apr 29 2020 at 00:11):

After writing the definition in terms of affine spaces, a natural starting point to make it usable might include proving lots of basic geometrical facts (both n-dimensional and 2-dimensional), including Tarski's axioms. At that point you could use either approach for proving further geometrical results. (To do coordinate proofs you'd also want functions of the form "choose a frame with these properties", like "let A be (0, 0) and B be (c, 0)".) Of course the reverse direction (constructing an affine space over a real inner product space from a structure satisfying Tarski's axioms) is also a theorem that could be proved.

view this post on Zulip Joseph Myers (Apr 29 2020 at 00:16):

I tend to find combinatorial geometry more interesting than the "here's a construction for a long sequence of points" type of problem, and synthetic geometry reasoning seems less often relevant for combinatorial problems.

view this post on Zulip Joseph Myers (Apr 29 2020 at 00:21):

I haven't tried defining any type classes in Lean, so don't know what would go wrong in a naive attempt to implement the definition of affine spaces and define Euclidean spaces on top of that. (But implementing it in terms of additive group actions would run into mathlib not having additive group actions, and I certainly don't understand the to_additive machinery for converting things between multiplicative and additive groups.)

view this post on Zulip Joseph Myers (May 17 2020 at 16:57):

I tried writing definitions of affine and Euclidean spaces (in the same repository as before), to see if I could get to the point of being able to state and prove the geometry problem on the paper I was formalising.

Although I proved very little to do with affine spaces, Lean didn't seem to have any particular problems with the definitions once I made types explicit in more places than might be ideal (otherwise it can't e.g. deduce the correct type of vectors for a subtraction of points to produce a vector). Should some such minimal definitions of affine and Euclidean spaces (whether or not these particular definitions) go in mathlib as a basis for any further work people wish to do in that area, even if many basic things people would want when using the definitions are likely missing?

But I ran into type class issues working with Euclidean spaces. I have a metric_space instance for affine spaces over normed spaces, but Lean won't deduce a metric space structure for Euclidean spaces from that. Here's a simplified self-contained example.

import analysis.normed_space.real_inner_product
import linear_algebra.basis

noncomputable theory

class has_vadd (V : Type*) (P : Type*) :=
(vadd : P  V  P)
(vsub : P  P  V)

def vadd {V : Type*} {P : Type*} [has_vadd V P] : P  V  P := has_vadd.vadd
def vsub {V : Type*} {P : Type*} [has_vadd V P] : P  P  V := has_vadd.vsub

infix `+`:65 := vadd
infix `-`:65 := vsub

class affine_space (k : Type*) (V : Type*) (P : Type*) [field k] [add_comm_group V]
    [vector_space k V] [nonempty P] [has_vadd V P] :=
(vadd_assoc :  (p : P) (v1 v2 : V), p + v1 + v2 = p + (v1 + v2))
(vadd_vsub :  (p1 p2 : P), p1 + (p2 - p1 : V) = p2)
(vsub_vadd :  (p : P) (v : V), p + v - p = v)

instance affine_space_has_dist (k : Type*) (V : Type*) (P : Type*) [normed_field k]
    [normed_group V] [normed_space k V] [nonempty P] [has_vadd V P] [affine_space k V P] :
  has_dist P :=
{ dist := λ x y, (x - y : V) }

class euclidean_vector_space (V : Type*) [inner_product_space V] [finite_dimensional  V]

class euclidean_affine_space (V : Type*) (P : Type*) [inner_product_space V]
    [finite_dimensional  V] [euclidean_vector_space V] [nonempty P] [has_vadd V P]
    [affine_space  V P]

variables (V : Type*) {P : Type*} [inner_product_space V]
    [finite_dimensional  V] [euclidean_vector_space V] [nonempty P] [has_vadd V P]
    [S : affine_space  V P] [euclidean_affine_space V P]

instance euclidean_affine_space_has_dist : has_dist P := @affine_space_has_dist  V P _ _ _ _ _ S

And this is the error from that last instance (where the @ and naming the affine space instance are just to get a more verbose error):

37:59: type mismatch at application
  affine_space_has_dist  V P
term
  S
has type
  @affine_space  V P real.field (@inner_product_space.to_add_comm_group V _inst_1)
    (@inner_product_space.to_module V _inst_1)
    _inst_4
    _inst_5
but is expected to have type
  @affine_space  V P (@normed_field.to_field  normed_field.normed_field)
    (@normed_group.to_add_comm_group V (@inner_product_space_is_normed_group V _inst_1))
    (@normed_space.to_module  V normed_field.normed_field (@inner_product_space_is_normed_group V _inst_1)
       (@inner_product_space_is_normed_space V _inst_1))
    _inst_4
    _inst_5

What's the right way to get those instances to match up, without causing problems later? (The metric space instance itself seems quite fragile; it "works" in the form I have it in the repository, in the sense that Lean accepts the proofs of metric space axioms, but if I have a slightly different set of type class instances visible when it's defined I get problems with e.g. norm_zero not working because the two sides of the equation have found different paths to add_comm_group and has_zero.)

view this post on Zulip Johan Commelin (May 17 2020 at 17:12):

Would it be an idea to add the metric to the definition of euclidean space?

view this post on Zulip Johan Commelin (May 17 2020 at 17:12):

Just like the definition of a metric space includes an entire topology

view this post on Zulip Johan Commelin (May 17 2020 at 17:13):

You could then define a custom "minimalist" constructor that builds all the "redundant" info from some core data

view this post on Zulip Patrick Massot (May 17 2020 at 17:16):

There are two separate issues issues. First the issue of affine spaces. You don't include the minimal test case: are you able to define affine maps between affine spaces (without having @ all over the place)?

view this post on Zulip Joseph Myers (May 17 2020 at 17:16):

I was trying to make it more general, since the metric space structure doesn't need anything more than a norm on the underlying vector space so can apply to affine spaces that aren't Euclidean spaces. But I can see if a less general version works.

view this post on Zulip Joseph Myers (May 17 2020 at 17:17):

Affine maps are on the long list of things that obviously ought to be added for a more complete implementation of affine spaces.

view this post on Zulip Patrick Massot (May 17 2020 at 17:18):

Then the metric space issue. Here Johan already explained the main trick, but there are a lot more details at https://hal.inria.fr/hal-02463336v2/document

view this post on Zulip Patrick Massot (May 17 2020 at 17:18):

Joseph, I strongly recommend you try to define affine maps very soon. This is a cruel test.

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:20):

The problem I think is that inner_product_space.to_module and normed_space.to_module are making different module structures.

view this post on Zulip Joseph Myers (May 17 2020 at 17:50):

I've added a definition of affine maps (and the composition of two affine maps, but not tried to do anything more with them).

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 17:54):

I'd define def Point := real × real and introduce inner_product_space on it.

view this post on Zulip Patrick Massot (May 17 2020 at 17:54):

I tried this long before the fashion of bundled maps began, so maybe things are easier now (although you will face coercion to function hell if you go that way). I also used + without subscript at that time. Maybe this was too much for Lean.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 17:56):

Then define lines, circles etc, and prove standard properties.

view this post on Zulip Joseph Myers (May 17 2020 at 19:33):

@Johan Commelin, including the distance and a requirement that it agrees with the norm worked for defining Euclidean spaces (and then deducing a metric space instance on them, rather than needing to bundle everything about the metric space properties in the Euclidean space definition).

@Yury G. Kudryashov, I'm trying to implement the abstract definition of a Euclidean space from Wikipedia. I then have an instance euclidean_affine_space (fin n → ℝ) (fin n → ℝ) to put an n-dimensional Euclidean space structure on fin n → ℝ. Yes, concepts such as lines (= affine subspaces of dimension 1), circles etc. will need defining to do much geometry.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:37):

What's wrong with a real inner product space?

view this post on Zulip Joseph Myers (May 17 2020 at 19:37):

I do at least now have Pythagoras (one entry on the hundred-theorems list) for three points in a Euclidean affine space.

lemma dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two (p1 p2 p3 : P) :
  dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 
     V p1 p2 p3 = real.pi / 2 :=

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:38):

This is true in any real inner product space

view this post on Zulip Joseph Myers (May 17 2020 at 19:40):

Only that points and vectors between points are generally thought of as different things in geometry, i.e. it's more precisely typed to state geometry theorems in the Euclidean affine space context.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:43):

What is your current definition?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:43):

I mean, the main class

view this post on Zulip Joseph Myers (May 17 2020 at 19:44):

/-- A `euclidean_vector_space V` is a finite-dimensional real inner
product space structure on the vectors `V`. -/
class euclidean_vector_space (V : Type*) [inner_product_space V] [finite_dimensional  V]

/-- A `euclidean_affine_space V P` is an affine space with points `P`
over a `euclidean_vector_space V`. We bundle the distance and require
it to be the same as results from the inner product. -/
class euclidean_affine_space (V : Type*) (P : Type*) [inner_product_space V]
    [finite_dimensional  V] [euclidean_vector_space V] [nonempty P] [has_dist P] [has_vadd V P]
    [affine_space  V P] :=
(dist_eq_norm_vsub :  (x y : P), dist x y = (x - y : V))

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:46):

Note that many theorems will not need finite_dimensional.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:46):

So I'd drop it.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:46):

And add as an additional requirement on V when actually needed.

view this post on Zulip Joseph Myers (May 17 2020 at 19:48):

It's part of the standard definition (that I took from Wikipedia), but I agree it will rarely be needed. Even things that need being finite-dimensional will often work in a finite-dimensional subspace of an infinite-dimensional space.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:49):

Instead of a typeclass euclidean_vector_space, you can define euclidean_space n to be fin n → real and introduce an inner_product_space instance on euclidean_space n.

view this post on Zulip Patrick Massot (May 17 2020 at 19:50):

I don't understand why you say that Yury

view this post on Zulip Joseph Myers (May 17 2020 at 19:51):

E.g. to define the circumcentre (in any number of dimensions) you need a finite affine-independent collection of points and can require the circumcentre to be in their affine span, rather than requiring n+1 points in a space that's n-dimensional.

view this post on Zulip Patrick Massot (May 17 2020 at 19:51):

We definitely want Euclidean spaces to have no preferred basis

view this post on Zulip Patrick Massot (May 17 2020 at 19:52):

And I also agree with Joseph that replacing affine spaces with artificial linear spaces is lame

view this post on Zulip Patrick Massot (May 17 2020 at 19:52):

And I'm very sad our calculus library is done in this artificial context

view this post on Zulip Patrick Massot (May 17 2020 at 19:53):

For instance, we discussed affine charts on projective spaces. How would you define a linear space structure on them (without choosing bases everywhere)?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:53):

Probably you're right.

view this post on Zulip Patrick Massot (May 17 2020 at 19:54):

However we still to have the usual discussions about what should be parameters and what should be extended

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:55):

What I want is to avoid requirement [finite_dimensional ...] in theorems that don't need it.

view this post on Zulip Patrick Massot (May 17 2020 at 19:55):

Sure

view this post on Zulip Joseph Myers (May 17 2020 at 19:55):

I'm happy to remove that requirement, it will just mean the definition isn't quite the same as the standard one.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:56):

I wonder if we can have some clever abbreviation here.

view this post on Zulip Patrick Massot (May 17 2020 at 19:56):

Wait, what's the difference between inner_product_space and euclidean_space then?

view this post on Zulip Sebastien Gouezel (May 17 2020 at 19:56):

You should just work with inner_product_space, almost all of your theorems will be true in this broader setting.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:57):

Or we can avoid the words euclidean_space and use inner_product_space

view this post on Zulip Patrick Massot (May 17 2020 at 19:57):

I was first!

view this post on Zulip Joseph Myers (May 17 2020 at 19:57):

If we remove the requirement, there wouldn't be euclidean_vector_space any more, but there would be euclidean_affine_space.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:57):

Why not normed_affine_space?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:58):

And you separately impose typeclass requirements on the underlying vector space.

view this post on Zulip Sebastien Gouezel (May 17 2020 at 19:58):

As for euclidean_affine_space, couldn't you rather require that you have a normed space structure on the vector space, and that the distance on the affine space should come from this distance, but without requiring a priori that the distance is euclidean?

view this post on Zulip Sebastien Gouezel (May 17 2020 at 19:59):

Yury, Patrick and I are saying exactly the same things in parallel. Maybe it's a hint that it's a natural design...

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 19:59):

I must admit that I started with something else but now I agree that I was wrong.

view this post on Zulip Joseph Myers (May 17 2020 at 20:00):

Isn't the inner product a stronger requirement than being normed? And attempting to define the metric for an affine space over a general normed space, then apply it with the extra requirement of the inner product, ran into the type class issues discussed above.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:01):

No, if you add [normed_space k V] as an argument.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:01):

In this case you can later require [inner_product_space V] and Lean will deduce [normed_space real V] automatically.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:02):

And I guess @Sebastien Gouezel wants some basic theory to be done over any normed field.

view this post on Zulip Patrick Massot (May 17 2020 at 20:03):

And then we'll want an instance saying that a linear space is an affine space over itself and the world will collapse

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:03):

Why?

view this post on Zulip Joseph Myers (May 17 2020 at 20:04):

But keep the bundled distance? Some other bits of theory (proving Tarski's axioms for betweenness) are for any affine space over an ordered field. I already have the instance that a vector space is an affine space over itself.

view this post on Zulip Patrick Massot (May 17 2020 at 20:04):

I don't why, it's simply we're already discussing a complicated class setup, and things are usually difficult.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:07):

To summarize, we need

  • affine_space k V P;
  • normed_affine_space k V P.

view this post on Zulip Jalex Stark (May 17 2020 at 20:09):

Joseph Myers said:

I'm happy to remove that requirement, it will just mean the definition isn't quite the same as the standard one.

I don't understand. Why is it important that your code is maximally close to the statement on wikipedia?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:11):

@Patrick Massot Looking back in this thread, I think that I understand what happened. I badly formulated what I wanted.

I never wanted the general theory to be written for fin n → real only. But we need a model Euclidean space sometimes, and once we drop the euclidean_space typeclass (and write the general theory for an inner_product_space) it seems natural to reuse this name as a type tag on fin n → real.

view this post on Zulip Patrick Massot (May 17 2020 at 20:11):

ok

view this post on Zulip Joseph Myers (May 17 2020 at 20:14):

@Jalex Stark Each place where a definition means something different from the conventional mathematical meaning of a phrase is a potential source of confusion. In this case there probably isn't much scope for confusion (and we can't avoid cases where different sources use the same phrase with different meanings and we have to pick one).

view this post on Zulip Jalex Stark (May 17 2020 at 20:15):

I don't think "the string of words you can find most easily on wikipedia" and "the conventional mathematical meaning" are terribly related

view this post on Zulip Jalex Stark (May 17 2020 at 20:15):

"the conventional mathematical meaning" of something is never fully captured by one formal definition

view this post on Zulip Jalex Stark (May 17 2020 at 20:16):

in terms of mathlib, it's captured by an API with several equivalent definitions at the core

view this post on Zulip Jalex Stark (May 17 2020 at 20:16):

in terms of "mathematics done without computers" it's captured by sociological phenomena that are fuzzier than concrete sentences on paper

namely the practice of doing and teaching mathematics

view this post on Zulip Joseph Myers (May 17 2020 at 20:38):

Defining normed_affine_space (with bundled dist) results in much the same type class issues as above.

import analysis.normed_space.real_inner_product

class has_vadd (V : Type*) (P : Type*) :=
(vadd : P  V  P)
(vsub : P  P  V)

def vadd {V : Type*} {P : Type*} [has_vadd V P] : P  V  P := has_vadd.vadd
def vsub {V : Type*} {P : Type*} [has_vadd V P] : P  P  V := has_vadd.vsub

infix `+`:65 := vadd
infix `-`:65 := vsub

class affine_space (k : Type*) (V : Type*) (P : Type*) [field k] [add_comm_group V]
    [vector_space k V] [nonempty P] [has_vadd V P] :=
(vadd_assoc :  (p : P) (v1 v2 : V), p + v1 + v2 = p + (v1 + v2))
(vadd_vsub :  (p1 p2 : P), p1 + (p2 - p1 : V) = p2)
(vsub_vadd :  (p : P) (v : V), p + v - p = v)

class normed_affine_space (k : Type*) (V : Type*) (P : Type*) [normed_field k] [normed_group V]
    [normed_space k V] [nonempty P] [has_dist P] [has_vadd V P] [affine_space k V P] :=
(dist_eq_norm_vsub :  (x y : P), dist x y = (x - y : V))

set_option pp.all true

class euclidean_affine_space (V : Type*) (P : Type*) [inner_product_space V] [nonempty P]
    [has_dist P] [has_vadd V P] [affine_space  V P] [normed_affine_space  V P]

Errors:

26:55: failed to synthesize type class instance for
V : Type ?l_1,
P : Type ?l_2,
_inst_1 : inner_product_space.{?l_1} V,
_inst_2 : nonempty.{?l_2+1} P,
_inst_3 : has_dist.{?l_2} P,
_inst_4 : has_vadd.{?l_1 ?l_2} V P,
_inst_5 :
  @affine_space.{0 ?l_1 ?l_2} real V P real.field (@inner_product_space.to_add_comm_group.{?l_1} V _inst_1)
    (@inner_product_space.to_module.{?l_1} V _inst_1)
    _inst_2
    _inst_4
 @affine_space.{0 ?l_1 ?l_2} real V P (@normed_field.to_field.{0} real normed_field.normed_field)
    (@normed_group.to_add_comm_group.{?l_1} V (@inner_product_space_is_normed_group.{?l_1} V _inst_1))
    (@normed_space.to_module.{0 ?l_1} real V normed_field.normed_field
       (@inner_product_space_is_normed_group.{?l_1} V _inst_1)
       (@inner_product_space_is_normed_space.{?l_1} V _inst_1))
    _inst_2
    _inst_4

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:45):

You could go for

import analysis.normed_space.real_inner_product

class has_vadd (V : Type*) (P : Type*) :=
(vadd : P  V  P)
(vsub : P  P  V)

def vadd {V : Type*} {P : Type*} [has_vadd V P] : P  V  P := has_vadd.vadd
def vsub {V : Type*} {P : Type*} [has_vadd V P] : P  P  V := has_vadd.vsub

infix `+`:65 := vadd
infix `-`:65 := vsub

class affine_space (k : Type*) (V : Type*) (P : Type*) [field k] [add_comm_group V]
    [vector_space k V] [nonempty P] [has_vadd V P] :=
(vadd_assoc :  (p : P) (v1 v2 : V), p + v1 + v2 = p + (v1 + v2))
(vadd_vsub :  (p1 p2 : P), p1 + (p2 - p1 : V) = p2)
(vsub_vadd :  (p : P) (v : V), p + v - p = v)

class normed_affine_space (k : Type*) (V : Type*) (P : Type*) [normed_field k] [normed_group V]
    [normed_space k V] [nonempty P] [has_vadd V P] [metric_space P] extends affine_space k V P :=
(dist_eq_norm_vsub :  (x y : P), dist x y = (x - y : V))

class euclidean_affine_space (V : Type*) (P : Type*) [inner_product_space V] [nonempty P]
    [metric_space P] [has_vadd V P] [normed_affine_space  V P]

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:46):

What's the difference?

view this post on Zulip Joseph Myers (May 17 2020 at 20:46):

That one assumes the metric space structure rather than proving that the distance defines one.

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:47):

The differences are that I have assumed that there is a metric space structure on P, not just a distance (so that you get the topology and everything), and that normed_affine_space now extends affine_space.

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:47):

A simple rule is that, if a typeclass does not depend on more type arguments than a previous typeclass, then it should extend it, not take it as a parameter.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:48):

BTW, affine_space should extend has_vadd. Also I'd avoid def vadd. You can use has_vadd.vadd in notation instead.

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:48):

It's not always a perfect rule, but quite often it's a good one.

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:49):

No, affine_space should not extend has_vadd as there is an additional type parameter, the field.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:49):

I always forget about this.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:49):

I mean, the fact that we can't extend in this case.

view this post on Zulip Kevin Buzzard (May 17 2020 at 20:50):

I never understood it in the first place. I am just hoping that it will all be easier in lean 4

view this post on Zulip Kevin Buzzard (May 17 2020 at 20:50):

All I know is that there are experts here who can tell me how to set things up with the definitions, and then the theorems I'm ok with

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:50):

The main issue with your definition, though, is that it's not the usual definition of an affine space. For instance, R2\mathbb{R}^2 with the R\mathbb{R} action acting by addition on the first coordinate is an affine space in your sense.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 20:51):

What is vsub?

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:51):

No, I'm wrong, because of your vsub, sorry.

view this post on Zulip David Wärn (May 17 2020 at 20:52):

Shouldn't an affine space be "a faithful and transitive group action by the additive group of a vector space"?

view this post on Zulip Joseph Myers (May 17 2020 at 20:53):

The full version (as opposed to the MWE) has comments explaining that it's defined directly since mathlib doesn't have additive group actions (and also vadd_zero isn't needed as an axiom because with this definition it can be deduced from the other axioms).

view this post on Zulip Sebastien Gouezel (May 17 2020 at 20:55):

If vadd and vsub only show up in the definition of an affine space, I don't know if you should have a separate class for them as you do, or if you should bundle them in the definition. The only drawback I can see is when you want to see an affine complex space as an affine real space, sharing the same vadd and vsub.

view this post on Zulip Joseph Myers (May 17 2020 at 20:56):

I think if they're defined as part of affine_space I then can't use the notation within that definition? That was why I defined them separately.

view this post on Zulip Sebastien Gouezel (May 17 2020 at 21:11):

Thinking back about this, you should define an affine space with respect to an add_comm_group, not with respect to a vector_space: your axioms don't involve the field action. And a normed affine space should be with respect to a normed_group.

view this post on Zulip Joseph Myers (May 17 2020 at 21:17):

Once I define affine subspaces and affine maps, the vector space becomes relevant. Should I still define affine_space as a torsor of a group action of an add_comm_group and then only introduce the field and vector space for those later definitions?

view this post on Zulip Kevin Buzzard (May 17 2020 at 21:29):

Yeah, why not. I remember when we defined group actions and the computer scientists looked at us and said "you don't mention inverses -- define monoid actions instead".

view this post on Zulip Sebastien Gouezel (May 17 2020 at 21:35):

Joseph Myers said:

Once I define affine subspaces and affine maps, the vector space becomes relevant. Should I still define affine_space as a torsor of a group action of an add_comm_group and then only introduce the field and vector space for those later definitions?

Yes, I think so. Then it means that you can extend has_vadd instead of taking it as a parameter, as you are not introducing new types into the game.

view this post on Zulip Joseph Myers (May 17 2020 at 21:47):

OK, I've rearranged things along those lines. With normed_affine_space extending affine_space (both of them not depending on a field any more) and euclidean_affine_space extending normed_affine_space, it now works for normed_affine_space and thus euclidean_affine_space to bundle only [has_dist P] rather than the full metric space structure, with the metric space properties of the distance then being proved as an instance for any normed_affine_space.

view this post on Zulip Joseph Myers (May 17 2020 at 21:49):

Should any of this be PRed to mathlib, or is further work needed there first? I can think of at least four separate pieces: (a) affine spaces; (b) normed affine spaces; (c) the geometrical definitions and results (such as angles and Pythagoras) that are proved for real inner product spaces as an intermediate step to proving them for Euclidean affine spaces; (d) Euclidean affine spaces and corresponding geometrical results.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 21:50):

Should any of this be PRed to mathlib?

You can start by opening a PR with what you already have.

view this post on Zulip Joseph Myers (May 17 2020 at 21:51):

I suppose affine spaces go in linear_algebra/affine_space.lean and normed affine spaces in something like analysis/normed_space/affine.lean?

view this post on Zulip Reid Barton (May 17 2020 at 21:58):

Does "affine space" here mean torsor for an arbitrary additive group?

view this post on Zulip Reid Barton (May 17 2020 at 21:59):

I only partly followed the conversation here.

view this post on Zulip Kevin Buzzard (May 17 2020 at 21:59):

That seems to be the conclusion

view this post on Zulip Joseph Myers (May 17 2020 at 22:00):

A commutative additive group is what we arrived at. I don't think that much actually depends on the commutative part, but if you remove that then you have to deal with left and right torsors (and the +ᵥ and -ᵥ notation becomes even less applicable).

view this post on Zulip Reid Barton (May 17 2020 at 22:01):

Then it should be called something like add_torsor and go under ... algebra?

view this post on Zulip Joseph Myers (May 17 2020 at 22:02):

Or add_comm_torsor since some bits do use commutativity?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 22:02):

The docstring should mention affine spaces.

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:04):

If at some point someone wants torsors for a nonabelian group, the group law will probably not be +.

view this post on Zulip Reid Barton (May 17 2020 at 22:06):

Come to think of it, do we have general group actions on sets? I forget

view this post on Zulip Joseph Myers (May 17 2020 at 22:06):

Only multiplicative actions, not additive.

view this post on Zulip Joseph Myers (May 17 2020 at 22:45):

Filed PR #2720 with the first piece (torsors of additive commutative group actions).

view this post on Zulip Johan Commelin (May 18 2020 at 12:50):

@Joseph Myers Sorry for the outdated style guidelines. I've PR'd an update over here: https://github.com/leanprover-community/leanprover-community.github.io/pull/21
(And thanks for pointing out that they were out of date :wink:)


Last updated: May 08 2021 at 10:12 UTC