Email Gateway (Aug 19 2022 at 16:25): Email Gateway (Aug 19 2022 at 16:25):From: Daniel Raggi <danielraggi@gmail.com>
I'm getting exceptions and having other kinds of problems when using
quickcheck or nitpick inside tactics. I define a tactic that should fail
when quickcheck finds a counterexample and shouldn't do anything otherwise,
as follows:
fun check_counter_tac ctxt thm =
let
val term = concl_of thm
in
case Quickcheck.test_terms ctxt (true, true) [] [(term, [])] of
NONE => Seq.single thm
| _ => Seq.empty
end;
Then I try to run the tactic in a proof, like this:
lemma "0=(1::nat)" apply (tactic "check_counter_tac @{context}")
but I get the following exception:
exception TYPE raised (line 273 of "sign.ML"):
Type error in application: incompatible operand type
Operator: If :: bool => (bool × term list) option => (bool × term list)
option => (bool × term list) option
Operand: TERM _ :: prop
bool => (bool × term list) option => (bool × term list) option => (bool ×
term list) option
prop
If
TERM _
The function Quickcheck.test_terms works fine otherwise, e.g., if I feed it
a term manually, or if I feed it the goal directly inside ML_val{**}.
I'm having the same problem when trying to use nitpick inside a tactic. I
don't get the exception, but it seems that the tactic is feeding the
nitpick function the same dummy term TERM _, and nitpick will never find a
counterexample. It writes:
Nitpicking goal:
TERM _.
and finds nothing.
Does anyone know what this is about?
Thanks,
Daniel
Email Gateway (Aug 19 2022 at 16:27):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Dear Daniel,
Am 20.11.2014 um 19:21 schrieb Daniel Raggi <danielraggi@gmail.com>:
I'm getting exceptions and having other kinds of problems when using
quickcheck or nitpick inside tactics
[...]
.Nitpicking goal:
TERM _.and finds nothing.
Does anyone know what this is about?
From this output, it would appear that the issue has nothing to do with Quickcheck and Nitpick, and everything to do with the string of tactics that were applied before you called those tools and that gave rise to "TERM _" (which I also don't know, but it looks like some dummy placeholder produced by some odd tactic).
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 16:29):From: Daniel Raggi <danielraggi@gmail.com>
Thanks for your reply, Jasmin. As you say, the problem seems to be the
input Quickcheck and Nitpick are receiving and not what they are doing.
However, I'm not applying anything before trying the checkers. Strangely
enough, I got around it using Nitipick, but Quickcheck still fails. And
nitpick doesn't fail but it still behaves strangely, outputting something
that lets me know that it is processing that mysterious dummy term "TERM _"
before processing the real goal.
If we have a tactic "check_tac" that runs Nitpick before doing its thing,
shouldn't we get the same from this:
lemma "0 = (1::nat)"
ML_val{*
val goal = #goal @{Isar.goal}
val ctxt = #context @{Isar.goal}
val t = check_tac ctxt goal
*}
and from this:
lemma "0 = (1::nat)"
apply (tactic "check_tac @{context}")
?
Instead, the first one prints:
Nitpicking goal:
0 = 1.
Nitpick found a counterexample:
Empty assignment
as expected, but the second one prints:
Nitpicking goal:
TERM _.
Nitpick found no counterexample.
Nitpicking goal:
0 = 1.
Nitpick found a counterexample:
Empty assignment
as if it is processing TERM _ before processing the term 0 = 1.
I'm attaching a minimalistic thy file just to showcase this behaviour. I
find it strange.
Daniel
dummyTERM.thy
Email Gateway (Aug 19 2022 at 16:31):From: Makarius <makarius@sketis.net>
This ML snipped looks non-canonical in various ways, so it is no surprise
that it does not work at all.
The "implementation" manual is the main source of information for proper
use of Isabelle/ML, including important naming conventions that direct the
reader/writer in the right direction what things actually mean. Static
types do not necessarily carry a meaning in ML, especially at the bottom
of the LCF kernel.
E.g. a goal state should not be called "thm", but "st"; concl_of a goal
state is its main conclusion, but that is private property of the system
as pointed out in the manual. It is actually very rare that you access the
goal state directly like above: there are combinators to put together
tactics without exposing the state directly.
Here is a more standard way to do it:
ML ‹
fun check_counter_tac ctxt =
SUBGOAL (fn (goal, _) =>
if is_none (Quickcheck.test_terms ctxt (true, true) [] [(goal, [])])
then all_tac else no_tac)
›
lemma "0 = (1::nat)"
apply (tactic ‹check_counter_tac @{context} 1›)
See especially "implementation" manual section 4.2 Tactics, maybe also
section 7.2 Proof methods. All of what is written there is important.
(This thread has nothing to do with quickcheck or nitpick in particular.)
Makarius
http://stop-ttip.org 944,730 people so far
Email Gateway (Aug 19 2022 at 16:31):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Daniel,
On 11/26/2014 05:47 PM, Makarius wrote:
This ML snipped looks non-canonical in various ways, so it is no surprise that it does not work at all.
this is maybe a bit too hash a criticism. A while ago, I had the very same problem in one of my
tactics that had worked without problems with earlier versions of Isabelle, and it took me several
hours of debugging to find the reason for this behaviour.
concl_of a goal state is its main conclusion, but that is private property of the system as pointed out in the manual.
The failure of your tactic is caused by the following changeset:
http://isabelle.in.tum.de/repos/isabelle/rev/31e283f606e2
In order to do "more static checking of proof methods", a proof method is first applied to the
dummy theorem "TERM _" before it gets applied to the actual proof state. The infrastructure
for proof methods expects "proper" tactics to return Seq.empty when applied to such dummy
theorems, rather than failing with an exception.
Greetings,
Stefan
Email Gateway (Aug 19 2022 at 16:31):From: Makarius <makarius@sketis.net>
That changeset is indeed quite important to produce early failure of
tactics that are not done right -- the intention was a different one, but
this is a good additional benefit.
Note that the explanation why the TERM occurs is merely informative --
these things belong to the system internals: they change quite a bit over
the years.
Makarius
http://stop-ttip.org 945,396 people so far
Email Gateway (Aug 19 2022 at 16:32):From: Daniel Raggi <danielraggi@gmail.com>
Thank you very much for your suggestions and references, Makarius and
Stefan. I'm updating my code and things work.
Daniel
Last updated: Apr 18 2024 at 20:16 UTC