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"

   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
Description: S/MIME Cryptographic Signature



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