Re: [isabelle] Why does "also" fail in this proof?



On Mon, 8 May 2006 14:13:48 +0200 (CEST)
Makarius <makarius at sketis.net> wrote:
> > Can someone explain why, in the attached theory file, I get this
> > error on the last line:
> 
> Because the calculational step does not make any progress -- your
> first step is reflexivity.

OK, with this hint I managed to fix that proof - thanks.

However, I would disagree that it does not make any progress. Two
strange things about this explanation:

1. Sometimes Isabelle does not object to a step which essentially just
introduces a lambda - but sometimes it does (assuming your explanation
above is correct). I cannot discern any rhyme or reason to this - it
appears to me to be arbitrary.

2. What's worse, I find myself in a Catch 22. Given the file I posted
previously, I want to prove from 

lemma tt_simp [simp]: "tt f g x == f x (g x)"

the following:

lemma doh2 [simp]: "tt f g == %x. f x (g x)"

- something that should be completely trivial to prove, because it
follows directly from the fact that a function is defined to be a lambda
in the lambda calculus (in fact, I would expect the simp rule to do
it). So let's try a one-step proof:

lemma doh2 [simp]: "tt f g == %x. f x (g x)" by simp

No, that fails. OK, let's try a patient, but verbose approach:

lemma doh2 [simp]: "tt f g == %x. f x (g x)"
proof -
  have "tt f g == %x. tt f g x" .
  also have "... == %x. f x (g x)" by simp
  finally show "tt f g == %x. f x (g x)"
qed

This yields:

*** empty result sequence -- proof command failed
*** At command "finally".

OK, let's try a compromise:

lemma doh2 [simp]: "tt f g == %x. f x (g x)"
proof -
  have "tt f g == %x. tt f g x" .
  finally show "tt f g == %x. f x (g x)" by simp
qed

With this, Isabelle complains "No calculation yet".

So the Catch 22 is: if I try to do it in 1 step, Isabelle can't seem
to simplify that much in one step. If I try to do it in 3 steps,
Isabelle effectively complains that I'm insulting its intelligence
(going by your explanation of what the problem is, anyway). If I try to
do it in 2 steps, Isabelle doesn't recognise a 2-step calculation as a
calculation (even though, it clearly is such, from a human POV). I
can't win!

Now, the weird thing is (and here I'm going back to my point 1),
Isabelle happily accepts this proof:

lemma doh [simp]: "const x == %y. x"
proof -
  have "const x == %y. const x y" .
  also have "... == %y. x" by (unfold const_def)
  finally show "const x == %y. x" .
qed

even though you claim, about lambda introductions like the one on the
first line:

"Such redundant cases are filtered out in
 order to achieve more robust guessing of rule instances."

So why is it that my proof of doh works, but my proofs of doh2
don't? There must be something more to it that I'm not getting.

> Also note that equality reasoning is usually performed at the 
> object-level, using "=" instead of "==".  (This is in contrast to the 
> other connectives !! and ==>, which usually work better than ALL and
> -->).

OK, but I'm confused about the distinction between object-level
equality and meta-equality. What advantage would that give me for these
types of proofs? What disadvantages? Would currying be affected -
and would my theory file get more verbose?

-- 
Robin





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