The Coq mailing list

[xiang sen <xiangsen AT ustc.edu>]

Ah, It' s my mistake!
I had thought it was the order of appearance in hypothesis.

Thanks!

Best regards
Xiang Sen


anoun AT labri.fr
 wrote:

> Hi sen,
> I think that every thing is all right in your example, the order should be 
> (siz2
> lnk2) to respect the order in the list of quantified variables
> 'forall (h1 h2 h:heap) (rf :rfile) (siz1 siz2 :nat)
>  (pr1 lnk1 pr2 lnk2 : addr)'
> You can reverse that order modifiying the statement of your axiom like this
> Axiom compose_MBlk_MBlk_MBlk: forall (h1 h2 h:heap) (rf :rfile) (pr1 lnk1 pr2
> lnk2 : addr)(siz1 siz2:nat),....
> Hope this helps!
> Houda
>
>  
>
> > 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).
> >    
>
>
> ----------------------------------------------------------------
> 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
>
>
>