Commit 04487e21 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Move xchanfge stuff in LambdaSepRO.

parent 0f47daa3
......@@ -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 *)
......
......@@ -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 *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment