# Zulip Chat Archive

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

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

(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