formalizing Hilbert's axioms for plane geometry

Stream: new members

[Marc Masdeu]

Hi there, I'm a mathematician getting started with Lean. After having done the natural number game and a few of the challenges, I wanted to start formalizing something easy, and I tried with Hilber'ts axioms.

So far, I have this little:

import tactic
-- We want to be able to define functions using the law of excluded middle
local attribute [instance, priority 0] classical.prop_decidable


noncomputable theory

open_locale classical

constants Points Lines : Type*
constant lies_on : Points → Lines → Prop

local infixl `∈` := lies_on

constant I1 : ∀ A B : Points,  A ≠ B → ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ )
--constant I11 : ∀ A B : Points,  A ≠ B → ∃ ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ )
--constant I12 : ∀ A B : Points, ∀ r s : Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s
constant I2 : ∀ ℓ : Lines, ∃ A B : Points, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ
constant I3 : ∃ A B C : Points, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) )))

lemma I11 : ∀ A B : Points,  A ≠ B → ∃ ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ) :=
begin
intros A B,
intro h,
cases I1 A B h with ℓ h1,
existsi ℓ,
cases h1 with H,
exact H,
end

lemma I12 : ∀ A B : Points, ∀ r s : Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s :=
begin
intros A B,
intros r s,
intro h,
intro hAr,
intro hBr,
intro hAs,
intro hBs,
cases I1 A B h with ℓ h1,
have r_is_ell : r = ℓ,
...
end

The axiom I1 is an if and only if statement, and I wanted to separate the two statements as I11 and I12. I succeeded with I11 (existence) but for I12 (uniqueness) I am having trouble. I end up with the following tactic state:

A B : Points,
r s : Lines,
h : A ≠ B,
hAr : A∈r,
hBr : B∈r,
hAs : A∈s,
hBs : B∈s,
ℓ : Lines,
h1 :
  (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) ℓ ∧ ∀ (y : Lines), (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) y → y = ℓ
⊢ r = s

and then I want to conclude by showing that r = ell = s, so I do have r_eq_ell : r = \ell. This gives me the first goal of showing r = ell, and there I get stuck:

2 goals
A B : Points,
r s : Lines,
h : A ≠ B,
hAr : A∈r,
hBr : B∈r,
hAs : A∈s,
hBs : B∈s,
ℓ : Lines,
h1 :
  (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) ℓ ∧ ∀ (y : Lines), (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) y → y = ℓ
⊢ r = ℓ

A B : Points,
r s : Lines,
h : A ≠ B,
hAr : A∈r,
hBr : B∈r,
hAs : A∈s,
hBs : B∈s,
ℓ : Lines,
h1 :
  (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) ℓ ∧
    ∀ (y : Lines), (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) y → y = ℓ,
r_eq_ell : r = ℓ
⊢ r = s

Thank you for any help!

PS: I know that I should be using classes or structures, but I am trying to keep it as simple as possible (and using as few non-math concepts as possible). Once I get something compiling I will try to understand how to make it up to standards.

[Johan Commelin]

@Marc Masdeu I think there are functions unique_of_exists_unique that take an ∃! foobar statement, and spit out the corresponding uniqueness statement.

[Johan Commelin]

But maybe you would rather prove it by yourself, as an exercise.

[Marc Masdeu]

Good to know (I had seen it elsewhere) but I would like to prove the exact statement of I12 (yes, as an exercice), and more so now that I got stuck :-).

[Johan Commelin]

