From: "Stüber, Sebastian" <email@example.com>
I am trying to use nitpick to find counterexample over (potentially) infinite lists. While playing with nitpick I encountered a strange behavior:
Nitpick seems to be unable to find counterexamples, if a message occurs twice in the list
codatatype 'a::type llist = LNil | LCons 'a "'a llist"
(* Notice that "a" occurs twice *)
lemma "LCons (a::nat) (LCons a LNil) ≠ z"
nitpick[expect=none] (* Should find something! *)
(* Allowing different messages, now nitpick can find something *)
lemma "LCons (a::nat) (LCons b LNil) ≠ z"
nitpick[expect=genuine] (* is working *)
With the normal (finite) list datatype, this problem does not occur.
Does anybody know the cause & how to fix it?
Sebastian Stüber, M.Sc.RWTH | Software Engineering
Lehrstuhl für Software Engineering | RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany | https://www.se-rwth.de
Phone ++49 241 80-21352
From: Jasmin Blanchette via Cl-isabelle-users <firstname.lastname@example.org>
Sorry for the delay in answering. Investigating Nitpick failures is tricky, especially that I developed the tool over 10 years ago.
I wasn't quite able to put my finger on the deep problem -- perhaps simply an issue in the translation from HOL terms to first-order relational logic (Kodkod's logic), which is optimized and hence quite subtle. However, while investigating the issue, I rephrased one of the codatatype constraints, hoping this would make the problem go away, and it did (at least with the "box" option on). This is not entirely satisfactory, but my middle-term goal is to replace Nitpick with the experimental Nunchaku, so I don't want to spend too much time on Nitpick.
If you wonder, the issue seems to be that the (lazy) lists [a] and [a, a] are considered bisimilar even if they are not. The bisimilarity check has a depth (bisim_depth), and indeed with bisim_depth = 1 we'd expect [a] and [a, a] to be identical. But here we're working with bisim_depth = 2, and hence they're different and thus it should be possible to construct a model that contains both. (The list [a] is needed to build [a, a], so it's unavoidable in a model.)
Last updated: Dec 05 2021 at 23:19 UTC