Email Gateway (Aug 22 2022 at 18:09): Email Gateway (Aug 22 2022 at 18:09):From: Makarius <makarius@sketis.net>
On 02/08/18 17:50, Peter Lammich wrote:
is there any particular reason why the ";" method combinator and the
more low-level THEN_ALL_NEW tactical process the new goals in a
backward fashion (except that implementing the backwards direction is
slightly more convenient).
That is the canonical order introduced by Larry Paulson about 3 decades
ago. For uniformity, it is used in various combinators whenever multiple
goals/premises need to be addressed.
So what are the deeper reasons that we have a backward ";" rather than
a forward ";", or why not simply have both?
For simplicity and uniformity. Having two possibilities everywhere
causes an exponential blowup. Having just one possibility avoids this.
While Eisbach is close to a clone of Ltac in Coq, it is merely a
convenience for plain and basic things. Isabelle/ML as the standard
implementation language for proof tools is still there, without the
complexity of Coq "plugins".
Makarius
Email Gateway (Aug 22 2022 at 18:09):From: Lawrence Paulson <lp15@cam.ac.uk>
It is difficult to remember, but I suspect that the point is to deliver stack-like behaviour with respect to the list of subgoals while avoiding the renumbering effects that would happen if low-numbered goals were processed first.
Larry
Email Gateway (Aug 22 2022 at 18:13):From: Makarius <makarius@sketis.net>
Here is some text from the "implementation" manual, referring e.g. to
ALLGOALS:
"""
Suppose that the goal state has n ≥ 0 subgoals. Many of these tacticals
address subgoal ranges counting downwards from n towards 1. This has the
fortunate effect that newly emerging subgoals are concatenated in the
result, without interfering each other. Nonetheless, there might be
situations where a different order is desired.
"""
Similarly for MRS and OF.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC