feat: synthetic geometry #7300

ah1112 · 2023-09-21T15:04:19Z

This is adding synthetic geometry using Avigad's axioms and formalizing Euclid Book I, through the Pythagorean theorem.

eric-wieser · 2023-09-26T15:25:01Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+class incidence_geometry :=
+/--Points in the plane-/
+(point : Type u)
+/--Lines in the plane-/
+(line : Type u)
+/--Circles in the plane-/
+(circle : Type u)
+
+/--A point being on a line-/
+(online : point → line → Prop)
+/--Two points being on the sameside of a line-/
+(sameside : point → point → line → Prop)
+/--Three points being in a row-/
+(B : point → point → point → Prop)
+/--A point being the center of a center-/
+(center_circle : point → circle → Prop)
+/--A point being on a circle-/
+(on_circle : point → circle → Prop)
+/--A point being inside a circle-/
+(in_circle : point → circle → Prop)
+/--That two lines intersect-/
+(lines_inter : line → line → Prop)
+/--A line and a circle intersect-/
+(line_circle_inter : line → circle → Prop)
+/--Two circles intersect-/
+(circles_inter : circle → circle → Prop)


The mathlib 4 naming guide says these Prop and Type fields should be named as Point, OnCircle, etc, with no underscores and PascalCase.

What you have looks like Lean 3 naming conventions!

Ok, I think I have changed what you requested. What's the next thing you would like me to revise?

Another lean4ism is using where instead of := and not using parentheses around the fields. Not sure if it's enforced style.

Ok, I made the parenthesis and := suggestions. What else would you like me to modify?

Mathlib/Geometry/Synthetic/Avigad/EuclidBookI.lean

tb65536 · 2023-10-10T20:48:38Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+area : Point → Point → Point → ℝ
+
+/--From a set of points getting one additional one-/
+more_pts : ∀ (S : Set Point), S.Finite → ∃ a, a ∉ S


Would it make more sense to instead assume that Point is infinite?

How would you suggest going about this? I am not really sure how to do it.

Suggested change

more_pts : ∀ (S : Set Point), S.Finite → ∃ a, a ∉ S

[more_pts : Infinite Point]

Interesting... How would I use this condition to get the same effect as the original? Previously I could write:
rcases more_pts ∅ Set.finite_empty with ⟨a, -⟩ to get a point, for example.

Apparently we're missing a Set.Finite version of Infinite.exists_not_mem_finset?

tb65536 · 2023-10-10T20:51:50Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+/--B is strict-/
+ne_13_of_B : ∀ {a b c}, B a b c → a ≠ c
+/--B is strict-/
+ne_23_of_B : ∀ {a b c}, B a b c → b ≠ c


I think this condition is redundant

I got rid of ne_23_of_B since it can be deduced from ne_12_of_B. I don't think ne_13_of_B is redundant though?

tb65536 · 2023-10-10T20:53:05Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+/--Degenerate areas are zero-/
+degenerate_area : ∀ a b, area a a b = 0
+/--Area is completely symmetric-/
+area_invariant : ∀ a b c, area a b c = area c a b ∧ area a b c = area a c b


I think usually we would break this up into two separate conditions

Ok, I have done so now!

eric-wieser · 2023-10-13T16:59:05Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+
+/-- `IncidenceGeometry` represents geometry in the Euclidean sense, with primitives for points
+lines and circles-/
+class IncidenceGeometry where


Everything after this where should be indented by two spaces

I see 4 spaces, not 2.

eric-wieser · 2023-10-13T17:00:16Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+open IncidenceGeometry
+-------------------------------------------------- Definitions -----------------------------------
+/--Points being on different sides of a line-/
+def diffside a b L := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L


Thee should be written as

Suggested change

def diffside a b L := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L

def DiffSide (a b : Point) (L : Line) : Prop :=

¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L

note:

Explicit type annotations

Use of CamelCase for Prop definitions

Wait, should the explicit type annotations also be true for the axioms? Or for theorems?

