The Coq mailing list

[casteran AT labri.fr]

Hello Houda,

 This is because H is considered as a pattern variable and is
no more bound to the name 'H'.

You can  use "type of" :


Ltac elimAnd H:=
let typ := type of H in
   match typ with ?A /\ ?B => elim H
   end.


Lemma tryTac:forall (A B:Prop), A/\B ->A/\A->B.
intros A B H H0.
elimAnd H.
auto.
Qed.

Pierre

Selon Houda Anoun 
<anoun AT labri.fr>:

> Hi everybody,
> I want to define a tactic that has an argument H which is a name of an
> hypothesis of the context that  will be used if some conditions are
> verified to simplify the current goal
> An example of such tactics is the following one: elimAnd
>
> Ltac elimAnd H:=
> match goal with H:?A/\?B |- _=>elim H; clear H; intros
> | _ =>idtac
> end.
>
> The tactic that I want to define has one argument H , the tactic has to
> check that the type of H is of the form A/\B if this is the case the
> tactic elim this hypothesis otherwise it does nothing
> Unfortunately while trying to test elimAnd I found that it doesn't
> always elim the hypothesis whose name is given as a parameter specially
> when the context contains several hypothesis of the form _/\_!
>
> An example of that is the following:
> Lemma tryTac:forall (A B:Prop), A/\B ->A/\A->B.
> intros A B H H0.
> elimAnd H.
> -------here the tactic elim H0 instead of H!!
>
> How can we solve the probleme without defining the tactic in ocaml?
>
> Concerning the definition of tactics using ocaml is there any tutorial
> explaining that and giving some basic examples??
> Thanks a lot in advance
>
> Houda
>
> --
> ==============================
> |      Houda ANOUN           |
> |         LaBRI              |
> | 351 Cours de la libération |
> |      33405 Talence         |
> |    phone: 0540002489       |
> |  e-mail 
>Â :anoun AT labri.fr
>     |
> =============================
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.