The Coq mailing list

[xiang sen <xiangsen AT ustc.edu>]

Pierre Casteran wrote:

> Selon xiang sen 
> <xiangsen AT ustc.edu>:
>
>  
>
> > Hi, all :
> >
> > When I apply a lemma on the current goal , there are many parameters
> > required to be specified.
> > But their order seems puzzling. What 's the mechanism of order
> > determination in coq. Thanks!
> >    
>
>  
An incomplete example, but it's enough.

Axiom compose_MBlk_MBlk_MBlk: forall (h1 h2 h:heap) (rf :rfile) (siz1 
siz2 :nat)
 (pr1 lnk1 pr2 lnk2 : addr),
 hdisj h1 h2 -> heap_eq (happend h1 h2) h ->
 pr1 < pr2 -> pr2 = pr1 + siz1 ->
 MBlk (pr1 + 2) lnk1 siz1 (h1,rf) ->
 MBlk (pr2 + 2) lnk2 siz2 (h2,rf) ->
 MBlk (pr1 + 2) lnk1 (hread' h1 (pr1 + 1) + hread' h2 (pr2 + 1))
 (hwrite h (pr1 + 1) (hread' h1 (pr1 + 1) + hread' h2 (pr2 + 1)), rf).

Ltac mblk3 :=
 match goal with
   | [H1 : MBlk (?pr1 + 2) ?lnk1 ?siz1 (?h1, ?rf), H2 : MBlk _ ?lnk2 
?siz2 (?h2, ?rf)
     |- MBlk (?pr1 + 2) ?lnk1 _ (_, ?rf)] =>
   apply compose_MBlk_MBlk_MBlk with siz1 siz2 lnk2; auto
 end.

As you see, the order is (siz2 lnk2) instead of (lnk2 siz2).
It the order is left-to -right, it should be (lnk2 siz2).

Best regards
Xiang Sen

> Hi, Xiang,
>
> Have you some examples of problems you encounter ?
>
> In general, the order is the left-to-right order.
> Nevertheles, some little problems can arise if you are working through a
> notation which permutes this order :
>
>  Notation "x < y" := (my_module-gt y x) : my_scope.
>
> You must consider that y is at the leftmost position, even if
> "x < y" is displayed.
>
> But this is not a big problem: In dubious situations, I use the
> command Check or About to look at the names of the parameters, and
> I use the (A:=t) feature (look at "apply with" and at "implicit parameters"
>
>
> Cheers,
>
> Pierre
>
>  
>
> > All the best!
> > Xiang 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
> >
> >    
>
>
>