Email Gateway (Aug 22 2022 at 13:04): Email Gateway (Aug 22 2022 at 13:04):From: Christian Sternagel <c.sternagel@gmail.com>
This would definitely be useful! +1 - chris
Email Gateway (Aug 22 2022 at 13:04):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
A student came to me and asked for a 6-week internship project (starting in August). Perhaps this could be something suitable for him? (But if anybody else wants to implement this, go ahead and don't wait for us.)
Jasmin
Email Gateway (Aug 22 2022 at 13:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I have written several Isar-style proofs of lemmas each of which is quite long (>1000
lines). As the proofs have evolved over time, I am not sure any more that I use every
intermediate result to prove the result. Is there any convenient way to find out whether
there are some unused intermediate steps?
I tried to use unused_thms before the final qed, but this gives me only top-level
theorems, not intermediate (named) facts stated with "have". I could imagine a diagnostic
command that one issues before the qed and it lists all the unused intermediate facts
since the last "next" or "proof" command on the same level. If this is not available,
could this be implemented and how hard would it be? Would anyone else find such a
functionality useful?
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 13:14):From: Tobias Nipkow <nipkow@in.tum.de>
On 29/04/2016 10:39, Andreas Lochbihler wrote:
Dear all,
I have written several Isar-style proofs of lemmas each of which is quite long
(>1000 lines). As the proofs have evolved over time, I am not sure any more that
I use every intermediate result to prove the result. Is there any convenient way
to find out whether there are some unused intermediate steps?I tried to use unused_thms before the final qed, but this gives me only
top-level theorems, not intermediate (named) facts stated with "have". I could
imagine a diagnostic command that one issues before the qed and it lists all the
unused intermediate facts since the last "next" or "proof" command on the same
level. If this is not available, could this be implemented and how hard would it
be? Would anyone else find such a functionality useful?
I would. Especially if it is integrated with the interface and marks such unused
local facts (on demand).
Tobias
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 13:14):From: Manuel Eberl <eberlm@in.tum.de>
Absolutely.
Email Gateway (Aug 22 2022 at 13:14):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
+1!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 13:14):From: Makarius <makarius@sketis.net>
On Tue, 3 May 2016, Thomas Sewell wrote:
Well, they could be optionally given dummy names. That would break the
usual rule that names in the PThms (other than Pure.blah) look up facts,
but would allow you to check whether they were really used.
The names in PThm nodes are not even right for global facts. It is an old
confusion that is still there until today.
The other option would be to check whether they were syntactically used,
of course.
That is the dual approach to inspecting the internal inferences: looking
at the source with its PIDE markup. Recently I have already added some
rendering for the use of formal entities, visually connecting definitions
and references of items. This includes facts, but there are more ways to
refer to facts than for most other items:
(1) via literal fact references (backquotes or cartouche notation)
(2) via declarations that put them into the context for tools to pick
them up later, e.g. the "simp" attribute and "simp" proof method
(1) might soon be included in the PIDE markup model: it is syntactically
relatively clear. (2) is more difficult, because the absence or presence
of a "simp del" declaration can affect the proof. It might be better just
to test-run the proof document, and see if it still works with or without
certain elements.
Makarius
Email Gateway (Aug 22 2022 at 13:18):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
That's a good idea. I don't know whether the current implementation of reasoning actually
supports such a command. Makarius might know better. But if it does, I guess that this
could be a reasonably-sized project for a student.
Andreas
Email Gateway (Aug 22 2022 at 13:19):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Andreas,
That's a good idea. I don't know whether the current implementation of reasoning actually supports such a command. Makarius might know better. But if it does, I guess that this could be a reasonably-sized project for a student.
For Sledgehammer (esp. MaSh), we had to do some fishing around in the local context to retrieve facts in Isar proofs. I am under the impression that all the information we would need is stored in some form.
Jasmin
Email Gateway (Aug 22 2022 at 13:20):From: Makarius <makarius@sketis.net>
I think the main challenge are such questions about internal naming of
derivations (the infamous PThm nodes). I've never fully understood the
scheme introduced by Larry Paulson and reformed by Stefan Berghofer, more
than 15 years ago. Nonetheless, I've tinkered with it out of necessity, to
make parallel proof checking work.
It is definitely worth revisiting all that, and unifying it with the
treatment in Sledgehammer.
Afterwards, a student project to wrap it up as PIDE print function etc.
would be rather trivial. Still worth to learn how that works, but from 6
weeks only 1 is probably required.
Makarius
Email Gateway (Aug 22 2022 at 13:22):From: Thomas Sewell <thomas.sewell@nicta.com.au>
I had a brief look at this a while ago. My understanding is that a
(small) change might be needed.
OK, so, PThms track the derivation steps of thms. There are special
nodes which mark where thms (and their derivations) are named. This is
called through Thm.name_derivation, and via Global_Theory.name_thm.
Point is, globally-anonymous facts, such as steps in proofs, don't have
named derivations (currently). So proof term summaries will see them as
just part of the proof of the facts they result in.
Well, they could be optionally given dummy names. That would break the
usual rule that names in the PThms (other than Pure.blah) look up facts,
but would allow you to check whether they were really used.
The other option would be to check whether they were syntactically used,
of course.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 23 2024 at 04:18 UTC