The Coq mailing list

[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?

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
> >
> >    
>
>
>