Chengsong Tan (Oct 16 2023 at 22:39): Chengsong Tan (Oct 16 2023 at 22:39):Hi all,
What does it mean for Vampire to say "problem is unprovable" after calling Sledgehammer on a goal?
If this means the lemma is counter-satsifiable, then how do I get a counterexample from there?
I tried nitpick and quickcheck with no luck.
(line 1593)
Transposed.thy
Thanks,
Chengsong
Mathias Fleury (Oct 17 2023 at 04:46):I don't have that message, but do not read anything into it. Just read it as a failure to find a proof
Mathias Fleury (Oct 17 2023 at 04:47):In general it is extremely hard from a Sledghammer to conclude about satisfiability, because you would have to check which facts have been translated
Mathias Fleury (Oct 17 2023 at 04:48):BTW in your goal, the fact that you unfold stuff by hand but not SWR that you just defined… you should start with SWR because you have no facts on it
Mathias Fleury (Oct 17 2023 at 04:56):And a final remark, this kind of stuff, you have to write by hand:
lemma [simp]: ‹Owner (CLEntry.block_state (devcache1 (T [a sHost= b]))) =
Owner (CLEntry.block_state (devcache1 T))›
‹Owner (CLEntry.block_state (devcache1 (T ++cl))) =
Owner (CLEntry.block_state (devcache1 T))›
‹Owner (CLEntry.block_state (devcache1 (T [ q -=req] ))) =
Owner (CLEntry.block_state (devcache1 T))›
‹Owner (CLEntry.block_state (devcache2 (T [a sHost= b]))) =
Owner (CLEntry.block_state (devcache2 T))›
‹Owner (CLEntry.block_state (devcache2 (T [ q -=req] ))) =
Owner (CLEntry.block_state (devcache2 T))›
‹Owner (CLEntry.block_state (devcache2 (T [ q' +=reqresp t k l] ))) =
Owner (CLEntry.block_state (devcache2 T))›
‹Owner (CLEntry.block_state (devcache2 (T ++cl))) =
Owner (CLEntry.block_state (devcache2 T))›
‹Owner (CLEntry.block_state (devcache1 (T [ q' +=reqresp t k l] ))) =
Owner (CLEntry.block_state (devcache1 T))›
by (auto simp: change_host_state_def update_clock_def consumeReq_def host_sends_response_def Let_def)
You don't want sledgehammer to inline the proof each time. You want this to be applied by auto
Chengsong Tan (Oct 17 2023 at 11:34):Mathias Fleury said:
BTW in your goal, the fact that you unfold stuff by hand but not SWR that you just defined… you should start with SWR because you have no facts on it
Hi Mathias,
By "you should start with SW[M]R" do you mean adding these definitions to the [simp] set? Or is it more like writing facts like the snippet you showed?
Chengsong Tan (Oct 17 2023 at 11:35):Mathias Fleury said:
And a final remark, this kind of stuff, you have to write by hand:
lemma [simp]: ‹Owner (CLEntry.block_state (devcache1 (T [a sHost= b]))) = Owner (CLEntry.block_state (devcache1 T))› ‹Owner (CLEntry.block_state (devcache1 (T ++cl))) = Owner (CLEntry.block_state (devcache1 T))› ‹Owner (CLEntry.block_state (devcache1 (T [ q -=req] ))) = Owner (CLEntry.block_state (devcache1 T))› ‹Owner (CLEntry.block_state (devcache2 (T [a sHost= b]))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache2 (T [ q -=req] ))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache2 (T [ q' +=reqresp t k l] ))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache2 (T ++cl))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache1 (T [ q' +=reqresp t k l] ))) = Owner (CLEntry.block_state (devcache1 T))› by (auto simp: change_host_state_def update_clock_def consumeReq_def host_sends_response_def Let_def)
Thanks a lot! This cartouche style I have. never seen before :)
Mathias Fleury (Oct 17 2023 at 13:47):Chengsong Tan said:
Mathias Fleury said:
BTW in your goal, the fact that you unfold stuff by hand but not SWR that you just defined… you should start with SWR because you have no facts on it
Hi Mathias,
By "you should start with SW[M]R" do you mean adding these definitions to the [simp] set? Or is it more like writing facts like the snippet you showed?
Currently your code look like:
definition SWR where ...
lemma "... SWR ..."
at this point you know nothing on SWR except for the definition. Hence you have to unfold the definition (you know nothing else!)
Mathias Fleury (Oct 17 2023 at 13:49):Typically, you have:
definition SWR where ...
lemma SWR_simp1[simp]: "..."
unfolding SWR_def by auto
lemma SWR_simp2[simp]: "..."
unfolding SWR_def by auto
lemma SWR_simp3[simp]: "..."
unfolding SWR_def by auto
lemma "... SWR ..."
Here the situation is different: in the last lemma, you actually already know things about SWR
Mathias Fleury (Oct 17 2023 at 13:51):Chengsong Tan said:
Mathias Fleury said:
And a final remark, this kind of stuff, you have to write by hand:
lemma [simp]: ‹Owner (CLEntry.block_state (devcache1 (T [a sHost= b]))) = Owner (CLEntry.block_state (devcache1 T))› ‹Owner (CLEntry.block_state (devcache1 (T ++cl))) = Owner (CLEntry.block_state (devcache1 T))› ‹Owner (CLEntry.block_state (devcache1 (T [ q -=req] ))) = Owner (CLEntry.block_state (devcache1 T))› ‹Owner (CLEntry.block_state (devcache2 (T [a sHost= b]))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache2 (T [ q -=req] ))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache2 (T [ q' +=reqresp t k l] ))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache2 (T ++cl))) = Owner (CLEntry.block_state (devcache2 T))› ‹Owner (CLEntry.block_state (devcache1 (T [ q' +=reqresp t k l] ))) = Owner (CLEntry.block_state (devcache1 T))› by (auto simp: change_host_state_def update_clock_def consumeReq_def host_sends_response_def Let_def)
Thanks a lot! This cartouche style I have. never seen before :)
I like cartouche (I find them less intrusive) and Makarius is actually pushing towards them and there are cases where you have to use them. But: this is currently only a choice.
Mathias Fleury (Oct 17 2023 at 13:52):Chengsong Tan said:
Mathias Fleury said:
BTW in your goal, the fact that you unfold stuff by hand but not SWR that you just defined… you should start with SWR because you have no facts on it
Hi Mathias,
By "you should start with SW[M]R" do you mean adding these definitions to the [simp] set? Or is it more like writing facts like the snippet you showed?
My impression is that you want to work with SWR most of the time (and not go deeper). Hence the simp rules will already take care of some simplifications. But I might be wrong… I did not bother reading the formalization :)
Last updated: May 01 2024 at 20:18 UTC