Discussion:
[isabelle] finishing a proof
Gergely Buday
2016-10-13 09:20:13 UTC
Hi,

I would like to write a forward proof in Isar to have

P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)

by hand it can be done through two implication eliminations using P and Q as assumptions, and then re-introducing implications but in the reverse order.

I wrote the following to formalise this:

theory Logic

imports Main

begin

lemma "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)"

proof -

assume premise : "P ⟶ (Q ⟶ R)"

assume p: "P"

have qr: "Q ⟶ R" by (simp add: p premise)

assume q: "Q"

have r: "R" by (simp add: q qr)

from this have "P ⟶ R" by (simp add: p)

from this have "Q ⟶ (P ⟶ R)" by (simp add: q)

thus "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)" by assumption

Failed to refine any pending goal

Local statement fails to refine any pending goal

Failed attempt to solve goal by exported rule:

(P ⟶ Q ⟶ R) ⟹ (P) ⟹ (Q) ⟹ (P ⟶ Q ⟶ R) ⟹ Q ⟶ P ⟶ R

It fails at the last line, it is not really clear why. Can you give a clue?

- Gergely
Mark Wassell
2016-10-13 10:25:10 UTC
Hi,

My non-expert view:

You have made too many assumptions - namely your assumptions p and q.

proof(rule impI)+

Cheers

Mark
Post by Gergely Buday
Hi,
I would like to write a forward proof in Isar to have
P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)
by hand it can be done through two implication eliminations using P and Q
as assumptions, and then re-introducing implications but in the reverse
order.
theory Logic
imports Main
begin
lemma "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)"
proof -
assume premise : "P ⟶ (Q ⟶ R)"
assume p: "P"
have qr: "Q ⟶ R" by (simp add: p premise)
assume q: "Q"
have r: "R" by (simp add: q qr)
from this have "P ⟶ R" by (simp add: p)
from this have "Q ⟶ (P ⟶ R)" by (simp add: q)
thus "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)" by assumption
Failed to refine any pending goal
Local statement fails to refine any pending goal
(P ⟶ Q ⟶ R) ⟹ (P) ⟹ (Q) ⟹ (P ⟶ Q ⟶ R) ⟹ Q ⟶ P ⟶ R
It fails at the last line, it is not really clear why. Can you give a clue?
- Gergely
Lawrence Paulson
2016-10-13 10:55:09 UTC
If you look at the State with the cursor after the proof keyword, you will see displayed what you are allowed to assume, which variables you must fix, and which conclusion you must show. Here you may assume "P ⟶ (Q ⟶ R)” and must show "Q ⟶ (P ⟶ R)”; to do that in single steps requires a nested proof. Or else do it as Mark suggested.

Larry
Post by Gergely Buday
Hi,
I would like to write a forward proof in Isar to have
P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)
by hand it can be done through two implication eliminations using P and Q as assumptions, and then re-introducing implications but in the reverse order.
theory Logic
imports Main
begin
lemma "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)"
proof -
assume premise : "P ⟶ (Q ⟶ R)"
assume p: "P"
have qr: "Q ⟶ R" by (simp add: p premise)
assume q: "Q"
have r: "R" by (simp add: q qr)
from this have "P ⟶ R" by (simp add: p)
from this have "Q ⟶ (P ⟶ R)" by (simp add: q)
thus "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)" by assumption
Failed to refine any pending goal
Local statement fails to refine any pending goal
(P ⟶ Q ⟶ R) ⟹ (P) ⟹ (Q) ⟹ (P ⟶ Q ⟶ R) ⟹ Q ⟶ P ⟶ R
It fails at the last line, it is not really clear why. Can you give a clue?
- Gergely
Alexander Kogtenkov via Cl-isabelle-users
2016-10-13 11:47:35 UTC
"assume" is used to state what is used as a premise of a goal, and neither P nor Q are given, that's why the proof fails. So, instead of proving a fact relying on "assume" you can prove a fact relying on "if we assume...":

proof -
assume "P ⟶ (Q ⟶ R)"
then have "Q ⟶ R" if p: P by (simp add: p)
then have "R"       if p: P and q: Q by (simp add: p q)
then have "P ⟶ R" if q: Q by (simp add: q)
then have "Q ⟶ (P ⟶ R)" by simp
then show ?thesis by assumption
qed

Given that "simp" is too powerful and could be used to prove the original lemma right away, you can also use explicit rules:

proof -
assume "P ⟶ (Q ⟶ R)"
then have "Q ⟶ R"         if p: P using p by (rule mp)
then have "R"               if p: P and q: Q using q by (rule mp) (insert p)
then have "P ⟶ R"         if q: Q by (rule impI) (insert q)
then show "Q ⟶ (P ⟶ R)" by (rule impI)
qed

Alexander Kogtenkov
Post by Gergely Buday
Hi,

I would like to write a forward proof in Isar to have

P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)

by hand it can be done through two implication eliminations using P and Q as assumptions, and then re-introducing implications but in the reverse order.

theory Logic
imports Main
begin

