Email Gateway (Aug 17 2022 at 14:43): Email Gateway (Aug 17 2022 at 14:43):From: Makarius <makarius@sketis.net>
On Tue, 9 May 2006, Robin Green wrote:
- What's worse, I find myself in a Catch 22. Given the file I posted
previously, I want to prove fromlemma 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
(in fact, I would expect the simp rule to do it).
You are right. The Simplifier setup does not anything like this for other
reasons (including historical ones).
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
Try this in the body:
show "%x. tt f g x == %x. f x (g x)" by simp
i.e. you make the Simplifier happy by stating an expanded form. The
result then fits into the pending problem due to alpha-beta-eta
conversion. All single-step refinements work by higher-order unification,
which includes these lambda conversions. Automated tools may have
slightly different ideas.
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" .
qedeven 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."
The filtering is on calculational results, not the original facts. Here
you did make some progress, becase the final rhs is different from the
first lhs. In the first example the latter were the same.
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?
Generally speaking, meta-level !! and ==> connectives express natural
deduction rules, which can be used directly. Object-level formula need to
be unpacked first, via usual intro/elim rules to reduce them to plain !!
and ==>.
Concerning equality, there is not much of a difference in HOL
theoretically. Practically speaking = is more convenient, because most
tools work directly with this form. For example, the calculational rules
for = include various mixed forms (substitution etc.) while == is limited
to plain transitivity.
Would currying be affected
No.
and would my theory file get more verbose?
Yes, if you pack everything into ALL --> etc. unnecessarily; proofs will
become more complicated. But this is not what the present examples were
about.
Makarius
Email Gateway (Aug 17 2022 at 14:43):From: Makarius <makarius@sketis.net>
On Sun, 7 May 2006, Robin Green wrote:
I'm using Isabelle 2005, and I've picked up how to do some calculational
proofs in a "monkey-see, monkey-do" kind of way - i.e. not really
understanding the connecting commands like "also" and "have" and "show".
'also' merely composes the background calculation with the last fact.
Several rules are tried in turn, cf. print_trans_rules.
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. Such redundant cases are filtered out in order to
achieve more robust guessing of rule instances. Try this to see what
happens internally:
thm calculation this transitive [OF calculation this]
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 -->).
Makarius
Email Gateway (Aug 17 2022 at 14:43):From: Robin Green <greenrd@greenrd.org>
On Mon, 8 May 2006 14:13:48 +0200 (CEST)
Makarius <makarius@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:
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.
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)"
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?
Email Gateway (Aug 17 2022 at 14:46):From: Robin Green <greenrd@greenrd.org>
I'm using Isabelle 2005, and I've picked up how to do some
calculational proofs in a "monkey-see, monkey-do" kind of way - i.e.
not really understanding the connecting commands like "also" and
"have" and "show".
Can someone explain why, in the attached theory file, I get this error
on the last line:
*** empty result sequence -- proof command failed
*** At command "also".
Previously when I hit this error, I found that I could delete the
previous line in the proof and the error would go away. But in this
case, if I delete the previous line, the combined step is too hard for
Isabelle to do in one step, as far as I can see.
Functor.thy
Last updated: Nov 21 2024 at 12:39 UTC