attempt at some geometry

Stream: new members

[Matt Earnshaw]

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]

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]

@Matt Earnshaw In general people tend to avoid constant completely, except for little demo purposes.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

A different option would be to turn all your constants into variables, and maybe make some of them implicit (using {})

[Johan Commelin]

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]

@Matt Earnshaw You have a typo in the unique_parallel axiom. You ask that l1 is parallel to l twice.

[Johan Commelin]

Also, can't you just ask that l1 is parallel to l2, and leave l completely out of the picture?

[Johan Commelin]

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]

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]

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]

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

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

[Matt Earnshaw]

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

[Johan Commelin]

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

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

[Matt Earnshaw]

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]

Look at the other lines I added to the top

[Johan Commelin]

noncomputable theory and open_locale classical

[Johan Commelin]

How can right, exact h close that goal? You need to apply symmetry somewhere.

[Matt Earnshaw]

ah I see

[Matt Earnshaw]

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

[Johan Commelin]

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

[Johan Commelin]

But I agree that lean seems to be happy with it

[Johan Commelin]

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]

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]

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]

oh wow, that was a real wtf

[Mario Carneiro]

the problem is

constants Pt Ln : Sort

[Mario Carneiro]

Sort = Prop

[Mario Carneiro]

therefore l₁ and l₂ are two proofs of the proposition Ln and are hence equal by proof irrelevance

[Bryan Gin-ge Chen]

Wow, indeed #check Pt gives Pt : Prop.

[Johan Commelin]

Aha, that's sneaky

[Johan Commelin]

@Matt Earnshaw The solution is to change Sort into Type

[Kevin Buzzard]

Or presumably a change to Sort u would also solve this.

[Mario Carneiro]

I would suggest Type u instead

[Johan Commelin]

Or presumably a change to Sort u would also solve this.

That would still allow Prop if u = 0

[Kevin Buzzard]

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

[Mario Carneiro]

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]

aha

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

How would you set it up?

[Kenny Lau]

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]

Nice (-;

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

I haven't been following this discussion

[Kenny Lau]

what are the axioms now?

[Johan Commelin]

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

I thought you could kick out the line l. But only once you know transivity...

[Kenny Lau]

isn't that covered by my exists_unique_parallel?

[Johan Commelin]

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

[Kenny Lau]

isn't that what it says?

[Johan Commelin]

I don't see how

[Johan Commelin]

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

[Johan Commelin]

/me should learn what exists_unique means

[Johan Commelin]

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]

yay

[Bryan Gin-ge Chen]

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]

@[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]

@[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]

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]

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]

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]

That lets you remove the noncomputable theory and open_locale classical.

[Johan Commelin]

Ooh, maybe I should revert my change...

[Johan Commelin]

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]

mario the linter says pre_geometry.has_parallel is bad

[Johan Commelin]

Did I goof up?

[Mario Carneiro]

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

[Mario Carneiro]

I think you should bundle a geometry and extract Pt and Ln components

[Johan Commelin]

Makes sense

[Johan Commelin]

@Mario Carneiro Something like?

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

[Kenny Lau]

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

I was thinking of using out_param

[Johan Commelin]

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

[Johan Commelin]

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]

would Ln Ω make you feel better?

[Johan Commelin]

Not that much ...

[Johan Commelin]

Maybe Ω should be a parameter?

[Kenny Lau]

maybe we should build an example

[Matt Earnshaw]

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]

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

Because I open parallel, I can just write refl instead of parallel.refl in the proof.

[Matt Earnshaw]

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]

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]

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

For quotients by equivalence relations, we use setoid, but you don't want that here

[Matt Earnshaw]

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]

Use exists_of_exists_unique

[Johan Commelin]

After that use choose

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Usually such axioms are added, right?

[Bryan Gin-ge Chen]

"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]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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]

yay the affine plane is a geometry

[Johan Commelin]

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

[Johan Commelin]

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

[Marc Masdeu]

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]

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

[Ali Sever]

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

[Marc Masdeu]

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

That would be great! Thanks

[Matt Earnshaw]

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]

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]

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]

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]

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]

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]

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]

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