Re: [isabelle] Quickcheck reports an incorrect counterexample



Hi all,

this is due to an erroneous handling of variable names in the quickcheck
framework, which will disappear in the next Isabelle release.

See also https://isabelle.in.tum.de/repos/isabelle/rev/ed5226fdf89d

Cheers,
	Florian

Am 12.04.21 um 11:15 schrieb Tobias Nipkow:
> 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: OpenPGP_signature
Description: OpenPGP digital signature



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