The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Eric,

>  (* on_last_hyp clear. - Error: Tactic failure *)
>  (* on_last_hyp ltac:(clear). - Loops forever? *)
>  (* on_last_hyp (fun X=>clear X). - Error: The reference clear was not
> found in the current environment. *)
>  on_last_hyp ltac:(fun X=>clear X). (* clear the last hypothesis *)
Although they seem similar to the user, a built-in tactic waiting for
an argument (like [clear]) is not handled internally by Ltac in the
same way as a user-defined tactic function, hence in your example the
first version fails while the last one works. Alternatively, you can
write "Ltac myclear H := clear H" and a call to "on_last_hyp myclear"
will behave as expected. The third version above fails because as you
probably guessed Ltac interprets the argument as a constr and not as a
tactic construction, unless you put ltac:(..) around. Last but not
least, I have to say I am quite bamboozled by the second one, that is
probably a bug since I don't see how on_last_hyp could loop (it never
backtracks since it raises fail with level 1).

>  (* on_last_hyp idtac. - Loops forever? *)
>  (* on_last_hyp ltac:(idtac). - Loops forever? *)
>  (* on_last_hyp (fun X=>idtac X). - Error: The reference clear was not
> found in the current environment. *)
>  (* on_last_hyp ltac:(fun X=>idtac X). - Error: Tactic failure *)
Same remarks as above with clear ; one difference though in the last
case : one needs to be aware of the exact semantics of ||. I used to
think that v1 || v2 was more or less "try v1 and if it FAILS then do
v2", but the second branch is used as soon as v1 fails TO PROGRESS, so
for instance "idtac 0 || idtac 1" will print 1, and in this case
on_last_hyp exits with failure since idtac does not make the goal
progress.

> (* Now, this was just for the sake of illustration. What I really want
> to do is to have tactical for combining hypotheses. The first one is a
> mapping, applying a tactic once and only once to every hypothesis, but I
> also need to apply a tactic to apply a tactic once and only once to all
> pairs of hypotheses (think about H1:a<=b H2:b<=c, looking for a way to
> saturate the environment with all consequences such as H3:a<=c), etc.
> Here is my latest unsuccessful attempt... *)
This is tricky business right there, I've always though that there
should be some built-in Ltac construction à la "map" that allows one
to address all hypotheses in the context in turn, because doing that
in Ltac can easily end up in infinte loops or very cumbersome context
manipulations. The problem is I dont think there is a really generic
way of performing such a "map" since it depends on what the tactic
applied at each step really does. For instance, the tactic may
introduce new hypotheses (should these new hypotheses be used in the
remaining part of the map or not ?), it may also clear or modify other
hypotheses (is map supposed to apply to all hypotheses as they were
when it was called, or to the context as it evolves during the map ?).
Altogether, the context is just a big stack of hypotheses, and a
tactic acts by modifying this stack and the goal, so iterating a
tactic over the very stack that it modifies requires some precise
semantics :)
It seems that depending on what you want to do, you can try and choose
the best way to perform the map (knowing that the tactic does not
modify the goal, for instance, lets you push used hypotheses to the
goal in order to avoid using the same hypothesis twice ; knowing that
an hypothesis can be discarded after it has been used, on the other
hand, makes things easier since you can just clear them on the fly).

> Ltac map_hyp tac := match goal with
>                    | [ H:_|-_ ] => first [tac H | idtac]; fail
>                    | _ => idtac
>                    end.
> Tactic Notation "for_hyp" tactic(T) := map_hyp ltac:(T).
> Theorem test_for_hyp:forall (n1:nat)(b1:bool)(n2:nat)(b2:bool), True.
> Proof.
>  intros.
>  for_hyp (fun X=>idtac X). (* Prints hypothesis names in revert order *)
>  for_hyp (fun X=>clear X). (* Does nothing apparent *)
>  for_hyp (fun X=>apply I). (* Concludes *)
> Qed.
This map_hyp does not do what you think it does, because of the
particular nature of matching in Ltac. When you fail in the first
branch, another branch is used instead and any modification to the
goal made before the failure is lost. So for instance, when iterating
clear, you just try every hypothesis H in turn, clearing H, and then
failing, bkactracking and restarting with the next hypothesis ; you
end up in the last branch and the tactic you finally apply is just
"idtac", which explains your observation.
Of course, if the tactic you apply in the loop has I/O "side effects",
like idtac in the first case, you still see these side effects, and
this is why you have the impression that it works in the first case,
but what you see is actually just a "trace" of all the try-and-misses
that Ltac did :) Finally, if the tactic happens to clear the goal, the
subsequent fail is not executed, and thus the match exits in the
regular way.

> Ltac map_hyp2 tac := match goal with
>                     | [ H:_|-_ ] => tac H; generalize H; clear H;
> map_hyp2 tac; intros H
>                     | _ => idtac
>                     end.
> (* Less elegant, especially if tac is for example "clear" *)
> Theorem test_map_hyp2:forall (n1:nat)(b1:bool)(n2:nat)(b2:bool), True.
> Proof.
>  intros.
>  map_hyp2 ltac:(fun X=>idtac X). (* Prints hypothesis names in revert
> order *)
>  map_hyp2 ltac:(fun X=>clear X). (* Does nothing apparent *)
>  map_hyp2 ltac:(fun X=>apply I). (* Concludes *)
> Qed.
In this case you are using the goal as a way to hide the hypotheses
already used, which is one good way of doing it. In particular, unlike
[map_hyp], it really works in the first example (the output is the
same, but this time [idtac] was really iterated on all hypotheses, and
not by backtracking after failures). But of course the tactic you
apply should not remove the hypothesis it is applied to, otherwise the
"generalize H; clear H" will fail (note that this is equivalent to
"revert H"), otherwise the branch fails and ends up using the default
branch, which is why when applied to "clear" it does nothing apparent.

> (* Any tip or advice ? Thanks in advance, Regards, Eric *)
Regarding your original problem of saturing inequalities, it is an
instance where the tactic you apply does not modify the goal, so you'd
like to use a similar trick to [map_hyp2], hiding the used hypotheses
in the goal. Unfortunately, one given hypothesis shall be used with
all the others hypotheses, so this is not easy to know when it is safe
hiding it. One way to do that though, is to let all hypotheses in the
context but make sure you are not doing the same step twice : the
[order] tactic, for ordered types, does exactly this saturation thing,
and here is the relevant excerpt of its main loop :

Ltac order_loop :=
 match goal with
 ...
 (* Transitivity of lt and le *)
 | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
    match goal with
      | H : x < z |- _ => fail 1
      | _ => generalize (lt_trans H1 H2); intro; order_loop
    end
 ...
 | _ => idtac
end.

Here, we use the fact that the matching non-linear (the same variable
may be used twice in the pattern) to make sure that we only match
pairs of hypotheses which are of interest, and then we perform another
match in the branch in order to make sure that the conclusion of this
saturation step that we're about to do is not already in the context.
If not, we add it and restart the loop ; if it is already there, we
fail with a level of 1, which means that Ltac will not backtrack in
this match, but in the original one above. This is vital since failing
with level 0 would end up in the saturation step being always
performed, and thus in an infinite loop ; failing with higher than 1
would end up the whole saturation loop.

You may look at the full code of the tactic if you re curious about
how to do such things with Ltac, its in
theories/Structures/OrdersTacs.v on the 8.3+ and trunk versions.

Hope this helps,

Stéphane L.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06