Zulip Chat Archive

Stream: new members

Topic: attempt at some geometry


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 08 2020 at 16:11):

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

view this post on Zulip Kevin Buzzard (Jan 08 2020 at 16:11):

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

view this post on Zulip 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

view this post on Zulip 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 {})

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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₂)

view this post on Zulip Matt Earnshaw (Jan 08 2020 at 19:19):

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

view this post on Zulip Matt Earnshaw (Jan 08 2020 at 19:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 08 2020 at 19:40):

Look at the other lines I added to the top

view this post on Zulip Johan Commelin (Jan 08 2020 at 19:41):

noncomputable theory and open_locale classical

view this post on Zulip Johan Commelin (Jan 08 2020 at 19:42):

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

view this post on Zulip Matt Earnshaw (Jan 08 2020 at 19:43):

ah I see

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 08 2020 at 19:48):

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

view this post on Zulip Johan Commelin (Jan 08 2020 at 19:48):

But I agree that lean seems to be happy with it

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 08 2020 at 20:31):

oh wow, that was a real wtf

view this post on Zulip Mario Carneiro (Jan 08 2020 at 20:31):

the problem is

constants Pt Ln : Sort

view this post on Zulip Mario Carneiro (Jan 08 2020 at 20:31):

Sort = Prop

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2020 at 20:34):

Wow, indeed #check Pt gives Pt : Prop.

view this post on Zulip Johan Commelin (Jan 08 2020 at 20:42):

Aha, that's sneaky

view this post on Zulip Johan Commelin (Jan 08 2020 at 20:45):

@Matt Earnshaw The solution is to change Sort into Type

view this post on Zulip Kevin Buzzard (Jan 08 2020 at 20:57):

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

view this post on Zulip Mario Carneiro (Jan 08 2020 at 20:59):

I would suggest Type u instead

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 08 2020 at 21:05):

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

view this post on Zulip 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.)

view this post on Zulip Matt Earnshaw (Jan 08 2020 at 21:48):

aha

view this post on Zulip 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 PP and a line ll, there exists one and only one line mm such that PP lies on mm and such that mlm\parallel l." In particular, note that PP does not have to belong to ll. 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

view this post on Zulip Kenny Lau (Jan 09 2020 at 04:15):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2020 at 04:17):

How would you set it up?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:05):

Nice (-;

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:14):

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

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:14):

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

view this post on Zulip Kenny Lau (Jan 09 2020 at 07:16):

I haven't been following this discussion

view this post on Zulip Kenny Lau (Jan 09 2020 at 07:16):

what are the axioms now?

view this post on Zulip 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₂

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:20):

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

view this post on Zulip Kenny Lau (Jan 09 2020 at 07:22):

isn't that covered by my exists_unique_parallel?

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:22):

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

view this post on Zulip Kenny Lau (Jan 09 2020 at 07:24):

isn't that what it says?

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:26):

I don't see how

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:27):

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

view this post on Zulip Johan Commelin (Jan 09 2020 at 07:35):

/me should learn what exists_unique means

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jan 09 2020 at 07:43):

yay

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2020 at 08:34):

That lets you remove the noncomputable theory and open_locale classical.

view this post on Zulip Johan Commelin (Jan 09 2020 at 08:35):

Ooh, maybe I should revert my change...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 09 2020 at 08:45):

mario the linter says pre_geometry.has_parallel is bad

view this post on Zulip Johan Commelin (Jan 09 2020 at 08:45):

Did I goof up?

view this post on Zulip Mario Carneiro (Jan 09 2020 at 08:46):

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

view this post on Zulip Mario Carneiro (Jan 09 2020 at 08:47):

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

view this post on Zulip Johan Commelin (Jan 09 2020 at 08:47):

Makes sense

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 09 2020 at 09:11):

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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Jan 09 2020 at 09:18):

would Ln Ω make you feel better?

view this post on Zulip Johan Commelin (Jan 09 2020 at 09:19):

Not that much ...

view this post on Zulip Johan Commelin (Jan 09 2020 at 09:20):

Maybe Ω should be a parameter?

view this post on Zulip Kenny Lau (Jan 09 2020 at 09:25):

maybe we should build an example

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 09 2020 at 14:55):

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

view this post on Zulip 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 ?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 09 2020 at 16:17):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 09 2020 at 19:09):

Use exists_of_exists_unique

view this post on Zulip Johan Commelin (Jan 09 2020 at 19:09):

After that use choose

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip Johan Commelin (Jan 09 2020 at 19:12):

Usually such axioms are added, right?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Matt Earnshaw (Jan 09 2020 at 19:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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) }

view this post on Zulip Kenny Lau (Jan 10 2020 at 05:32):

yay the affine plane is a geometry

view this post on Zulip 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:

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip Ali Sever (Jan 15 2020 at 14:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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