have r_is_ell : r = ℓ,
{ apply h1.right,
  split,
  assumption' },

[Johan Commelin]

Alternative:

rcases I1 A B h with ⟨ℓ, h1_left, h1_right⟩,
have r_is_ell : r = ℓ,
{ apply h1_right,
  split,
  assumption' },

[Johan Commelin]

I changed cases to rcases. That allows you to do "recursive" cases. (And I didn't attempt to give meaningful names to the hypotheses)

[Marc Masdeu]

aha! Is there a way to resolve the have with tactics? I am not so comfortable yet with switching from one way to the other..

[Johan Commelin]

What do you mean?

[Johan Commelin]

I proved the have using tactics. I used { ... } to "zoom in" on one goal

[Johan Commelin]

But you don't need to write those curly braces, if you don't want to

[Johan Commelin]

Or do you want to avoid the have altogether?

[Marc Masdeu]

Oh I see. I am trying myself now. I thought that the {} was used to construct directly a term. I am in the right thread...

[Johan Commelin]

rcases I1 A B h with ⟨ℓ, h1_left, h1_right⟩,
transitivity,
{ apply h1_right,
  split,
  assumption' },
{ symmetry,
  apply h1_right,
  split,
  assumption' }

[Johan Commelin]

Proof without have

[Johan Commelin]

Shorter version:

rcases I1 A B h with ⟨ℓ, h1_left, h1_right⟩,
transitivity,
swap, symmetry,
all_goals
{ apply h1_right,
  split,
  assumption' },

[Marc Masdeu]

OK, I got it. I thought that h1 was a function so that I could apply it by doing something like h1 r but this never worked. I hadn't thought of doing the .right and I still don't see the reasoning behind it.

[Johan Commelin]

Sure, it also took me some time to parse it. But it is of the form ... ∧ ...

[Johan Commelin]

And the right hand side is a function

[Marc Masdeu]

Oh! How can I check this kind of things inside a proof? If h1 was defined outside, I would start trying #check h1, #check h1 r and so on, but I couldn't do anything like that inside the proof...

[Johan Commelin]

Are you using VScode?

[Johan Commelin]

Because it lists your entire context in the tactic state

[Johan Commelin]

In the same place where you would see the output of #check foobar

[Marc Masdeu]

No, I'm using cocalc (I want some summer camp students to be able to play around with this, and wanted to set something up easy to use for them)

[Johan Commelin]

But where do you see the output of #check h1 in CoCalc?

[Johan Commelin]

Probably in some message window somewhere

[Johan Commelin]

You are also seeing the goal that you want to prove somewhere. Right above it should be a list of all your hypotheses.

[Marc Masdeu]

Yes, there is a message window. But if I want to know the type of something, for example, I can't ask for it there.

[Johan Commelin]

I'm copy-pasting this from your first message:

2 goals
A B : Points,
r s : Lines,
h : A ≠ B,
hAr : A∈r,
hBr : B∈r,
hAs : A∈s,
hBs : B∈s,
ℓ : Lines,
h1 :
  (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) ℓ ∧ ∀ (y : Lines), (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) y → y = ℓ
⊢ r = ℓ

[Marc Masdeu]

Yes, I see the hypotheses and everything, and they get updated as I advance. A lot like the web interface of the natural number game. What I don't have is autocompletion.

[Johan Commelin]

That's where you can see h1 : (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) ℓ ∧ ∀ (y : Lines), (λ (ℓ : Lines), A∈ℓ ∧ B∈ℓ) y → y = ℓ

[Johan Commelin]

That's the type of h1

[Johan Commelin]

Hmm... what exactly do you mean? I thought CoCalc had some form of autocomplete

[Marc Masdeu]

I don't think it has any autocompletion (unless I have it disabled somehow!). What I meant --and maybe it's still me being stupid-- is that if I want to run some command (like h1 r) inside the proof to see what it would give me, I will probably get a useless error.

[Alex J. Best]

If you are in a tactic block and you want to know the type of something you can have what_am_i := thing_I_dont_know, then in the info at cursor block you should see what_am_i : ℕ or whatever it is

[Marc Masdeu]

Oh @Alex J. Best this is clever! Thanks.

[Alex J. Best]

Screen-Shot-2020-01-15-at-14.27.06.png

[Johan Commelin]

@Marc Masdeu Aha, I see. This might be one way to "hack" it:

rcases I1 A B h with ⟨ℓ, h1⟩,
have test := h1 r,

This will give you an error

[Johan Commelin]

Aah, ok, Alex beat me (-;

[Marc Masdeu]

You guys are incredibly helpful! Thanks!!

[Alex J. Best]

This is normally how I build terms, start with a function /lemma I want to apply with no arguments as have, then add arguments one by one till it gets to what I want.

[Marc Masdeu]

Aha. Yes, I want to learn how to translate the way we do math usually, into Lean.
I'll go back and try to prove a few more stupid lemmas. Probably will come back very soon...

[Johan Commelin]

Good luck! (-;

[Alex J. Best]

Some form of tab completion works for me in Cocalc by the way Screen-Shot-2020-01-15-at-14.30.23.png

[Alex J. Best]

I typed apply and. then hit tab, the first 20 results were random general things, but then it showed me various and related lemmas and their types.
Actually it worked better when I did apply a then tab then continued typing. I think the . was doing something a little funny with the tab completion.

[Marc Masdeu]

I'll try. I seem to remember that in VScode the completion appeared without the tab, this confused me.

[Marc Masdeu]

OK, so I'm a bit further down. So far, I have:

import tactic
-- We want to be able to define functions using the law of excluded middle
local attribute [instance, priority 0] classical.prop_decidable


noncomputable theory

open_locale classical

universe u
constant Points : Type u
constant Lines : set(set Points)
constant lies_on : Points → Lines → Prop

local infixl `∈` := lies_on
notation x `∋` y := lies_on y x
constant I1 : ∀ A B : Points,  A ≠ B → ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ )
constant I2 : ∀ ℓ : Lines, ∃ A B : Points, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ
constant I3 : ∃ A B C : Points, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) )))

notation p `xor` q := (p ∧ ¬ q) ∨ (q ∧ ¬ p)

lemma I11 : ∀ A B : Points,  A ≠ B → ∃ ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ) :=
begin
intros A B,
intro h,
cases I1 A B h with ℓ h1,
existsi ℓ,
cases h1 with H,
exact H,
end

lemma I12 : ∀ A B : Points, ∀ r s : Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s :=
begin
intros A B,
intros r s,
intro h,
intro hAr,
intro hBr,
intro hAs,
intro hBs,
cases I1 A B h with ℓ h1,
transitivity ℓ,
have r_eq_ell : r = ℓ,
apply h1.right,
split,
exact hAr,
exact hBr,
exact r_eq_ell,
have s_eq_ell : s = ℓ,
apply h1.right,
split,
exact hAs,
exact hBs,
symmetry,
exact s_eq_ell,
end

lemma there_are_two_points : ∃ A B : Points, (A ≠ B) :=
begin
cases I3 with A BCh,
cases BCh with B Ch,
cases Ch with C h,
cases h with hh,
existsi A,
existsi B,
exact hh,
end

lemma distinct_lines_have_at_most_one_common_point {r s : Lines} {A B : Points} (hrs: r ≠ s) (hAr: A ∈ r) (hAs: A ∈ s) (hBr: B ∈ r) (hBs: B ∈ s) : A = B :=
begin
suffices not_A_eq_B : ¬ (A ≠ B),
cc,
intro h,
suffices Q : r = s,
contradiction,
exact I12 A B r s h hAr hBr hAs hBs,
end

definition intersect (r s : Lines) := ∃ A : Points, A ∈ r ∧ A∈ s
definition parallel (r s : Lines) := (r = s) ∨ (¬ intersect r s)
local infixl `||` := parallel

constant parallel_postulate {A : Points} {ℓ r s : Lines} : A ∈ r ∧ A ∈ s ∧ r || ℓ ∧ s || ℓ → r = s

constant between : Points → Points → Points → Prop
notation A `*` B `*` C := between A B C
definition colinear (A B C : Points) := ∃ ℓ : Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ
-- definition noncolinear (A B C : Points) := ¬ colinear A B C

constant B11 {A B C : Points} : (A * B * C) → (C * B * A)
constant B12 {A B C : Points} : (A * B * C) → (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ colinear A B C)
constant B2 {A B : Points} : ∃ C, A * B * C
constant B3 {A B C : Points} {ℓ : Lines} : (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ) → ((A * B * C) ∧ ¬( B * A * C ) ∧ ¬ (A * C * B)) ∨ (¬ (A * B * C) ∧ ( B * A * C ) ∧ ¬ (A * C * B)) ∨ (¬ (A * B * C) ∧ ¬( B * A * C ) ∧ (A * C * B))
-- constant B4 {A B C D: Points} {ℓ : Lines}: (noncolinear A B C) ∧ (¬ A ∈ ℓ) ∧ (¬ B ∈ ℓ) ∧ (¬ C ∈ ℓ) ∧ (D ∈ ℓ) ∧ (A * D * B)  → (∃ E : Points, (A * E * C) xor (B * E * C))

def line_segment (A B : Points) : set Points := {A} ∪ {B} ∪ {C : Points | A * C * B}
local infix `#` := line_segment

def triangle (A B C : Points) (h: colinear A B C) : set Points := A#B ∪ A#C ∪ B#C

lemma segments_are_symmetric: ∀ A B : Points, A # B = B # A :=
begin
intros A B,
rw set.subset.antisymm_iff,
split,
intro x,
intro h,
have hh : x = A ∨ x = B ∨ A * x * B,
{
cases h with h1 h2,
cases h1 with ha hb,
left,
cases ha,
exact ha,
exfalso,
exact ha,
cases hb,
right,
left,
exact hb,
exfalso,
exact hb,
right,
right,
exact h2,
},
cases hh with H1 H2,
left,
right,
rw set.singleton_def,
left,
exact H1,
cases H2 with H G,
left,
left,
rw set.singleton_def,
left,
exact H,
right,
...
end

I am trying to prove that the segments AB and BA are the same, and I'm having lots of trouble. The "math" way to prove it is:
recall that AB is defined to be the union of {A}, {B} and the points in between A and B. We have axiom I12 which says that x is betwen A and B implies x is between B and A. So obviously the segments AB and BA are equal. What I do in Lean is quite longer, but first I turn to a double inclusion (I would like to know how to prove the second one "by symmetry"), and I'm trying to finish one of the inclusions. I'm at the point where it's "enough" to apply axiom I12: my goal looks like:

A B x : Points,
h : x ∈ A#B,
G : A * x*B
⊢ x ∈ {C : Points | B * C*A}

and I want to tell Lean to "expand" hypothesis G and use I12. Any hints?

[Johan Commelin]

Ooof, some of your lines are quite long (-;

[Johan Commelin]

In your definition of triangle, I think you want ¬ colinear A B C

[Johan Commelin]

Also, the Lean keyword for ... is sorry

[Johan Commelin]

@Marc Masdeu Here is one way to use symmetry to reduce to 1 inclusion:

begin
  suffices : ∀ A B : Points, A # B ⊆ B # A,
  { intros A B, apply set.subset.antisymm; solve_by_elim },
  intros A B,
intro x,
intro h,
sorry

[Johan Commelin]

Ideally, the wlog tactic would do this for you. But I usually end up in a big fight if I try to use it.

[Johan Commelin]

@Marc Masdeu Here's another hint: First prove two lemmas A ∈ A#B and B ∈ A#B. They will be useful in lots of places.

[Johan Commelin]

Also, you overwrote the standard meaning of ∈, so my suggestions no longer typecheck

[Johan Commelin]

lemma segments_are_symmetric: ∀ A B : Points, A # B = B # A :=
begin
  suffices : ∀ A B : Points, A # B ⊆ B # A,
  { intros A B, apply set.subset.antisymm; solve_by_elim },
  intros A B,
  intros x h,
  rcases h with ⟨⟨rfl | ⟨⟨⟩⟩⟩ | rfl | ⟨⟨⟩⟩⟩ | h,
  { unfold line_segment, finish },
  { unfold line_segment, finish },
  { unfold line_segment, have := B11 h, finish },
end

[Johan Commelin]

@Marc Masdeu I found that crazy rcases line, by writing rcases? h and copying from the message window.

[Johan Commelin]

All those weird brackets and rfls tell Lean that most of the things you need to do are really very trivial.

[Johan Commelin]

What remains are the (mildly :wink:) interesting cases.

[Johan Commelin]

finish is a tactic that says: "Given the current hypothesis, this is elementary logic. I can do that."

[Alex J. Best]

Just for fun I did this too without looking at Johan's, I think they're fundamentally the same? I didn't know the crazy rcases thing though.

lemma segments_are_symmetric: ∀ A B : Points, A # B = B # A :=
begin
suffices : ∀ A B : Points, A # B ⊆ B # A,
{
  intros,
  exact le_antisymm (this A B) (this B A),-- i just typed library_search to get this,
},
rintros A B x hx,
unfold line_segment at *,
simp at *,
rw or.assoc at hx,
apply or.elim3 hx,
all_goals {intros,try{cc},},
apply or.intro_right,
exact B11 a,
end

[Marc Masdeu]

Thanks guys, I'm studying your solutions now...

[Marc Masdeu]

About @Johan Commelin complaint about long lines: I definitely agree with it, but how would you go about writing the simple statement "Given three distinct points on a line, exactly one of them is between the other two" in a concise way?

[Alex J. Best]

I guess Johan just means put some line breaks in at natural looking points (lean won't care)

[Marc Masdeu]

I guess Johan just means put some line breaks in at natural looking points (lean won't care)

Oh :sweat_smile:

[Marc Masdeu]

Also, you overwrote the standard meaning of ∈, so my suggestions no longer typecheck

@Johan Commelin to solve this, I have decided to go back to set theory. That means that Points should be a set, and that Lines should be a set of sets of points. If I initialize

Points : set Type u
Lines : set set Points

then my axioms start to misbehave, because I assume that it doesn't make sense to write A : Points and instead I should write someting like A \in Points. Am I right?

[Kevin Buzzard]

I would be tempted to let points be in a type, and lines be subsets of points, if you want to go down the subset route.

[Kenny Lau]

one would first have to prove lines.ext then

[Kevin Buzzard]

I can prove that

[Kevin Buzzard]

it follows from propext

[Marc Masdeu]

I would be tempted to let points be in a type, and lines be subsets of points, if you want to go down the subset route.

I have two reasons to do that: I am trying to copy Hartshorne's UTM book and he defines points to be a set. The second reason is so that in this way I don't need to define what A \in ell means.

Your intermediate approach seems to solve my second concern, I will try that.

[Marc Masdeu]

one would first have to prove lines.ext then

What is that?

[Kevin Buzzard]

he defines points to be a set

That's because he's thinking about framing things in terms of set theory. There are two kinds of sets. There are subsets of a given set, like the even numbers, and there are generic sets about which we know nothing -- and in type theory those are types.

[Kevin Buzzard]

lines.ext is the statement that two lines are equal if and only for all points P, P is in line 1 iff it's in line 2. One can prove this in Lean no problem.

[Kevin Buzzard]

In contrast to the "generic" set of points, a line is a subset. Subsets are different to sets.

[Marc Masdeu]

And two subsets are not automatically equal iff they contain the same elements? I am getting lost.

[Kevin Buzzard]

I don't know anything about the various ways of doing this stuff. I know that Ali Sever followed Tarski, and IIRC a line was an abstract type. What does Hartshorne do?

[Kevin Buzzard]

And two subsets are not automatically equal iff they contain the same elements? I am getting lost.

It is a trivial theorem, but it is not true by definition.

[Kevin Buzzard]

In fact it is equivalent to propositional extensionality, which is talked about at great length here. As a mathematician you should just ignore all this. Kenny is a constructivist, he is just trolling really.

[Kevin Buzzard]

Remember that in set theory there is an axiom which says that two sets with the same elements are equal.

[Kevin Buzzard]

Equal sets have the same elements -- this is obvious. Sets with the same elements are equal -- this is a theorem, whose one-line proof is "it's an axiom"

[Kevin Buzzard]

so you will have to supply a one-line proof ;-)

[Marc Masdeu]

From Hartshorne: "We simply postulate a set, whose elements are called points, together with certain subsets, which we call lines. We do not say what the points are, nor which subsets form lines, but we do require that these undefined notions obey certain axioms..."

[Kevin Buzzard]

OK so you should make a type of points, and let lines be subsets. Then everything will work just the way Hartshorne wants.

[Marc Masdeu]

Equal sets have the same elements -- this is obvious. Sets with the same elements are equal -- this is a theorem, whose one-line proof is "it's an axiom"

Oh. And Lean standard doesn't come with these theorems proven for you? I would imagine that if Lean knows what a set is, then it knows all the basic theorems on set theory.

[Kevin Buzzard]

The difference between type theory and set theory is that in type theory, the only sets you can have are subsets of a fixed set. It took me a long time to realise that mathematicians use the concept of set in two different ways.

[Kevin Buzzard]

It could easily be a theorem in core Lean. Kenny is just trolling. He seems to have caused you a great deal of confusion. There is nothing special about lines.ext. You will have to prove lots of theorems.

[Kevin Buzzard]

The point is that if you make a new definition (e.g. lines) then you will have to prove lots of theorems about that definition.

[Marc Masdeu]

Oh I see. And yes, I'm becoming more confused the more I learn. This is fine, though!

import tactic
local attribute [instance, priority 0] classical.prop_decidable

noncomputable theory
open_locale classical

universe u
constant Points : Type u
constant Lines : set (set Points)
constant I1 : ∀ A B : Points,  A ≠ B → ∃! ℓ : Lines, ( A ∈ ℓ ) ∧ ( B ∈ ℓ )

Why does Lean complain in the last line?

---- > I figured it out! Now Lines is a set :-)

[Kevin Buzzard]

Take a look at the way Lean does complex numbers. A new definition, and then immediately you have to prove a bunch of trivial theorems about complex. Lean might have lots of theorems about sets, but if you define lines then you have to prove theorems about lines including trivial theorems.

[Marc Masdeu]

Take a look at the way Lean does complex numbers. A new definition, and then immediately you have to prove a bunch of trivial theorems about complex. Lean might have lots of theorems about sets, but if you define lines then you have to prove theorems about lines including trivial theorems.

I see. That will keep me busy.

[Marc Masdeu]

This morning I sweated to prove (with help!)

lemma I12 : ∀ A B : Points, ∀ r s : Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s

I modified it now to work with lines being sets of points:

lemma I12 : ∀ A B : Points, ∀ r s ∈ Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s

But the proof I had stopped working. I am stuck at:

lemma I12 : ∀ A B : Points, ∀ r s ∈ Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s :=
begin
intros A B r s rL sL h hAr hBr hAs hBs,
apply unique_of_exists_unique (I1 A B h),
sorry,
end

and I am trying to complete it using the fact that I1 is a lot stronger...

Moreover, I don't like that there are so many hypothesis. It seems that this is a side effect of working with sets.

[Bryan Gin-ge Chen]

If you use variables you can state some hypotheses just once at the beginning of a section or namespace. See 2.6 of Theorem Proving in Lean if you haven't already.

[Bryan Gin-ge Chen]

Oh, I guess you may also want to state your lemma like this to avoid the giant intros at the start of the proof:

lemma I12 {A B : Points} {r s : set Points} (rL : r ∈ Lines) (sL : s ∈ Lines)
  (h : A ≠ B) (hAr : A ∈ r) (hBr : B ∈ r) (hAs : A ∈ s) (hBs : B ∈ s) : r = s :=
sorry

[Johan Commelin]

@Marc Masdeu At this point, if you really want to pursue the geometry formalisation (instead of just fooling around to learn more Lean), I think it would be useful to look at the previous attempts.

[Marc Masdeu]

Marc Masdeu At this point, if you really want to pursue the geometry formalisation (instead of just fooling around to learn more Lean), I think it would be useful to look at the previous attempts.

Oh I do want to fool around. Formalizing geometry was just what I picked as a testing grounds, since it doesn't itself have much pre-requisites. Eventually I will want to teach students how to use this, so I better learn a bit first.

[Bryan Gin-ge Chen]

Could you post what you have in its entirety? Otherwise I can only guess how you corrected I1.

[Marc Masdeu]

import tactic
-- We want to be able to define functions using the law of excluded middle
local attribute [instance, priority 0] classical.prop_decidable


noncomputable theory
open_locale classical

universe u
constant Points : Type u
constant Lines : set(set(Points))

constant I1 : ∀ A B : Points,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ )
constant I2 : ∀ ℓ ∈ Lines, ∃ A B : Points, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ
constant I3 : ∃ A B C : Points, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) )))

