Coq Ltac and Ltac2 hypothesis iterator tactics

allhyps.v

(*** Creating Ltac and Ltac2 tactics to iterate over hypotheses in a goal ***)

(*The purpose is to create a tactics in each of Ltac and Ltac2 which accept a
 tactic function argument (referred to as "tac") that is then called iteratively
on each hypothesis in the current goal, with at most one call per hypothesis -
exactly one call if all tac calls succeed, or until tac fails, at which point
the whole iterator fails.  The tactics will come in pairs.  One of the pair will
iterate over the hypotheses top-down, and the other bottom-up, as both of these
directions are commonly needed for different reasons, depending on the
intentions of tac.  Additionally, other than changes made to the goal by tac,
these iterator tactics should not alter the goal in any way.  The current names
of hypotheses should be preserved, even if the user has Set Mangle Names turned
on.  Also, when tac is called on each hypothesis, the goal as seen by tac should
be as it was initially, other than any changes made by previous iterations'
calls to tac.

One way to do this in Ltac uses a recursive function that captures hypotheses by
reverting and re-introducing them with the same name.  It constructs two
continuations so that all hypotheses can be fully re-introduced by the first
continuation (icont) prior to any calls to tac, all of which occur in the second
continuation (tcont):*)

Ltac allhyps_bu tac := (*bottom-up version*)
  let rec loop icont tcont :=
      lazymatch goal with
      | H : _ |- _ => revert H;
                    loop ltac:(intro H; icont) ltac:(tcont; tac H)
      | _ => icont; tcont
      end
  in loop ltac:(idtac) ltac:(idtac).

Ltac allhyps_td tac := (*top-down version*)
  let rec loop icont tcont :=
      lazymatch goal with
      | H : _ |- _ => revert H;
                    loop ltac:(intro H; icont) ltac:(tac H; tcont)
      | _ => icont; tcont
      end
  in loop ltac:(idtac) ltac:(idtac).

(*The above allhyps tactics make use of the fact that lazymatch on the goal with
a pattern looking for a hypothesis with any type will match the bottom
hypothesis in the goal, if one exists.  We use lazymatch instead of match
because we do not wish to have any within-match-construct backtracking on
failure, and also to preserve the failure level if tac fails (although, in this
particular case, match would also work equally well because the only potential
failures are in tcont, which is only called in the last default "_" match branch
- it's still good practice to use lazymatch when no backtracking for further
matches is desired, as it makes debugging easier and makes the tactic's
intentions more clear).  Note that the only difference between the bu and td
allhyps variants is the order of tac H vs. tcont calls in the tcont continuation
- hence the final tcont continuation of one is the reverse of the other.*)

Goal nat -> nat -> nat -> nat -> False. (*a small test*)
Proof.
  intros a b c d.
  Show Proof.
  allhyps_bu ltac:(fun h => idtac h). (*prints on separate lines: d c b a*)
  allhyps_td ltac:(fun h => idtac h). (*prints on separate lines: a b c d*)
  (*unfortunately, they do leave their revert/re-intro tracks in the proof term,
  in the form of additional lambdas and applications of those lambdas, if you
  care about that:*)
  Show Proof.
Abort.

