## 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 constants

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

A different option would be to turn all your constants into variables, 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.

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

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


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?

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


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

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

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)

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: Dec 20 2023 at 11:08 UTC