# Zulip Chat Archive

## Stream: new members

### Topic: attempt at some geometry

#### Matt Earnshaw (Jan 08 2020 at 16:08):

as an exercise I wanted to try proving some theorems from Artin's *Geometric Algebra*, but I quickly hit a wall -- maybe due to being weak on the basics, maybe due to infelicitous transcription of the axioms. here is what I have so far, but as you can see I did not make much progress on the first lemma, just unsure how to proceed! apologies for the very vague 'question' but any tips or pointers would be appreciated.

-- constants of types subsume the usual statement of a theory's signature and axioms constants Pt Ln : Sort constant belongs : Pt → Ln → Prop constant parallel : Ln → Ln → Prop -- Artin def 2.1: can and ought we to formulate this as a term of type parallel l₁ l₂? this should be a definition not an axiom - is 'constant' appropriate? constant eq_or_no_common_pt_implies_parallel (l₁ l₂ : Ln) : (l₁ = l₂ ∨ ¬∃ p : Pt, belongs p l₁ ∧ belongs p l₂) → parallel l₁ l₂ -- Artin axiom 1: distinct points determine unique line constant unique_ln_bw_two_pts (p₁ p₂ : Pt) : (p₁ ≠ p₂) → ∃ p₁p₂ : Ln, belongs p₁ p₁p₂ ∧ belongs p₂ p₁p₂ ∧ (∀ l : Ln, belongs p₁ l ∧ belongs p₂ l → p₁p₂ = l) -- Artin axiom 2: exists unique parallel constant exists_parallel (p : Pt) (l : Ln) : (∃ l₁ : Ln, parallel l l₁ ∧ belongs p l₁) constant unique_parallel (p : Pt) (l l₁ l₂ : Ln) : (parallel l l₁ ∧ parallel l l₂ ∧ belongs p l₁ ∧ belongs p l₁) → l₁ = l₂ lemma line_parallel_to_itself (l : Ln) : reflexive parallel := begin have h₁ := eq_or_no_common_pt_implies_parallel l l, have h₂ := eq.refl l, sorry end theorem parallel_is_equivalence : equivalence parallel := begin -- split, -- exact line_parallel_to_itself, end

#### Kevin Buzzard (Jan 08 2020 at 16:10):

lemma line_parallel_to_itself (l : Ln) : reflexive parallel := begin intro l, apply eq_or_no_common_pt_implies_parallel, left, refl, end

#### Johan Commelin (Jan 08 2020 at 16:11):

@Matt Earnshaw In general people tend to avoid `constant`

completely, except for little demo purposes.

#### Kevin Buzzard (Jan 08 2020 at 16:11):

[note that I have proved it like a computer scientist -- I wrote the proof backwards]

#### Johan Commelin (Jan 08 2020 at 16:12):

But for testing things out, it's fine. And in that cases your "axioms" should also be encoded as `constant`

s

#### Johan Commelin (Jan 08 2020 at 16:14):

A different option would be to turn all your `constant`

s into `variable`

s, and maybe make some of them *implicit* (using `{}`

)

#### Johan Commelin (Jan 08 2020 at 16:14):

In the end, if you move away from `constant`

, your best bet would be to bundle all your data and axioms into a `structure`

#### Johan Commelin (Jan 08 2020 at 16:16):

@Matt Earnshaw You have a typo in the `unique_parallel`

axiom. You ask that `l1`

is parallel to `l`

twice.

#### Johan Commelin (Jan 08 2020 at 16:16):

Also, can't you just ask that `l1`

is parallel to `l2`

, and leave `l`

completely out of the picture?

#### Johan Commelin (Jan 08 2020 at 16:18):

Another remark: usually it's better to not use `\and`

in assumptions, but to just state the clauses as separate assumptions. That makes it easier to use the lemma/axiom

#### Matt Earnshaw (Jan 08 2020 at 17:22):

thanks both, this is very helpful already. now I am trying to make headway on the symmetry part of the equivalence relation proof. It seem necessary to introduce the converse `constant parallel_implies_eq_or_no_common_pt (l₁ l₂ : Ln) : parallel l₁ l₂ → (l₁ = l₂ ∨ ¬∃ p : Pt, belongs p l₁ ∧ belongs p l₂)`

(which finally *defines* parallel). then

lemma symmetric_parallel : symmetric parallel := begin intros l₁ l₂ h, have x := (parallel_implies_eq_or_no_common_pt l₁ l₂) h, cases x, rw x, apply line_parallel_to_itself, end

with context

l₁ l₂ : Ln, h : parallel l₁ l₂, x : ¬∃ (p : Pt), belongs p l₁ ∧ belongs p l₂ ⊢ parallel l₂ l₁

now what I *want* to do is use `and.symm`

to swap the terms in `x`

, but am stuck there.

#### Bryan Gin-ge Chen (Jan 08 2020 at 18:41):

I'm sure this can be golfed (note that I imported `logic.basic`

(for `not_exists`

) and `tactic.basic`

(for `rintro`

) from mathlib):

constant parallel_implies_eq_or_no_common_pt (l₁ l₂ : Ln) : parallel l₁ l₂ → (l₁ = l₂ ∨ ¬∃ p : Pt, belongs p l₁ ∧ belongs p l₂) lemma symmetric_parallel : symmetric parallel := begin intros l₁ l₂ h, have x := (parallel_implies_eq_or_no_common_pt l₁ l₂) h, cases x, rw x, { apply line_parallel_to_itself l₂, }, { apply eq_or_no_common_pt_implies_parallel, apply or.inr, rw [not_exists] at x ⊢, rintro x' ⟨h₁,h₂⟩, exact x x' ⟨h₂,h₁⟩, }, end

#### Johan Commelin (Jan 08 2020 at 19:04):

@Matt Earnshaw Shouldn't `parallel`

actually be a definition, as in:

def parallel (l₁ l₂ : Ln) := l₁ = l₂ ∨ (¬∃ p : Pt, belongs p l₁ ∧ belongs p l₂)

#### Matt Earnshaw (Jan 08 2020 at 19:19):

@Bryan Gin-ge Chen thanks that's helpful. think I have the transitivity proof down now

#### Matt Earnshaw (Jan 08 2020 at 19:20):

@Johan Commelin yes, it should be, thanks. makes things neater