(*What if we didn't want the iterator to alter the proof term at all?
Obviously, that would only be possible if tac itself didn't alter the proof
term.  But suppose that we desire no additional alterations from the iterator.
There is a way to do that in Ltac1 based on the following
constructor-within-ltac-within-constr trick, where the reverts occur within a
constr, hence don't alter the outer goal:*)

Ltac revert_all := repeat lazymatch goal with H:_ |- _ => revert H end.

Goal nat -> nat -> nat -> nat -> False.
  intros a b c d.
  Show Proof.
  let x:=constr:(ltac:(revert_all; constructor):True) in idtac x.
  (*notice how x captures the hypotheses as arguments to a function...*)
  Show Proof. (*...without altering the proof term*)
Abort.

(*This trick (which the author discovered, and is appropriately ashamed of) uses
the fact that the constructor tactic, when presented with a multi-arrow-typed
goal produced by reverting all hypotheses, where the ultimate type is easily
constructed on its own (like True, hence the cast to True in the constr), will
automatically construct the appropriate trivial function instance of that
multi-arrow type and apply it to dismiss its arguments, which are the
hypotheses.  And, of course, it depends on the fact that a constr constructed
with a goal in focus shares hypotheses with that goal.  We can capture x in a
tactic, and use a recursive match to strip them out of x one at a time.  The
result would be slower (demonstrated below) than the above dual-continuation
based tactics.  Also, the code is certainly less transparent and thus prone to
maintenance issues.  Also note that it skips hypotheses that have values, which
can be remedied by having revert_all strip those values.  Left as an exercise
for the curious kludge-loving reader.*)

(*If we use iterators as basic building blocks for complex tactic libraries,
then the overhead per iteration will be important.  Can we make versions of
these tactics that have lower overhead per iteration?  One source of this
overhead is the use of revert and intro tactics to capture the hypotheses, since
these are altering the goal, even though they balance so that the goal is
ultimately preserved (in the case of the above constructor trick, the reverts
don't alter the outer goal, nor are they balanced with re-intros, but they do
alter the goal within the constr, which still takes time).  Is there a way to
iterate over hypotheses without performing any goal alterations along the way?

We can accomplish this in Ltac2.  Ltac2 contains a function, Control.hyps, that
provides direct information about all hypotheses in a goal as a single list
without any need to alter the goal (or to create and alter a constr).  The
following pair of Ltac2 iterator tactics use this: *)

From Ltac2 Require Import Ltac2.

Ltac2 allhyps_bu2 (tac : constr -> unit) :=
  let rec loop hs :=
      match hs with
      | h3 :: hs =>
        match h3 with
        | (h, _, _) => loop hs;
                      tac (Control.hyp h)
        end
      | _ => ()
     end
  in loop (Control.hyps ()).

Ltac2 allhyps_td2 (tac : constr -> unit) :=
  let rec loop hs :=
      match hs with
      | h3 :: hs =>
        match h3 with
        | (h, _, _) => tac (Control.hyp h);
                      loop hs
        end
      | _ => ()
      end
  in loop (Control.hyps ()).

(* Some explanation: At the time of this writing, Ltac2 does not yet support
nested match patterns like "(h, _, _)::hs", hence the need for nesting the
matches instead.  The list returned from Control.hyps is a list of triples [hyp
name as ident, hyp value as constr option, hyp type as constr] in top-down
hypothesis order.  We only need the hypotheses names for our iterators, but we
prefer to have each as a constr instead of an ident.  A constr is a bit more
useful than an ident, especially if we will be passing Ltac tac functions to
this Ltac2 iterator, because while there is a direct way to pass constrs across
the Ltac/Ltac2 interface, no direct way exists for idents.  The Control.hyp
function maps the hypothesis name ident to a corresponding constr for the
hypothesis name.  Note the distinction: Control.hyps vs. Control.hyp have
different but complementary functions.  The first returns the list of hypothesis
triples, the second does ident-to-constr conversion for hypothesis name idents.

There is one detail about these Ltac2 iterators that might be problematic.  What
happens if one iteration of tac clears a hypothesis that a subsequent iteration
of tac is given?  If that happens with these iterator tactics, the Control.hyp
function will fail when attempting to map the no-longer-existing hypothesis
ident to a constr.  This failure would occur outside the control of tac itself,
such that tac cannot decide to use a "try" tactical to prevent failure in such
cases and allow iteration to continue, or instead to allow the whole iteration
to fail.  We can create safer versions that don't fail outside tac by first
mapping the list of hyp triples directly to a list of constrs prior to the first
iteration, hence before any tac calls that might clear hypotheses: *)

Ltac2 allhyps_bu2s (tac : constr -> unit) :=
  let rec loop hs :=
      match hs with
      | h :: hs => loop hs; tac h
      | _ => ()
      end
  in loop (List.map (fun (h, _, _) => Control.hyp h) (Control.hyps ())).

Ltac2 allhyps_td2s (tac : constr -> unit) :=
  let rec loop hs :=
      match hs with
      | h :: hs => tac h; loop hs
      | _ => ()
      end
  in loop (List.map (fun (h, _, _) => Control.hyp h) (Control.hyps ())).

(*The result will be very slightly slower, due to having to construct the
intermediate list of hypothesis name constrs instead of consuming the list of
triples directly.  Note that we could offer more alternatives - it might be
desirable for some iteration step to halt the overall iteration without failing
and undoing all previous iteration steps, while also offering a way for a
failure to undo all iteration steps.  We can use Ltac2 exceptions to do that, or
we could structure the iteration as a continuation passed as an additional
argument to tac - these are left as exercises for the reader.

Since clearing hypotheses during iterations over hypotheses is not likely the
norm for tac functions given to these iterators, but still possible, it might be
worth keeping both safe and unsafe iterators.  However, the performance
difference is insignificant compared to the advantage of either vs. the Ltac
iterators, hence one might only wish to keep the safe ones.*)

(*How to interface to these Ltac2 iterators from Ltac?  The use case of an
Ltac2 iterator tactic being fed Ltac tac functions will likely be a common step
as users incrementally convert over from Ltac to Ltac2.  We'll use the safer
versions of the above Ltac2 iterators, and wrap them in Ltac tactics that
encapsulate the necessary interfacing:*)

Ltac2 app1c (tac : Ltac1.t)(c:constr) :=
  Ltac1.apply tac [Ltac1.of_constr c] Ltac1.run.

(*The interface between Ltac and Ltac2 is performed in two parts, one in Ltac2
wrapping tac and the other in Ltac wrapping each Ltac2 iterator.  First is
app1c, which is an Ltac2 function that applies an Ltac tactic function tac to a
single constr argument c.  Note that all Ltac values have the same Ltac2 type,
Ltac1.t.  Hence, tac, even though we expect it to be a function of a single
argument, doesn't have an arrow ("->") type as one would expect in a strictly
typed language.  If we gave it the more illustrative type "Ltac1.t -> unit", it
instead would be an Ltac2 function that takes an arbitrary Ltac value, which is
not what we want here.

The app1c function performs 3 steps.  First, it converts c from an Ltac2 constr
to an Ltac1.t value using Ltac2's Ltac1.of_constr, and places the result in an
Ltac2 list using Ltac2's "[...]" notation.  Next, it applies tac to that list
using Ltac2's Ltac1.apply (not to be confused with the ubiquitous Ltac apply
tactic!), which passes the applied result continuation-style as a tactic thunk
to its third argument.  That third argument is Ltac2's Ltac1.run, which takes
the now argumentless Ltac thunk and finally executes it.

Note the lack of type safety surrounding the application of the Ltac tac.  Its
type isn't checked, its argument type isn't checked, and the result type of its
application to that argument isn't checked.  If tac doesn't take exactly one
argument, and that argument isn't the Ltac equivalent of a constr, then a
runtime failure would occur.  We lose the benefits of Ltac2 type safety when
interfacing with Ltac.

Note that it is possible to have a version of tac such that the continuation
call from Ltac1.apply to Ltac1.run is not necessary (in which case, a no-op
thunk (fun _ => ()) can be used as the final argument to Ltac1.apply instead of
Ltac1.run).  That would happen if tac was written to be an "immediate" Ltac
thunk by having a single top-level match (or lazymatch, or multimatch) or by
returning a value (the semantics of Ltac is notoriously convoluted here, among
other places - Ltac2 does not share this complexity).  Such immediate thunks
would run as soon as their arguments are applied, hence within the Ltac1.apply
call itself.  However, as we want a general purpose iterator that does not
require nor discriminate against immediate Ltac thunks, we use Ltac1.run as the
continuation for Ltac1.apply.  This way, it won't matter if tac is an immediate
thunk or not.  If it is, it runs in Ltac1.apply.  If it isn't, then it runs
within Ltac1.run.  Additionally, if it is an immediate thunk that returns an
argumentless tactic, that argumentless tactic runs in Ltac1.run.  If it is an
immediate thunk that doesn't return a value, then Ltac1.run turns into a no-op.
But, having all of these special cases end up the same way is what we would
normally want to occur given a general-purpose iterator.*)

