*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Quickcheck reports an incorrect counterexample*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 12 Apr 2021 11:15:25 +0200*In-reply-to*: <a8931d75-f465-63e6-0255-fbd330df1a6b@starkeffect.com>*References*: <a8931d75-f465-63e6-0255-fbd330df1a6b@starkeffect.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:78.0) Gecko/20100101 Thunderbird/78.9.1

Eugene,

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Quickcheck reports an incorrect counterexample***From:*Florian Haftmann

**References**:**[isabelle] Quickcheck reports an incorrect counterexample***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] Issues with locale interpretation
- Next by Date: [isabelle] Datatype definition can be slow
- Previous by Thread: [isabelle] Quickcheck reports an incorrect counterexample
- Next by Thread: Re: [isabelle] Quickcheck reports an incorrect counterexample
- Cl-isabelle-users April 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list