[isabelle-dev] [isabelle] Odd failure to match local statement with pending goal.

[Lawrence Paulson]

Many thanks for your analysis. It looks like an interaction involving "fix" and bound variables.

But we need to move the discussion to isabelle-dev at mailbroy.informatik.tu-muenchen.de.

Larry

On 2 Aug 2011, at 22:55, Brian Huffman wrote:

> On Tue, Aug 2, 2011 at 2:10 PM, Bertram Felgenhauer
> <bertram.felgenhauer at googlemail.com> wrote:
>> Hi,
>> 
>>> As Larry stated, this is indeed a strange problem. I tried to find a
>>> minimal example; here is what I came up with:
>>> 
>>> -------------------
>>> lemma
>>>  shows  "⋀c d. d ∈ Z ⟹ x = c ⟹
>>>        ∃e. e ∈ {_. ∃e. e ∈ Z ∧ y = e}"
>>>  apply (unfold mem_Collect_eq)
>>> proof -
>>>  fix s t
>>>  assume "x = s" and "t ∈ Z"
>>>  then show "∃s t. t ∈ Z ∧ y = t"
>>>    sorry
>>> qed
>>> -------------------
>>> The show statement fails with
>> [...]
>> 
>> So do we know whether this is an obscure feature or possibly a bug?
>> (If it's a feature I'd love to hear the underlying story.)
> 
> It certainly looks like a bug to me. I don't have an idea yet of why
> it happens, but I found an even smaller example. I constrained
> everything to type "nat" just to rule out any weirdness with
> polymorphism. Note the repeated bound variable name in the goal (the
> argument to Q is the second "c", which pretty-prints as "ca"). This
> seems to be necessary to make the error happen.
> 
> lemma
>  shows "⋀(a::nat) (b::nat). P a b ⟹ ∀(c::nat) (c::nat). Q c"
> proof -
>  fix s t :: nat assume "P s t"
>  thus "∀(s::nat) (t::nat). Q t" (* Local statement will fail to refine... *)
> 
> Swapping the order of the bound variable names in the conclusion also
> gives the same error:
> 
>  thus "∀(t::nat) (s::nat). Q s"
> 
> Just about any other modification to the lemma or proof that I could
> think of seems to make it work again.
> 
> - Brian
>