Zulip Chat Archive

Stream: new members

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


view this post on Zulip Matt Kempster (Mar 31 2021 at 21:23):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 21:25):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:41):

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.

view this post on Zulip Matt Kempster (Mar 31 2021 at 21:44):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:44):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:45):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 21:47):

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

view this post on Zulip Matt Kempster (Mar 31 2021 at 21:47):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 21:48):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:48):

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?

view this post on Zulip Matt Kempster (Mar 31 2021 at 21:51):

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:

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:51):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:52):

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

view this post on Zulip Kevin Buzzard (Mar 31 2021 at 21:53):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:55):

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.

view this post on Zulip Heather Macbeth (Mar 31 2021 at 21:59):

Actually, sorry, it's more complicated. An inner product induces an element of (ΛnV)2(\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 ΛnV\Lambda^nV^*.

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:02):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:04):

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

view this post on Zulip Heather Macbeth (Mar 31 2021 at 22:05):

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.

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:06):

I mean square the output after applying the map I guess

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:07):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 22:14):

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

view this post on Zulip Joseph Myers (Apr 01 2021 at 00:20):

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

view this post on Zulip Joseph Myers (Apr 01 2021 at 00:25):

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.

view this post on Zulip Heather Macbeth (Apr 01 2021 at 00:33):

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

view this post on Zulip Matt Kempster (Apr 01 2021 at 00:33):

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?

view this post on Zulip Joseph Myers (Apr 01 2021 at 00:34):

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

view this post on Zulip Matt Kempster (Apr 01 2021 at 00:35):

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?

view this post on Zulip Heather Macbeth (Apr 01 2021 at 00:35):

Precisely!

view this post on Zulip Matt Kempster (Apr 01 2021 at 03:39):

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!!

view this post on Zulip Matt Kempster (Apr 01 2021 at 03:51):

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!

view this post on Zulip Bryan Gin-ge Chen (Apr 01 2021 at 03:55):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 01 2021 at 03:57):

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

view this post on Zulip Matt Kempster (Apr 01 2021 at 03:59):

Thanks for the tips, Bryan.

Opened #6989. Feel free to review!


Last updated: May 14 2021 at 00:42 UTC