*To*: Isabelle-Users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Quickcheck reports an incorrect counterexample*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Sun, 11 Apr 2021 09:55:56 -0400*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0

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

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" lemma BAD: 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

**Follow-Ups**:**Re: [isabelle] Quickcheck reports an incorrect counterexample***From:*Tobias Nipkow

- Previous by Date: [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice
- Next by Date: Re: [isabelle] Issues with locale interpretation
- Previous by Thread: [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice
- 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