Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Francois Pottier <Francois.Pottier@inria.fr>
Hello,
I am trying to gain an initial understanding of both Isabelle/HOL
and the Isar structured proof language. My main sources are the
Isabelle/HOL tutorial and Markus Wenzel's PhD thesis. I have some
questions about proofs by induction.
I have been trying to write a few simple proofs about simply-typed
lambda-calculus. Here is a typical statement, a substitution lemma:
lemma substitution:
assumes p: "(env1, e1, t1) : judgments"
assumes q: "(env2, e2, t2) : judgments"
assumes e: "ALL y. y ~= x --> env1 y = env2 y"
assumes f: "env1 x = t2"
shows "(env2, subst x e2 e1, t1) : judgments"
(For reference, I include the definitions that lead up to this lemma
at the end of this message.) (For simplicity, my environments are
total functions from variable names to types.)
If I try to attack a proof of this statement by saying
using p proof (induct)
then Isabelle presents me with new subgoals that are plain wrong.
The first of these, for instance, is
1. !!env xa. (env2, subst x e2 (EVar xa), env xa) : judgments
I can understand how these subgoals appear. The induction principle for
judgments (judgments.induct) involves a schematic variable ?P that must
satisfy the equation
?P env1 e1 t1 = ((env2, subst x e2 e1, t1) : judgments)
(This equation is obtained by considering the fact p and the statement's final
"shows" clause. The facts q, e, and f are apparently ignored in this process.)
This leads to the candidate
?P = %env1 e1 t1. ((env2, subst x e2 e1, t1) : judgments)
which is inappropriate.
My questions are,
how should I reformulate the statement (or the proof) so that appropriate
sub-goals arise? should I explicitly provide a value for the variable ?P in
the proof script? or should I modify the statement so that the hypotheses q,
e, and f are moved into the shows clause, using explicit implications?
the Isabelle tutorial suggests that this kind of induction
requires a strengthened statement, typically making use of
the object-level quantifiers ALL and -->. However, Wenzel's
thesis suggests that this is no longer necessary in Isabelle/Isar,
and that it is possible to stick with the meta-level quantifiers
!! and ==>. What's the final word?
I will of course continue to explore on my own, but any help would be warmly
welcome. Pointers to Isabelle/Isar developments that perform proofs by
induction with multiple hypotheses or multiple parameters, like above, would
also be very interesting to me.
Best regards,
Email Gateway (Aug 17 2022 at 13:27):From: Makarius <makarius@sketis.net>
On Mon, 10 Oct 2005, Francois Pottier wrote:
I have been trying to write a few simple proofs about simply-typed
lambda-calculus. Here is a typical statement, a substitution lemma:lemma substitution:
assumes p: "(env1, e1, t1) : judgments"
assumes q: "(env2, e2, t2) : judgments"
assumes e: "ALL y. y ~= x --> env1 y = env2 y"
assumes f: "env1 x = t2"
shows "(env2, subst x e2 e1, t1) : judgments"
If I try to attack a proof of this statement by saying
using p proof (induct)
then Isabelle presents me with new subgoals that are plain wrong.
The first of these, for instance, is1. !!env xa. (env2, subst x e2 (EVar xa), env xa) : judgments
The problem here is that your goal statement is not fully general wrt. to
the induction principle, using an expression "subst x e2 e1" in place of
an inductive variable.
In order to make this work, one may reformulate the goal in terms of a
local definition of that expression, then perform the induction, then
unfold the definition in each inductive case:
lemma substitution:
assumes p: "(env1, e1, t1) : judgments"
assumes q: "(env2, e2, t2) : judgments"
assumes e: "ALL y. y ~= x --> env1 y = env2 y"
shows "!!x e1 e2. e == subst x e2 e1 ==> (env2, e, t1) : judgments"
using p
proof (induct)
case JVar
then show ?case apply (simp only:) sorry
next
case JAbs
then show ?case apply (simp only:) sorry
next
case JApp
then show ?case apply (simp only:) sorry
qed
Note that the 'apply (simp only:)' above just demonstrate the machanics.
A proper proof would spell this out differently.
- the Isabelle tutorial suggests that this kind of induction
requires a strengthened statement, typically making use of
the object-level quantifiers ALL and -->. However, Wenzel's
thesis suggests that this is no longer necessary in Isabelle/Isar,
and that it is possible to stick with the meta-level quantifiers
!! and ==>.
!! ==> == instead of ALL --> = spare you 2 more bookeeping steps to get
rid of the logical connectives in the goal and the final result.
What's the final word?
An even better version of the 'induct' method, that is able to do
generalizations and local definitions (induction over structured
expressions) on the fly. I don't know if this will be the final word, but
it would move even further from fiddling with connectives, emphasizing
actual reasoning instead.
Makarius
Last updated: May 03 2024 at 08:18 UTC