The Coq mailing list

[Eric Jaeger <eric.jaeger AT ssi.gouv.fr>]

Stéphane Lescuyer a écrit :
> ...
> 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 :)

Following the clarifications provided by Stéphane, here is my latest
best attempt for a map tactical - it is expected to work with clear as
well as intros (that is even when adding or removing hypotheses during
execution). Please feel free to comment for improvements.

  Regards, Eric

(* A map tactic that works once for every hypothesis present when the
   tactic is invoked; it uses the recursion context to store the list
   of hypotheses *)
Ltac map_hyp tac :=
 try (match goal with
      | [ H':_|-_ ] => revert H'; map_hyp tac; intros H'; tac H'
      end).
Tactic Notation "for_hyp" tactic(tac) := map_hyp ltac:(tac).

(* A second version allowing to exclude one specific hypothesis; should
   probably be recoded using the previous one *)
Ltac map_hyp_except tac H :=
 try (match goal with
      | [ H':_|-_ ] => match H' with
                       | H => fail 1
                       | _ => revert H'; map_hyp_except tac H;
                              intros H'; tac H'
                       end
      end).
Tactic Notation "for_hyp" tactic(T) "except" ident(H) :=
 map_hyp_except ltac:(T) H.

(* A tactic to apply a tactic to pairs of existing hypotheses; this one
   does not care about the order (it will generate (H,H') or (H',H) but
   not both) but will unfortunately consider (H,H) *)
Ltac map_pair tac :=
 try(match goal with [ H:_|-_] => revert H; map_pair tac; intros H;
                                  for_hyp (fun X=>tac H X)
     end).

(* This tactic uses the previous one but does nothing for pairs (H,H) *)
Tactic Notation "for_pair" tactic(T) :=
 map_pair ltac:(fun X Y=>match X with Y => idtac | _ => T X Y end).

(* This tactic does nothing for pairs (H,H) and try both (H,H') and
(H',H) *)
Tactic Notation "for_cpl" tactic(T) :=
 map_pair ltac:(fun X Y=>match X with Y => idtac | _ => try (T X Y); try
(T Y X) end).

(* This is a previous unsucessful attempt to generate pairs; other
attempts were trying to use map_hyp_except, but none was successful

Ltac map_pair tac :=
 let rec map_pair2 H :=
  try(match goal with [ H':_|-_] => revert H'; map_pair2 H; intros H';
tac H H' end)
 in
 let rec map_pair1 :=
  try(match goal with [ H:_|-_] => revert H; map_pair1; map_pair2 H;
intros H end)
 in map_pair1.
Tactic Notation "for_pair" tactic(T) := map_pair ltac:(T).
*)

Theorem test:forall (b1 b2 b3 b4:bool), True.
Proof.
 intros.
 for_hyp (fun X=>idtac X).
 for_hyp (fun X=>idtac X) except b1.
 for_hyp (fun X=>idtac X) except b2.
 for_hyp (fun X=>idtac X) except b3.
 for_hyp (fun X=>idtac X) except b4.
 for_pair (fun X Y=>idtac "(" X "," Y ")").
 for_cpl (fun X Y=>idtac "(" X "," Y ")").
 apply I.
Qed.