From exists_unique to a function

Stream: new members

[Marc Masdeu]

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]

doesn't basic_general need to take h?

[Mario Carneiro]

Wait, basic_general is inconsistent

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Reid Barton]

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]

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]

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]

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

[Marc Masdeu]

(deleted)

[Kevin Buzzard]

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

[Kevin Buzzard]

Constants and axioms are dangerous.

[Marc Masdeu]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

Do you understand the full error message?

[Kevin Buzzard]

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]

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

[Marc Masdeu]

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

[Mario Carneiro]

Your axioms are still not correct:

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

you probably want Omega and L to be constants too

[Marc Masdeu]

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

[Mario Carneiro]

does the real version look like this?

[Mario Carneiro]

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]

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]

So what's the actual question?

[Marc Masdeu]

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]

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

[Kevin Buzzard]

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]

(working on this)...

[Marc Masdeu]

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]

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]

I didn't know about indefinite_description!

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

it could be @[irreducible] def

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

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]

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]

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.