## Stream: new members

### Topic: forward proof

#### lini (Nov 12 2022 at 16:20):

hello im new to lean, i want to ask particular question but not sure how too post it here

#### lini (Nov 12 2022 at 16:23):

so i have this functions

def excluded_middle : Prop :=
∀a : Prop, a ∨ ¬ a

def peirce : Prop :=
∀a b : Prop, ((a → b) → a) → a

def double_negation : Prop :=
∀a : Prop, (¬¬ a) → a

i need to do forward proof of this
lemma peirce_of_dn :
double_negation → peirce :=

but i got stuck since yesterday

#### lini (Nov 12 2022 at 16:27):

∀a : Prop, a ∨ ¬ a 

def peirce : Prop :=
∀a b : Prop, ((a → b) → a) → a 

def double_negation : Prop :=
∀a : Prop, (¬¬ a) → a 

lemma peirce_of_dn :
double_negation → peirce :=

but i got stuck since yesterday
i need to do forward proof of this


#### Eric Wieser (Nov 12 2022 at 16:29):

Can you take another look at #backticks and edit (with the :pencil: icon) your message accordingly?

#### Eric Wieser (Nov 12 2022 at 16:30):

(In particular, the   s need to be on their own line)

#### Arthur Paulino (Nov 12 2022 at 16:35):

You can add several lines to the "code block" (the content between backticks):

∀a : Prop, a ∨ ¬ a

def peirce : Prop :=
∀a b : Prop, ((a → b) → a) → a

def double_negation : Prop :=
∀a : Prop, (¬¬ a) → a

lemma peirce_of_dn :
double_negation → peirce :=


Sorry, this is not super friendly for people who aren't used to writing markdown content. You can click on the three dots at the top right corner of this message and see what I wrote with "View message source"

#### lini (Nov 12 2022 at 16:49):

ooooh thank you let me try it again

#### lini (Nov 12 2022 at 16:51):

∀a : Prop, a ∨ ¬ a

def peirce : Prop :=
∀a b : Prop, ((a → b) → a) → a

def double_negation : Prop :=
∀a : Prop, (¬¬ a) → a


but i got stuck since yesterday
i need to do forward proof of this

lemma peirce_of_dn :
double_negation → peirce :=


#### Eric Wieser (Nov 12 2022 at 17:00):

There's no need to post it again, you can edit your original post

#### Junyan Xu (Nov 12 2022 at 17:06):

lemma peirce_of_dn :
double_negation → peirce :=
begin
intros h1 a b h2,
apply h1,
end


and you only need intro, apply, and exfalso to complete the proof.

#### lini (Nov 12 2022 at 17:23):

Junyan Xu said:

lemma peirce_of_dn :
double_negation → peirce :=
begin
intros h1 a b h2,
apply h1,
end


and you only need intro, apply, and exfalso to complete the proof.

but is it not backward proof?

#### Junyan Xu (Nov 12 2022 at 17:25):

Oh sorry, I missed the forward requirement. But once you work out a backward proof, you can extract a forward proof from it. (Instead of exfalso, use docs#false.elim or docs#absurd.)

#### Junyan Xu (Nov 12 2022 at 17:26):

So for example the two lines of tactics above translate to

lemma peirce_of_dn :
double_negation → peirce :=
λ h1 a b h2, h1 a _


I don't think you should restrict yourself to a "forward thinking mode" when working out the proof :)

#### lini (Nov 12 2022 at 17:29):

Junyan Xu said:

Oh sorry, I missed the forward requirement. But once you work out a backward proof, you can extract a forward proof from it. (Instead of exfalso, use docs#false.elim or docs#absurd.)

I tried it like this but got error

lemma peirce_of_dn :
double_negation → peirce :=
fix a b : Prop,
assume hda : ¬¬a → a,
assume habaa : ((a → b) → a),
(assume hna : ¬a,
have hab : a → b, from
(assume ha : a, show b, from false.elim (hna ha)),
have ha : a, from habaa hab,
show false, from hna ha)


#### lini (Nov 12 2022 at 17:33):

may i know what is command in forward proof that equal to apply in backward proof?

#### Junyan Xu (Nov 12 2022 at 17:34):

The first lines don't make sense, you must intro/assume variables in the order they appear, in this case:

assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),


#### Junyan Xu (Nov 12 2022 at 17:38):

By the way are you using Lean 3 or Lean 4? fix seems not recognized at all by Lean 3.

#### lini (Nov 12 2022 at 17:41):

Junyan Xu said:

By the way are you using Lean 3 or Lean 4? fix seems not recognized at all by Lean 3.

hmm im not sure, i think i use lean 3..
fix works in my side..

#### lini (Nov 12 2022 at 17:44):

Junyan Xu said:

The first lines don't make sense, you must intro/assume variables in the order they appear, in this case:

assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),


