Email Gateway (Aug 19 2022 at 09:23): Email Gateway (Aug 19 2022 at 09:23):From: Joachim Breitner <breitner@kit.edu>
Dear List,
I am stumbling over a pattern here that requires me to do duplicate a
lot of proofs, and wondering if there there is a better approach.
Say I have an inductive predicate defined like this:
x ⇓ x
and
f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y
x ⇓ y
and a predicate P on the x’s and y’s that for which I have proven
P_preserved: x ⇓ y ==> P x ==> P y
by showing (in the context opened by the induction method)
P x ==> P (f1 x y)
P (f2 x y) ==> P (f3 x y)
P (f3 x y) ==> P y
Next, I need to to prove that another predicate Q is preserved, at least
when P holds:
Q_preserved: x ⇓ y ==> Q x ==> P x ==> P y
In this proof, to actually use the induction hypotheses, I again will
have to show
P x ==> P (f1 x y),
will have to invoke P_preserved with
f1 x y ⇓ f2 x y &&& P (f1 x y)
and then, again, have to show
P (f2 x y) ==> P (f3 x y)
for the second induction hypothesis.
Is there a pattern that would simplify this a bit? Ideally, in the
induction proof for Q, the method will provide me with
P x, P (f1 x y), P(f2 x y), P (f3 x y), P (f4 x y), P y
as induction premises. And preferably something more automatic than
stating the three implications in the proof of P_preserved as separate
named lemmas before proving them.
I know that it is not possible to derive that just from P_preserved.
Maybe the inductive command could generate a definition that captures
the notion of a predicate that, if it holds for one judgment, it holds
for all judgments occurring along the derivation tree, and then the
induct method could be made to use "hold_along_derivation_tree P" to
inject the necessary premises at each step.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:23):From: Ramana Kumar <rk436@cam.ac.uk>
(forwarding to list because I used the wrong email address)
---------- Forwarded message ----------
From: Ramana Kumar <Ramana.Kumar@cl.cam.ac.uk>
Date: Fri, Nov 16, 2012 at 5:19 PM
Subject: Re: [isabelle] Composable induction invariants
To: Joachim Breitner <breitner@kit.edu>
Cc: "cl-isabelle-users@lists.cam.ac.uk" <cl-isabelle-users@lists.cam.ac.uk>
Sorry, I meant the strong induction would give you:
f1 x y ⇓ f2 x y
in addition to
Q (f1 x y) ==> Q (f2 x y)
as hypotheses when trying to prove
Q x ==> Q y
in the inductive case.
On Fri, Nov 16, 2012 at 5:16 PM, Ramana Kumar <Ramana.Kumar@cl.cam.ac.uk>wrote:
I presume for Q_preserved the last consequent should be Q y rather than P
y?One approach is to use what in HOL4 we call a "strong" induction
principle, which gives you x ⇓ y as an induction hypothesis when trying to
prove Q (f1 x y) etc. Then you can apply your existing P_preserved theorem
to that. Would that give you everything you need?I think you can prove the strong induction from the induction Isabelle
automatically generates (although perhaps not just "by induction").On Fri, Nov 16, 2012 at 3:12 PM, Joachim Breitner <breitner@kit.edu>wrote:
Dear List,
I am stumbling over a pattern here that requires me to do duplicate a
lot of proofs, and wondering if there there is a better approach.Say I have an inductive predicate defined like this:
x ⇓ x
and
f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y
x ⇓ y
and a predicate P on the x’s and y’s that for which I have proven
P_preserved: x ⇓ y ==> P x ==> P y
by showing (in the context opened by the induction method)
P x ==> P (f1 x y)
P (f2 x y) ==> P (f3 x y)
P (f3 x y) ==> P yNext, I need to to prove that another predicate Q is preserved, at least
when P holds:
Q_preserved: x ⇓ y ==> Q x ==> P x ==> P y
In this proof, to actually use the induction hypotheses, I again will
have to show
P x ==> P (f1 x y),
will have to invoke P_preserved with
f1 x y ⇓ f2 x y &&& P (f1 x y)
and then, again, have to show
P (f2 x y) ==> P (f3 x y)
for the second induction hypothesis.Is there a pattern that would simplify this a bit? Ideally, in the
induction proof for Q, the method will provide me with
P x, P (f1 x y), P(f2 x y), P (f3 x y), P (f4 x y), P y
as induction premises. And preferably something more automatic than
stating the three implications in the proof of P_preserved as separate
named lemmas before proving them.I know that it is not possible to derive that just from P_preserved.
Maybe the inductive command could generate a definition that captures
the notion of a predicate that, if it holds for one judgment, it holds
for all judgments occurring along the derivation tree, and then the
induct method could be made to use "hold_along_derivation_tree P" to
inject the necessary premises at each step.Thanks,
Joachim--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner
Email Gateway (Aug 19 2022 at 09:24):From: Joachim Breitner <breitner@kit.edu>
Dear Ramana,
Isabelle’s induct method already provides me "f1 x y ⇓ f2 x y", and I
can use this to prove what I need, but not without repeating the proofs
that I have done already inside P_preserves and using P_preserves
itself.
I think one approach that does not involve too much copy’n’paste (but
still some would be this: I start with the normal inductive definition:
f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y
x ⇓ x x ⇓ y
Then i copy’n’paste it to create a stronger version:
P x f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y;
P x; P y; P (f1 xy); P (f2 x y);
P (f3 x y; P (f4, x y)
______ _________________________________
x ⇓' x x ⇓' y
An easy consequence will be:
x ⇓' y ==> P x &&& P y
Now I prove this lemma:
x ⇓ y ==> P x ==> x ⇓' y
by induction over the definition of ⇓. In this proof, I will have to do
the steps that I want to avoid doing more than once, e.g.
P x ==> P (f1 x y)
P (f2 x y) ==> P (f3 x y)
P (f3 x y) ==> P y
The lemma P_preserved is now an easy consequence of the the previous
two lemmas.
Now to prove
Q_preserved: x ⇓ y ==> Q x ==> P x ==> P y
I first obtain x ⇓' y and then prove
x ⇓' y ==> Q y
by induction over ⇓'. At this point, Isabelle’s induct method will allow
me to assume all the "P something" statements that I need in the
inductive steps.
Disclaimer: I have not implemented this yet (currently, I have just
copied the proofs), but I guess I will before I copy them the second or
third time.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:24):From: Ramana Kumar <rk436@cam.ac.uk>
I see... no obvious tricks are coming to my mind, but that doesn't mean
there aren't any.
Your approach to define a relation that carries the P around seems pretty
good.
One other approach would be to prove the three theorems you want to prove
only once as separate lemmas independent of any induction.
I.e., prove
P x ==> P (f1 x y)
(and add whatever extra hypotheses are necessary, which will always be
provided in an induction context)
as a standalone lemma, then use it whenever you need. (And similarly for
the other two.)
Email Gateway (Aug 19 2022 at 09:24):From: Joachim Breitner <breitner@kit.edu>
Hi,
right, this is the straight-forward solution, but it does involve too
much copy’n’paste. In my case, x and f1 x y are somewhat large and
changing expressions, so just writing out these separate lammas (which
would also have to include any conditions on the induction rules) is
tedious, let alone coming up with good names for them :-)
Thanks for your input,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC