The Coq mailing list

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

Selon xiang sen 
<xiangsen AT ustc.edu>:

> Thanks.
>
> But what I want is matching several hypothesis,
> because I need multi hypoth in the tac.
> You mean, it's necessary to use "match .. match ..." instead of
> "match goal with [h1: t1; h2 :t2;..|-C]"?
>
> I find in P.203 of Coq art that "The keywords "match goal with "
> indicate that patterns are applied to match the goal. The patterns
> have the form [h1 : t1; h2 : t2; ..|- C]=>tac". Why what I do does not work?
>

OK,

 But it seems to work !

Ltac bimatch T :=
 match goal with | [h1:T, h2:T |- _] => clear h1 end.


Goal nat -> nat -> nat -> nat -> bool.
intros.
 bimatch nat.
 bimatch nat.
 bimatch nat.

 Restart.

 intros; repeat bimatch nat.


The reason why I proposed another solution was in your first mail:


> Ltac indom :=
> match goal with
> | [h1 : heap; h2 : heap] |- ] => clear h1
> end.
> (** doesn't work **)

In fact, it is syntactically incorrect.

Pierre

If bimatch doesn't fit your requisites, please tell us what the tactic must
do (i.e. to which kind of goals it must be applied, and which subgoals
it must generate).


Cheers,

Pierre




> Pierre Casteran wrote:
>
> >Hi,
> >
> > This version with an auxiliary tactic clearloop is a little better
> >(wrt. the number of goal matchings).
> >
> >Pierre
> >
> >
> >(* auxiliary tactic *)
> >Ltac clearloop h1:=
> >                  (clear h1 ;
> >                     match goal with | [h2 : heap |- _] => clearloop h2
> >                                     | _ => fail 1 end)
> >                  || idtac.
> >
> >(* main tactic *)
> >Ltac clearheap2 :=
> >  match goal with |
> >    [h1 : heap |- _] => clearloop h1
> >  end.
> >
> >
> >Goal heap -> heap -> nat -> heap -> heap ->nat.
> > intros.
> > clearheap2.
> > auto.
> >Qed.
> >
> >
> >
> >
> >
> >>Hi,
> >>
> >> Are you looking for a tactic which keeps only one hypothesis of
> >>type heap ?
> >>
> >> If so, it seems that a tactic like that works :
> >>
> >>
> >>Parameter heap:Prop.
> >>
> >>
> >>Ltac clearheap :=
> >>  match goal with |
> >>    [h1 : heap |- _] =>
> >>                  (clear h1 ;
> >>                     match goal with | [h1 : heap |- _] => clearheap
> >>                                     | _ => fail 1 end)
> >>                  || idtac
> >>  end.
> >>
> >>Goal heap -> heap -> nat -> heap -> heap ->nat.
> >> intros.
> >> clearheap.
> >> auto.
> >>Qed.
> >>
> >>
> >>
> >>Pierre
> >>
> >>
> >>
> >>
> >>Selon xiang sen 
> >><xiangsen AT ustc.edu>:
> >>
> >>
> >>
> >>>Hi, everyone!
> >>>
> >>>(*I define indom as :*)
> >>>Ltac indom :=
> >>>match goal with
> >>>| [h1 : heap |- _] => clear h1
> >>>end.
> >>>
> >>>(*This is ok.*)
> >>>(*but *)
> >>>Ltac indom :=
> >>>match goal with
> >>>| [h1 : heap; h2 : heap] |- ] => clear h1
> >>>end.
> >>>(** doesn't work **)
> >>>
> >>>How to resolve?
> >>>Thanks
> >>>
> >>>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
> >>>
> >>>
> >>>
> >>--
> >>Pierre Casteran
> >>
> >>http://www.labri.fr/Perso/~casteran/
> >>
> >>(+33) 540006931
> >>
> >>----------------------------------------------------------------
> >>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.