I've only looked in detail at this file so far, so for now just these defs

eric-wieser · 2023-10-13T17:01:43Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+/--Getting a circle with center and point on it-/
+circle_of_ne : ∀ {a b}, a ≠ b → ∃ α, CenterCircle a α ∧ OnCircle b α
+/--If lines intersect then this gives you the point of intersection-/
+pt_of_linesinter : ∀ {L M}, LinesInter L M → ∃ a, OnLine a L ∧ OnLine a M


Suggested change

pt_of_linesinter : ∀ {L M}, LinesInter L M → ∃ a, OnLine a L ∧ OnLine a M

pt_of_linesInter : ∀ {L M}, LinesInter L M → ∃ a, OnLine a L ∧ OnLine a M

If a theorem is about FooBar x, it should have fooBar in its name not foobar. I think the naming guide explains this a little better than I have.

I see... Should the theorem then be Point_of_LinesInter instead?

No, they should be point_of_lineInter; the first letter is kept lowercase. It's somewhat arbitrary, but it's what the style guidelines say, and following them makes things consistent.

done I think?

eric-wieser · 2023-10-13T17:03:23Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+  (angle b a c = angle e d f ↔ length b c = length e f)
+
+variable [i : IncidenceGeometry]
+open IncidenceGeometry


I think you probably want

Suggested change

open IncidenceGeometry

namespace IncidenceGeometry

Ok! Just out of curiosity, why do we want to do this? I changed it in the Axioms file and in EuclidBookI, but was not able to do it for Tactics since the elab expressions started to break?

Again, for now this advice is only for this axioms file. It means that the axioms end up in the same namespace as the derived definitions.

eric-wieser · 2023-10-22T09:52:38Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+class IncidenceGeometry where
+/--Points in the plane-/
+Point : Type u
+/--Lines in the plane-/
+Line : Type u
+/--Circles in the plane-/
+Circle : Type u


I suspect this typeclass will be more usable as

Suggested change

class IncidenceGeometry where

/--Points in the plane-/

Point : Type u

/--Lines in the plane-/

Line : Type u

/--Circles in the plane-/

Circle : Type u

class IncidenceGeometry (Point : Type u) where

/--Lines in the plane-/

Line : Type u

/--Circles in the plane-/

Circle : Type u

because then we can add an instance that says "euclidean space satisfies the axioms of "incidence geometry".

When I try to change this, variable [i : IncidenceGeometry] breaks, along with anything that requires points. How do I get around this?

You change it to {Point : Type*} [IncidenceGeometry Point]

Ok. It seems if I do that, then I would have to write i.Line or i.rightangle every time? Is there some way to avoid this?

eric-wieser · 2023-10-22T20:48:43Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+/--Points being on different sides of a line-/
+def DiffSide (a b : Point) (L : Line) := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L


Please add explicit types here. I think for all of the below, the explicit type is

Suggested change

/--Points being on different sides of a line-/

def DiffSide (a b : Point) (L : Line) := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L

/--Points being on different sides of a line-/

def DiffSide (a b : Point) (L : Line) : Prop := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L

My bad! Will do

urkud · 2023-12-28T02:26:28Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+    /--The area made by three points-/
+    area : Point → Point → Point → ℝ
+    /--From a set of points getting one additional one-/
+    more_pts : ∀ (S : Set Point), S.Finite → ∃ a, a ∉ S


The Mathlib way to say this is Infinite Point.

urkud · 2023-12-28T02:28:27Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+universe u
+
+/-- `IncidenceGeometry` represents geometry in the Euclidean sense, with primitives for points
+lines and circles-/


Do you use some specific book as the source for the list of axioms? If yes, then this should be mentioned both in the module docstring and in the typeclass docstring.

urkud · 2023-12-28T02:30:30Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+lines and circles-/
+class IncidenceGeometry where
+    /--Points in the plane-/
+    Point : Type u


If Point is a data field of the typeclass, not an argument, then we can't have 2 instances in the same universe without having lots of issues.

urkud · 2023-12-28T02:34:19Z

