From: Sander van Rijnswou <svanrijnswou@gmail.com>

Hi,

I ran into a case where Nitpick finds a counterexample to a true lemma. The

proof checks out, so apparently I can't use Nitpick in this situation? I

don't understand why though. This was posted earlier on Zulip, but it was

suggested to repost here.

Thanks for your comments,

lemma

fixes a b:: int

assumes "b≠0"

shows "rat_of_int a * (Fract 1 b) = (Fract a b)"

(* nitpick finds a counterexample; sometimes a=0, b=3 sometimes a=2,

b=2*)

nitpick

(* sledgehammer finds a proof *)

by (metis Fract_of_int_eq mult.commute mult.left_neutral mult_rat)

The thy file is attached.

question.thy

From: Stepan Holub <holub@karlin.mff.cuni.cz>

Hi,

in order to understand what is happening in Nitpick you can add

parameters (see the User's Guide in the Isabelle documentation).

In your example, putting

nitpick[show_all, eval = "rat_of_int a * Fract 1 b" "Fract a b" "λ x

y. Fract x y"]

I obtain

Nitpick found a counterexample:

Free variables:

a = 2

b = 2

Evaluated terms:

rat_of_int a * Fract 1 b = 1

Fract a b = _
Fract =

(λx. _)

(- 1 := (λx. _)(0 := 0), 0 := (λx. _)(0 := 0, 1 := 0),

1 := (λx. _)(0 := 0, 1 := 1, 2 := 1 div 2), 2 := (λx. _)(0 := 0,

1 := 2))

Types:

nat = {0, 1, 2, 3, …}

int = {- 1, 0, 1, 2, …}

rat = {0, 1 / 2, 1, 2, …}

You can see here that Nitpick approximates infinite types with a small

model, where ... represents a single additional element.

From the output you see how Fract is defined in this model. While

Fract 1 2 = 1 div 2, Fract 2 2 is undefined. Whence the fake

counterexample.

Best

Stepan

Last updated: Dec 08 2021 at 09:20 UTC