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

  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


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