notation p `xor` q := (p ∧ ¬ q) ∨ (q ∧ ¬ p)

lemma I12 : ∀ A B : Points, ∀ r s ∈ Lines, (A ≠ B) →  (A ∈ r) →  (B ∈ r) →  (A ∈ s) → (B ∈ s) →  r = s :=
begin
intros A B r s rL sL h hAr hBr hAs hBs,
apply unique_of_exists_unique (I1 A B h),

end

[Kevin Buzzard]

Does open_locale classical not automatically do the local attribute business? What happens if you delete line 3?

[Marc Masdeu]

I don't see any change. I copied line 3 from somewhere, and kept the comment since I do want to use the LEM.

[Bryan Gin-ge Chen]

The unfolds are unnecessary, but may help you see what's going on.

lemma I12 {A B : Points} {r s : set Points} (rL : r ∈ Lines) (sL : s ∈ Lines)
  (h : A ≠ B) (hAr : A ∈ r) (hBr : B ∈ r) (hAs : A ∈ s) (hBs : B ∈ s) : r = s :=
begin
  apply unique_of_exists_unique (I1 A B h),
  { unfold exists_unique,
    use rL,
    split,
    split,
    assumption,
    assumption,
    finish, },
  { unfold exists_unique,
    use sL,
    split,
    split,
    assumption,
    assumption,
    finish, },
end

[Marc Masdeu]

Thanks! Now that we are at this. You changed a lot the definition of the lemma, by removing all the foralls, for example. What is the difference between the two, and which form should I prefer? The form that I had was a bit similar to what I would do in math, and this notation breaks the symmetry between forall and exists, right?

[Marc Masdeu]

@Bryan Gin-ge Chen I don't understand what did the finish do...