#### Johan Commelin (Jan 08 2020 at 19:32):

@Matt Earnshaw This is what I have atm:

import tactic noncomputable theory open_locale classical -- constants of types subsume the usual statement of a theory's signature and axioms constants Pt Ln : Sort constant belongs : Pt → Ln → Prop def parallel (l₁ l₂ : Ln) := l₁ = l₂ ∨ (¬∃ p : Pt, belongs p l₁ ∧ belongs p l₂) -- Artin axiom 1: distinct points determine unique line constant unique_ln_bw_two_pts (p₁ p₂ : Pt) : (p₁ ≠ p₂) → ∃ p₁p₂ : Ln, belongs p₁ p₁p₂ ∧ belongs p₂ p₁p₂ ∧ (∀ l : Ln, belongs p₁ l ∧ belongs p₂ l → p₁p₂ = l) -- Artin axiom 2: exists unique parallel constant exists_parallel (p : Pt) (l : Ln) : (∃ l₁ : Ln, parallel l l₁ ∧ belongs p l₁) constant unique_parallel (p : Pt) (l₁ l₂ : Ln) (h₁₂ : parallel l₁ l₂) (hp₁ : belongs p l₁) (hp₂ : belongs p l₁) : l₁ = l₂ lemma parallel_refl : reflexive parallel := begin intro l, left, refl end lemma parallel_symm : symmetric parallel := begin rintros l₁ l₂ (rfl|h), { exact parallel_refl _ }, { right, contrapose! h, apply exists_imp_exists _ h, intro p, exact and.symm } end lemma parallel_trans : transitive parallel := begin rintros l₁ l₂ l₃ (rfl|h₁₂) (rfl|h₂₃), { exact parallel_refl _ }, { right, assumption }, { right, assumption }, { sorry }, end theorem parallel_is_equivalence : equivalence parallel := ⟨parallel_refl, parallel_symm, parallel_trans⟩

#### Johan Commelin (Jan 08 2020 at 19:33):

I'm using some tactics that aren't in core. But I think the help cutting through boilerplate.

#### Matt Earnshaw (Jan 08 2020 at 19:37):

that gives me `contrapose only applies to nondependent arrows between decidable props`

, though I am satisfied with the following (but still good to see alternatives)

lemma parallel_symmetric : symmetric parallel := begin intros l₁ l₂ h, cases h, { rw h, left, refl }, { right, exact h }, end

#### Johan Commelin (Jan 08 2020 at 19:40):

Look at the other lines I added to the top

#### Johan Commelin (Jan 08 2020 at 19:41):

`noncomputable theory`

and `open_locale classical`

#### Johan Commelin (Jan 08 2020 at 19:42):

How can `right, exact h`

close that goal? You need to apply symmetry somewhere.

#### Matt Earnshaw (Jan 08 2020 at 19:43):

ah I see

#### Matt Earnshaw (Jan 08 2020 at 19:45):

hm, I suppose it's only working due to tactic magic - in which case I prefer yours

#### Johan Commelin (Jan 08 2020 at 19:48):

But you are only using basic tactics, so there shouldn't be any magic at all.

#### Johan Commelin (Jan 08 2020 at 19:48):

But I agree that lean seems to be happy with it

#### Johan Commelin (Jan 08 2020 at 19:53):

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := h

doesn't work. So I really don't get why your version does work. Maybe something with the existential, but it's still weird

#### Johan Commelin (Jan 08 2020 at 20:01):

lemma parallel_trans : transitive parallel := begin rintros l₁ l₂ l₃ (rfl|h₁₂) (rfl|h₂₃), { exact parallel_refl _ }, { right, assumption }, { right, assumption }, { by_cases h₁₃ : l₁ = l₃, { subst h₁₃, exact parallel_refl _ }, { right, contrapose! h₁₃, rcases h₁₃ with ⟨p, hp₁, hp₂⟩, apply unique_parallel p l₂, all_goals { try {right}, assumption } } } end

The last line of the proof abuses the weird behaviour that I don't understand

#### Johan Commelin (Jan 08 2020 at 20:21):

that gives me

`contrapose only applies to nondependent arrows between decidable props`

, though I am satisfied with the following (but still good to see alternatives)

lemma parallel_symmetric : symmetric parallel :=

begin

intros l₁ l₂ h,

cases h,

{ rw h,

left,

refl },

{ right,

exact h },

end

@Mario Carneiro Do you understand what's going on?

#### Mario Carneiro (Jan 08 2020 at 20:31):

oh wow, that was a real wtf

#### Mario Carneiro (Jan 08 2020 at 20:31):

the problem is

constants Pt Ln : Sort

#### Mario Carneiro (Jan 08 2020 at 20:31):

`Sort = Prop`

#### Mario Carneiro (Jan 08 2020 at 20:32):

therefore `l₁`

and `l₂`

are two proofs of the proposition `Ln`

and are hence equal by proof irrelevance

#### Bryan Gin-ge Chen (Jan 08 2020 at 20:34):

Wow, indeed `#check Pt`

gives `Pt : Prop`

.

#### Johan Commelin (Jan 08 2020 at 20:42):

Aha, that's sneaky

#### Johan Commelin (Jan 08 2020 at 20:45):

@Matt Earnshaw The solution is to change `Sort`

into `Type`

#### Kevin Buzzard (Jan 08 2020 at 20:57):

Or presumably a change to `Sort u`

would also solve this.

#### Mario Carneiro (Jan 08 2020 at 20:59):

I would suggest `Type u`

instead

#### Johan Commelin (Jan 08 2020 at 21:03):

Or presumably a change to

`Sort u`

would also solve this.

That would still allow `Prop`

if `u = 0`

#### Kevin Buzzard (Jan 08 2020 at 21:05):

Yes, but presumably the invalid proof still stops working...

#### Mario Carneiro (Jan 08 2020 at 21:11):

It will, but if you try to do any constructions they won't be able to live in the same universe `Sort u`

in all likelihood, they will have to live in `Sort (max 1 u)`

or similar and that will be inconvenient. (This is why most type constructors like `list`

work on `Type u`

instead of `Sort u`

.)

#### Matt Earnshaw (Jan 08 2020 at 21:48):

aha

