Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] finishing a proof


view this post on Zulip Email Gateway (Aug 22 2022 at 14:15):

From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
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?

view this post on Zulip Email Gateway (Aug 22 2022 at 14:15):

From: Mark Wassell <mpwassell@gmail.com>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:15):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:15):

From: Alexander Kogtenkov via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
"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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:15):

From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Alexander Kogtenkov wrote:

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?

view this post on Zulip Email Gateway (Aug 22 2022 at 14:16):

From: Alexander Kogtenkov via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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


Last updated: Apr 20 2024 at 04:19 UTC