# Zulip Chat Archive

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

You could start with

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

You could start with

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

and your task is just to fill in the underscore.

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