[Bryan Gin-ge Chen]

At a mathematical level they're equivalent. There are slight differences when it comes to how Lean interprets them due to the fact that I made A, B, r and s "implicit arguments" using curly braces.

In Lean what I wrote is generally preferred since it saves a lot of typing. (Using variables would be even better). Could you say more about the symmetry you expect between forall and exists?

finish is a tactic which is able to clear "obvious" goals if they just boil down to logical manipulation. In this case, it turns out that you can just as well use intros, refl instead of finish.

[Marc Masdeu]

Could you say more about the symmetry you expect between forall and exists?

Well, how would you write in Lean these two statements (which I see as "symmetrical"):
for all x, P(x) and there exists x, P(x).

[Bryan Gin-ge Chen]

I'd write them like this: ∀ x, P x, ∃ x, P x. They behave rather differently though.

[Kevin Buzzard]

They are yin and yang

[Bryan Gin-ge Chen]

"forall x" indicates to me that the thing that follows is a function of x. (It just happens to take values in the world of logical propositions). Lean lets us write such statements using more function-oriented syntax (we can give x as an argument to the function).

[Marc Masdeu]

Yes, that's the symmetry that I meant! But you see, if you want to write a lemma one could write:
lemma hasP : \forall x : Type, P x or lemma existsP : \exists x : Type, P x. The first one can be rewritten as
lemma hasP {x : Type} : P x. What about the second?

[Kevin Buzzard]

You can't move the exists to the left of the colon. They are different in that respect.

[Kevin Buzzard]

The general concept of "negation" switches them around

[Marc Masdeu]

You can't move the exists to the left of the colon. They are different in that respect.

I think that this is what I was observing. I guess one gets used to it.

[Johan Commelin]

I guess this constructive logic leaking through....

[Johan Commelin]

Because there they aren't symmetric at all.

[Kevin Buzzard]

They are like night and day. "I can see in the day, how come I can't see in the night?"

[Bryan Gin-ge Chen]

Since forall gives rise to functions maybe exists should arise from co-functions (in the sense of "co-data"?)...

[Chris Hughes]

It is a coproduct.

[Chris Hughes]

And functions are products.

[Kevin Buzzard]

@Marc Masdeu -- here's the difference between sets and types. If a mathematician says "let G be a group and let S be a set, and imagine G acts on S, blah blah blah..." then they don't actually mean this, because imagine the chaos that would ensue if a random element of G (which is just a random set) turned out to coincidentally be an element of S, or a subset of S, or something? You could imagine that this would be irritating -- or just a bit weird. We don't say "assume moreover that G and S are disjoint" though, because sometimes we might well want to set G = S. What is happening is that we want elements of G to be "things of type G" and elements of S to be "things of type S" and we know that even if there were some random sets which happened to be in G and in S by accident, it won't matter, because as long as we know what we're doing, and we call them g if they're in G and s if they're in S, we can "pretend they're different".

This is why you want points to be a type, because a point will always be "a thing which is a point", you'll never use a point to do anything else other than being a point. Computer scientists say "a thing of type Point" for "a thing which is a point".

On the other hand, you absolutely want to allow lines to contain a common point, and this is a natural part of the theory. So you don't want lines to be types, you want them to be subsets, or possibly subtypes, of the type of points.

[Marc Masdeu]

@Kevin Buzzard thanks for the very nice explanation. We usually don't think about this, and it's surprising how long one can be doing maths without ever having this clarified.

[Vaibhav Karve]

The difference between type theory and set theory is that in type theory, the only sets you can have are subsets of a fixed set. It took me a long time to realise that mathematicians use the concept of set in two different ways.

@Kevin Buzzard Can you elaborate on that? Things that obey ZFC is one way i can think of. What's the other?

[Mario Carneiro]

There are sets, and then there are subsets. These are treated in the same way by ZFC

[Mario Carneiro]

Sometimes, you just talk about an arbitrary set taken from the universe of all sets. These are like types in type theory. Other times you have a set that lives in another set, for example an open set in a topology. These admit a reasonable notion of intersection, complement, and other such things, and they are represented by elements of the type set A

[Marc Masdeu]

OK back to Hilbert's axioms. I have introduced a few more axioms and proved some more basic lemmas about them. The file is getting long and Lean takes time to react after each small change, so I decide to reorganize things a bit.

• Is it possible to "input" (in the LaTeX terminology) a file, so that Lean just inserts the content of that file at the beginning?
  A better way would be to start writing a structure, and this is the route I'd like to take (mainly for the sake of learning how to do it). So I have:

import tactic

noncomputable theory

-- We want to be able to define functions using the law of excluded middle
open_locale classical

universe u

structure HilbertPlane (Point : Type u) :=

(Lines : set(set(Point)))
(lies_on : Point → Lines → Prop)

(I1 : ∀ A B : Point,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2 : ∀ ℓ ∈ Lines, ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))
(between : Point → Point → Point → Prop)

and Lean seems happy so far. But for the next axioms I want to have some notation. In the previous version I had something like

notation A `*` B `*` C := between A B C
definition colinear (A B C : Point) := ∃ ℓ ∈ HilbertPlane.Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ

but now both lines fail. I assume that this gets me out of the structure, but I would really like to have such notation inside to be able to both state the axioms in a more readable way, and also in order to be able to use the HilbertPlane structure in an easy way later when writing theorems.
How is this done in Lean (I looked at @Ali Sever solution and in the list of axioms there is no notation being added...).
Thanks!

[Kevin Buzzard]

import = input

[Kevin Buzzard]

Marc -- if you want to get confused about imports, take a look at my lecture for today

[Marc Masdeu]

Marc -- if you want to get confused about imports, take a look at my lecture for today

I thought that import was more like \include. In particular, if I split a file into two files (foo.lean and bar.lean) and put import foo in bar.lean I get complaints all over.

[Johan Commelin]

@Marc Masdeu You can use import, but you will have to reopen namespaces and such

[Marc Masdeu]

I thought @Kevin Buzzard and @Johan Commelin would tell me to definitely pursue my second option (structures). Is it that it it's not so easy to do what I wanted?

[Mario Carneiro]

You can do the notation in the middle of defining the structure by enclosing it in parentheses, like so:

structure HilbertPlane (Point : Type u) :=

(Lines : set(set(Point)))
(lies_on : Point → Lines → Prop)

(I1 : ∀ A B : Point,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2 : ∀ ℓ ∈ Lines, ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))
(between : Point → Point → Point → Prop)
(notation A `*` B `*` C := between A B C)

The definition is however not so easy

[Mario Carneiro]

You could make it another part of the structure, but then it isn't guaranteed to have the definition you want and you have to impose that separately

[Johan Commelin]

Concerning using notation in the definition of a structure: See how it's done for categories a long time ago: https://github.com/leanprover-community/mathlib/blob/c06fb67cf8b7bcc3e5e76c46b699d01cd4c212a6/src/category_theory/category.lean#L46L54

[Johan Commelin]

Aha, Mario beat me.

[Johan Commelin]

You have to restate the notation after the definition if you want it to exist outside the structure definition

[Mario Carneiro]

Otherwise, you have to define the structure in two stages, like so:

structure PreHilbertPlane (Point : Type u) :=

(Lines : set(set(Point)))
(lies_on : Point → Lines → Prop)

(I1 : ∀ A B : Point,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2 : ∀ ℓ ∈ Lines, ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))
(between : Point → Point → Point → Prop)
(notation A `*` B `*` C := between A B C)

definition colinear {Point} (Ω : PreHilbertPlane Point) (A B C : Point) :=
∃ ℓ ∈ Ω.Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ

structure HilbertPlane (Point : Type u) extends PreHilbertPlane Point :=
(notation `colinear` := colinear to_PreHilbertPlane)
(foo : ∀ a, colinear a a a)
(etc : ...)

[Johan Commelin]

How about extending the code that Kenny built in the other thread?

[Marc Masdeu]

That code has lots of things that I don't understand: class, instance, @[...], ... Also, the set of axioms is different. There are several formalizations of geometry, what I am trying to do is: take Hartshorne's UTM book and translate some chapters into Lean. I'd like to do this in the most straightforward way: ideally, you should be able to translate clear pen-and-paper thoughts into Lean, not having to re-think them. So if at some point he introduces a definition, I'd like to do so at the same point, etcetera.

[Marc Masdeu]

@Mario Carneiro Is that Lean-Kosher and not a hack? I want to think about between and colinear in a very similar way. One is an undefined property that 3 points can have, whereas the other is a defined property.

[Mario Carneiro]

The way I wrote it in the last code snippet, it is a defined property

[Mario Carneiro]

The version with it being an undefined property with a characterization looks like this:

