forward proof

Stream: new members

[lini]

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

[lini]

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]

∀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]

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

[Eric Wieser]

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

[Arthur Paulino]

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]

ooooh thank you let me try it again

[lini]

∀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]

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

[Junyan Xu]

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]

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]

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]

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]

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]

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

[Junyan Xu]

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]

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

[lini]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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