diff --git a/model/ExampleRO.v b/model/ExampleRO.v index 35b3c27d3410b58e4f3c6ae8601e706eecf68012..3414db694ba2da2d365609fe4cd4ecd2c649b529 100644 --- a/model/ExampleRO.v +++ b/model/ExampleRO.v @@ -108,78 +108,6 @@ Proof using. intros. applys* rule_consequence. applys* rule_frame. Qed. Hint Resolve Normal_hsingle. - - - -(* ---------------------------------------------------------------------- *) -(* rebind xchange to work on triples, which are not [local] *) - -Lemma xchange_lemma' : forall H1 H1' H2 t H Q, - (H1 ==> H1') -> - (H ==> H1 \* H2) -> - triple t (H1' \* H2) Q -> - triple t H Q. -Proof using. - introv W1 W2 M. applys~ rule_consequence M. - hchange W2. hchanges W1. -Qed. - -Ltac xchange_apply L cont1 cont2 ::= - eapply xchange_lemma'; - [ applys L | cont1 tt | cont2 tt (*xtag_pre_post*) ]. - -Ltac xchange_with_core cont1 cont2 H H' ::= - eapply xchange_lemma' with (H1:=H) (H1':=H'); - [ | cont1 tt | cont2 tt (* xtag_pre_post*) ]. - - - -(* ---------------------------------------------------------------------- *) -(* ** rebind [xpull] *) - - -(** Lemmas *) - -Lemma xpull_hprop' : forall t H1 H2 (P:Prop) Q, - (P -> triple t (H1 \* H2) Q) -> triple t (H1 \* (\[P] \* H2)) Q. -Proof using. - intros. rewrite hstar_comm_assoc. apply~ rule_extract_hprop. -Qed. - -Lemma xpull_hexists' : forall t H1 H2 A (J:A->hprop) Q, - (forall x, triple t (H1 \* ((J x) \* H2)) Q) -> - triple t (H1 \* (hexists J \* H2)) Q. -Proof using. - intros. rewrite hstar_comm_assoc. rewrite hstar_hexists. - applys rule_extract_hexists. - intros. rewrite~ hstar_comm_assoc. -Qed. - -Ltac xpull_hprop tt ::= - apply xpull_hprop'; [ intro ]. - -Ltac xpull_hexists tt ::= - apply xpull_hexists'; [ intro ]. - -Ltac xpull_step tt ::= - let go HP := - match HP with _ \* ?HN => - match HN with - | ?H \* _ => - match H with - | \[] => apply xpull_empty - | \[_] => xpull_hprop tt - | hexists _ => xpull_hexists tt - | _ ~> Id _ => xpull_id tt - | _ \* _ => apply xpull_assoc - | _ => apply xpull_keep - end - | \[] => fail 1 - | _ => apply xpull_starify - end end in - on_formula_pre ltac:(go). - - (* ********************************************************************** *) (* * Formalisation of higher-order iterator on a reference *) diff --git a/model/LambdaSepRO.v b/model/LambdaSepRO.v index 8674f58e256bf64c0f4f10c4f5abdeb8c4aa48de..a92ab5dc00f18140c0ec998152736600e38c8ec5 100644 --- a/model/LambdaSepRO.v +++ b/model/LambdaSepRO.v @@ -1099,7 +1099,7 @@ Proof using. Qed. (* ---------------------------------------------------------------------- *) -(* ** Customizing xpull *) +(* ** Customizing xpull for RO triples, which are not local *) Lemma xpull_hprop (H1 H2 : hprop) (P : Prop) (Q : val -> hprop) (t : trm) : (P -> triple t (H1 \* H2) Q) -> triple t (H1 \* \[P] \* H2) Q. @@ -1119,8 +1119,30 @@ Lemma xpull_id A (x X : A) (H1 H2 : hprop) (Q : val -> hprop) (t : trm) : Proof using. intros. rewrite repr_eq. apply xpull_hprop. auto. Qed. Ltac xpull_hprop tt ::= apply xpull_hprop; intro. -Ltac xpull_hexists tt := apply xpull_hexists; intro. -Ltac xpull_id tt := apply xpull_id; intro. +Ltac xpull_hexists tt ::= apply xpull_hexists; intro. +Ltac xpull_id tt ::= apply xpull_id; intro. + +(* ---------------------------------------------------------------------- *) +(* ** Customizing xchange for RO triples, which are not local *) + +Lemma xchange_lemma' : forall H1 H1' H2 t H Q, + (H1 ==> H1') -> + (H ==> H1 \* H2) -> + triple t (H1' \* H2) Q -> + triple t H Q. +Proof using. + introv W1 W2 M. applys~ rule_consequence M. + hchange W2. hchanges W1. +Qed. + +Ltac xchange_apply L cont1 cont2 ::= + eapply xchange_lemma'; + [ applys L | cont1 tt | cont2 tt (*xtag_pre_post*) ]. + +Ltac xchange_with_core cont1 cont2 H H' ::= + eapply xchange_lemma' with (H1:=H) (H1':=H'); + [ | cont1 tt | cont2 tt (* xtag_pre_post*) ]. + (* ---------------------------------------------------------------------- *) (* ** Term rules *)