Ltac allhyps_bu2s1 :=
  ltac2:(tac |- Control.enter (fun _ => allhyps_bu2s (app1c tac))).

Ltac allhyps_td2s1 :=
  ltac2:(tac |- Control.enter (fun _ => allhyps_td2s (app1c tac))).

(* The second part of the interface consists of a wrapper for each of the two
Ltac2 iterators, allhyps_bu2s and allhyps_td2s (we're using the safe versions,
but the unsafe versions can be used instead).  Each consists of an ltac2:
quotation, which creates a function with bindings on the left of the turnstile
"|-" and body on the right.  Thus, the two wrapper tactics are themselves
functions of a single argument, tac.

Within the ltac2: quotation, we use app1c to convert tac to an Ltac2 tactic and
pass that to the corresponding Ltac2 iterator, within a thunk passed to
Control.enter.  The purpose of Control.enter is to make sure that the iterator
runs in the context of a single focussed goal.  Making sure that the context of
execution is not multiple goals is something that would happen automatically if
we stayed within Ltac.  In Ltac2, if we didn't use Control.enter to make sure
the context is not multiple focussed goals, a failure might occur when calling
Control.hyps, as this function fails if more than one goal is under focus.  If
there were no goals under focus, it would succeed, but return information about
section variables instead (if there are any).

The requirement to use Control.enter actually illustrates a potential semantic
benefit of Ltac2 over Ltac: in Ltac, because focus changes are done
automatically based on the nature of the tactic or tactical used, it is very
difficult to gain and maintain control over multiple focussed goals as a single
execution thread instead of a separate (but similar) execution thread on each
goal in focus.  In Ltac2, this is under explicit control.  This is a potential
benefit for more complex tactics that need to consider multiple goals together,
as is sometimes the case for instance when the goals share evars and the desire
is for a faster proof search than can be accomplished using backtracking alone.
Or even if they don't share evars, but proof search is faster when goals are
attempted in a different order to how they are presented, and that order is best
selected by probing information contained in the goals.*)

Set Default Proof Mode "Classic". (*we want to use Ltac interactively*)

Goal nat -> nat -> nat -> nat -> False.
Proof.
  intros a b c d.
  Show Proof.
  allhyps_bu2s1 ltac:(fun h => idtac h). (*d c b a*)
  allhyps_td2s1 ltac:(fun h => idtac h). (*a b c d*)
  Show Proof. (*Another benefit: the proof term is not altered!*)
Abort.

Goal True. (*performance test*)
  do 2000 pose proof I. (*generate many hypotheses*)
  (*use optimize_heap to make sure timings don't include gc overhead due to
  previous computations*)
  optimize_heap.
  (*Timings obviously depend on hardware, hence your milage may vary: *)
  time allhyps_td ltac:(fun _ => idtac). (*1.75 secs*)
  optimize_heap.
  (*the constructor trick is very slow for large numbers of hypotheses - even
  when just forming the constr without performing the iteration:*)
  time let x:=constr:(ltac:(revert_all; constructor):True) in idtac. (*8.90 secs*)
  optimize_heap.
  (*Ltac2 is wicked fast!:*)
  time allhyps_td2s1 ltac:(fun _ => idtac). (*0.03 secs*)
Abort.