Hello! Have a proof of Heron's Area Formula!

Stream: new members

[Matt Kempster]

Hi all! I discovered lean a couple days ago and have been thoroughly enjoying it. I noticed that Heron's Area Formula was on the list of missing theorems of the big 100, so as a fun experiment I attempted a proof. Lo and behold, I actually managed to do it!

Warning: The proof is incredibly, terribly messy. I know it can be simplified drastically - I will have fun doing that soon! But I was excited that I had killed my last sorry and want to share:

https://github.com/matt-kempster/mathlib/commit/a9981fde5877c78edfa70e64bd99ce225dc1a4f2

Let me know if you have any pointed feedback - ways to rewrite sections, etc. I will be opening a PR soon; first I must:

• Extract the proof into the archive directory (instead of being inlined into geometry.lean
• Clean it up (obviously)
• Double-check that I actually proved the right thing/formulated it correctly/don't need to prove anything else

Thanks for reading!

P.S.: hello! Good to be here! :D

[Bryan Gin-ge Chen]

Welcome! Heron's area formula might well deserve to be in the main library rather than the archive, actually.

[Heather Macbeth]

Ideally, someday, the LHS of your equation will be volume (convex_hull {p1, p2, p3}), where volume is a measure naturally induced on the affine Euclidean space in question, coming from the Euclidean inner product.

[Matt Kempster]

Agreed, that's how the other theorem provers seem to be doing it. I wonder if Freek is okay with this formulation or not :)

[Heather Macbeth]

In my mind the main point would be that a real inner product (element of $\operatorname{Sym}^2V^*$) induces a volume form (element of $\Lambda^nV^*$). @Eric Wieser might be able to comment on how far away this is ...

[Heather Macbeth]

Is this also how other theorem provers do it? Or is it a more concrete construction of the associated measure? (I don't know if the other theorem provers have much in the way of tensors, etc.)

[Eric Wieser]

I think that @Amelia Livingston has more to say about exterior powers than I do

[Matt Kempster]

I just looked. It appears that HOL Light and Isabelle use the convex hull formulation, while Metamath, Coq, and Mizar all use the same formulation I did (based on distances between three points).

[Eric Wieser]

Although exterior powers over a dual space (if that's what the * is) are isomorphic to docs#alternating_map, right?

[Heather Macbeth]

Matt Kempster said:

I just looked. It appears that HOL Light and Isabelle use the convex hull formulation, while Metamath, Coq, and Mizar all use the same formulation I did (based on distances between three points).

What is the measure on the space in which the convex hull is taken? Effectively, is the space itself R^n (with the product measure) or a general affine Euclidean space?

[Matt Kempster]

Heather Macbeth said:

What is the measure on the space in which the convex hull is taken? Effectively, is the space itself R^n (with the product measure) or a general affine Euclidean space?

I'm no expert in either of those theorem provers, but it looks like they both use R^2:

• https://www.cs.ru.nl/~freek/100/hol.html#57
• http://www.cse.unsw.edu.au/~kleing/top100/#57

[Heather Macbeth]

If you work in $\mathbb{R}^2$, we do have the measure, but you lose all the nice geometric expression. A little unsatisfactory either way :)

[Heather Macbeth]

(To be clear, it's our library that's unsatisfactory, not your proof!) :big_smile:

[Kevin Buzzard]

@Matt Kempster Freek told me that he explicitly avoids saying precisely how the theorem should be formalised and is happy if different people interpret a result in different ways. I think at least one of the proofs of Pythagoras's theorem just points to a definition of a norm on R^2 for example.

[Heather Macbeth]

Eric Wieser said:

Although exterior powers over a dual space (if that's what the * is) are isomorphic to docs#alternating_map, right?

@Eric Wieser Yes, so we want a construction of the alternating map induced by an inner product, and also a construction of the measure induced by an alternating map to the scalar field.

[Heather Macbeth]

Actually, sorry, it's more complicated. An inner product induces an element of $(\Lambda^nV^*)^{\otimes 2}$. This determines a density, and hence a measure, where a density is defined to be a $\pm$-equivalence class of elements of $\Lambda^nV^*$.

[Eric Wieser]

The closest I can offer right now for alternating maps derived from a quadratic form is the clifford_algebra.ι_wedge definition in my repo

[Eric Wieser]

Square the result of that, and conjure an inverse algebra map, and I think you have your volume (squared)

[Heather Macbeth]

What do you mean by "square" here? It's clear if the object is an element of the top exterior power, and squaring produces an element of the tensor square of the top exterior power; it's less clear to me what is meant if the object is an alternating map.

[Eric Wieser]

I mean square the output after applying the map I guess

[Eric Wieser]

Which maybe doesn't make much sense if we're working with alternating maps only as a conveniently isomorphic object

[Eric Wieser]

Having actual exterior power objects in mathlib would certainly make this clearer!

[Joseph Myers]

The convention used for geometry results in mathlib is that you have {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P], so an arbitrary (possibly infinite-dimensional) Euclidean space, and then if the result is specific to two dimensions you have a two-dimensional subspace {s : affine_subspace ℝ P} [finite_dimensional ℝ s.direction] (hd : findim ℝ s.direction = 2) and hypotheses that points are in it. Then you possibly have a variant of the result when the whole space is two-dimensional, for convenience of people using it in that context. (E.g. when stating an IMO geometry problem it makes sense to have [finite_dimensional ℝ V] (hd2 : findim ℝ V = 2) rather than embedding the plane in a possibly larger space.) (When working with a triangle, you don't need those extra hypotheses, but you would if e.g. dealing with four points that must be coplanar.)

I think area in Heron (in mathlib proper) ought to be using the measure theory part of the library. To give and justify a definition of area/volume for an arbitrary Euclidean (affine) space by reference to one for euclidean_space ℝ (fin n) (I'm not sure how close what we have on product measures is to giving us the latter), you need (a) an isometry from the arbitrary space to the euclidean_space (which we have, more or less, given an isometry between P and V from vadd_const etc. together with linear_isometry_equiv.of_inner_product_space) and (b) a proof that the measure on the euclidean_space is invariant under isometries, which I don't think we have, to show the definition is genuinely independent of the arbitrary choice of isometry used. (More generally, we ought to have that any affine map multiplies the measure by the absolute value of the determinant.)

Then you have the matter of expressing results on area / volume in a way that makes sense for a two-dimensional triangle in a larger-dimensional space, so want a notion of two-dimensional measure meaningful in that context (and to show it's equal to measure in a two-dimensional space when you use coercions to treat the subspace as a Euclidean space itself; I'm not sure we have all those coercions yet). (As an example of why that generality is useful, clearly we ought to have the result that the volume of a (possibly degenerate) n-dimensional simplex is equal to 1/n * volume of base * height, which is talking about both (n-1)-dimensional and n-dimensional volumes in the same space.)

I think convex hull makes sense as the thing you are taking the measure of (see Yury's past unfinished attempts to redo convexity in mathlib for affine spaces, #2910).

In the absence of being a statement about areas in a form properly linked to the measure theory part of the library, maybe the archive is a better place for the proof (with a view to being moved into mathlib proper once linked with measure theory).

[Joseph Myers]

Also, Heron (in a form going in mathlib proper) shouldn't have the hypotheses you have that the points are different; it's true for all degenerate triangles as well, and might sometimes be useful in degenerate cases.

[Heather Macbeth]

@Matt Kempster, by the way, I don't know if you have seen the proof for the area of a disc, by James Arthur, Ben Davidson and Andrew Souther:
https://github.com/leanprover-community/mathlib/blob/cc9915282edc5c432650e4838535cdef9f65c086/archive/100-theorems-list/9_area_of_a_circle.lean#L75
They take the opposite approach from you (with the opposite "problem"): it's stated using measure theory for a disc in ℝ × ℝ (so someday it will also generalize to metric.ball in a Euclidean affine space).

[Matt Kempster]

Joseph Myers said:

Also, Heron (in a form going in mathlib proper) shouldn't have the hypotheses you have that the points are different; it's true for all degenerate triangles as well, and might sometimes be useful in degenerate cases.

This is true, I was thinking about this. I suppose a workaround would be to define the area of a degenerate triangle as 0, right?

[Joseph Myers]

I think any reasonable definition should result in the area of a degenerate triangle being 0 without needing to special-case it in the definition (even if sometimes special cases are needed in the proofs).

[Matt Kempster]

Heather Macbeth said:

Matt Kempster, by the way, I don't know if you have seen the proof for the area of a disc, by James Arthur, Ben Davidson and Andrew Souther:
https://github.com/leanprover-community/mathlib/blob/cc9915282edc5c432650e4838535cdef9f65c086/archive/100-theorems-list/9_area_of_a_circle.lean#L75
They take the opposite approach from you (with the opposite "problem"): it's stated using measure theory for a disc in ℝ × ℝ (so someday it will also generalize to metric.ball in a Euclidean affine space).

Neat! By opposite "problem" you mean that it uses measure theory and wants to one day be part of Euclidean world, whereas my Heron proof is in Euclidean world and will one day be part of measure theory land?

[Heather Macbeth]

Precisely!

[Matt Kempster]

I have opened #6988 for this, after a lot of simplification and refactoring. I'm actually rather happy with the proof now!

My questions (copy-pasted from the PR, comment there if you'd like):

• Is there a linter I can run?
• Do you have any feedback on the proof style? Let me know where I can simplify or improve things.
• What is the deal with the required rotate, { exact V }, { exact _inst_1 }, that I have, and what do those lines do? Can I get rid of those extra 2 goals?

Also, hi to the following people whose names I recognize in here:

• @Jalex Stark
• @Aaron Anderson
• @Henry Swanson
• @Bolton Bailey

What a cool coincidence that you guys are here!!

[Matt Kempster]

Oh, I've just realized that I didn't do the workflow properly; I worked on a branch of a fork, instead of a branch of the main repository. Is this OK, or should I kill my PR and make a new one?

My github username is matt-kempster - could I have access to create new branches of mathlib? Thanks!

[Bryan Gin-ge Chen]

Yes, please open a PR from the main repository. I've just sent you an invitation: https://github.com/leanprover-community/mathlib/invitations

[Bryan Gin-ge Chen]

We have two linters that are run by our CI scripts. To run them locally, see this post.

[Matt Kempster]

Thanks for the tips, Bryan.

Opened #6989. Feel free to review!