Email Gateway (Aug 18 2022 at 20:31): Email Gateway (Aug 18 2022 at 20:31):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
So if you have something inconsistent, you get to experience both the
cheap thrills of sledgehammer, and the dashing of your naive dreams with
refute. Still, automation is great. You want your naivety demolished as
soon as possible.
Refute is finding a model. I simplified everything down to a theorem
which states a simple axiom as an exists instead of a forall, and refute
finds a model, although metis proves the theorem. I don't know how to
interpret the results of refute. Here's the theory.
typedecl sT
axiomatization
empty_set::sT and
inS::"sT => sT => bool" (infixl "∈⇣σ" 55)
where
empty_ax:"!(x::sT). ~(x ∈⇣σ empty_set)"
theorem --"refute finds a model"
"~(?(x::sT). x ∈⇣σ empty_set)"
nitpick
refute
oops
theorem --"metis proves it."
"~(?(x::sT). x ∈⇣σ empty_set)"
by (metis empty_ax)
Refute returns this message:
Model found:
Size of types: ?'b: 1, sT: 1
empty_set: sTs_1ax.sT0
op ∈⇣σ: {(sTs_1ax.sT0, {(sTs_1ax.sT0, True)})}
Can anyone tell me how to interpret the refute message? Is there
documentation on the web that tells me how to read the output of an SAT
solver?
Actually, it looks like it might be saying that the empty_set is an
element of the empty_set.
I could try to come up with a fix based on that hunch, but I spent 3 or
4 hours before I figured out to simplified the theory to the bare bones.
It would be nice to know for sure, and if anyone wants to tell me how to
fix the problem, that would be okay.
Attached is the complete theory.
Regards,
GB
sTs_1ax.thy
Email Gateway (Aug 18 2022 at 20:31):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Gottfried,
Refute is finding a model. I simplified everything down to a theorem which states a simple axiom as an exists instead of a forall, and refute finds a model, although metis proves the theorem. I don't know how to interpret the results of refute. Here's the theory.
Refute is unsound in the presence of axioms, because it will fail to pick these up. For cases like these, you have to use Nitpick.
As a general rule, Nitpick subsumes Refute and there is no reason to use the latter. Refute is provided for historical reasons and might disappear in a future release.
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 20:31):From: Tjark Weber <webertj@in.tum.de>
refute simply disregards user-supplied axioms (other than type and
constant definitions). See Section 3.4 (page 52) of
http://user.it.uu.se/~tjawe125/publications/weber08satbased.html
for a brief discussion. As you noticed, this may well lead to spurious
(counter-)models in the presence of such axioms.
I suggest that you use nitpick instead, which -- for all practical
intents and purposes -- is a worthy successor to refute.
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 20:31):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Jasmin, thanks for the info. I'm happy to simplify my life where possible.
How about quickcheck? Is that something I should forget? I do this:
theorem --"refute finds a model"
"!(x::sT). ~(x ∈⇣σ empty_set)"
quickcheck
And it gives me this:
Quickchecking...
No active testers for quickcheck
The examples I saw in the list archives didn't give quickcheck any
options, though I tried this, after looking at isar-ref.pdf:
quickcheck [exhaustive]
Thanks,
GB
Email Gateway (Aug 18 2022 at 20:32):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Tjark,
I like worthy successors.
I had a look at the section you referenced. Thanks.
Regards,
GB
Email Gateway (Aug 18 2022 at 20:32):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
If you use "axiomatization", yes. Quickcheck requires executable definitions / code equations.
Jasmin
Last updated: Apr 20 2024 at 08:16 UTC