The Coq mailing list

[anoun AT labri.fr]

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.