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

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 25 2022 at 01:11 UTC