[isabelle-dev] Nitpick counterexample generator now available

[Jasmin Blanchette]

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