structure HilbertPlane (Point : Type u) :=

(Lines : set(set(Point)))
(lies_on : Point → Lines → Prop)

(I1 : ∀ A B : Point,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2 : ∀ ℓ ∈ Lines, ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))
(between : Point → Point → Point → Prop)
(notation A `*` B `*` C := between A B C)
(colinear : Point → Point → Point → Prop)
(colinear_def : ∀ A B C, colinear A B C ↔ ∃ ℓ ∈ Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ)
(etc : ...)

[Marc Masdeu]

The way I wrote it in the last code snippet, it is a defined property

Yes, I meant that the way between and colinear are introduced in the code is very different (and also now I have an extra structure, which may be useful but requires changing the layout I had initially)...

[Marc Masdeu]

@Mario Carneiro Oh! So the last code snippet does work? This is exactly what I was looking for.

[Mario Carneiro]

There is a third option, which is to have colinear be a (large) notation in the definition, resulting in complicated axioms, but then pick up the pieces afterward

structure HilbertPlane (Point : Type u) :=

(Lines : set(set(Point)))
(lies_on : Point → Lines → Prop)

(I1 : ∀ A B : Point,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2 : ∀ ℓ ∈ Lines, ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))
(between : Point → Point → Point → Prop)
(notation A `*` B `*` C := between A B C)
(notation `colinear` := λ A B C : Point, ∃ ℓ ∈ Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ)
(foo : ∀ a, colinear a a a)

def colinear {Point} (Ω : HilbertPlane Point) (A B C : Point) :=
∃ ℓ ∈ Ω.Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ

theorem HilbertPlane.foo' {Point} (Ω : HilbertPlane Point) :
  ∀ a, colinear Ω a a a := HilbertPlane.foo _

[Mario Carneiro]

Note that the actual type of HilbertPlane.foo here is:

#print HilbertPlane.foo
-- def HilbertPlane.foo : ∀ {Point : Type u} (c : HilbertPlane Point) (a : Point),
--   (λ (A B C : Point), ∃ (ℓ : set Point) (H : ℓ ∈ c.Lines), A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ) a a a

[Mario Carneiro]

There are several formalizations of geometry, what I am trying to do is: take Hartshorne's UTM book and translate some chapters into Lean. I'd like to do this in the most straightforward way: ideally, you should be able to translate clear pen-and-paper thoughts into Lean, not having to re-think them. So if at some point he introduces a definition, I'd like to do so at the same point, etcetera.

Sadly, this approach generally doesn't work out in the long term. Trying to stick too closely to a mathematical presentation can make your job harder than it already is

[Mario Carneiro]

Using a math text as a guide is a good idea, but expect to have to make small modifications frequently

[Marc Masdeu]

Sadly, this approach generally doesn't work out in the long term. Trying to stick too closely to a mathematical presentation can make your job harder than it already is

I agree with you that if you want to make such code available to others it is best to think carefully on design so that you don't run into problems later. My goal is different: I am trying to learn Lean "as a user", and one way is to see how everything that a book (or myself) would want to put in a paper can be translated. Same happens when you program: writing a library / module is very different than translating an idea you have for an algorithm into python, say.

[Mario Carneiro]

I think what you are doing is a valuable way to learn, and a math text is a good starting point. I'm just saying that you shouldn't be afraid to make modifications in service of easier formalization

[Mario Carneiro]

which is itself important for learning how to write "lean idioms", things that work with the theorem prover rather than against it

[Marc Masdeu]

Completely agree. When I learned Python, the code that I wrote looked a lot like what I would have written in C. The more I learned, the more Python slang I could fluently speak and then I started thinking of my algorithms in a more pythonic way. I am at the first stage with Lean.

[Mario Carneiro]

While I am not saying you should just pick up Kenny's code, it does have a lot of idioms in it that could be useful for you

[Marc Masdeu]

I am trying to understand what's in there, but I find it hard (I don't yet know enough Lean language).

[Sebastien Gouezel]

colinear or collinear?

[Marc Masdeu]

I have put the definitions into a class, split the code into two files and I am running into more problems.

1. I learned that I couldn't put the definitions in axioms.lean because then things broke. I changed the file name into hpdefs.lean and suddenly it worked. This was utterly frustrating, is there a simple explanation?
2. I don't now how to use the notations that I defined in the class I made, in another file.

This is my code so far:

hpdefs.lean file:

import tactic

namespace hilbertplane

noncomputable theory

-- We want to be able to define functions using the law of excluded middle
open_locale classical

universe u

notation p `xor` q := (p ∧ ¬ q) ∨ (q ∧ ¬ p)

