proof of P → Q → P

Stream: new members

[Patrick Thomas]

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.

[Kevin Buzzard]

So you are intentionally not conflating Proof P with P?

[Patrick Thomas]

Yes.

[Kevin Buzzard]

A function Proof P -> Proof P would be id

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Patrick Thomas]

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

[Kenny Lau]

just ignore those things

[Patrick Thomas]

Can it be done without them?

[Kenny Lau]

I mean, what is your current code?

[Kenny Lau]

because what you wrote at the beginning doesn't compile

[Kenny Lau]

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

[Patrick Thomas]

I have what I posted wrapped in a namespace.

[Patrick Thomas]

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

[Kenny Lau]

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

[Patrick Thomas]

What do the dollar signs denote?

[Kenny Lau]

it denotes a bracket to the right

[Kenny Lau]

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

[Kenny Lau]

is equivalent

[Patrick Thomas]

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

[Kenny Lau]

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

[Patrick Thomas]

Thank you!