# [isabelle] Quickcheck reports an incorrect counterexample

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

```
```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 \<and> 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 \<equiv> 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' \<and> Coinitial N N'
then App (resid M M') (resid N N') else Nil)"
| "resid (App M N) (App' M' N') = (if Coinitial M M' \<and> Coinitial N N'
then subst (resid M M') (resid N N') else Nil)"
| "resid (App' M N) (App' M' N') = (if Coinitial M M' \<and> Coinitial N N'
then subst (resid M M') (resid N N') else Nil)"
| "resid (App' M N) (App M' N') = (if Coinitial M M' \<and> Coinitial N N'
then App' (resid M M') (resid N N') else Nil)"
| "resid _ _ = Nil"

shows "\<And>x. Ide (Var x) \<Longrightarrow> \<forall>X Y. Src X = Var x \<and> Src Y = Var x \<longrightarrow> resid X Y \<noteq> Nil"
(*
proof (prove)
goal (1 subgoal):
1. \<And>x. Ide (Var x) \<Longrightarrow> \<forall>X Y. Src X = Var x \<and> Src Y = Var x \<longrightarrow> resid X Y \<noteq> lambda.Nil
Auto Quickcheck found a counterexample:
x = 0
X = Var 0
Y = Var 1
*)
proof -
fix x
show "\<forall>X Y. Src X = Var x \<and> Src Y = Var x \<longrightarrow> resid X Y \<noteq> 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 \<noteq> Nil"
using X Y
apply (cases X)
apply auto
apply (cases Y)
by auto
qed
qed

end
```

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