Congruent triangles

Stream: Is there code for X?

[Tianchen Zhao]

Do we have congruent triangles in matlib? Most proofs in Euclidean geometry are in vectors and I am thinking of writing about congruent and similar triangles and prove some theorems.

Also, although I can prove, for example, SAS using vectors and law of cosines etc., I am thinking of including a Euclidean style proof there. He proved SAS by moving the triangles so that they overlap. I can prove that by introducing translation, rotation and symmetry as conformal isometries (do we have that in matlib?) and then replicating Euclid's proof.

[Hanting Zhang]

I don't think we have much of anything about triangles. We do have docs#isometry

[Heather Macbeth]

This was actually discussed recently:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Formalising.20geometry.20exercises/near/242996042

[Heather Macbeth]

See in particular this comment and after:

Joseph Myers said:

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.

[Heather Macbeth]

The most specialized kind of isometry available in mathlib is docs#linear_isometry. It would be good to develop a theory of "affine isometry"; the work would be to combine the appropriate features of docs#linear_isometry and docs#affine_map.

[Eric Wieser]

Is there anything we can do to unify docs#linear_isometry_equiv and docs#quadratic_form.isometry?

[Heather Macbeth]

Not until we unify inner product spaces and quadratic forms, which is blocked by the dreaded conjugate linear map issue.

[Eric Wieser]

In particular, for docs#clifford_algebra.map I needed a quadratic_form version of docs#linear_isometry, but one doesn't exist so I had to work with it unbundled.

[Tianchen Zhao]

btw most things about geometry in lean are done in a more general setting. Is there a way to work, for example, only at 2 dimensions? Or is that really necessary?

[Kevin Buzzard]

There is Heather's Hack.

[Kevin Buzzard]

This is a very cool way to get directed angles painlessly and ensure you're in 2 dimensions like good old Euclid 1

[Heather Macbeth]

@Kevin Buzzard, were you in fact able to do geometry using this definition?

[Tianchen Zhao]

Heather Macbeth said:

See in particular this comment and after:

Joseph Myers said:

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.

I might be considering too naively. I understand congruence of figures should be defined with isometries and rigid motions, but for triangles isn't it more efficient to just use vectors and eg law of cosines to "solve" them (this way is no longer "Euclidean" though). For example, two triangles satisfying SAS are the same as we can solve for all other angles and sides given only the lengths of the two sides and the angle between them.

[Kevin Buzzard]

doing geometry: I didn't try yet :-( -- right now I seem to be very inefficiently trying to work on about 10 projects all of which have been hanging over since term started (it's just finished last Friday). I'm thinking that this sort of mathematics might be interesting for (a) a summer project or (b) a school talk so I'll chase it up in the end.

[Joseph Myers]

Tianchen Zhao said:

Heather Macbeth said:

See in particular this comment and after:

Joseph Myers said:

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.

I might be considering too naively. I understand congruence of figures should be defined with isometries and rigid motions, but for triangles isn't it more efficient to just use vectors and eg law of cosines to "solve" them (this way is no longer "Euclidean" though). For example, two triangles satisfying SAS are the same as we can solve for all other angles and sides given only the lengths of the two sides and the angle between them.

A principle followed in mathlib is to state and prove results with the weakest assumptions that make sense. A triangle bundles three affinely independent points. But neither "three" or "affinely independent" is needed at all for results on congruence, so those results aren't really about triangles at all, they've about indexed families and should be stated and proved accordingly (unless the triangle result is actually needed separately to derive the arbitrary-dimension result, but I don't think it is).

You could, for example, probably derive the result (a) from my previous comment using inner_weighted_vsub to show that a subfamily of points in one family is affinely independent iff and only if the corresponding subfamily of points in the other family (with the same pairwise distances) is, and proving further lemmas that apply to any affine space (over a vector space) to deduce the dimension property from that. Then for (b) you might define some concrete isometries that you use in an induction step, to go from an isometric equivalence mapping corresponding points in an affine subspace to one that makes corresponding points in a larger affine subspace match as well. Once you have SSS congruence in such a general form for indexed families of points, you could deduce SAS congruence (i.e. if all distances from a single point in the family, and all angles at that point, match in the two families, then you have congruence under the same conditions as before), because knowing the distances and angles at one point in the family immediately gives you all the other pairwise distances. Again, the result being proved is not restricted at all to triangles (although you may have used the law of cosines to determine the other pairwise distances from the distances and angles at one point).