Zulip Chat Archive

Stream: new members

Topic: proof of P → Q → P


view this post on Zulip Patrick Thomas (Mar 16 2019 at 22:41):

I am attempting to prove P → Q → P from just the ideas introduced at the beginning of Section 3.1 of Theorem Proving in Lean:

constant implies : Prop  Prop  Prop

constant Proof : Prop  Type

constant modus_ponens :
    Π p q : Prop, Proof (implies p q)  Proof p  Proof q

constant implies_intro :
    Π p q : Prop, (Proof p  Proof q)  Proof (implies p q)

variables P Q : Prop

As an easier start, I think I can prove P → P as:

#check implies_intro P P (λ x : Proof P, x)

I am not certain that this is right though. It means there is a sort of built in axiom that Proof P → Proof P?

In attempting to prove P → Q → P, I have:

#check implies_intro Q P
#check implies_intro P (implies Q P)

but I am struggling to put these together.

view this post on Zulip Kevin Buzzard (Mar 16 2019 at 23:14):

So you are intentionally not conflating Proof P with P?

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:15):

Yes.

view this post on Zulip Kevin Buzzard (Mar 16 2019 at 23:15):

A function Proof P -> Proof P would be id

view this post on Zulip Kevin Buzzard (Mar 16 2019 at 23:17):

I am not an expert in this sort of nonsense, but I would imagine that you have to be extremely careful to distinguish between the -> arrow and the implies arrow if you are doing it like this.

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:18):

prelude
notation `Prop` := Sort 0
notation f ` $ `:1 a:0 := f a

constant implies : Prop  Prop  Prop

constant Proof : Prop  Type

constant modus_ponens :
    Π {p q : Prop}, Proof (implies p q)  Proof p  Proof q

constant implies_intro :
    Π {p q : Prop}, (Proof p  Proof q)  Proof (implies p q)

variables P Q : Prop

noncomputable example : Proof (implies P (implies Q P)) :=
implies_intro $ λ hp, implies_intro $ λ hq, hp

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:26):

Thank you. I don't think I'm familiar with prelude, notation and noncomputable.

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:29):

just ignore those things

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:29):

Can it be done without them?

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:31):

I mean, what is your current code?

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:31):

because what you wrote at the beginning doesn't compile

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:31):

it complains that there is already a definition of "implies"

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:33):

I have what I posted wrapped in a namespace.

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:33):

namespace section_3_1
constant implies : Prop  Prop  Prop

constant Proof : Prop  Type

constant modus_ponens :
    Π p q : Prop, Proof (implies p q)  Proof p  Proof q

constant implies_intro :
    Π p q : Prop, (Proof p  Proof q)  Proof (implies p q)

variables P Q : Prop
end section_3_1

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:34):

namespace section_3_1
constant implies : Prop  Prop  Prop

constant Proof : Prop  Type

constant modus_ponens :
    Π {p q : Prop}, Proof (implies p q)  Proof p  Proof q

constant implies_intro :
    Π {p q : Prop}, (Proof p  Proof q)  Proof (implies p q)

variables P Q : Prop

noncomputable example : Proof (implies P (implies Q P)) :=
implies_intro $ λ hp, implies_intro $ λ hq, hp
end section_3_1

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:35):

What do the dollar signs denote?

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:37):

it denotes a bracket to the right

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:38):

noncomputable example : Proof (implies P (implies Q P)) :=
implies_intro (λ hp, implies_intro (λ hq, hp))

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:38):

is equivalent

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:43):

Sorry, if you don't mind, what would it look like without the implicit arguments?

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:44):

namespace section_3_1
constant implies : Prop  Prop  Prop

constant Proof : Prop  Type

constant modus_ponens :
    Π p q : Prop, Proof (implies p q)  Proof p  Proof q

constant implies_intro :
    Π p q : Prop, (Proof p  Proof q)  Proof (implies p q)

variables P Q : Prop

noncomputable example : Proof (implies P (implies Q P)) :=
implies_intro P (implies Q P) (λ hp, implies_intro Q P (λ hq, hp))
end section_3_1

view this post on Zulip Patrick Thomas (Mar 16 2019 at 23:47):

Thank you!


Last updated: May 08 2021 at 04:14 UTC