The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon xiang sen 
<xiangsen AT ustc.edu>:

> Ah! Thanks a lot!
>
> But if I define splitex like this :
> Ltac splitex :=
> repeat match goal with
>  | H : ex _ _ |- _ => inversion_clear H
>  end.
>

If you type
 About ex
You will see that ex's first argument "A" is implicit :


ex : forall A : Type, (A -> Prop) -> Prop

Argument A is implicit
Argument scopes are [type_scope _]
Expands to: Inductive Coq.Init.Logic.ex



So, in order to write your tactic splitex, you can either do the same as 
Houda,
or something like :

Ltac splitex :=
repeat match goal with
 | H : ex (A:= _) _ |- _ => inversion_clear H
 end.


But the pattern with two plain positional arguments won't work.

Pierre




> Then
> (**** Example **)
>
> Require Omega.
> Lemma ex_try:forall m,(exists n:nat, n<m)->(exists n:nat,n+2<m)->m>=3.
> intros.
> splitex.
>
> splitex doesn't work.
>
> Why ? :)
>
> Sen
>
>
> anoun AT labri.fr
>  wrote:
>
> >Hi Sen,
> >Your tactic works if you use the type 'ex' instead of its notation (exists
> _:_,
> >)
> >
> >Ltac splitex :=
> >repeat match goal with
> > | H : ex _ |- _ => inversion_clear H
> > end.
> >
> >(*very simple example*)
> >
> >Require Omega.
> >Lemma ex_try:forall m,(exists n:nat, n<m)->(exists n:nat,n+2<m)->m>=3.
> >intros.
> >splitex.
> >omega.
> >Qed.
> >
> >
> >Houda
> >
> >
> >
> >>Hi , everyone :
> >>
> >>I used below to define a tactic :
> >>
> >>Ltac splitex :=
> >>repeat match goal with
> >>| H : exists _:_, _ |- _ => inversion_clear H
> >>end.
> >>
> >>But it does not work. Coqtop reports :
> >>Syntax error: [constr:ident] expected after 'exists' (in
> >>[constr:binder_constr]
> >>
> >>All the best!
> >>Sen
> >>--------------------------------------------------------
> >>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.
> >--------------------------------------------------------
> >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
> >
> >
> >
> >
>
> --------------------------------------------------------
> 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
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

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