[isabelle] finishing a proof

[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.



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]

Hi,

My non-expert view:

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

Try starting your proof with

proof(rule impI)+

Cheers

Mark

On 13 October 2016 at 10:15, Gergely Buday <buday....@uni-eszterhazy.hu>
wrote:

[Lawrence Paulson]

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

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


>"Gergely Buday" <buday....@uni-eszterhazy.hu>:

[Gergely Buday]

Alexander Kogtenkov wrote:

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

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]

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


>"Gergely Buday" <buday....@uni-eszterhazy.hu>:
>