Formalising geometry exercises

Stream: new members

[Kunhao Zheng]

Hello all,
I am seeking to formalize some geometry exercises (mostly on high school or undergrad level), I have seen the topic about Euclidean Geometry here. In the current mathlib there is already geometry in euclidean space, but that's more or less algebraic. And also there is an axiomatic geometry repo based on Tarski's.

I would like to know whether mathlib or this repo is ready to formalize exercises involving congruent triangles or, angle in circles? If yes, which is more appropriate? And if not, if there is any undergoing plan on enriching mathlib's geometry and I will be happy to see if I can contribute?

Thanks!

[Kevin Buzzard]

My understanding is that currently Lean is ready to be doing the kind of high-school geometry proofs but that nobody is working on it. For example I suspect that we are ready to state things like "angle at centre equals twice angle at circumference" but I think that nobody stated yet, although I might be out of date here.

[Joseph Myers]

There are lots of different things referred to as "angle" in informal geometry that need to be distinguished in formal geometry. "angle at centre" is an angle from 0 to 2π, where the choice between θ and 2π-θ has to be disambiguated using information about which of two possible arcs the "angle at circumference" is on. We don't have a definition of that kind of angle in mathlib; what we have defined is an undirected angle from 0 to π. So stating that result requires first working out the right way to define such angles that's best for building up everything that uses such angles, and then you need to build out the associated API for such angles in mathlib.

[Joseph Myers]

Congruence is probably more accessible right now, in that you probably only need one definition and there's a straightforward and natural form of that definition. Say that two indexed families of points, with the same index type, in two possibly different metric spaces (or more generally, in mathlib, pseudo_emetric_spaces), are congruent if there exists an isometric equivalence between those metric spaces that maps the points of one family to corresponding points of the other.

Then SSS congruence for triangles says that two triangles in the same Euclidean space are congruent if corresponding side lengths are equal. But that's not the right form of result for mathlib, because something much more general is true. If you want to prove a version of SSS congruence for mathlib, I think you should aim for something like this:

Consider two indexed families of points, with the same index type (not necessarily finite), in two possibly different Euclidean spaces, such that all the distances between corresponding pairs of points in the two families are equal. (a) The (directions of) the affine spans of the two families have the same dimension. (b) If that dimension is finite, and there is an isometric equivalence between the two Euclidean spaces (which might themselves be infinite-dimensional), then the two families are congruent. (c) As a special case, which is often what you want to use in geometry problems, if the index type is a fintype and the two Euclidean spaces are the same, then the two families are congruent. (And SSS congruence for triangles is a further special case of that, which never needs to be given as a separate theorem at all.)

You probably need to prove lots of lemmas along the way to doing that, but it shouldn't involve setting up lots of definitions.

[Heather Macbeth]

We don't have the affine isometry group yet, although I have been thinking of defining it (and would be glad of your thoughts, @Joseph Myers). I am imagining a file very similar to analysis.normed_space.linear_isometry, which completes the analogy
linear_equiv : affine_equiv :: linear_isometry_equiv : X

[Heather Macbeth]

At the moment, one can talk about a docs#isometry of Euclidean space, but it would be good to be able to work habitually with an "affine isometry equiv" which has the linearity property bundled in.

[Heather Macbeth]

Note that thanks to the Mazur-Ulam theorem (docs#isometric.to_real_linear_isometry_equiv) this is no loss of generality.

[Joseph Myers]

A couple of remarks there: (a) if we define affine isometric equivs then euclidean_geometry.reflection should become one (at present it's just a bundled isometric equiv); (b) Mazur-Ulam only covers the bijective case, an isometry of Euclidean spaces that isn't surjective is also necessarily an affine map (I formalized that, but didn't PR it to mathlib because what I did was specific to the Euclidean case and it was pointed out on Zulip that it should be done more generally for isometries of (affine spaces over) strictly convex normed spaces (so first we need to define strictly convex spaces)).

[Kunhao Zheng]

I would also like to know if we are ready to formalize statement like 2 circles are tangent at point Xor 2 lines are parallel (of course in dim = 2)? From docs#sphere, seems that we are talking about points and we don't have an object that describe a sphere?

[Kunhao Zheng]

In the style of mathlib, what is the ideal way of saying that 2 lines are parallel? I don't have a clear idea but I guess we will have to go into linear_algebra.affine_space?

[Yury G. Kudryashov]

See docs#metric.sphere for an object describing a sphere.

[Yury G. Kudryashov]

There are different ways to formalize "two spheres are tangent at point X":

• r₁ + r₂ = dist O₁ O₂ or abs (r₁ - r₂) = dist O₁ O₂;
• the submanifolds have the same tangent plane (needs lots of definitions from geometry/manifold);
• two spheres have exactly one common point.
  Some day we should have a tfae lemma about these (and possibly some other) definitions.

[Yury G. Kudryashov]

For the "tangent plane" version of the definition, one can define the tangent plane to a sphere using an explicit formula, then

• glue this to the manifold library (can be done later; AFAIR, we don't have tangent subspaces to submanifolds yet);
• prove that the definition based on this explicit formula (two spheres intersect at X and share the tangent plane at this point) is equivalent to the other two definitions (at least if 0 < r₁ and 0 < r₂).

[Joseph Myers]

A line is an affine subspace whose direction has dimension 1. To say two affine subspaces s₁ and s₂ are parallel, use s₁.direction = s₂.direction. Since there are lots of lemmas about the directions of affine subspaces, and equality is also convenient to use, this may well be more convenient than having an explicit definition of parallel.

(If it's possible one affine subspace is empty and the other is a single point, equality of directions might not be quite what you want because both of those have the trivial submodule as their direction. But if you already know you're dealing with nonempty subspaces, that's not an issue.)

[Joseph Myers]

(For the most part, lemmas about dimensions of affine spaces and subspaces are only present for finrank, not the possibly-infinite cardinal-valued rank. So finrank ℝ s.direction = 1 is how you say that s is a line.)

[Joseph Myers]

I certainly expect it will be useful, for lots of Euclidean geometry purposes, to define a structure for bundled spheres (bundling centre and radius; with appropriate has_mem and has_coe instances, and various definitions for operations that can usefully be carried out involving spheres). The main formalization question arising there is whether such a structure should also bundle a nondegeneracy condition (positive radius), or whether it will be more convenient to use such a structure if that condition is not bundled but is instead a hypothesis on lemmas that need it (many may only need nonnegative radius rather than requiring it to be positive).

[Joseph Myers]

Definitions that make sense for bundled spheres include, for example, tangency (to affine subspaces and to other spheres), power of a point, radical axis / plane / hyperplane (= affine subspace of points with equal power with respect to two spheres), inversion, pole and polar. All such definitions should, when added, have lots of routine lemmas added at the same time to provide a basic API to help use the definition. There would also naturally be definitions that produce a bundled sphere; a bundled circumsphere definition, for example, that puts together circumcenter and circumradius, and the image of a sphere under an isometric equivalence as another bundled sphere. These of course need their own routine lemmas.

[Heather Macbeth]

Heather Macbeth said:

We don't have the affine isometry group yet, although I have been thinking of defining it (and would be glad of your thoughts, Joseph Myers). I am imagining a file very similar to analysis.normed_space.linear_isometry, which completes the analogy
linear_equiv : affine_equiv :: linear_isometry_equiv : X

Done in #8660.