#### Bryan Gin-ge Chen (Jan 09 2020 at 04:10):

Aside from the typo that Johan already pointed out, there's actually another issue with the type of `unique_parallel`

:

constant unique_parallel (p : Pt) (l₁ l₂ : Ln) (h₁₂ : parallel l₁ l₂) (hp₁ : belongs p l₁) (hp₂ : belongs p l₂) : l₁ = l₂

This says that given a point `p`

, two parallel lines `l₁`

and `l₂`

passing through `p`

must be equal to each other. However, Artin phrased axiom 2 this way: "Given a point $P$ and a line $l$, there exists one and only one line $m$ such that $P$ lies on $m$ and such that $m\parallel l$." In particular, note that $P$ does not have to belong to $l$. Here's a minimal fix:

constant unique_parallel (p : Pt) (l l₁ l₂ : Ln) (h₁ : parallel l l₁) (h₂ : parallel l l₂) (hp₁ : belongs p l₁) (hp₂ : belongs p l₂) : l₁ = l₂

Here's Johan's snippet updated with the `Type*`

fix and the fix above, as well as a proof of `parallel_trans`

. I also made a few parameters implicit with curly braces:

import tactic noncomputable theory open_locale classical -- constants of types subsume the usual statement of a theory's signature and axioms constants Pt Ln : Type* constant belongs : Pt → Ln → Prop def parallel (l₁ l₂ : Ln) := l₁ = l₂ ∨ (¬∃ p : Pt, belongs p l₁ ∧ belongs p l₂) -- Artin axiom 1: distinct points determine unique line constant unique_ln_bw_two_pts {p₁ p₂ : Pt} : (p₁ ≠ p₂) → ∃ p₁p₂ : Ln, belongs p₁ p₁p₂ ∧ belongs p₂ p₁p₂ ∧ (∀ l : Ln, belongs p₁ l ∧ belongs p₂ l → p₁p₂ = l) -- Artin axiom 2: exists unique parallel constant exists_parallel (p : Pt) (l : Ln) : (∃ l₁ : Ln, parallel l l₁ ∧ belongs p l₁) constant unique_parallel {p : Pt} {l l₁ l₂ : Ln} (h₁ : parallel l l₁) (h₂ : parallel l l₂) (hp₁ : belongs p l₁) (hp₂ : belongs p l₂) : l₁ = l₂ lemma parallel_refl : reflexive parallel := begin intro l, left, refl end lemma parallel_symm : symmetric parallel := begin rintros l₁ l₂ (rfl|h), { exact parallel_refl _ }, { right, contrapose! h, apply exists_imp_exists _ h, intro p, exact and.symm } end lemma parallel_trans : transitive parallel := begin intros l₁ l₂ l₃ h₁₂ h₂₃, by_cases H : ∃ p, belongs p l₁ ∧ belongs p l₃, { rcases H with ⟨p, h₁, h₃⟩, have : l₁ = l₃ := unique_parallel (parallel_symm h₁₂) h₂₃ h₁ h₃, subst this, exact parallel_refl l₁, }, { right, exact H, }, end theorem parallel_is_equivalence : equivalence parallel := ⟨parallel_refl, parallel_symm, parallel_trans⟩

#### Kenny Lau (Jan 09 2020 at 04:15):

also I think all of these should be structure / class instead of constants

#### Bryan Gin-ge Chen (Jan 09 2020 at 04:17):

How would you set it up?

#### Kenny Lau (Jan 09 2020 at 06:59):

