[isabelle] Quickcheck reports an incorrect counterexample · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quickcheck reports an incorrect counterexample

Email Gateway (Apr 11 2021 at 13:56):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
For lemma BAD below (theory also attached), Quickcheck reports an incorrect counterexample.
X = Var 0 and Y = Var 1 are not consistent with the hypothesis Src X = Var x ∧ Src Y = Var x.

A checked proof of the supposedly incorrect lemma is given.

- Gene Stark

theory Barf
imports Main
begin

datatype lambda =
Nil
| Var nat
| Lam lambda
| App lambda lambda
| App' lambda lambda

fun Ide
where "Ide Nil = False"
| "Ide (Var i) = True"
| "Ide (Lam M) = Ide M"
| "Ide (App X Y) = (Ide X ∧ Ide Y)"
| "Ide (App' X Y) = False"

fun raise
where "raise Nil = Nil"
| "raise (Var i) = Var (Suc i)"
| "raise (Lam M) = Lam (raise M)"
| "raise (App M N) = App (raise M) (raise N)"
| "raise (App' M N) = App' (raise M) (raise N)"

fun Src
where "Src Nil = Nil"
| "Src (Var i) = Var i"
| "Src (Lam M) = Lam (Src M)"
| "Src (App M N) = App (Src M) (Src N)"
| "Src (App' M N) = App (Src M) (Src N)"

abbreviation Coinitial
where "Coinitial X Y ≡ Src X = Src Y"

fun resid
where "resid (Var i) (Var i') = (if i = i' then Var i else Nil)"
| "resid (Lam M) (Lam M') = (if Coinitial M M' then Nil else Lam (resid M M'))"
| "resid (App M N) (App M' N') = (if Coinitial M M' ∧ Coinitial N N'
then App (resid M M') (resid N N') else Nil)"
| "resid (App M N) (App' M' N') = (if Coinitial M M' ∧ Coinitial N N'
then subst (resid M M') (resid N N') else Nil)"
| "resid (App' M N) (App' M' N') = (if Coinitial M M' ∧ Coinitial N N'
then subst (resid M M') (resid N N') else Nil)"
| "resid (App' M N) (App M' N') = (if Coinitial M M' ∧ Coinitial N N'
then App' (resid M M') (resid N N') else Nil)"
| "resid _ _ = Nil"

lemma BAD:
shows "⋀x. Ide (Var x) ⟹ ∀X Y. Src X = Var x ∧ Src Y = Var x ⟶ resid X Y ≠ Nil"
(*
proof (prove)
goal (1 subgoal):

1. ⋀x. Ide (Var x) ⟹ ∀X Y. Src X = Var x ∧ Src Y = Var x ⟶ resid X Y ≠ lambda.Nil
Auto Quickcheck found a counterexample:
x = 0
X = Var 0
Y = Var 1
*)
proof -
fix x
show "∀X Y. Src X = Var x ∧ Src Y = Var x ⟶ resid X Y ≠ Nil"
proof (intro allI impI, elim conjE)
fix X Y
assume X: "Src X = Var x" and Y: "Src Y = Var x"
show "resid X Y ≠ Nil"
using X Y
apply (cases X)
apply auto
apply (cases Y)
by auto
qed
qed

end
Barf.thy

Email Gateway (Apr 12 2021 at 09:15):

From: Tobias Nipkow <nipkow@in.tum.de>
Eugene,

Thanks for this curious example. It looks like there is a bug in the treatment
of (outermost) universal quantifiers as opposed to free variables. When you
remove the !!x, the problem goes away. It seems nobody ever noticed because most
of the time one drops these outermost universals.

Tobias

On 11/04/2021 15:55, Eugene W. Stark wrote:

For lemma BAD below (theory also attached), Quickcheck reports an incorrect counterexample.
X = Var 0 and Y = Var 1 are not consistent with the hypothesis Src X = Var x ∧ Src Y = Var x.

A checked proof of the supposedly incorrect lemma is given.

- Gene Stark

theory Barf
imports Main
begin

datatype lambda =
Nil
| Var nat
| Lam lambda
| App lambda lambda
| App' lambda lambda

fun Ide
where "Ide Nil = False"
| "Ide (Var i) = True"
| "Ide (Lam M) = Ide M"
| "Ide (App X Y) = (Ide X ∧ Ide Y)"
| "Ide (App' X Y) = False"

fun raise
where "raise Nil = Nil"
| "raise (Var i) = Var (Suc i)"
| "raise (Lam M) = Lam (raise M)"
| "raise (App M N) = App (raise M) (raise N)"
| "raise (App' M N) = App' (raise M) (raise N)"

fun subst
where "subst X Nil = Nil"
| "subst X (Var 0) = X"
| "subst X (Var i) = Var i"
| "subst X (Lam M) = Lam (subst (raise X) M)"
| "subst X (App M N) = App (subst X M) (subst X N)"
| "subst X (App' M N) = App' (subst X M) (subst X N)"

fun Src
where "Src Nil = Nil"
| "Src (Var i) = Var i"
| "Src (Lam M) = Lam (Src M)"
| "Src (App M N) = App (Src M) (Src N)"
| "Src (App' M N) = App (Src M) (Src N)"

abbreviation Coinitial
where "Coinitial X Y ≡ Src X = Src Y"

fun resid
where "resid (Var i) (Var i') = (if i = i' then Var i else Nil)"
| "resid (Lam M) (Lam M') = (if Coinitial M M' then Nil else Lam (resid M M'))"
| "resid (App M N) (App M' N') = (if Coinitial M M' ∧ Coinitial N N'
then App (resid M M') (resid N
N') else Nil)"
| "resid (App M N) (App' M' N') = (if Coinitial M M' ∧
Coinitial N N'
then subst (resid M M') (resid N N') else Nil)"
| "resid (App' M N) (App' M' N') = (if Coinitial M M' ∧
Coinitial N N'
then subst (resid M M') (resid N N') else Nil)"
| "resid (App' M N) (App M' N') = (if Coinitial M M' ∧
Coinitial N N'
then App' (resid M M') (resid
N N') else Nil)"
| "resid _ _ = Nil"

lemma BAD:
shows "⋀x. Ide (Var x) ⟹ ∀X Y. Src X = Var
x ∧ Src Y = Var x ⟶ resid X Y ≠ Nil"
(*
proof (prove)
goal (1 subgoal):
1. ⋀x. Ide (Var x) ⟹ ∀X Y. Src X = Var
x ∧ Src Y = Var x ⟶ resid X Y ≠ lambda.Nil
Auto Quickcheck found a counterexample:
x = 0
X = Var 0
Y = Var 1
*)
proof -
fix x
show "∀X Y. Src X = Var x ∧ Src Y = Var x ⟶ resid X Y ≠ Nil"
proof (intro allI impI, elim conjE)
fix X Y
assume X: "Src X = Var x" and Y: "Src Y = Var x"
show "resid X Y ≠ Nil"
using X Y
apply (cases X)
apply auto
apply (cases Y)
by auto
qed
qed

end

smime.p7s

Email Gateway (Apr 16 2021 at 05:28):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

this is due to an erroneous handling of variable names in the quickcheck
framework, which will disappear in the next Isabelle release.

Cheers,
Florian
OpenPGP_signature

Last updated: Apr 20 2024 at 04:19 UTC