lemma "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)"
proof -
assume premise : "P ⟶ (Q ⟶ R)"
assume p: "P"
have qr: "Q ⟶ R" by (simp add: p premise)
assume q: "Q"
have r: "R" by (simp add: q qr)
from this have "P ⟶ R" by (simp add: p)
from this have "Q ⟶ (P ⟶ R)" by (simp add: q)
thus "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)" by assumption

Failed to refine any pending goal
Local statement fails to refine any pending goal
(P ⟶ Q ⟶ R) ⟹ (P) ⟹ (Q) ⟹ (P ⟶ Q ⟶ R) ⟹ Q ⟶ P ⟶ R

It fails at the last line, it is not really clear why. Can you give a clue?

- Gergely
Gergely Buday
2016-10-13 12:56:21 UTC
Post by Alexander Kogtenkov via Cl-isabelle-users
"assume" is used to state what is used as a premise of a goal, and neither P
nor Q are given, that's why the proof fails. So, instead of proving a fact relying
proof -
assume "P ⟶ (Q ⟶ R)"
then have "Q ⟶ R" if p: P by (simp add: p)
then have "R" if p: P and q: Q by (simp add: p q)
then have "P ⟶ R" if q: Q by (simp add: q)
then have "Q ⟶ (P ⟶ R)" by simp
then show ?thesis by assumption
qed
Given that "simp" is too powerful and could be used to prove the original
proof -
assume "P ⟶ (Q ⟶ R)"
then have "Q ⟶ R" if p: P using p by (rule mp)
then have "R" if p: P and q: Q using q by (rule mp) (insert p)
then have "P ⟶ R" if q: Q by (rule impI) (insert q)
then show "Q ⟶ (P ⟶ R)" by (rule impI) qed
Thanks.

A question:

if I write

lemma assumes pqr: "P ⟶ (Q ⟶ R)" shows "Q ⟶ (P ⟶ R)"
proof -
assume "P ⟶ Q ⟶ R"
then have "Q ⟶ R" if p: P using p by (rule mp)
then have "R" if p: P and q: Q using q by (rule mp) (insert p)
then have "P ⟶ R" if q: Q by (rule impI) (insert q)
then have "Q ⟶ (P ⟶ R)" by (rule impI)

I have

have Q ⟶ P ⟶ R
proof (state)
this:
Q ⟶ P ⟶ R

goal (1 subgoal):
1. Q ⟶ P ⟶ R

which I guess should be trivial to solve but it resisted any attempt.

What is wrong here?

- Gergely
Alexander Kogtenkov via Cl-isabelle-users
2016-10-13 17:03:16 UTC
The form "assumes-shows" separates facts, so if in the proof you want to rely on the facts from "assumes", you need to tell it by adding

using assms proof -

Then your version completes without an issue. (You can also use "pqr" instead of a general "assms" to refer to the particular fact.)

Another variant is to replace "assume" with the fact itself. In this case "using assms" is not required:

proof -
note pqr
...

Finally, you can just use "pqr" in the proof itself. Then neither "assume" nor "note" is required:

lemma assumes pqr: "P ⟶ (Q ⟶ R)" shows "Q ⟶ (P ⟶ R)"
proof -
have "Q ⟶ R" if p: P using pqr p by (rule mp)
then have "R" if p: P and q: Q using q by (rule mp) (insert p pqr)
then have "P ⟶ R" if q: Q by (rule impI) (insert q pqr)
then show "Q ⟶ (P ⟶ R)" by (rule impI) (insert pqr)
qed

Alexander Kogtenkov
Post by Gergely Buday
Post by Alexander Kogtenkov via Cl-isabelle-users
"assume" is used to state what is used as a premise of a goal, and neither P
nor Q are given, that's why the proof fails. So, instead of proving a fact relying
proof -
assume "P ⟶ (Q ⟶ R)"
then have "Q ⟶ R" if p: P by (simp add: p)
then have "R" if p: P and q: Q by (simp add: p q)
then have "P ⟶ R" if q: Q by (simp add: q)
then have "Q ⟶ (P ⟶ R)" by simp
then show ?thesis by assumption
qed
Given that "simp" is too powerful and could be used to prove the original
proof -
assume "P ⟶ (Q ⟶ R)"
then have "Q ⟶ R" if p: P using p by (rule mp)
then have "R" if p: P and q: Q using q by (rule mp) (insert p)
then have "P ⟶ R" if q: Q by (rule impI) (insert q)
then show "Q ⟶ (P ⟶ R)" by (rule impI) qed
Thanks.
if I write
lemma assumes pqr: "P ⟶ (Q ⟶ R)" shows "Q ⟶ (P ⟶ R)"
proof -
assume "P ⟶ Q ⟶ R"
then have "Q ⟶ R" if p: P using p by (rule mp)
then have "R" if p: P and q: Q using q by (rule mp) (insert p)
then have "P ⟶ R" if q: Q by (rule impI) (insert q)
then have "Q ⟶ (P ⟶ R)" by (rule impI)
I have
have Q ⟶ P ⟶ R
proof (state)
Q ⟶ P ⟶ R
1. Q ⟶ P ⟶ R
which I guess should be trivial to solve but it resisted any attempt.
What is wrong here?
- Gergely