Zulip Chat Archive

Stream: new members

Topic: From exists_unique to a function


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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 16:53):

doesn't basic_general need to take h?

view this post on Zulip Mario Carneiro (Nov 13 2020 at 16:55):

Wait, basic_general is inconsistent

view this post on Zulip Mario Carneiro (Nov 13 2020 at 16:56):

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 16:56):

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

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

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

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

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

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

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

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

view this post on Zulip Marc Masdeu (Nov 13 2020 at 18:12):

(deleted)

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

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 18:15):

Constants and axioms are dangerous.

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

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

view this post on Zulip 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 R2\mathbb{R}^2"

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

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

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

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 18:24):

Do you understand the full error message?

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

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 18:26):

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

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:29):

Your axioms are still not correct:

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

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:31):

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:31):

you probably want Omega and L to be constants too

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:31):

does the real version look like this?

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

view this post on Zulip 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 (Pr.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 (Pr.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 (Pr.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.AS.B)  (r.originE)))
    /- 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) 
        ((AB)  (DE))  ((BC)  (EF))  ((AC)  (DF)))
    /- 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)
        ( : α.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') : (AB  A'B')  (AC  A'C')  ( B A C   B' A' C') 
        (BC  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.AT.B  R.AR.B)  (T.AT.C  R.AR.C)  (T.BT.C  R.BR.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.AT.B)  P  pts (T.BT.C)  P  pts (T.AT.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.AT.B)  P  pts (T.BT.C)  P  pts (T.AT.C) := by refl

@[simp] lemma mem_pts (P : Ω) (T : Triangle Ω) :
    P  T 
    P  pts (T.AT.B)  P  pts (T.BT.C)  P  pts (T.AT.C) := by refl

end Triangle

end HilbertPlane

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 18:33):

So what's the actual question?

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

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

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

view this post on Zulip Marc Masdeu (Nov 13 2020 at 18:35):

(working on this)...

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

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

view this post on Zulip Marc Masdeu (Nov 13 2020 at 19:27):

I didn't know about indefinite_description!

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:34):

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

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

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

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 20:50):

it could be @[irreducible] def

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

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

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

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

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

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