Email Gateway (Feb 26 2021 at 10:36): Email Gateway (Feb 26 2021 at 10:36):From: "Stüber, Sebastian" <stueber@se-rwth.de>
Dear all,
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
An Example:
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! *)
oops
(* Allowing different messages, now nitpick can find something *)
lemma "LCons (a::nat) (LCons b LNil) ≠ z"
nitpick[expect=genuine] (* is working *)
oops
With the normal (finite) list datatype, this problem does not occur.
Does anybody know the cause & how to fix it?
Sincerely,
Sebastian Stüber
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
nitpick_test.thy
Email Gateway (Jul 14 2021 at 12:34):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Sebastian,
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.)
Cheers,
Jasmin
Last updated: Jan 04 2025 at 20:18 UTC