Email Gateway (Aug 22 2022 at 14:15): 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?
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
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
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
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):
which I guess should be trivial to solve but it resisted any attempt.
What is wrong here?
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: Nov 21 2024 at 12:39 UTC