Mathlib/Geometry/Synthetic/Avigad/Axioms.lean

+    /--Angles are nonnegative-/
+    angle_nonneg : ∀ a b c, 0 ≤ angle a b c
+    /--Lengths are nonnegative-/
+    length_nonneg : ∀ a b, 0 ≤ length a b


I see that you don't require the triangle inequality here. What implies it? Can we extend MetricSpace X instead of introducing domain-specific length? Note that the goal of Mathlib is to have different parts of the library play well with each other.

ah1112 added 12 commits September 20, 2023 10:35

Added axioms

fd0e943

Adding tactics

75afb88

Adding Book I

3a0fc5e

Fixed wlog

cdbe15d

Linter changes

f8432ab

Linter changes

d0640c3

Linter changes

9844564

Linter changes

cd7cab4

Linter changes

7167247

Linter changes

b41ed54

Eliminated comments

ba0da9e

Replacing with some push_contra

8f9d852

ah1112 added help-wanted The author needs attention to resolve issues awaiting-review t-euclidean-geometry Affine and axiomatic geometry labels Sep 21, 2023

ah1112 added 8 commits September 21, 2023 14:23

Added files to Mathlib.lean

5522b9d

Changed Folders

cb32bc1

Fixing perma issues

69724b1

Adding docstrings

86d559d

Fixed Docstrings

e05107c

Leaving only one universe

0f7f3e0

Fixing perma tactic

79d01a0

Making linter changes

3cca692

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 23, 2023

eric-wieser reviewed Sep 26, 2023

View reviewed changes

ah1112 and others added 3 commits September 28, 2023 14:57

Changed Point Line Circle

7e0814f

Changed names of primitive functions

5f926fb

Merge branch 'master' into AHE_synthetic_geometry

e6cbc18

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 29, 2023

Changed fields in axioms

75cc897

github-actions bot reviewed Oct 7, 2023

View reviewed changes

Lint changes

aeaded8

github-actions bot reviewed Oct 7, 2023

View reviewed changes

Lint change

49414ec

tb65536 reviewed Oct 10, 2023

View reviewed changes

Split area_invariant, deduced ne_23_of_B

b270a8a

eric-wieser reviewed Oct 13, 2023

View reviewed changes

ah1112 added 2 commits October 21, 2023 20:18

Naming conventions

d74db92

Rest of Book I

2d82083

eric-wieser reviewed Oct 22, 2023

View reviewed changes

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Oct 22, 2023

ah1112 added 2 commits October 22, 2023 14:13

lint

aed5519

Explicit type annotations

bd3afe9

eric-wieser reviewed Oct 22, 2023

View reviewed changes

Explicit type descriptions

de65f49

ah1112 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 27, 2023

urkud reviewed Dec 28, 2023

View reviewed changes

urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jan 23, 2024

	more_pts : ∀ (S : Set Point), S.Finite → ∃ a, a ∉ S
	[more_pts : Infinite Point]

	def diffside a b L := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L
	def DiffSide (a b : Point) (L : Line) : Prop :=
	¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L

	pt_of_linesinter : ∀ {L M}, LinesInter L M → ∃ a, OnLine a L ∧ OnLine a M
	pt_of_linesInter : ∀ {L M}, LinesInter L M → ∃ a, OnLine a L ∧ OnLine a M

		/--Points being on different sides of a line-/
		def DiffSide (a b : Point) (L : Line) := ¬OnLine a L ∧ ¬OnLine b L ∧ ¬SameSide a b L

feat: synthetic geometry #7300

Are you sure you want to change the base?

feat: synthetic geometry #7300

Conversation

ah1112 commented Sep 21, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ah1112 Oct 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Oct 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Oct 22, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Oct 22, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ah1112 Oct 13, 2023 •

edited

Loading

eric-wieser Oct 13, 2023 •

edited

Loading

eric-wieser Oct 22, 2023 •

edited

Loading

eric-wieser Oct 22, 2023 •

edited

Loading