Some olympiad formalisations

Stream: new members

[Joseph Myers]

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)?

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

(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.)

[Joseph Myers]

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

[Joseph Myers]

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?

2. 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.)

[Reid Barton]

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?)

[Johan Commelin]

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

[Patrick Massot]

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)

[Johan Commelin]

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.

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

Then you apply negation, and another exp.

[Johan Commelin]

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

[Patrick Massot]

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

[Reid Barton]

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

[Johan Commelin]

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

[Patrick Massot]

Assuming of course $\cong$ means diffemorphism.

[Reid Barton]

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.

[Johan Commelin]

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`

[Reid Barton]

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

[Johan Commelin]

But exp_neg_inv_glue would also do the trick, right?

[Kevin Buzzard]

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.

[Sebastien Gouezel]

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

[Patrick Massot]

And then we can claim Lean does AI

[Patrick Massot]

Sébastien, this fancy sigmoid name is AI

[Alastair Horn]

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?

[Kevin Buzzard]

Geocoq is synthetic, right?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Alastair Horn]

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

[Reid Barton]

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.

[Alastair Horn]

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.

[Joseph Myers]

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.

[Joseph Myers]

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.

[Joseph Myers]

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.)

[Joseph Myers]

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.)

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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)?

[Joseph Myers]

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.

[Joseph Myers]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Joseph Myers]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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.

[Yury G. Kudryashov]

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

[Joseph Myers]

@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.

[Yury G. Kudryashov]

What's wrong with a real inner product space?

[Joseph Myers]

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 :=

[Yury G. Kudryashov]

This is true in any real inner product space

[Joseph Myers]

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.

[Yury G. Kudryashov]

What is your current definition?

[Yury G. Kudryashov]

I mean, the main class

[Joseph Myers]

/-- 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)∥)

[Yury G. Kudryashov]

Note that many theorems will not need finite_dimensional.

[Yury G. Kudryashov]

So I'd drop it.

[Yury G. Kudryashov]

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

[Joseph Myers]

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.

[Yury G. Kudryashov]

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.

[Patrick Massot]

I don't understand why you say that Yury

[Joseph Myers]

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.

[Patrick Massot]

We definitely want Euclidean spaces to have no preferred basis

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

Probably you're right.

[Patrick Massot]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

Sure

[Joseph Myers]

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

[Yury G. Kudryashov]

I wonder if we can have some clever abbreviation here.

[Patrick Massot]

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

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

Or we can avoid the words euclidean_space and use inner_product_space

[Patrick Massot]

I was first!

[Joseph Myers]

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

[Yury G. Kudryashov]

Why not normed_affine_space?

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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?

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

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

[Joseph Myers]

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.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

Why?

[Joseph Myers]

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.

[Patrick Massot]

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

[Yury G. Kudryashov]

To summarize, we need

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

[Jalex Stark]

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?

[Yury G. Kudryashov]

@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.

[Patrick Massot]

ok

[Joseph Myers]

@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).

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Joseph Myers]

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

[Sebastien Gouezel]

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]

[Yury G. Kudryashov]

What's the difference?

[Joseph Myers]

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

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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.

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

I always forget about this.

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

What is vsub?

[Sebastien Gouezel]

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

[David Wärn]

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

[Joseph Myers]

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).

[Sebastien Gouezel]

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.

[Joseph Myers]

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.

[Sebastien Gouezel]

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.

[Joseph Myers]

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?

[Kevin Buzzard]

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".

[Sebastien Gouezel]

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.

[Joseph Myers]

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.

[Joseph Myers]

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.

[Yury G. Kudryashov]

Should any of this be PRed to mathlib?

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

[Joseph Myers]

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

[Reid Barton]

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

[Reid Barton]

I only partly followed the conversation here.

[Kevin Buzzard]

That seems to be the conclusion

[Joseph Myers]

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).

[Reid Barton]

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

[Joseph Myers]

Or add_comm_torsor since some bits do use commutativity?

[Yury G. Kudryashov]

The docstring should mention affine spaces.

[Kevin Buzzard]

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

[Reid Barton]

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

[Joseph Myers]

Only multiplicative actions, not additive.

[Joseph Myers]

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

[Johan Commelin]

@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:)