Hi Tobias,
> lemma "k dvd n ~ k dvd (n+1::nat)"
> nitpick
>
> "works" but does not find a counterexample.
I tried it here and got a "potential" counterexample with k = 0 and n
= 0 (assuming "~" is "==>" in your formula). Is that what you got?
The root of the problem is the existential quantifier in the dvd
definition. Much of the loss of precision in Nitpick (and the
unsoundness in Refute) comes from such existential quantifiers, which
occur in definitions like dvd but also in inductive predicates. I
suspect we ran in exactly the same problem in POPLmark (+ the fact
that nat_case wasn't specialized properly).
I guess the following TODOs are in order:
1. Document such limitations better in the manual.
2. Handle more special cases where I can guess that the existentially-
bound variable must be representable ("EX k. a = b * k" is such an
example; if a and b are representable, then so is any k that satisfies
a = b * k, for nat).
3. Later, maybe: Find more general/powerful principles to improve the
precision (e.g., rethink the whole three-valued logic), based on our
experiences with the current approach.
Jasmin
