Re: [isabelle] Odd failure to match local statement with pending goal.



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





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