# Zulip Chat Archive

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

?

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

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 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 (Mar 16 2019 at 23:26):

Thank you. I don't think I'm familiar with `prelude`

, `notation`

and `noncomputable`

.

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

just ignore those things

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

Can it be done without them?

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

I mean, what is your current code?

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

because what you wrote at the beginning doesn't compile

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

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

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

I have what I posted wrapped in a namespace.

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

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

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

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

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