Email Gateway (Aug 18 2022 at 13:36): Email Gateway (Aug 18 2022 at 13:36):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,
the induct method is very convenient when proving lemmas by induction
over an inductive definition: All extra assumptions that are not
consumed as specified by the consumes attribute for the induction rule
are packaged into the proposition P, variables with explicit
instantiations of the form k=="t" generate additional assumptions, and
variables specified by arbitrary get universally quantified.
In contrast, the coinduct method seems to be very disappointing for
coinductively defined predicates: I have not yet found a way to make it
considers not only the first assumption that is chained in, but the
conjunction of all of them. Neither seem defining instantiations to be
supported, nor have I found a counterpart to arbitrary.
Currently, I always introduce a new variable for defined instantiations,
manually add the equation to the conjunction of the assumptions and
existentially quantify over variables that I would list after arbitrary
in an induction. Inside the proof, the first thing to do is to unpack
all assumptions again.
Can I somehow avoid all this clutter in my Isar proof scripts?
Regards,
Andreas
Email Gateway (Aug 18 2022 at 13:37):From: Lawrence Paulson <lp15@cam.ac.uk>
I am glad that somebody out there is using coinduction. I suspect that
very little development has gone into this area and it is really
driven by what people ask for.
Larry
Email Gateway (Aug 18 2022 at 13:37):From: Makarius <makarius@sketis.net>
In principle "coinduct" could do the dual of the local context management
of "induct". I have a sketch of that on a pile of things that should be
done eventually, but empirically there are signigicantly less users of
coinduction than induction (and even that needs some updating).
BTW, Jesper Bengtson (Uppsala) has been using coninduction a lot. The
present "coinduct" method was prompted by him some years ago -- originally
he was still using erule_tac x = y in ... (Too many other diversions have
prevented to continue this further.)
Makarius
Last updated: May 03 2024 at 12:27 UTC