class HilbertPlane:=
    (Point : Type u)
    (Lines : set(set(Point)))

    (I1 : ∀ A B : Point,  A ≠ B → ∃! (ℓ ∈ Lines), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
    (I2 : ∀ ℓ ∈ Lines, ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
    (I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ ∈ Lines, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))
    (between : Point → Point → Point → Prop)
    (notation A `*` B `*` C := between A B C)
    (collinear : Point → Point → Point → Prop)
    (collinear_def : ∀ A B C, collinear A B C ↔ ∃ ℓ ∈ Lines, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ)
    (noncollinear : Point → Point → Point → Prop)
    (noncollinear_def : ∀ A B C, noncollinear A B C ↔ ¬ collinear A B C)

    (B11 (A B C : Point) : (A * B * C) → (C * B * A))
    (B12 (A B C : Point) : (A * B * C) → (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ collinear A B C))
    (B2 (A B : Point) : ∃ C, A * B * C)
    (B3 (A B C : Point) {ℓ ∈ Lines}
        (hAB : A ≠ B) (hAC : A ≠ C) (hBC : B ≠ C)
        (hAl : A ∈ ℓ) (hBl : B ∈ ℓ) (hCl : C ∈ ℓ) :
        ((A * B * C) ∧ ¬( B * A * C ) ∧ ¬ (A * C * B)) ∨
        (¬ (A * B * C) ∧ ( B * A * C ) ∧ ¬ (A * C * B)) ∨
        (¬ (A * B * C) ∧ ¬( B * A * C ) ∧ (A * C * B)))

    (B4 (A B C D: Point) {ℓ ∈ Lines}
        (hnc: noncollinear A B C)
        (hnAl: ¬ (A ∈ ℓ)) (hnBl: ¬ B ∈ ℓ) (hnCl: ¬ C ∈ ℓ)
        (hDl: D ∈ ℓ) (hADB: A * D * B) : (∃ E : Point, (A * E * C) xor (B * E * C)))

    (intersect : set Point → set Point → Prop)
    (intersect_def (r s : set(Point)) : (intersect r s ↔ ∃ A : Point, A ∈ r ∧ A ∈ s))

    (parallel : set Point → set Point → Prop)
    (parallel_def (r s : set Point) : parallel r s ↔  r ∈ Lines ∧ s ∈ Lines → (r = s) ∨ (¬ (intersect r s)))
    (notation r `||` s := parallel r s)

    (parallel_postulate {A : Point} {ℓ r s : set Point}
        (h1 : ℓ ∈ Lines) (hr : r ∈ Lines) (hs : s ∈ Lines) :
        A ∈ r ∧ A ∈ s ∧ r || ℓ ∧ s || ℓ → r = s)

    (line_segment (A B : Point) : set Point := {A} ∪ {B} ∪ {C | A * C * B})
    (notation A `#` B := line_segment A B)
    (triangle (A B C : Point)  (h: noncollinear A B C) : set Point := (A#B) ∪ (A#C) ∪ (B#C))

end hilbertplane

firstlemmas.lean

import .hpdefs

open hilbertplane

variables {Ω : HilbertPlane}
variables {A B C: Ω.Point}
variables {ℓ r s : set(Ω.Point)}


lemma I11 :  ∀ A B, A ≠ B → ∃ ℓ ∈ Ω.Lines, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ) :=
begin
intros A B,
intro h,
cases HilbertPlane.I1 A B h with ℓ h1,
existsi ℓ,
cases h1 with H,
exact exists_of_exists_unique H,
end

lemma endpoints_are_in_segment (A B : Ω.Point) : A ∈ A#B ∧ B ∈ A#B :=
begin
split; {
unfold line_segment,
finish,
}
end

and the lemma endpoints_are_in_segment bothers Lean because it doesn't understand the # notation. Any pointers? Thank you.

[Mario Carneiro]

The filename thing sounds mysterious. Could you describe more precisely what you did and what happened?

[Mario Carneiro]

One possibility that comes to mind is that axioms is a keyword, so if you write import axioms it will import nothing and then start declaring axioms

[Mario Carneiro]

If you really want to call the file axioms.lean, you can import it using french quote escapes: import «axioms»

[Mario Carneiro]

As for notations, you have to redeclare all the notations outside the structure because they are scoped to the structure definition itself

[Marc Masdeu]

The filename thing sounds mysterious. Could you describe more precisely what you did and what happened?

Rename the file hpdefs.lean into axioms.lean. Then in firstlemmas.lean have the first line import .axioms and Lean complains. But your explanation is reasonable. I will avoid this file name in the future.

[Marc Masdeu]

OK, I got stuck again. I don't see why the following code does not work:

import tactic

noncomputable theory

-- We want to be able to define functions using the law of excluded middle
open_locale classical

universe u

class HilbertPlane:=
    (Point : Type u)
    (Lines : set(set(Point)))
    (line_segment : Point → Point → set Point)
    (line_segment_def (A B : Point) : line_segment A B = {A} ∪ {B})

constant Ω : HilbertPlane

lemma endpoints_are_in_segment (A B : Ω.Point) : (A ∈ (Ω.line_segment A B)) :=
begin
sorry,
end

It is frustrating, since this works perfectly:

import tactic

noncomputable theory

-- We want to be able to define functions using the law of excluded middle
open_locale classical

universe u

constant Point : Type u
constant Lines : set(set(Point))
definition line_segment (A B : Point) : set Point := {A} ∪ {B}

lemma endpoints_are_in_segment (A B : Point) : (A ∈ line_segment A B) :=
begin
unfold line_segment,
finish,
end

Apart from the solution, I would appreciate being able to tell in the future how to fix these issues (by reading at errors, or using "debugging" commands in Lean). I hope I didn't have to constantly ask Zulip...

[Mario Carneiro]

Let's start with the error message.

invalid field notation, function 'HilbertPlane.line_segment' does not have explicit argument with type (HilbertPlane ...)

Okay, that's weird. What type does it actually have?

#print HilbertPlane.line_segment

@[reducible]
def HilbertPlane.line_segment : Π [c : HilbertPlane], HilbertPlane.Point → HilbertPlane.Point → set HilbertPlane.Point :=
λ [c : HilbertPlane], [HilbertPlane.line_segment c]

Notice that c here, the HilbertPlane argument in question, is in square brackets. That means it is intended to be inferred by type class inference. Why? Because you called HilbertPlane a class rather than a structure.

[Mario Carneiro]

The idea with typeclass arguments is that you don't specify them, you let lean figure them out. Let's try that:

lemma endpoints_are_in_segment (A B : Ω.Point) : (A ∈ (line_segment A B)) := sorry

unknown identifier 'line_segment'

Thanks lean. Guess we need to open the namespace

open HilbertPlane
lemma endpoints_are_in_segment (A B : Ω.Point) : (A ∈ (line_segment A B)) := sorry

failed to synthesize type class instance for
A : Point,
B : Point
⊢ HilbertPlane

Okay, getting closer. It says it can't find an instance of HilbertPlane. (Notice also that it omits the Ω in Point. Clearly that's how it expects you to write it.) I will note at this point that HilbertPlane has no arguments, which is rather unusual for a typeclass. It's really only a useful construct if there is only ever one HilbertPlane around, but maybe that's the case for you.

[Mario Carneiro]

In any case, we can add it as an instance variable, and then lean should find it:

variable [HilbertPlane]

open HilbertPlane
lemma endpoints_are_in_segment (A B : Point) : (A ∈ (line_segment A B)) := sorry

kernel failed to type check declaration 'endpoints_are_in_segment' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ [_inst_1 : HilbertPlane] (A B : Point), A ∈ line_segment A B
elaborated value:
  λ [_inst_1 : HilbertPlane] (A B : Point), sorry
nested exception message:
invalid reference to undefined universe level parameter 'u_1'

Ooh, these are extra special errors that you get if you managed to fool the tactic framework into producing an invalid proof. I think this will go away if you actually finish the proof, though.

[Mario Carneiro]

variable [HilbertPlane]

open HilbertPlane
lemma endpoints_are_in_segment (A B : Point) : (A ∈ (line_segment A B)) :=
by simp [line_segment_def]

kernel failed to type check declaration 'endpoints_are_in_segment' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ [_inst_1 : HilbertPlane] (A B : Point), A ∈ line_segment A B
elaborated value:
  λ [_inst_1 : HilbertPlane] (A B : Point),
    eq.mpr
      ...
      trivial
nested exception message:
invalid reference to undefined universe level parameter 'u_1'

Apparently my hope was unfounded. This is an actual bug in lean, so I'm not sure what the best workaround is, but explicitly including the instance seems to work:

variable [Ω : HilbertPlane]
include Ω

open HilbertPlane
lemma endpoints_are_in_segment (A B : Point) : (A ∈ (line_segment A B)) :=
by simp [line_segment_def] -- works

[Marc Masdeu]

Oh wow! This is a great explanation!! I will see if I can fit this into the rest of the code. Still, I doubt I'd be able to debug something like this in the future. Lean is hard.

[Patrick Massot]

I really don't see the point of having a type class with no argument. Why don't you make the type of points a parameter of HilbertPlane? This would be useful if you want to extend to three-dimensional geometry. Then you'll have subtypes having a HilbertPlane structure.

[Mario Carneiro]

@Patrick Massot One reason you might not want to use HilbertPlane P where P is the type of points is that there are also lines to deal with. Would you write Lines P for that type?

[Kevin Buzzard]

Oh wow! This is a great explanation!! I will see if I can fit this into the rest of the code. Still, I doubt I'd be able to debug something like this in the future. Lean is hard.

Algebraic number theory is hard. There's a learning curve. I couldn't do my first year example sheets for a long time. Working on them taught me basic logic, then defining schemes taught me about classes and structures, and then I learnt how to read the error messages, and now I can usually solve problems myself. The way to learn it is to do exactly what you're doing -- try some maths at a level which is suitable for your current formalisation skills and ask when you get stuck, then repeat

[Marc Masdeu]

@Mario Carneiro and @Patrick Massot I will probably deal with these issues later...

[Marc Masdeu]

Now I have a file hpdefs.lean and a file lesson1.lean, this second one with some lemmas that seem to compile (I'm still using CoCalc for this). I want to start a new file, lesson2.lean. I type this into the new file:

import .lesson1

open hilbertplane

variables {Ω : HilbertPlane}

and it already complains that "imported file '/home/user/leanprojects/test/src/lesson1.lean' uses sorry" (which I can't see in that file). So what does that error message mean actually?

[Patrick Massot]

The sorry may be in a file imported by lesson1

[Marc Masdeu]

lesson1 only imports hpdefs, which has no sorry's either...

[Marc Masdeu]

It turns out that cocalc had issues with some sort of caching. I restarted everything and the complaint went away... Thanks @Patrick Massot !

[Marc Masdeu]

This question should be quick: I have the state:

Ω : HilbertPlane,
A : HilbertPlane.Point
⊢ {C : HilbertPlane.Point | A * C*A} = ∅

This is a trivial statement, directly following from the axiom:

    (B12 (A B C : Point) : (A * B * C) → (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ collinear A B C))

but I don't see how to do it in Lean. I would like to say to Lean:
1) Let C be a point in the left set.
2) By B12 A B A we have A \neq A, contradiction.

[Patrick Massot]

A generic start would be ext C, suffices : ¬ A*C*A, by simpa,.

[Marc Masdeu]

The ext C is what I didn't know...

[Marc Masdeu]

I then intro'd h : A * C * A
I want to apply B12's second inequality (one of the 4 and statements). I suceeded with

have g := (HilbertPlane.B12 A C A) h,
finish,

:grinning:

[Marc Masdeu]

It's clear how to proceed here:

Tactic State
Ω : HilbertPlane,
A : HilbertPlane.Point,
ℓ : set HilbertPlane.Point,
h : A ∉ ℓ
⊢ {A} ∩ ℓ = ∅

I even found something called set.inter_singleton_eq_empty, which looks like would finish this instantly. But I don't now how to apply it.

It's clear that this is not the most direct way:

ext C,
split,
{
intro h,
exfalso,
cases h with h3 h4,
finish,
},
simp,

How could I do easier? On a related note, if I managed to prove a statement in some sort of convoluted way (like above), can I ask Lean to give me a proof that I can paste back to avoid using complicated tactics?

[Johan Commelin]

@Marc Masdeu That name reads like the singleton is on the right hand side of ∩

[Johan Commelin]

Is there also set.singleton_inter_eq_empty?

[Johan Commelin]

Otherwise, maybe rw set.inter_comm?

[Johan Commelin]

(I just made up that name, but it should exist.)

[Johan Commelin]

Also squeeze_simp [h] might be able to help

[Marc Masdeu]

Otherwise, maybe rw set.inter_comm?

This worked! So I finished it with:

rw set.inter_comm,
rw set.inter_singleton_eq_empty,
exact h1,

Great!

[Johan Commelin]

@Marc Masdeu Does this mean that set.singleton_inter_eq_empty is missing? If so, that's a (tiny) hole in the library

[Marc Masdeu]

It does exist, and it clears the goal in one less line :-).

[Johan Commelin]

I guess you could save another line if you don't rw but exact

[Johan Commelin]

@Marc Masdeu Do you know about suggest?

[Johan Commelin]

I guess if you type suggest for your initial problem, it would tell you how to close the goal in 1 line.

[Marc Masdeu]

Marc Masdeu Do you know about suggest?

Oh no, I didn't know about this one! I am getting a bit mixed up with suggest, simp, simpa, finish, cc and so on...

[Johan Commelin]

Haha, I can imagine

[Johan Commelin]

suggest is extremely useful.

[Johan Commelin]

So useful that I wish there was a dedicated window showing its results, without having to type it myself.

[Marc Masdeu]

Now that I have you here, do you know of an analogue for rcases to deal with

h : p \and q \and r \and s

I would like to do something like split_h into \langle h1, h2, h3, h4 \rangle. Instead, i do:

have hAB := h1.left,
have h2 := h1.right,
have hAC := h2.left,
have h3 := h2.right,
have hBC := h3.left,
have h4 := h3.right,

[Reid Barton]

That's what rcases does

[Reid Barton]

split_h into -> rcases h with

[Marc Masdeu]

Oh, I just tried and it did work. I am realising that it works in different settings (I had just used it in \exists A B C... type statements)

[Marc Masdeu]

So useful that I wish there was a dedicated window showing its results, without having to type it myself.

I haven't managed to use suggest from CoCalc. Is this a VSCode feature?

[Reid Barton]

Ah yes. rcases works on any inductive type, including equality, and I think also quotients

[Johan Commelin]

So useful that I wish there was a dedicated window showing its results, without having to type it myself.

I haven't managed to use suggest from CoCalc. Is this a VSCode feature?

@Marc Masdeu No, it's pure mathlib. But it's not that old. So maybe CoCalc is using an old version of mathlib? Did you install it yourself on CoCalc, or are you using the mathlib that is available by default? (That one might be >1yr old.)

[Marc Masdeu]

Marc Masdeu No, it's pure mathlib. But it's not that old. So maybe CoCalc is using an old version of mathlib? Did you install it yourself on CoCalc, or are you using the mathlib that is available by default? (That one might be >1yr old.)

I just cloned the newest version, put it in CoCalc and it doesn't work. Do I have to open any particular namespace? It doesn't recognize it.

[Reid Barton]

Oh, you need import tactic.suggest

[Bryan Gin-ge Chen]

Either import tactic.basic or import tactic should work too.

[Kevin Buzzard]

also with cocalc you have to know that its Lean is reading the leanpkg.path in the root directory of the project as opposed to any other one in any other directory.

[Marc Masdeu]

Haven't succeeded yet... I checked that I was using the right mathlib version by changing the folder and then failing to import anything. I changed the folder back. @Kevin Buzzard Yes, I did know that I have no control over where Lean takes its files from.

[Kevin Buzzard]

you have control, it's just that you basically have one piece of control per cocalc project (and if you have one paid cocalc project with many lean projects in then it can get messy)

[Julien Narboux]

@Kevin Buzzard our formalization of Hilbert's geometry, use just a type for lines. In fact, I think we did not need sets at all to formalize Hilbert's geometry. Our axioms are here:
https://github.com/GeoCoq/GeoCoq/blob/master/Axioms/hilbert_axioms.v

[Julien Narboux]

We proved that those axioms are mutually interpretable with those of Tarski, so the formalization is ok in this sense.

[Patrick Massot]

What do you gain by explicitly embedding all those decidability assumption instead of just using classical reasoning everywhere in the library? I would understand the idea of delimiting results that are classically valid, but those assumption are there at the very bottom of the hierarchy, right?

[Patrick Massot]

I would also be curious to know why you don't introduce notations like A ∈ L for IncidL A L. There is no risk of being misled by notations instead of following the rules since Coq is checking everything.

[Patrick Massot]

I can't read two_points_on_line : forall l, { A : Point & { B | IncidL B l /\ IncidL A l /\ A <> B}}. I understand it says each lines contains at least two distinct points, but I don't understand the way it is stated. What is the syntax here?

[Patrick Massot]

For people interested in GeoCoq, here the regex translation Coq -> Lean of the first class in Julien's file (modulo the strange syntax that I translated using my maths intuition without understanding the Coq syntax).

class Hilbert_neutral_dimensionless :=
(Point : Type)
(Line  : Type)
(Plane : Type)
(EqL   : Line → Line → Prop)
(EqL_Equiv : equivalence EqL)
(EqP   : Plane → Plane → Prop)
(EqP_Equiv : equivalence EqP)
(IncidL : Point → Line → Prop)
(IncidP : Point → Plane → Prop)
(IncidL_morphism :
  ∀ P l m, IncidL P l → EqL l m → IncidL P m)
(IncidL_dec : ∀ P l, IncidL P l ∨ ¬ IncidL P l)
(IncidP_morphism :
  ∀ M p q, IncidP M p → EqP p q → IncidP M q)
(IncidP_dec : ∀ M p, IncidP M p ∨ ¬ IncidP M p)
(eq_dec_pointsH : ∀ A B : Point, A=B ∨ ¬ A=B)

/- Group I Incidence -/
(line_existence :
  ∀ A B, A ≠ B → ∃ l, IncidL A l ∧ IncidL B l)
(line_uniqueness :
  ∀ A B l m,
    A ≠ B →
    IncidL A l → IncidL B l → IncidL A m → IncidL B m →
    EqL l m)
(two_points_on_line :
  ∀ l, ∃ A B : Point, IncidL B l ∧ IncidL A l ∧ A ≠ B)
(ColH :=
  fun A B C, ∃ l, IncidL A l ∧ IncidL B l ∧ IncidL C l)
(PP : Point)
(PQ : Point)
(PR : Point)
(lower_dim_2 : PP ≠ PQ ∧ PQ ≠ PR ∧ PP ≠ PR ∧ ¬ ColH PP PQ PR)
(plane_existence :
  ∀ A B C, ¬ ColH A B C → ∃ p, IncidP A p ∧ IncidP B p ∧ IncidP C p)
(one_point_on_plane :
  ∀ p, ∃ A, IncidP A p)
(plane_uniqueness :
  ∀ A B C p q,
    ¬ ColH A B C →
    IncidP A p → IncidP B p → IncidP C p → IncidP A q → IncidP B q → IncidP C q →
    EqP p q)
(IncidLP :=
   fun l p, ∀ A, IncidL A l → IncidP A p)
(line_on_plane :
  ∀ A B l p,
    A ≠ B →
    IncidL A l → IncidL B l → IncidP A p → IncidP B p →
    IncidLP l p)

/- Group II Order -/
(BetH   : Point → Point → Point → Prop)
(between_diff : ∀ A B C, BetH A B C → A ≠ C)
(between_col :  ∀ A B C, BetH A B C → ColH A B C)
(between_comm : ∀ A B C, BetH A B C → BetH C B A)
(between_out :  ∀ A B, A ≠ B → ∃ C, BetH A B C)
(between_only_one : ∀ A B C, BetH A B C → ¬ BetH B C A)
(cut :=
  fun l A B , ¬ IncidL A l ∧ ¬ IncidL B l ∧
               ∃ I, IncidL I l ∧ BetH A I B)
(pasch :
  ∀ A B C l p,
    ¬ ColH A B C →
    IncidP A p → IncidP B p → IncidP C p → IncidLP l p → ¬ IncidL C l → cut l A B →
    cut l A C ∨ cut l B C)

/- Group III Congruence -/
(CongH : Point → Point → Point → Point → Prop)
(cong_permr : ∀ A B C D, CongH A B C D → CongH A B D C)
(outH :=
  fun P A B, BetH P A B ∨ BetH P B A ∨ (P ≠ A ∧ A = B))
(cong_existence :
  ∀ A B A' P l,
    A ≠ B → A' ≠ P →
    IncidL A' l → IncidL P l →
    ∃ B', IncidL B' l ∧ outH A' P B' ∧ CongH A' B' A B)
(cong_pseudo_transitivity :
  ∀ A B C D E F,
    CongH A B C D → CongH A B E F → CongH C D E F)
(disjoint := fun A B C D, ¬ ∃ P, BetH A P B ∧ BetH C P D)
(addition :
  ∀ A B C A' B' C',
    ColH A B C → ColH A' B' C' →
    disjoint A B B C → disjoint A' B' B' C' →
    CongH A B A' B' → CongH B C B' C' →
    CongH A C A' C')
