## Stream: new members

### Topic: From exists_unique to a function

#### Marc Masdeu (Nov 13 2020 at 16:46):

Hello,

I'm sorry that this question is quite similar to another one that I asked a while ago. I'd like to fix the code below:

import tactic

noncomputable theory
open_locale classical

variables {Ω L : Type}
variables {A B : Ω}
variables {ℓ : L}
variables {p : Ω → L → Prop}

axiom basic_general : (A = B → ∃ ℓ : L, p A ℓ)
axiom basic_neq : (A ≠ B → ∃! ℓ : L, p A ℓ ∧ p B ℓ)

def line_through_points (A B : Ω) : L :=
begin
by_cases h : A = B,
{
exact classical.some basic_general, -- this doesn't work
},
{
exact classical.some (basic_neq h),  -- this doesn't work, either
}
end

lemma line_through_left : p A (line_through_points A B) :=
begin
sorry  -- how to prove this? should use classical.some_spec...
end

lemma line_through_right : p B (line_through_points A B) :=
begin
sorry  -- how to prove this? should use classical.some_spec...
end

lemma line_unique : A ≠ B → p A ℓ → p B ℓ → ℓ = line_through_points A B :=
begin
sorry
end


Essentially, I have two axioms (or lemmas, whatever) that guarantee the existence of a line through two points. If the points are distinct, then the line is unique. From this I would like to have a function that outputs a line in any case (when the points are equal, it will be one of the possibly infinitely many, I don't care). It is then in line_unique that the hypothesis of the points being different will get used.

I (think that I) know that by_cases shouldn't be used because I am constructing data, but I don't know how to do it properly. Any hints?

Thank you.

#### Mario Carneiro (Nov 13 2020 at 16:53):

doesn't basic_general need to take h?

#### Mario Carneiro (Nov 13 2020 at 16:55):

Wait, basic_general is inconsistent

#### Mario Carneiro (Nov 13 2020 at 16:56):

example : false := let ⟨_, f⟩ := @basic_general unit unit () () (λ _ _, false) rfl in f


#### Mario Carneiro (Nov 13 2020 at 16:56):

it seems unlikely that you want p to be a variable here

#### Mario Carneiro (Nov 13 2020 at 16:58):

basic_ne is also inconsistent for a similar reason

example : false := let ⟨_, ⟨f, _⟩, _⟩ := @basic_neq bool unit ff tt (λ _ _, false) bool.ff_ne_tt in f


#### Reid Barton (Nov 13 2020 at 16:58):

A cleaner setup is to first prove a lemma that for any points A B, there is a line through A and B

#### Reid Barton (Nov 13 2020 at 16:59):

use classical.some on that to define line_through_points, and classical.some_spec to prove the next two lemmas

#### Reid Barton (Nov 13 2020 at 16:59):

and for the last one you don't care what the definition of line_through_points A B is as long as you know it's also a line through A and B

#### Marc Masdeu (Nov 13 2020 at 17:53):

Mario Carneiro said:

it seems unlikely that you want p to be a variable here

Sorry, I wanted a constant there. This is me failing to write a proper MWE...

#### Kevin Buzzard (Nov 13 2020 at 18:09):

You edited your code above (changing a variable to a constant) so now Mario's observations don't apply, but neither do most of your comments. The first thing that you say doesn't work is easily fixed, the second thing you say doesn't work now works, and the things you say you can't prove now don't even compile.

#### Marc Masdeu (Nov 13 2020 at 18:11):

I'm working now on doing what @Reid Barton suggested. Just changed it back so now everything still applies...

(deleted)

#### Kevin Buzzard (Nov 13 2020 at 18:14):

When Ali Sever set all this up in Lean he didn't ever need to use a constant.

#### Kevin Buzzard (Nov 13 2020 at 18:15):

Constants and axioms are dangerous.

#### Marc Masdeu (Nov 13 2020 at 18:15):

Yes, I am trying to set it up so that advanced results can be proved easily. This is the MWE I cooked up to ask the question.

#### Marc Masdeu (Nov 13 2020 at 18:16):

I have set it up in a structure (actually a class). The axioms originally were non-constructive, then I thought it would be easier to work with them if they were constructive. But now I think the best is to have them non-construtive, and then have some constructive functions and lemmas.

#### Kevin Buzzard (Nov 13 2020 at 18:17):

Yeah, Ali used a class. This then somehow reduces the question "is there actually a model of what you're doing" to "can you prove these theorems about $\mathbb{R}^2$"

#### Marc Masdeu (Nov 13 2020 at 18:18):

I also thought that it would be nice that line_through_points didn't need them to be different (a bit similar to the 1/0 issue). This way, in constructing proofs (a la Euclid) I'd say things like "take the line throught these two points", later on I'll see whether I need it to be unique (and use they are different) or not.

#### Marc Masdeu (Nov 13 2020 at 18:23):

So far I have this:

import tactic

noncomputable theory
open_locale classical

variables {Ω L : Type}
variables {A B : Ω}
constant p : Ω → L → Prop

constant basic_general : (A=B → ∃ ℓ : L, p A ℓ ∧ p B ℓ)

constant basic_neq : (A ≠ B → ∃! ℓ : L, p A ℓ ∧ p B ℓ)

lemma exists_line_through_points (A B : Ω) : (∃ ℓ : L, p A ℓ ∧ p B ℓ ) :=
begin
by_cases h : A = B,
{
exact basic_general h,
},
{
apply exists_of_exists_unique (basic_neq h),
},
end

def line_through_points (A B : Ω) : L :=
begin
exact classical.some (exists_line_through_points A B),
end

lemma line_through_left : p A (line_through_points A B) :=
begin
sorry
end

lemma line_through_right : p B (line_through_points A B) :=
begin
sorry
end

lemma line_unique : A ≠ B → p A ℓ → p B ℓ → ℓ = line_through_points A B :=
begin
sorry
end


#### Marc Masdeu (Nov 13 2020 at 18:23):

But line_through_left doesn't typecheck, it says it doesn't know how to synthethize placeholder.

#### Kevin Buzzard (Nov 13 2020 at 18:24):

Do you understand the full error message?

#### Kevin Buzzard (Nov 13 2020 at 18:25):

line_through_points A B gives

line_through_points : Π {Ω L : Type}, Ω → Ω → L
don't know how to synthesize placeholder
context:
Ω : Type,
A B : Ω
⊢ Type


#### Kevin Buzzard (Nov 13 2020 at 18:26):

Try to be the compiler. The error message is correct.

#### Marc Masdeu (Nov 13 2020 at 18:29):

To me, line_through_points takes two terms of type Omega and spits out a term of type L.

#### Mario Carneiro (Nov 13 2020 at 18:29):

Your axioms are still not correct:

example : false := match @basic_general unit empty () () rfl with end


#### Kevin Buzzard (Nov 13 2020 at 18:30):

To Lean, line_through_points takes two types Omega and L, which Lean is supposed to guess because they are in {}s, and then two terms of type Omega (meaning that Lean can easily guess Omega) and then it's supposed to return a term of type L, but you didn't tell Lean what L was, and there's no way it can guess.

#### Mario Carneiro (Nov 13 2020 at 18:31):

the problem is that p is too general, it quantifies over all possible types

#### Mario Carneiro (Nov 13 2020 at 18:31):

you probably want Omega and L to be constants too

#### Marc Masdeu (Nov 13 2020 at 18:31):

I think that @Kevin Buzzard and @Mario Carneiro are pointing to the same issue: I did a terrible mwe

#### Mario Carneiro (Nov 13 2020 at 18:31):

does the real version look like this?

#### Mario Carneiro (Nov 13 2020 at 18:32):

usually an MWE is made by deleting irrelevant things from the real example, so I wouldn't expect a constant to become a variable

#### Marc Masdeu (Nov 13 2020 at 18:32):

Not at all.

import tactic

noncomputable theory
open_locale classical

def pts {α β : Type*} [has_mem α β] (S : β) : set α := {x : α | x ∈ S}

@[simp] lemma mem_pts {α β : Type*} [has_mem α β] (x : α) (S : β) : x ∈ pts S ↔ x ∈ S :=  by refl

notation p xor q := (p ∧ ¬ q) ∨ (q ∧ ¬ p)
def xor3 (p q r : Prop) : Prop := (p ∧ ¬ q ∧ ¬ r) ∨ (¬ p ∧ q ∧ ¬ r) ∨ (¬ p ∧ ¬ q ∧ r)

class PreHilbertPlane (Point : Type*) :=
(Line : Type*)
(belongs : Point → Line → Prop)
(between : Point → Point → Point → Prop)

(notation A ∈ ℓ := belongs A ℓ)

-- I1: there is a unique line passing through two distinct points.
(I1' {A B : Point} (h : A ≠ B) : ∃! (ℓ : Line) , A ∈ ℓ ∧ B ∈ ℓ)

-- I2: any line contains at least two points.
(I2' (ℓ : Line) : ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)

-- I3: there exists 3 non-collinear points.
(I3' : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))

namespace PreHilbertPlane
variables {Ω : Type*} [PreHilbertPlane Ω]

instance : has_mem Ω (Line Ω) := ⟨belongs⟩

instance Line.has_coe : has_coe (Line Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem (p : Ω) (ℓ : Line Ω) : p ∈ (ℓ : set Ω) ↔ p ∈ ℓ := by refl

def points_between (A B : Ω) : set Ω := {P : Ω | between A P B}
notation A * B * C := PreHilbertPlane.between A B C

-- Put the axioms in terms of this has_mem
lemma I1 {A B : Ω} (h : A ≠ B) : ∃! (ℓ : Line Ω), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ) := I1' h
lemma I2 (ℓ : Line Ω) : ∃ A B : Ω, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ := I2' ℓ
lemma I3 : ∃ A B C : Ω, A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ ∀ ℓ : Line Ω, A ∈ ℓ ∧ B ∈ ℓ → ¬ C ∈ ℓ := I3'

def collinear (A B C : Ω) := ∃ (ℓ : Line Ω), A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ
@[simp] lemma collinear_iff {A B C : Ω} :
collinear A B C ↔ ∃ ℓ : Line Ω, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ :=
begin
rw collinear,
end

def intersect (r s : Line Ω) := ∃ A, A ∈ r ∧ A ∈ s

def parallel (r s : Line Ω) := (r = s) ∨ (¬ intersect r s)
notation r || s := parallel r s

end PreHilbertPlane

open PreHilbertPlane

/-- A segment is created by giving two points. -/
structure Segment (Point : Type*) :=
(A : Point) (B : Point)
notation A ⬝:100 B := Segment.mk A B

namespace Segment
variables {Ω : Type*} [PreHilbertPlane Ω]

/--
When thought of as a set, it is the the set consisting of the endpoints
and all the points between them
-/
instance : has_mem Ω (Segment Ω) :=
⟨λ P S, P = S.A ∨ P = S.B ∨ S.A * P * S.B⟩

instance has_coe_to_set : has_coe (Segment Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (S : Segment Ω) :
P ∈ (S : set Ω) ↔ (P = S.A ∨ P = S.B ∨ S.A * P * S.B) := by refl

@[simp] lemma mem_pts (P : Ω) (S : Segment Ω) :
P ∈ S ↔ (P = S.A ∨ P = S.B ∨ S.A * P * S.B) := by refl

end Segment

structure Ray (Point : Type*):=
(origin : Point) (target : Point)
notation A => B := Ray.mk A B

namespace Ray
variables {Ω : Type*} [PreHilbertPlane Ω]

instance : has_mem Ω (Ray Ω) :=
⟨λ P r, P = r.origin ∨ (collinear r.origin P r.target ∧ ¬ r.origin ∈ pts (P⬝r.target))⟩

instance has_coe_to_set : has_coe (Ray Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (r : Ray Ω) :
P ∈ (r : set Ω) ↔
P = r.origin ∨ (collinear r.origin P r.target ∧ ¬ r.origin ∈ pts (P⬝r.target)) := by refl
@[simp] lemma mem_pts (P : Ω) (r : Ray Ω) :
P ∈ pts r ↔ P = r.origin ∨ (collinear r.origin P r.target ∧ ¬ r.origin ∈ pts (P⬝r.target)) := by refl

end Ray

structure Angle (Point : Type*) :=
(A : Point) (x : Point) (B : Point)
notation ∟:100 := Angle.mk

namespace Angle
variables {Ω : Type*} [PreHilbertPlane Ω]

def nondegenerate (a : Angle Ω) := ¬ collinear a.A a.x a.B

instance : has_mem Ω (Angle Ω) :=
⟨λ P a, P ∈ pts (a.x=>a.A) ∨ P ∈ pts (a.x=>a.B)⟩

instance has_coe_to_set : has_coe (Angle Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (a : Angle Ω) :
P ∈ (a : set Ω) ↔
P ∈ pts (a.x=>a.A) ∨ P ∈ pts (a.x=>a.B) := by refl

@[simp] lemma mem_pts (P : Ω) (a : Angle Ω) :
P ∈ a ↔
P ∈ pts (a.x=>a.A) ∨ P ∈ pts (a.x=>a.B) := by refl

end Angle

class HilbertPlane (Point : Type*) extends PreHilbertPlane Point :=
/- Betweenness is symmetric -/
(B11 {A B C : Point} : (A * B * C) → (C * B * A))
/- If A * B * C then the three points are distinct and collinear. -/
(B12 {A B C : Point} : (A * B * C) → (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ collinear A B C))
/- Given two distinct points A, B, there is a third point C such that A * B * C.-/
(B2 {A B : Point} (h: A ≠ B) : ∃ C, A * B * C)
/- Given 3 distinct collinear points A B C, exactly one of them is between the other two.-/
(B3 {A B C : Point} (h: collinear A B C) :
xor3 (A * B * C) ( B * A * C ) (A * C * B))

(B4 {A B C D : Point} {ℓ : Line} -- Pasch
(hnc: ¬ collinear A B C)
(hnAl: ¬ (A ∈ ℓ)) (hnBl: ¬ B ∈ ℓ) (hnCl: ¬ C ∈ ℓ)
(hDl: D ∈ ℓ) (hADB: A * D * B) :
(∃ E ,  E ∈ ℓ ∧ (A * E * C)) xor (∃ E, E ∈ ℓ ∧ (B * E * C)))

(seg_cong : Segment Point → Segment Point → Prop)
(notation X ≅:50 Y := seg_cong X Y)
(ang_cong : Angle Point → Angle Point → Prop)
(notation X ≃:50 Y := ang_cong X Y)

/- Given a segment AB and a ray C->D, there is a unique point E on C->D such that
AB ≅ CE. -/
(C1 (S : Segment Point) (r : Ray Point) :
∃! E, (E ∈ pts r) ∧ ((S.A⬝S.B) ≅ (r.origin⬝E)))
/- Congruence of segments is reverse-transitive -/
(C21 (S T U): (S ≅ T) → (S ≅ U) → (T ≅ U))
/- Congruence of segments is reflexive.
Note that this together with C21 implies symmetry of congruence. -/
(C22 (S) : S ≅ S)
/- Congruence of segments respects the notion of sum of segments -/
(C3 (A B C D E F) : (A * B * C) → (D * E * F) →
((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))
/- Given a nondegenerate angle α, a segment AB, and a point s,
construct a point E on the same side as s, such that ∟EAB ≃ α. -/
(C4 (α : Angle Point) (S : Ray Point) (s : Point)
(hα : α.nondegenerate) (hs : ¬ collinear s S.origin S.target)
(hr : S.origin ≠ S.target) :  ∃! E : Point,
(∟ E S.origin S.target ≃ α) ∧
∀ x, (E * x * s) → ∀ (ℓ : Line), S.origin ∈ ℓ ∧ S.target ∈ ℓ
→ ¬ x ∈ ℓ)
/-
(C4spec (α : Angle Point) (S : Ray Point) (s : Point)
(hα : α.nondegenerate) (hs : ¬ collinear s S.origin S.target)
(hr : S.origin ≠ S.target) : (∟ (C4 α S s hα hs hr) S.origin S.target ≃ α) ∧
(∀ (x : Point), ((C4 α S s hα hs hr) * x * s) → ¬ x ∈ line_through hr))
(C4uniq (α : Angle Point) (S : Ray Point) (s : Point) (Z : Point)
(hBAC : α.nondegenerate) (hs : ¬ collinear s S.origin S.target) (hr : S.origin ≠ S.target) :
(∟ Z S.origin S.target ≃ α) →
((∀ (x : Point), (Z * x * s) → ¬ x ∈ line_through hr)) →
pts (S.origin=>Z) = pts (S.origin=>(C4 α S s hBAC hs hr)))
-/
/- Congruence of angles is reverse-transitive.-/
(C5 (α β γ : Angle Point) : α ≃ β → α ≃ γ → β ≃ γ)
/- Given triangles T and T', if they have two sides and their middle angle
congruent, then the third sides and the other two angles are also congruent.-/
(C6 (A B C A' B' C') : (A⬝B ≅ A'⬝B') → (A⬝C ≅ A'⬝C') → (∟ B A C ≃ ∟ B' A' C') →
(B⬝C ≅ B'⬝C') ∧ (∟ A B C ≃ ∟ A' B' C') ∧ (∟ A C B ≃ ∟ A' C' B'))

class EuclideanPlane (Point : Type*) extends HilbertPlane Point :=
(parallel_postulate {ℓ r s : Line} :
(intersect r s) ∧ (r || ℓ) ∧ (s || ℓ) → (r = s))

namespace HilbertPlane

notation X ≅:50 Y:50 := HilbertPlane.seg_cong X Y
notation X ≃:50 Y:50 := HilbertPlane.ang_cong X Y

structure Triangle (Point : Type*) :=
(A : Point) (B : Point) (C : Point)
notation ▵:100 := Triangle.mk

namespace Triangle
variables {Ω : Type*} [HilbertPlane Ω]

def nondegenerate (T : Triangle Ω) := ¬ collinear T.A T.B T.C

def congruent_triangles (T R : Triangle Ω) :=
(T.A⬝T.B ≅ R.A⬝R.B) ∧ (T.A⬝T.C ≅ R.A⬝R.C) ∧ (T.B⬝T.C ≅ R.B⬝R.C)
∧ (∟ T.B T.A T.C ≃ ∟ R.B R.A R.C)
∧ (∟ T.A T.C T.B ≃ ∟ R.A R.C R.B)
∧ (∟ T.C T.B T.A ≃ ∟ R.C R.B R.A)

instance : has_mem Ω (Triangle Ω) :=
⟨λ P T, P ∈ pts (T.A⬝T.B) ∨ P ∈ pts (T.B⬝T.C) ∨ P ∈ pts (T.A⬝T.C)⟩

instance has_coe_to_set : has_coe (Triangle Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (T : Triangle Ω) :
P ∈ (T : set Ω) ↔
P ∈ pts (T.A⬝T.B) ∨ P ∈ pts (T.B⬝T.C) ∨ P ∈ pts (T.A⬝T.C) := by refl

@[simp] lemma mem_pts (P : Ω) (T : Triangle Ω) :
P ∈ T ↔
P ∈ pts (T.A⬝T.B) ∨ P ∈ pts (T.B⬝T.C) ∨ P ∈ pts (T.A⬝T.C) := by refl

end Triangle

end HilbertPlane


#### Kevin Buzzard (Nov 13 2020 at 18:33):

So what's the actual question?

#### Marc Masdeu (Nov 13 2020 at 18:33):

Mario Carneiro said:

usually an MWE is made by deleting irrelevant things from the real example, so I wouldn't expect a constant to become a variable

I guess I was trying to aks a question and provide an example to illustrate, and I messed up.

#### Mario Carneiro (Nov 13 2020 at 18:33):

aha, so you should probably delete unneeded fields from the structure and using sorry for the lemmas

#### Kevin Buzzard (Nov 13 2020 at 18:35):

You can change those by refl tactic proofs to iff.rfl term proofs (I remark this in passing while I'm waiting for the question :D )

#### Marc Masdeu (Nov 13 2020 at 18:35):

(working on this)...

#### Marc Masdeu (Nov 13 2020 at 18:44):

import tactic

noncomputable theory
open_locale classical

def pts {α β : Type*} [has_mem α β] (S : β) : set α := {x : α | x ∈ S}

@[simp] lemma mem_pts {α β : Type*} [has_mem α β] (x : α) (S : β) : x ∈ pts S ↔ x ∈ S :=  by refl

class PreHilbertPlane (Point : Type*) :=
(Line : Type*)
(belongs : Point → Line → Prop)
(between : Point → Point → Point → Prop)

(notation A ∈ ℓ := belongs A ℓ)

-- I1: there is a unique line passing through two distinct points.
(I1' {A B : Point} (h : A ≠ B) : ∃! (ℓ : Line) , A ∈ ℓ ∧ B ∈ ℓ)

-- I3: there exists 3 non-collinear points.
(I3' : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))

namespace PreHilbertPlane
variables {Ω : Type*} [PreHilbertPlane Ω]

instance : has_mem Ω (Line Ω) := ⟨belongs⟩

instance Line.has_coe : has_coe (Line Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem (p : Ω) (ℓ : Line Ω) : p ∈ (ℓ : set Ω) ↔ p ∈ ℓ := by refl

-- Put the axioms in terms of this has_mem
lemma I1 {A B : Ω} (h : A ≠ B) : ∃! (ℓ : Line Ω), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ) := I1' h
lemma I3 : ∃ A B C : Ω, A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ ∀ ℓ : Line Ω, A ∈ ℓ ∧ B ∈ ℓ → ¬ C ∈ ℓ := I3'

end PreHilbertPlane

open PreHilbertPlane
variables {Ω : Type*} [PreHilbertPlane Ω]

variables {A B C : Ω}
variables {ℓ r s : Line Ω}

lemma I11 (h: A ≠ B) : ∃ (ℓ : Line Ω), A ∈ ℓ ∧ B ∈ ℓ := exists_of_exists_unique (I1 h)

lemma I12
(h: A ≠ B) (hAr: A ∈ r) (hBr : B ∈ r) (hAs : A ∈ s) (hBs : B ∈ s) : r = s :=
begin
apply unique_of_exists_unique (I1 h);
tauto,
end

lemma there_are_two_points : ∃ A B : Ω, (A ≠ B) :=
begin
rcases I3 with ⟨A, ⟨B, ⟨C, ⟨h1, h2⟩⟩⟩⟩,
use [A, B],
assumption,
end

def line_through_points (A B : Ω) : Line Ω:=
begin
sorry
end

lemma line_through_points_left {A B : Ω}: A ∈ (line_through_points A B) :=
begin
sorry
end

lemma line_through_points_right {A B : Ω}: B ∈ (line_through_points A B) :=
begin
sorry
end

lemma line_unique {A B : Ω} : A ≠ B → A ∈ ℓ → B ∈ ℓ → ℓ = line_through_points A B :=
begin
sorry
end


The question: I'd like to fill in the sorrys. But after what @Reid Barton suggested maybe I can work it out myself!

#### Mario Carneiro (Nov 13 2020 at 18:56):

lemma exists_point_ne : ∀ A, ∃ B : Ω, A ≠ B :=
begin
intro A,
obtain ⟨B, C, hBC⟩ := @there_are_two_points Ω _,
by_cases A = B,
{ subst h, exact ⟨_, hBC⟩ },
{ exact ⟨_, h⟩ }
end

def line_through_points_aux (A B : Ω) : {ℓ : Line Ω // A ∈ ℓ ∧ B ∈ ℓ} :=
begin
apply classical.indefinite_description,
by_cases A = B,
{ subst B, obtain ⟨B, h⟩ := exists_point_ne A,
obtain ⟨ℓ, h, _⟩ := I11 h,
exact ⟨ℓ, h, h⟩ },
{ exact I11 h }
end

def line_through_points (A B : Ω) : Line Ω := (line_through_points_aux A B).1

lemma line_through_points_left {A B : Ω}: A ∈ line_through_points A B :=
(line_through_points_aux A B).2.1

lemma line_through_points_right {A B : Ω}: B ∈ (line_through_points A B) :=
(line_through_points_aux A B).2.2

lemma line_unique {A B : Ω} : A ≠ B → A ∈ ℓ → B ∈ ℓ → ℓ = line_through_points A B :=
λ ab al bl, I12 ab al bl line_through_points_left line_through_points_right


#### Marc Masdeu (Nov 13 2020 at 19:27):

I didn't know about indefinite_description!

#### Mario Carneiro (Nov 13 2020 at 19:34):

you can also use classical.choice instead, it's basically the same proof

#### Mario Carneiro (Nov 13 2020 at 19:36):

to use some and some_spec you would factor the proof a little differently:

theorem line_through_points_aux (A B : Ω) : ∃ ℓ : Line Ω, A ∈ ℓ ∧ B ∈ ℓ :=
begin
by_cases A = B,
{ subst B, obtain ⟨B, h⟩ := exists_point_ne A,
obtain ⟨ℓ, h, _⟩ := I11 h,
exact ⟨ℓ, h, h⟩ },
{ exact I11 h }
end

def line_through_points (A B : Ω) : Line Ω := classical.some (line_through_points_aux A B)

lemma line_through_points_left {A B : Ω}: A ∈ line_through_points A B :=
(classical.some_spec (line_through_points_aux A B)).1

lemma line_through_points_right {A B : Ω}: B ∈ (line_through_points A B) :=
(classical.some_spec (line_through_points_aux A B)).2


#### Kevin Buzzard (Nov 13 2020 at 20:45):

How come

def line_through_points_aux (A B : Ω) : {ℓ : Line Ω // A ∈ ℓ ∧ B ∈ ℓ} :=
begin
apply classical.indefinite_description,
by_cases A = B,
{ subst B, obtain ⟨B, h⟩ := exists_point_ne A,
obtain ⟨ℓ, h, _⟩ := I11 h,
exact ⟨ℓ, h, h⟩ },
{ exact I11 h }
end


is clearly not best practice, making a definition in tactic mode and using eq.rec etc, and yet you don't run into any trouble? The some/some_spec route I completely understand and this would have been the route I would have taken.

#### Reid Barton (Nov 13 2020 at 20:50):

Because you never plan to look at the definition again anyways, just use the information encoded in the type

#### Mario Carneiro (Nov 13 2020 at 20:50):

it could be @[irreducible] def

#### Kevin Buzzard (Nov 13 2020 at 20:52):

Aah I see! You don't need to use any properties of the term the function produces, other than the fact that its type is its type.

#### Marc Masdeu (Nov 14 2020 at 10:49):

Here is my solution (the first lemma should be written in a much shorter way, I know). Thanks so much for all the discussion. This is helping me in understanding the differences between Prop and Type.

lemma exists_line_through_points (A B : Ω) : ∃ (ℓ : Line Ω), A ∈ ℓ ∧ B ∈ ℓ :=
begin
by_cases h : A = B,
{
subst h,
have H : ∃ C D : Ω, C ≠ D := there_are_two_points,
obtain ⟨C, D, hCD⟩ := H,
by_cases hAC : A = C,
{
subst hAC,
have h2 : ∃ ℓ : Line Ω, A ∈ ℓ ∧ D ∈ ℓ := I11 hCD,
obtain ⟨ℓ, hAℓ, hCℓ⟩ := h2,
use ℓ,
tauto,
},
have h2 : ∃ ℓ : Line Ω, A ∈ ℓ ∧ C ∈ ℓ := I11 hAC,
obtain ⟨ℓ, hAℓ, hCℓ⟩ := h2,
use ℓ,
tauto,
},
{
exact I11 h,
}
end

def line_through_points (A B : Ω) : Line Ω :=
classical.some (exists_line_through_points A B)

lemma line_through_points_left {A B : Ω} : A ∈ (line_through_points A B) :=
(classical.some_spec (exists_line_through_points A B)).1

lemma line_through_points_right {A B : Ω} : B ∈ (line_through_points A B) :=
(classical.some_spec (exists_line_through_points A B)).2

lemma points_mem_of_line_through_points {A B : Ω} : A ∈ (line_through_points A B) ∧ B ∈ (line_through_points A B) :=
⟨line_through_points_left, line_through_points_right⟩

lemma line_unique {A B : Ω} : A ≠ B → A ∈ ℓ → B ∈ ℓ → ℓ = line_through_points A B :=
λ h hAℓ hBℓ, unique_of_exists_unique (I1 h) ⟨hAℓ, hBℓ⟩ points_mem_of_line_through_points


#### Ruben Van de Velde (Nov 14 2020 at 10:59):

Maybe you could factor out a lemma that there exists a line through one point for the first

#### Eric Wieser (Nov 17 2020 at 14:27):

Kevin Buzzard said:

Aah I see! You don't need to use any properties of the term the function produces, other than the fact that its type is its type.

Does this mean that you should mark the def a lemma, even though doing so is obviously unusual?

#### Yakov Pechersky (Nov 17 2020 at 14:41):

I don't think this is the case. I think the tactic here works because classical.indefinite_description constructs data out of a p : Line Ω → Prop term and a (h : ∃ x, p x) term, which is the supplied proof. The apply classical.indefinite_description step takes care of inferring the p data, and the rest (the Prop term) can be done via tactics as usual.

#### Yakov Pechersky (Nov 17 2020 at 15:38):

That's also because that def is equivalent to the following:

def line_through_points_aux (A B : Ω) : {ℓ : Line Ω // A ∈ ℓ ∧ B ∈ ℓ} :=
classical.indefinite_description _ (dite (A = B)
(λ h, exists.elim (exists_point_ne A)
(λ C hne, exists.elim (I11 hne)
(λ ℓ ⟨hA, hC⟩, ⟨_, hA, h ▸ hA⟩)))
I11)


and my understanding is that subst and obtain are term-friendly.

Last updated: May 14 2021 at 04:22 UTC