Yiming Xu (Sep 12 2024 at 12:40): Yiming Xu (Sep 12 2024 at 12:40):Firstly, code:
datatype form = VAR "num"
| FALSE
| DISJ "form" "form"
| NOT "form"
| DIAM "form"
fun propform :: "form ⇒ bool"
where
"propform FALSE = True"
| "propform (VAR p) = True"
| "propform (DISJ f1 f2) = (propform f1 ∧ propform f2)"
| "propform (NOT f) = propform f"
| "propform (DIAM f) = False"
definition IMP_def : "IMP f1 f2 = DISJ (NOT f1) f2"
fun peval :: "(num ⇒ bool) ⇒ form ⇒ bool" where
"peval σ (VAR p) = σ p"
| "peval σ (DISJ f1 f2) = (peval σ f1 ∨ peval σ f2)"
| "peval σ FALSE = False"
| "peval σ (NOT f) = (¬ peval σ f)"
| "peval σ (DIAM f) = False"
definition ptaut_def : "ptaut f ⟷ propform f ∧ (∀σ. peval σ f)"
lemma ptaut_MP : "ptaut (IMP f1 f2) ∧ ptaut f1 ⟹ ptaut f2"
proof -
show ?thesis sorry
qed
The formulas are modal formulas. "propform" defines propositional formulas, which are modal formulas without modal operators.
Yiming Xu (Sep 12 2024 at 12:41):"peval" is propositional evaluation, takes an assignment of the truth values of the propositional variables, and returns the truth value of the whole formula.
Yiming Xu (Sep 12 2024 at 12:42):"ptaut" means "propositional tautology".
Yiming Xu (Sep 12 2024 at 12:43):I want to prove the lemma taut_MP, saying if (f1 -> f2) is a propositional tautology and f1 is a propositional tautology, then so is f2. It should follow from the definition of propositional tautology and IMP_def.
Yiming Xu (Sep 12 2024 at 12:43):But I got this error:
Yiming Xu (Sep 12 2024 at 12:44):
Mathias Fleury (Sep 12 2024 at 12:45):The proof is trivial to do (here you are missing the assumption), I think that reading a tutorial like the prog-prove would be very useful (it is available in the documentation panel)
Yiming Xu (Sep 12 2024 at 12:45):It says "Successful attempt to solve goal by exported rule" and said "Failed to finish proof", seems contradictory.
Yiming Xu (Sep 12 2024 at 12:46):Mathias Fleury said:
The proof is trivial to do (here you are missing the assumption), I think that reading a tutorial like the prog-prove would be very useful (it is available in the documentation panel)
I did, sorry maybe I have forgot some important things.
Mathias Fleury (Sep 12 2024 at 12:46):No: one refers to the show (yes the goal is something you want to prove) and the other to the proof (is this going through?)
Mathias Fleury (Sep 12 2024 at 12:48):Yiming Xu said:
Mathias Fleury said:
The proof is trivial to do (here you are missing the assumption), I think that reading a tutorial like the prog-prove would be very useful (it is available in the documentation panel)
I did, sorry maybe I have forgot some important things.
Like reading the Isar chapter?
lemma ptaut_MP :
assumes "ptaut (IMP f1 f2)" and "ptaut f1"
shows "ptaut f2"
proof -
show ?thesis using assms sorry
qed
I now understand thy are not contradictory. Let me quickly try and alternative.
Yiming Xu (Sep 12 2024 at 12:50):Yes, I read the Isar chapter and then forgot the "using" stuff just after several days...
Yiming Xu (Sep 12 2024 at 12:50):lemma ptaut_MP : assumes a : "ptaut (IMP f1 f2) ∧ ptaut f1" shows b: "ptaut f2"
proof -
show ?thesis using a by (simp add: IMP_def ptaut_def)
qed
That works.
Yiming Xu (Sep 12 2024 at 12:51):Thank you for the hint... I admit I read too fast.
Mathias Fleury (Sep 12 2024 at 13:01):Please write it assumes "ptaut (IMP f1 f2)" and "ptaut f1". It makes things easier later
Yiming Xu (Sep 12 2024 at 13:01):Thanks! I will do it now.
Yiming Xu (Sep 12 2024 at 13:44):I think I do not understand the "successful attempt to solve goal by exported rule" message:
image.png
Yiming Xu (Sep 12 2024 at 13:44):If it is solved, why the red underscore?
Mathias Fleury (Sep 12 2024 at 13:45):Try to use "show False"
Mathias Fleury (Sep 12 2024 at 13:47):I do not think that it is possible to fail on the first message (aka writing the correct thing to prove) without failing the section (the tactic work)
Mathias Fleury (Sep 12 2024 at 13:47):Mathias Fleury said:
Try to use "show False"
there you will the see show failing (aka the first message not working)
Yiming Xu (Sep 12 2024 at 13:49):Sorry I am afraid I do not get it. What does "show False" refer to?
Yiming Xu (Sep 12 2024 at 13:50):
Mathias Fleury (Sep 12 2024 at 13:57):You have two messages:
1. the show is correct
2. the proof of the show went through
Mathias Fleury (Sep 12 2024 at 13:58):There are three cases:
- the show is incorrect (like show False)
- the show is correct ("successful attempt to solve goal by exported rule") but the proof does not go through (by highlighted in red) -- this triggered your question
- the show is correct ("successful attempt to solve goal by exported rule") and the proof goes through
Mathias Fleury (Sep 12 2024 at 13:59):And I wanted to make sure that you saw all three cases
Yiming Xu (Sep 12 2024 at 14:00):I (hope I) see. So the error message for show False , in the screenshot above, is because Isabelle knows that False cannot be proved?
Mathias Fleury (Sep 12 2024 at 14:01):It is important to have all three cases, because tactics can take a long time. Otherwise Isabelle needs to wait for the by to finish before continuing procesing
Mathias Fleury (Sep 12 2024 at 14:01):Yiming Xu said:
I (hope I) see. So the error message for show False , in the screenshot above, is because Isabelle knows that False cannot be proved?
No, it knows that this is not what you are trying to prove: you are trying to prove b, so proving False is not allowed
Yiming Xu (Sep 12 2024 at 14:02):Ah I see. It only wants to confirm I am attempting to prove the correct goal.
Yiming Xu (Sep 12 2024 at 14:03):So it then knows once it is proved, the next part of the whole proof will go through.
Yiming Xu (Sep 12 2024 at 14:03):If I am attempting the wrong goal, then maybe even my tactics work for my wrong goal, the rest of the proof cannot work.
Mathias Fleury (Sep 12 2024 at 14:03):It does not wait for the tactic to succeed, so you can have a "by simp" that takes 40minutes and still continue working
Yiming Xu (Sep 12 2024 at 14:04):But if it knows I am attempting on the correct goal, then it does not need have to wait me to prove it, and can safely proceed the rest of proof.
Mathias Fleury (Sep 12 2024 at 14:05):for a simp I never saw this, but having slow fastforce (more than one minute) happens
Yiming Xu (Sep 12 2024 at 14:05):Mathias Fleury said:
for a simp I never saw this, but having slow fastforce (more than one minute) happens
It is impressive that you trust it that it will eventually solve it...
Mathias Fleury (Sep 12 2024 at 14:07):It usually happens that way: you have a fast call. Then one Isabelle update later, it becomes slower. Then one Isabelle update later, it becomes slower again… but you are working on something that depends on that lemma, so the motivation to improve the proof is low
Mathias Fleury (Sep 12 2024 at 14:08):Think of one call in HOL: you have built HOL the first time you needed it. After that you do not care how long each tactic took. You only care that it worked
Yiming Xu (Sep 12 2024 at 14:09):I see. I only have a big metis around 40s. But that one is just because I think "what else can it be", and I was surprised it takes so long.
Yiming Xu (Sep 12 2024 at 14:09):Mathias Fleury said:
Think of one call in HOL: you have built HOL the first time you needed it. After that you do not care how long each tactic took. You only care that it worked
That's true! Makes a lot of sense.
Last updated: Dec 21 2024 at 16:20 UTC