(CongaH :
  Point → Point → Point → Point → Point → Point → Prop)
(conga_refl : ∀ A B C, ¬ ColH A B C → CongaH A B C A B C)
(conga_comm : ∀ A B C, ¬ ColH A B C → CongaH A B C C B A)
(conga_permlr :
  ∀ A B C D E F, CongaH A B C D E F → CongaH C B A F E D)
(same_side := fun A B l, ∃ P, cut l A P ∧ cut l B P)
(same_side' :=
  fun A B X Y,
    X ≠ Y ∧
    ∀ l, IncidL X l → IncidL Y l → same_side A B l)
(conga_out_conga :
  ∀ A B C D E F A' C' D' F',
   CongaH A B C D E F →
   outH B A A' → outH B C C' → outH E D D' → outH E F F' →
   CongaH A' B C' D' E F')
(cong_4_existence :
  ∀ A B C O X P,
    ¬ ColH P O X → ¬ ColH A B C →
    ∃ Y, CongaH A B C X O Y ∧ same_side' P Y O X)
(cong_4_uniqueness :
  ∀ A B C O P X Y Y',
    ¬ ColH P O X  → ¬ ColH A B C →
    CongaH A B C X O Y → CongaH A B C X O Y' →
    same_side' P Y O X → same_side' P Y' O X →
    outH O Y Y')
(cong_5 :
  ∀ A B C A' B' C',
    ¬ ColH A B C → ¬ ColH A' B' C' →
    CongH A B A' B' → CongH A C A' C' →
    CongaH B A C B' A' C' →
    CongaH A B C A' B' C')

[Reid Barton]

{ A : Point & ... } is a dependent pair I think, like Σ (A : Point), .... After that comes a subtype.

[Patrick Massot]

Thanks Reid. So this is again intuitionistic stuff.

[Mario Carneiro]

Those := lines don't work in lean the way I infer they work in coq

[Patrick Massot]

Really?

[Patrick Massot]

Oh yes

[Patrick Massot]

I should have known what they do in Lean.

[Patrick Massot]

How do we do that in Lean then?

[Mario Carneiro]

I'm actually kind of curious how this is supported in coq

[Patrick Massot]

Introduce a notation only?

[Mario Carneiro]

you could do that, or you could add a field in the structure (possibly using := to give it the obvious default value) and then another field asserting equality to the required definition

[Mario Carneiro]

you won't get defeq of the field to its definition, although for an axiomatization like this it doesn't matter

[Reid Barton]

huh yeah, what is the type of ColH in the coq version?

[Patrick Massot]

Point -> Point -> Point -> Prop

[Patrick Massot]

It says three point sit on the same line.

[Reid Barton]

But isn't it actually (T : Hilbert_neutral_dimensionless) -> T.Point -> T.Point -> T.Point -> Prop or something?

[Mario Carneiro]

I think in coq that is actually a let binder in the middle of the structure

[Mario Carneiro]

which is not something you can do in lean

[Mario Carneiro]

but coq has support for let binders in the context, unlike lean, so that might be easier to support

[Reid Barton]

then does the type of plane_existence for example have a let binder in it?

[Mario Carneiro]

In Hilbert_neutral_dimensionless.mk, there is a let binder in the middle of the long string of arguments; in Hilbert_neutral_dimensionless.plane_existence there is a reference to an external definition Hilbert_neutral_dimensionless.ColH

[Mario Carneiro]

or at least, that's how I would implement it

[Mario Carneiro]

but in lean if you tried that the kernel would unfold the let and in a definition this deep that could be a significant performance problem

[Mario Carneiro]

in coq they have "zeta reduction" which is Gamma, x : A := t |- x ~> t, while in lean what I call zeta reduction is Gamma |- (let x : A := t in e) ~> e[t/x]

[Reid Barton]

sort of like lazy vs call-by-name evaluation?

[Reid Barton]

well, maybe not that much like it

[Reid Barton]

but somehow the work of substituting is delayed, I guess

[Patrick Massot]

I've played the game of rewriting the beginning using notations (and getting rid of avoiding the equality sign):

class Hilbert_neutral_dimensionless :=
(Point : Type)
(Line  : Type)
(Plane : Type)
[IncidL :  has_mem Point  Line]
[IncidP : has_mem Point Plane]

/- Group I Incidence -/
(line_existence :
  ∀ A B, A ≠ B → ∃ l : Line, A ∈ l ∧ B ∈ l)
(line_uniqueness :
  ∀ A B (l m : Line),
    A ≠ B →
    A ∈ l → B ∈ l → A ∈ m → B ∈ m →
    l = m)
(two_points_on_line :
  ∀ l : Line, ∃ A B, B ∈ l ∧ A ∈ l ∧ A ≠ B)
(notation `ColH⟮`A`, `B`, `C `⟯` := ∃ l : Line, A ∈ l ∧ B ∈ l ∧ C ∈ l)
(PP : Point)
(PQ : Point)
(PR : Point)
(lower_dim_2 : PP ≠ PQ ∧ PQ ≠ PR ∧ PP ≠ PR ∧ ¬ ColH⟮PP, PQ, PR⟯)
(plane_existence :
  ∀ A B C, ¬ ColH⟮A, B, C⟯ → ∃ p : Plane, A ∈ p ∧ B ∈ p ∧ C ∈ p)
(one_point_on_plane :
  ∀ p : Plane, ∃ A, A ∈ p)
(plane_uniqueness :
  ∀ A B C (p q : Plane),
    ¬ ColH⟮A, B, C⟯ →
    A ∈ p → B ∈ p → C ∈ p → A ∈ q → B ∈ q → C ∈ q →
    p = q)
(notation l `⊆` p := ∀ A, A ∈ (l : Line) → A ∈ (p : Plane))
(line_on_plane :
  ∀ A B l p,
    A ≠ B →
    A ∈ l → B ∈ l → A ∈ p → B ∈ p →
    l ⊆ p)

/- Group II Order -/
(BetH : Point → Point → Point → Prop)
(notation A `✶`:55 B:60 `✶`:55 C:60 := BetH A B C)
(between_diff : ∀ A B C, A ✶ B ✶ C → A ≠ C)
(between_col :  ∀ A B C, A ✶ B ✶ C → ColH⟮A, B, C⟯)
(between_comm : ∀ A B C, A ✶ B ✶ C → C ✶ B ✶ A)
(between_out :  ∀ A B, A ≠ B → ∃ C, A ✶ B ✶ C)
(between_only_one : ∀ A B C, A ✶ B ✶ C → ¬ B ✶ C ✶ A)
(notation `⟮`A `|`:55 l`|`:55 B `⟯` := ¬ A ∈ l ∧ ¬ B ∈ l ∧
               ∃ I, I ∈ l ∧ A ✶ I ✶ B) -- cut: A and B are separated by l
(pasch :
  ∀ A B C (l : Line) (p : Plane),
    ¬ ColH⟮A, B, C⟯ →
    A ∈ p → B ∈ p → C ∈ p → l ⊆ p → ¬ C ∈ l → ⟮A |l| B⟯ →
    ⟮A |l| C⟯ ∨ ⟮B |l| C⟯)

[Reid Barton]

the has_mem fields threw me for a moment. Clever

[Patrick Massot]

The down-side of this trick is it requires type annotations later on (otherwise Lean cannot tell what is a line and what is a plane).

[Patrick Massot]

Julien, the relevant definitions here are:

class has_mem (α : Type u) (γ : Type v) := (mem : α → γ → Prop)
infix ∈ := has_mem.mem

[Patrick Massot]

So every time Lean sees A ∈ P and can infer the types of A and P are X and Y, it tries to solve the type class problem has_mem X Y.

[Mario Carneiro]

My fonts don't know what you are using for ColH

[Mario Carneiro]

unless you actually are bordering the variables with boxes

[Mario Carneiro]

can't you just use regular brackets or braces there?

[Reid Barton]

unicode character combining red rectangle

[Mario Carneiro]

I want to react to this with an emoji that no font supports

[Reid Barton]

it's actually MATHEMATICAL LEFT FLATTENED PARENTHESIS

[Reid Barton]

but in my experience regular parentheses work fine in notation, yes

[Kevin Buzzard]

@Ali Sever sent me a README.md for his work, so at least now we can get some sort of an idea as to what he was doing.

[Patrick Massot]

About parenthesis: the key feature of the funny parentheses is there is no risk of confusion with other parenthesis so you don't need to understand the dark art of precedence settings. I'd love to see some really practical guide to setting precedences in our mathlib docs.