## Stream: new members

### Topic: proof of P → Q → P

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

#### Kevin Buzzard (Mar 16 2019 at 23:14):

So you are intentionally not conflating Proof P with P?

Yes.

#### Kevin Buzzard (Mar 16 2019 at 23:15):

A function Proof P -> Proof P would be id

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

#### Kenny Lau (Mar 16 2019 at 23:18):

prelude
notation Prop := Sort 0
end section_3_1


#### Patrick Thomas (Mar 16 2019 at 23:35):

What do the dollar signs denote?

#### Kenny Lau (Mar 16 2019 at 23:37):

it denotes a bracket to the right

#### Kenny Lau (Mar 16 2019 at 23:38):

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


is equivalent

#### Patrick Thomas (Mar 16 2019 at 23:43):

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

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


#### Patrick Thomas (Mar 16 2019 at 23:47):

Thank you!

Last updated: May 08 2021 at 04:14 UTC