lemma peirce_of_dn :
double_negation → peirce :=
--fix a b : Prop,
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
(assume hna : ¬a,
have hab : a → b, from
(assume ha : a, show b, from false.elim (hna ha)),
have ha : a, from habaa hab,
show false, from hna ha)


the first assume becomes error

#### Junyan Xu (Nov 12 2022 at 17:50):

There's error because the type of the fourth line and below doesn't match, it doesn't happen at the first assume. If you write

lemma peirce_of_dn :
double_negation → peirce :=
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a), _


and place your cursor at the underscore, you see that hda a b habaa are successfully assumed/introduced, but the goal is a and it's not ¬a → something, so it's invalid to assume hna : ¬a there.

#### lini (Nov 12 2022 at 18:03):

Junyan Xu said:

There's error because the type of the fourth line and below doesn't match, it doesn't happen at the first assume. If you write

lemma peirce_of_dn :
double_negation → peirce :=
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a), _


and place your cursor at the underscore, you see that hda a b habaa are successfully assumed/introduced, but the goal is a and it's not ¬a → something, so it's invalid to assume hna : ¬a there.

yah, but it means that i have to find a way to get "a" this is the case that i failed

#### Junyan Xu (Nov 12 2022 at 18:12):

Since you have hda around you can do

assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
have nna : ¬¬a, from
assume na : ¬a,
have ha : a, from _,
na ha,
hda a nna


#### alini (Nov 12 2022 at 18:25):

Junyan Xu said:

Since you have hda around you can do

assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
have nna : ¬¬a, from
assume na : ¬a,
have ha : a, from _,
na ha,
hda a nna


but what does the from _  means?

#### Junyan Xu (Nov 12 2022 at 18:34):

It means you need to fill in the underscore; you see a red squiggle there right? If you put your input cursor there, you see the goal is a again but now you have (a → b) → a and ¬a in the context.

#### alini (Nov 12 2022 at 18:38):

lemma peirce_of_dn :
double_negation → peirce :=
fix a b : Prop,
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
have nna : ¬¬a, from
(assume hna : ¬a,
have hab : a → b, from
(assume ha : a, show b, from false.elim (hna ha)),
have ha : a, from habaa hab,
show false, from hna ha)


i tried this but the lemma becomes yellowa

#### alini (Nov 12 2022 at 18:39):

lini said:

lemma peirce_of_dn :
double_negation → peirce :=
fix a b : Prop,
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
have nna : ¬¬a, from
(assume hna : ¬a,
have hab : a → b, from
(assume ha : a, show b, from false.elim (hna ha)),
have ha : a, from habaa hab,
show false, from hna ha)


i tried this but the lemma becomes yellowa

means that its still error

#### Junyan Xu (Nov 12 2022 at 18:49):

You are close! Just remove fix a b from the beginning and show a at the end:

lemma peirce_of_dn :
double_negation → peirce :=
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
have nna : ¬¬a, from
(assume hna : ¬a,
have hab : a → b, from
(assume ha : a, show b, from false.elim (hna ha)),
have ha : a, from habaa hab,
show false, from hna ha),
show a, from hda a nna


#### alini (Nov 12 2022 at 18:50):

Junyan Xu said:

You are close! Just remove fix a b from the beginning and show a at the end:

lemma peirce_of_dn :
double_negation → peirce :=
assume hda : ∀ a, ¬¬a → a,
assume a b,
assume habaa : ((a → b) → a),
have nna : ¬¬a, from
(assume hna : ¬a,
have hab : a → b, from
(assume ha : a, show b, from false.elim (hna ha)),
have ha : a, from habaa hab,
show false, from hna ha),
show a, from hda a nna
`

OH MYY GOD! THANK YOUU!!!

Last updated: Dec 20 2023 at 11:08 UTC