universes u v class has_parallel (Ln : Type v) := (parallel : Ln → Ln → Prop) infix ` ∥ `:50 := has_parallel.parallel class pre_geometry (Pt : Type u) (Ln : Type v) extends has_mem Pt Ln. instance pre_geometry.has_parallel (Pt : Type u) (Ln : Type v) [pre_geometry Pt Ln] : has_parallel Ln := ⟨λ L₁ L₂, L₁ = L₂ ∨ ¬∃ p, p ∈ L₁ ∧ p ∈ L₂⟩ class geometry (Pt : Type u) (Ln : Type v) extends pre_geometry Pt Ln := (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') section variables (Pt : Type u) (Ln : Type v) [pre_geometry Pt Ln] include Pt @[refl] theorem parallel.refl {L : Ln} : L ∥ L := or.inl rfl @[symm] theorem parallel.symm {L₁ L₂ : Ln} (h : L₁ ∥ L₂) : L₂ ∥ L₁ := or.cases_on h (or.inl ∘ eq.symm) $ λ h, or.inr $ λ ⟨p, hp1, hp2⟩, h ⟨p, hp2, hp1⟩ end

#### Johan Commelin (Jan 09 2020 at 07:05):

Nice (-;

#### Johan Commelin (Jan 09 2020 at 07:14):

Kenny, I'm not sure if one can prove transitivity now

#### Johan Commelin (Jan 09 2020 at 07:14):

It seems one needs the crazy version of unique parallel for that

#### Kenny Lau (Jan 09 2020 at 07:16):

I haven't been following this discussion

#### Kenny Lau (Jan 09 2020 at 07:16):

what are the axioms now?

#### Johan Commelin (Jan 09 2020 at 07:20):

@Kenny Lau

constant unique_parallel (p : Pt) (l l₁ l₂ : Ln) : (parallel l l₁ ∧ parallel l l₂ ∧ belongs p l₁ ∧ belongs p l₁) → l₁ = l₂

#### Johan Commelin (Jan 09 2020 at 07:20):

I thought you could kick out the line `l`

. But only once you know transivity...

#### Kenny Lau (Jan 09 2020 at 07:22):

isn't that covered by my `exists_unique_parallel`

?

#### Johan Commelin (Jan 09 2020 at 07:22):

I didn't try too hard, but I couldn't write down a proof immediately

#### Kenny Lau (Jan 09 2020 at 07:24):

isn't that what it says?

#### Johan Commelin (Jan 09 2020 at 07:26):

I don't see how

#### Johan Commelin (Jan 09 2020 at 07:27):

Sorry, I'm confused. I think I understand now

#### Johan Commelin (Jan 09 2020 at 07:35):

/me should learn what `exists_unique`

means

#### Johan Commelin (Jan 09 2020 at 07:35):

section variables (Pt : Type u) (Ln : Type v) [geometry Pt Ln] include Pt @[trans] lemma parallel.trans {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := begin by_cases h₁₃ : L₁ = L₃, { left, assumption }, rcases h₁₂ with rfl|h₁₂, { assumption }, rcases h₂₃ with rfl|h₂₃, { right, assumption }, right, rintro ⟨p, H₁, H₂⟩, apply h₁₃, apply unique_of_exists_unique (geometry.exists_unique_parallel p L₂) ⟨H₁, _⟩ ⟨H₂, _⟩, { symmetry, right, assumption }, { right, assumption }, end end

#### Kenny Lau (Jan 09 2020 at 07:43):

yay

#### Bryan Gin-ge Chen (Jan 09 2020 at 07:44):

Alternatively:

section variables (Pt : Type u) (Ln : Type v) [geometry Pt Ln] include Pt @[refl] theorem parallel.refl {L : Ln} : L ∥ L := or.inl rfl @[symm] theorem parallel.symm {L₁ L₂ : Ln} (h : L₁ ∥ L₂) : L₂ ∥ L₁ := or.cases_on h (or.inl ∘ eq.symm) $ λ h, or.inr $ λ ⟨p, hp1, hp2⟩, h ⟨p, hp2, hp1⟩ open_locale classical @[trans] theorem parallel.trans {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := begin by_cases H : ∃ p, p ∈ L₁ ∧ p ∈ L₃, { rcases H with ⟨p, h₁, h₃⟩, have : L₁ = L₃ := by { rcases geometry.exists_unique_parallel p L₂ with ⟨L, ⟨hp, hL⟩, hᵤ⟩, have hL₁₂ : L₁ = L := hᵤ L₁ ⟨h₁, parallel.symm Pt Ln h₁₂⟩, have hL₁₃ : L₃ = L := hᵤ L₃ ⟨h₃, h₂₃⟩, rw [hL₁₂, hL₁₃], }, subst this, }, { right, exact H, }, end

#### Johan Commelin (Jan 09 2020 at 07:51):

@[trans] lemma parallel.trans {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := begin apply classical.or_iff_not_imp_right.mpr, rw not_not, rintro ⟨p, H₁, H₂⟩, apply unique_of_exists_unique (geometry.exists_unique_parallel p L₂) ⟨H₁, _⟩ ⟨H₂, _⟩, { symmetry, assumption }, { assumption }, end

#### Johan Commelin (Jan 09 2020 at 08:17):

@[trans] lemma parallel.trans {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := begin suffices : (∃ (p : Pt), p ∈ L₁ ∧ p ∈ L₃) → L₁ = L₃, { apply classical.or_iff_not_imp_right.mpr, rwa not_not, }, rintro ⟨p, H₁, H₂⟩, apply unique_of_exists_unique (geometry.exists_unique_parallel p L₂); finish, end

I wish there was a hammer that would kill the second line.

#### Johan Commelin (Jan 09 2020 at 08:21):

The following script really captures the essentials of the proof, I think:

@[trans] lemma jmc_wishes {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := begin suffices : (∃ (p : Pt), p ∈ L₁ ∧ p ∈ L₃) → L₁ = L₃, { sorry }, rintro ⟨p, H₁, H₂⟩, have : ∃! (L' : Ln), p ∈ L' ∧ L₂ ∥ L' := geometry.exists_unique_parallel p L₂, sorry, end

The `sorry`

s should be filled in with a 1-word hammer tactic.

#### Bryan Gin-ge Chen (Jan 09 2020 at 08:28):

In honor of Kenny's term proofs of `refl`

and `symm`

, I present this monstrosity:

@[trans] theorem parallel.trans_t {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := (classical.em (∃ p, p ∈ L₁ ∧ p ∈ L₃)).elim (λ ⟨p, h₁, h₃⟩, or.inl $ unique_of_exists_unique (geometry.exists_unique_parallel p L₂) ⟨h₁, parallel.symm Pt Ln h₁₂⟩ ⟨h₃, h₂₃⟩) or.inr

#### Johan Commelin (Jan 09 2020 at 08:32):

I changed the definition of parallel:

import tactic noncomputable theory open_locale classical universes u v class has_parallel (Ln : Type v) := (parallel : Ln → Ln → Prop) infix ` ∥ `:50 := has_parallel.parallel class pre_geometry (Pt : Type u) (Ln : Type v) extends has_mem Pt Ln. instance pre_geometry.has_parallel (Pt : Type u) (Ln : Type v) [pre_geometry Pt Ln] : has_parallel Ln := ⟨λ L₁ L₂, (∃ (p : Pt), p ∈ L₁ ∧ p ∈ L₂) → L₁ = L₂⟩ class geometry (Pt : Type u) (Ln : Type v) extends pre_geometry Pt Ln := (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') section variables (Pt : Type u) (Ln : Type v) [pre_geometry Pt Ln] include Pt @[refl] theorem parallel.refl {L : Ln} : L ∥ L := λ _, rfl @[symm] theorem parallel.symm {L₁ L₂ : Ln} (h : L₁ ∥ L₂) : L₂ ∥ L₁ := λ ⟨p, hp⟩, (h ⟨p, hp.symm⟩).symm end section variables (Pt : Type u) (Ln : Type v) [geometry Pt Ln] include Pt @[trans] lemma parallel.trans {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := begin rintro ⟨p, H₁, H₂⟩, apply unique_of_exists_unique (geometry.exists_unique_parallel p L₂), all_goals { split; assumption <|> symmetry; assumption } end end

#### Bryan Gin-ge Chen (Jan 09 2020 at 08:34):

That lets you remove the `noncomputable theory`

and `open_locale classical`

.

#### Johan Commelin (Jan 09 2020 at 08:35):

Ooh, maybe I should revert my change...

#### Johan Commelin (Jan 09 2020 at 08:43):

Using namespaces:

import tactic universes u v class has_parallel (Ln : Type v) := (parallel : Ln → Ln → Prop) infix ` ∥ `:50 := has_parallel.parallel class pre_geometry (Pt : Type u) (Ln : Type v) extends has_mem Pt Ln. instance pre_geometry.has_parallel (Pt : Type u) (Ln : Type v) [pre_geometry Pt Ln] : has_parallel Ln := ⟨λ L₁ L₂, (∃ (p : Pt), p ∈ L₁ ∧ p ∈ L₂) → L₁ = L₂⟩ class geometry (Pt : Type u) (Ln : Type v) extends pre_geometry Pt Ln := (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') namespace has_parallel variables {Pt : Type u} {Ln : Type v} [pre_geometry Pt Ln] include Pt @[refl] theorem parallel.refl {L : Ln} : L ∥ L := assume _, rfl @[symm] theorem parallel.symm {L₁ L₂ : Ln} (h : L₁ ∥ L₂) : L₂ ∥ L₁ := assume ⟨p, hp⟩, (h ⟨p, hp.symm⟩).symm end has_parallel namespace has_parallel variables {Pt : Type u} {Ln : Type v} [geometry Pt Ln] include Pt @[trans] lemma parallel.trans {L₁ L₂ L₃ : Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := assume ⟨p, H₁, H₂⟩, unique_of_exists_unique (geometry.exists_unique_parallel p L₂) ⟨H₁, h₁₂.symm⟩ ⟨H₂, h₂₃⟩ end has_parallel

#### Mario Carneiro (Jan 09 2020 at 08:45):

mario the linter says `pre_geometry.has_parallel`

is bad

#### Johan Commelin (Jan 09 2020 at 08:45):

Did I goof up?

#### Mario Carneiro (Jan 09 2020 at 08:46):

it's a bit tricky; you can't infer that instance because `Pt`

is dangling

#### Mario Carneiro (Jan 09 2020 at 08:47):

I think you should bundle a geometry and extract `Pt`

and `Ln`

components

#### Johan Commelin (Jan 09 2020 at 08:47):

Makes sense

#### Johan Commelin (Jan 09 2020 at 09:00):

@Mario Carneiro Something like?

structure pre_geometry : Type 1 := (Pt : Type) (Ln : Type) [has_mem : has_mem Pt Ln]

#### Kenny Lau (Jan 09 2020 at 09:02):

it's a bit tricky; you can't infer that instance because

`Pt`

is dangling

I was thinking of using `out_param`

#### Johan Commelin (Jan 09 2020 at 09:11):

I guess that for potential "applications" that might be better.

#### Johan Commelin (Jan 09 2020 at 09:12):

I currently have:

import tactic universes u v class has_parallel (Ln : Type v) := (parallel : Ln → Ln → Prop) infix ` ∥ `:50 := has_parallel.parallel structure pre_geometry : Type 1 := (Pt : Type) (Ln : Type) [has_mem : has_mem Pt Ln] attribute [instance] pre_geometry.has_mem instance pre_geometry.has_parallel {Ω : pre_geometry} : has_parallel Ω.Ln := ⟨λ L₁ L₂, (∃ (p : Ω.Pt), p ∈ L₁ ∧ p ∈ L₂) → L₁ = L₂⟩ class geometry extends pre_geometry := (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') namespace has_parallel variables {Ω : pre_geometry} @[refl] theorem parallel.refl {L : Ω.Ln} : L ∥ L := assume _, rfl @[symm] theorem parallel.symm {L₁ L₂ : Ω.Ln} (h : L₁ ∥ L₂) : L₂ ∥ L₁ := assume ⟨p, hp⟩, (h ⟨p, hp.symm⟩).symm end has_parallel namespace has_parallel variables {Ω : geometry} @[trans] lemma parallel.trans {L₁ L₂ L₃ : Ω.Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := assume ⟨p, H₁, H₂⟩, unique_of_exists_unique (geometry.exists_unique_parallel p L₂) ⟨H₁, h₁₂.symm⟩ ⟨H₂, h₂₃⟩ end has_parallel

I don't really like the `Ω.Ln`

etc...

#### Mario Carneiro (Jan 09 2020 at 09:18):

would `Ln Ω`

make you feel better?

#### Johan Commelin (Jan 09 2020 at 09:19):

Not that much ...

#### Johan Commelin (Jan 09 2020 at 09:20):

Maybe `Ω`

should be a parameter?

#### Kenny Lau (Jan 09 2020 at 09:25):

maybe we should build an example

#### Matt Earnshaw (Jan 09 2020 at 14:24):

it's helpful to see experienced folk grappling with this. need to learn typeclasses and structures properly to totally get it but this is neat. -- @Johan Commelin in your most recent version above is it possible to write down equivalence as a term of type `equivalence ...`

? (I tried like `equivalence parallel`

in the has_parallel namespace but it seems not quite right)

#### Johan Commelin (Jan 09 2020 at 14:54):

@Matt Earnshaw Voila:

namespace has_parallel open parallel variables {Ω : geometry} lemma parallel.equivalence : equivalence (infer_instance : has_parallel Ω.Ln).parallel := ⟨λ _, refl, λ _ _ h, h.symm, λ _ _ _ h₁ h₂, h₁.trans h₂⟩ end has_parallel

#### Johan Commelin (Jan 09 2020 at 14:55):

Because I `open parallel`

, I can just write `refl`

instead of `parallel.refl`

in the proof.

#### Matt Earnshaw (Jan 09 2020 at 16:05):

thanks. that starts to look a bit inelegant but i won't worry about it at this stage. trying to push on with Theorem 2.2 concerning pencils of parallel lines. as a test I tried the following:

def pencil (l : Ω.Ln) := {m : Ω.Ln | l ∥ m} lemma pencil_of_line_contains_line (l : Ω.Ln) : l ∈ pencil l := parallel.refl

which works, but I don't really understand how lean figures out that `parallel.refl`

is a term of `l ∈ pencil l`

?

#### Bryan Gin-ge Chen (Jan 09 2020 at 16:12):

`set Ln`

is the type of predicates on `Ln`

, i.e. functions from `Ln`

to `Prop`

. In particular `x ∈ { y | P }`

means the same thing as `P x`

. Thus `l ∈ pencil l`

translates to `l ∥ l`

.

(edit: I thought there was some discussion of this in TPiL or Logic & Proof but I didn't see any. However, the start of init.logic is fairly readable.)

#### Johan Commelin (Jan 09 2020 at 16:16):

@Matt Earnshaw I should note that `equivalence`

isn't used that much in mathlib. On the other hand, the three lemmas tagged with `@[refl]`

, `@[symm]`

and `@[trans]`

are very useful.

#### Johan Commelin (Jan 09 2020 at 16:17):

For quotients by equivalence relations, we use `setoid`

, but you don't want that here

#### Matt Earnshaw (Jan 09 2020 at 18:52):

didn't complete Thm 2.2 yet but for the next part it looks like it would be useful to have notation for the unique line between points. so far:

def plus (p q : Ω.Pt) {neq : p ≠ q} : Ω.Ln := begin have h₁ := Ω.exists_unique_ln_bw_two_pts, have h₂ := h₁ neq, sorry end

this gives me unique existence as an hypothesis but stuck on how to eliminate

#### Johan Commelin (Jan 09 2020 at 19:09):

Use `exists_of_exists_unique`

#### Johan Commelin (Jan 09 2020 at 19:09):

After that use `choose`

#### Johan Commelin (Jan 09 2020 at 19:10):

For several reasons, it is usually better to use term-mode for definitions, and use tactic mode only for proofs

#### Johan Commelin (Jan 09 2020 at 19:11):

So once you have finished this definition, you can try to use `classical.some _`

for the definition.

#### Johan Commelin (Jan 09 2020 at 19:12):

(Btw, do you already know that a point exists? Do you know that more than 1 point exists?)

#### Johan Commelin (Jan 09 2020 at 19:12):

Usually such axioms are added, right?

#### Bryan Gin-ge Chen (Jan 09 2020 at 19:20):

"Axiom 3: There exist three distinct points A, B, C such that C does not lie on the line A + B. We also say that there exist three non-collinear points."

(Not sure how legal this link is, but see https://archive.org/details/geometricalgebra033556mbp/page/n63)

#### Matt Earnshaw (Jan 09 2020 at 19:23):

right, I wrote this as `(exists_three_noncollinear : ∀ (L : Ln), ∃ (a b c : Pt), ¬(a ∈ L ∧ b ∈ L ∧ c ∈ L)`

, but having the plus notation might give a form that is easier to reason with.

#### Matt Earnshaw (Jan 09 2020 at 19:24):

in fact what is wrote is wrong because need to specify distinctness

#### Johan Commelin (Jan 09 2020 at 19:29):

I think the plus notation can work, if you have a statement of the form

lemma exists_ln_of_pt_of_pt (x y : Pt) : \exists L : Ln, x \in L \and y \in L := sorry

#### Johan Commelin (Jan 09 2020 at 19:31):

Then you can define

def add (x y : Pt) : Ln := classical.some (exists_ln_of_pt_of_pt x y) instance : has_add \Omega.Pt := \<add\> lemma left_mem_add (x y : Pt) : x \in (x + y) := (classical.some_spec (exists_ln_of_pt_of_pt x y)).1 lemma right_mem_add (x y : Pt) : y \in (x + y) := (classical.some_spec (exists_ln_of_pt_of_pt x y)).2

#### Kevin Buzzard (Jan 09 2020 at 19:32):

Here's how @Ali Sever did it last year: https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Geometry/axioms.lean

#### Bryan Gin-ge Chen (Jan 09 2020 at 22:39):

Sadly you'll have to use another symbol since `has_add.add`

has expected type `a -> a -> a`

(and this is built into core), but you want `Pt -> Pt -> Ln`

.

#### Kenny Lau (Jan 10 2020 at 05:32):

import tactic.ext tactic.ring universes u v class has_parallel (Ln : Type v) := (parallel : Ln → Ln → Prop) infix ` ∥ `:50 := has_parallel.parallel structure pre_geometry : Type (max u v+1) := (Pt : Type u) (Ln : Type v) [has_mem : has_mem Pt Ln] attribute [instance] pre_geometry.has_mem instance pre_geometry.has_parallel {Ω : pre_geometry} : has_parallel Ω.Ln := ⟨λ L₁ L₂, (∃ (p : Ω.Pt), p ∈ L₁ ∧ p ∈ L₂) → L₁ = L₂⟩ class geometry extends pre_geometry := (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') namespace has_parallel variables {Ω : pre_geometry} @[refl] theorem parallel.refl {L : Ω.Ln} : L ∥ L := assume _, rfl @[symm] theorem parallel.symm {L₁ L₂ : Ω.Ln} (h : L₁ ∥ L₂) : L₂ ∥ L₁ := assume ⟨p, hp⟩, (h ⟨p, hp.symm⟩).symm end has_parallel namespace has_parallel variables {Ω : geometry} @[trans] lemma parallel.trans {L₁ L₂ L₃ : Ω.Ln} (h₁₂ : L₁ ∥ L₂) (h₂₃ : L₂ ∥ L₃) : L₁ ∥ L₃ := assume ⟨p, H₁, H₂⟩, unique_of_exists_unique (geometry.exists_unique_parallel p L₂) ⟨H₁, h₁₂.symm⟩ ⟨H₂, h₂₃⟩ end has_parallel def affine_plane.pre (k : Type u) [has_add k] [has_mul k] : pre_geometry := { Pt := k × k, Ln := (k × k) ⊕ k, -- it is kP^2 - [0:0:1] -- x+by=c or y=c has_mem := ⟨λ p L, sum.rec_on L (λ bc, p.1 + bc.1 * p.2 = bc.2) (λ c, p.2 = c)⟩ } theorem affine_plane.exists_unique_ln_bw_two_pts (k : Type u) [field k] {p₁ p₂ : (affine_plane.pre k).Pt} (hp : p₁ ≠ p₂) : ∃! L : (affine_plane.pre k).Ln, p₁ ∈ L ∧ p₂ ∈ L := begin refine or.cases_on (classical.em (p₁.2 = p₂.2)) (λ h, _) (λ h, _), { refine ⟨sum.inr p₁.2, ⟨rfl, h.symm⟩, λ L hL, _⟩, cases hL with hpL1 hpL2, cases L with bc c, { change _ = _ at hpL1, change _ = _ at hpL2, change _ = _ at h, rw h at hpL1, exact absurd (prod.ext (add_right_cancel (hpL1.trans hpL2.symm)) h) hp }, { exact congr_arg _ hpL1.symm } }, { have : p₁.2 - p₂.2 ≠ 0 := mt eq_of_sub_eq_zero h, refine ⟨sum.inl ((p₂.1 - p₁.1) / (p₁.2 - p₂.2), (p₂.1 * p₁.2 - p₁.1 * p₂.2) / (p₁.2 - p₂.2)), ⟨_, _⟩, λ L hL, _⟩, { change p₁.1 + (p₂.1 - p₁.1) / (p₁.2 - p₂.2) * p₁.2 = (p₂.1 * p₁.2 - p₁.1 * p₂.2) / (p₁.2 - p₂.2), rw [div_mul_eq_mul_div, add_div_eq_mul_add_div _ _ this], congr' 1, ring }, { change p₂.1 + (p₂.1 - p₁.1) / (p₁.2 - p₂.2) * p₂.2 = (p₂.1 * p₁.2 - p₁.1 * p₂.2) / (p₁.2 - p₂.2), rw [div_mul_eq_mul_div, add_div_eq_mul_add_div _ _ this], congr' 1, ring }, { cases hL with hpL1 hpL2, cases L with bc c, { cases bc with b c, change p₁.1 + b * p₁.2 = c at hpL1, change p₂.1 + b * p₂.2 = c at hpL2, have hb := hpL1.trans hpL2.symm, rw [← eq_sub_iff_add_eq', add_comm, add_sub_assoc, ← sub_eq_iff_eq_add', ← mul_sub, ← eq_div_iff_mul_eq _ _ this] at hb, rw [hb, div_mul_eq_mul_div, add_div_eq_mul_add_div _ _ this] at hpL1, rw [hb, ← hpL1], congr' 3, ring }, { exact absurd (hpL1.trans hpL2.symm) h } } } end /- p₁.1 + b p₁.2 = c p₂.1 + b p₂.2 = c c = p₁.1 + b p₁.2 p₁.1 + b p₁.2 = p₂.1 + b p₂.2 b = (p₂.1 - p₁.1) / (p₁.2 - p₂.2) c = (p₁.1 * (p₁.2 - p₂.2) + (p₂.1 - p₁.1) * p₁.2) / (p₁.2 - p₂.2) c = (p₁.1 * p₁.2 - p₁.1 * p₂.2 + p₂.1 * p₁.2 - p₁.1 * p₁.2) / (p₁.2 - p₂.2) c = (p₂.1 * p₁.2 - p₁.1 * p₂.2) / (p₁.2 - p₂.2) -/ theorem affine_plane.pre.parallel (k : Type u) [field k] (L₁ L₂ : (affine_plane.pre k).Ln) : L₁ ∥ L₂ ↔ (∃ b c c' : k, L₁ = sum.inl (b, c) ∧ L₂ = sum.inl (b, c')) ∨ (∃ c c' : k, L₁ = sum.inr c ∧ L₂ = sum.inr c') := begin split, { intro h, classical, by_cases hL : ∃ p, p ∈ L₁ ∧ p ∈ L₂, { specialize h hL, subst h, cases L₁ with bc c, { cases bc with b c, left, exact ⟨_, _, _, rfl, rfl⟩ }, { right, exact ⟨_, _, rfl, rfl⟩ } }, { cases L₁ with bc c; cases L₂ with bc' c', { cases bc with b c, cases bc' with b' c', have hb : b = b', { by_contra hb, have : b - b' ≠ 0 := sub_ne_zero_of_ne hb, apply hL, refine ⟨((b * c' - b' * c)/(b - b'), (c - c') / (b - b')), _, _⟩, { change (b * c' - b' * c) / (b - b') + b * ((c - c') / (b - b')) = c, rw [← mul_div_assoc, ← add_div, div_eq_iff_mul_eq this], ring }, { change (b * c' - b' * c) / (b - b') + b' * ((c - c') / (b - b')) = c', rw [← mul_div_assoc, ← add_div, div_eq_iff_mul_eq this], ring } }, subst hb, exact or.inl ⟨_, _, _, rfl, rfl⟩ }, { cases bc with b c, refine hL.elim ⟨(c - b * c', c'), _, _⟩, { change c - b * c' + b * c' = c, rw sub_add_cancel }, { change c' = c', refl } }, { cases bc' with b' c', refine hL.elim ⟨(c' - b' * c, c), _, _⟩, { change c = c, refl }, { change c' - b' * c + b' * c = c', rw sub_add_cancel } }, { exact or.inr ⟨_, _, rfl, rfl⟩ } } }, { rintros (⟨b, c, c', rfl, rfl⟩ | ⟨c, c', rfl, rfl⟩) ⟨p, hp1, hp2⟩, { have : c = c' := hp1.symm.trans hp2, rw this }, { have : c = c' := hp1.symm.trans hp2, rw this } } end /- x + by = c x + b'y = c' y = (c - c') / (b - b') x = c - by = (cb - cb' - bc + bc') / (b - b') = (bc' - b'c) / (b - b') x + by = c y = c' -/ -- this is "computable" theorem affine_plane.exists_unique_parallel (k : Type u) [field k] (p : (affine_plane.pre k).Pt) (L : (affine_plane.pre k).Ln) : ∃! L' : (affine_plane.pre k).Ln, p ∈ L' ∧ L ∥ L' := begin cases L with bc c, { cases bc with b c, refine ⟨sum.inl (b, p.1 + b * p.2), ⟨rfl, _⟩, λ L hL, _⟩, { rw affine_plane.pre.parallel, exact or.inl ⟨_, _, _, rfl, rfl⟩ }, { cases hL with hpL hL, rw affine_plane.pre.parallel at hL, rcases hL with ⟨b', c', c'', ⟨⟩, rfl⟩ | ⟨_, _, ⟨⟩, _⟩, change p.1 + b * p.2 = c'' at hpL, rw ← hpL } }, { refine ⟨sum.inr p.2, ⟨rfl, _⟩, λ L hL, _⟩, { rw affine_plane.pre.parallel, exact or.inr ⟨_, _, rfl, rfl⟩ }, { cases hL with hpL hL, rw affine_plane.pre.parallel at hL, rcases hL with ⟨_, _, _, ⟨⟩, _⟩ | ⟨c, c', ⟨⟩, ⟨⟩⟩, change p.2 = c' at hpL, rw hpL } } end def affine_plane (k : Type u) [field k] : geometry := { exists_unique_ln_bw_two_pts := @affine_plane.exists_unique_ln_bw_two_pts k _, exists_unique_parallel := affine_plane.exists_unique_parallel k, .. (affine_plane.pre k) }

#### Kenny Lau (Jan 10 2020 at 05:32):

yay the affine plane is a geometry

#### Johan Commelin (Jan 15 2020 at 08:36):

@Marc Masdeu We had a discussion about axiomatic geometry in this thread about a week ago :wink:

#### Johan Commelin (Jan 15 2020 at 08:37):

Might contain some relevant bits. (Now I will start reading your post :oops:.) Oooh, and welcome by the way :smiley:

#### Marc Masdeu (Jan 15 2020 at 08:40):

Might contain some relevant bits. (Now I will start reading your post :oops:.) Oooh, and welcome by the way :smiley:

@Johan Commelin thank you! I had seen the thread, but couldn't find any `\exists !`

statement. This will be useful for when I try to make things nice and Lean-ish.

#### Kevin Buzzard (Jan 15 2020 at 12:44):

My student @Ali Sever ploughed through loads of this stuff in Lean! A link is somewhere in one of the threads ;-)

#### Ali Sever (Jan 15 2020 at 14:31):

I'll try to make summary of what I did and how my code works.

#### Marc Masdeu (Jan 15 2020 at 14:54):

I'll try to make summary of what I did and how my code works.

That would be great! Thanks

#### Matt Earnshaw (Jan 21 2020 at 14:38):

coming back to this, i need to get back to proofs but for now am playing with the code that was produced above and trying other ways of setting it up, to get a feel for basics.

Kenny had instead had a `structure`

that was a bit like a "structure" in model-theoretic terms and then defined a class extending that it that turned the "structure" into a "theory". would it be misleading to think along these model-theoretic lines as a rule of thumb for using `structure`

and `class`

?

My first thought was that defining a `class`

`has_parallel`

seems like overkill because I'm only expecting one type to use it, so I just added `parallel`

to my `structure`

. But then to define it, it seems like I have to introduce a constant, which seems ugly?

structure abstract_affine : Type 1 := (Pt : Type) (Ln : Type) (parallel : Ln → Ln → Prop) (infix ` ∥ `:50 := parallel) [has_mem : has_mem Pt Ln] (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') (exists_three_noncollinear : ∀ (L : Ln), ∃ (a b c : Pt) (a ≠ b) (b ≠ c), ¬(a ∈ L ∧ b ∈ L ∧ c ∈ L)) constant Ω : abstract_affine attribute [instance] abstract_affine.has_mem -- Artin def 2.1 def Ω.parallel (l₁ l₂ : Ω.Ln) := l₁ = l₂ ∨ (¬∃ p : Ω.Pt, p ∈ l₁ ∧ p ∈ l₂) infix ` ∥ `:50 := Ω.parallel @[refl] theorem parallel.refl {L : Ω.Ln} : L ∥ L := begin left, refl, end

#### Matt Earnshaw (Jan 21 2020 at 14:40):

also, it's a way off but my goal originally was to prove an equivalence of categories of models of abstract affine planes and of skew fields (/ planes-with-pappus and fields). But perhaps it is more apt to prove "equality of types"? Is that a done thing?

#### Chris Hughes (Jan 21 2020 at 14:51):

The only difference between class and structure is to do with how the arguments are inferred. If you define a class, then when you pass an argument of that type to a function, you will expect Lean to infer that argument using Type class inference. So for example, we don't want to have to provide explicitly the ring structure on the reals every time we use it, so `ring`

is a class. The downside of this is that I can't easily talk about multiple elements of the type `ring R`

, which is fine, because there's usually only one ring structure on a given type that I want to consider.

The model theoretic analogy is a very loose one, you can have Propositions as part of both structures and classes.

#### Chris Hughes (Jan 21 2020 at 14:52):

My suggested setup is the following

class abstract_affine (Pt : Type*) (Ln : Type*) := (parallel : Ln → Ln → Prop) (infix ` ∥ `:50 := parallel) [has_mem : has_mem Pt Ln] (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') (exists_three_noncollinear : ∀ (L : Ln), ∃ (a b c : Pt) (a ≠ b) (b ≠ c), ¬(a ∈ L ∧ b ∈ L ∧ c ∈ L)) variables {Pt Ln : Type} [abstract_affine Pt Ln]

#### Chris Hughes (Jan 21 2020 at 14:55):

You should always use `variable`

instead of constant. With the variable keyword you will be proving things in the generality of all `abstract_affine`

spaces. `constant`

adds an axiom that there is an `abstract_affine`

space, but then all the theorems you prove will only apply to the constant you added, and not to an arbitrary affine space.

#### Matt Earnshaw (Jan 21 2020 at 14:57):

You should always use

`variable`

instead of constant. With the variable keyword you will be proving things in the generality of all`abstract_affine`

spaces.`constant`

adds an axiom that there is an`abstract_affine`

space, but then all the theorems you prove will only apply to the constant you added, and not to an arbitrary affine space.

ah yes, should know this by now, good reminder

#### Matt Earnshaw (Jan 21 2020 at 15:12):

My suggested setup is the following

class abstract_affine (Pt : Type*) (Ln : Type*) := (parallel : Ln → Ln → Prop) (infix ` ∥ `:50 := parallel) [has_mem : has_mem Pt Ln] (exists_unique_ln_bw_two_pts : ∀ {p₁ p₂ : Pt}, p₁ ≠ p₂ → ∃! L : Ln, p₁ ∈ L ∧ p₂ ∈ L) (exists_unique_parallel : ∀ (p : Pt) (L : Ln), ∃! L' : Ln, p ∈ L' ∧ L ∥ L') (exists_three_noncollinear : ∀ (L : Ln), ∃ (a b c : Pt) (a ≠ b) (b ≠ c), ¬(a ∈ L ∧ b ∈ L ∧ c ∈ L)) variables {Pt Ln : Type} [abstract_affine Pt Ln]

in this setup I cannot figure out how one then defines parallelism

#### Matt Earnshaw (Jan 21 2020 at 15:13):

the rest of what you said is also helpful, thanks. I see why it makes more sense to use a class here

Last updated: May 13 2021 at 23:16 UTC