coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Eric Jaeger <eric.jaeger AT ssi.gouv.fr>
- To: coq-club AT inria.fr
- Cc: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
- Subject: Re: [Coq-Club] Ltac, again
- Date: Mon, 03 May 2010 09:31:31 +0200
- Organization: ANSSI
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.
- Re: [Coq-Club] Ltac, again, Eric Jaeger
- Re: [Coq-Club] Ltac, again, Eric Jaeger
Archive powered by MhonArc 2.6.16.