# Re: [isabelle] Quickcheck reports an incorrect counterexample

```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"

```
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

```
```
```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.