Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nitpick finds counterexample to proven lemma


view this post on Zulip Email Gateway (Mar 03 2021 at 10:01):

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

view this post on Zulip Email Gateway (Mar 06 2021 at 09:03):

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