Commit 63c020e4 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More consistent naming for frame preserving updates.

parent 9d629ec8
...@@ -318,17 +318,17 @@ Proof. ...@@ -318,17 +318,17 @@ Proof.
* by intros Hx z ?; exists y; split; [done|apply (Hx z)]. * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
* by intros Hx z n ?; destruct (Hx z n) as (?&<-&?). * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
Qed. Qed.
Lemma ra_updateP_id (P : A Prop) x : P x x : P. Lemma cmra_updateP_id (P : A Prop) x : P x x : P.
Proof. by intros ? z n ?; exists x. Qed. Proof. by intros ? z n ?; exists x. Qed.
Lemma ra_updateP_compose (P Q : A Prop) x : Lemma cmra_updateP_compose (P Q : A Prop) x :
x : P ( y, P y y : Q) x : Q. x : P ( y, P y y : Q) x : Q.
Proof. Proof.
intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y). intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y).
Qed. Qed.
Lemma ra_updateP_weaken (P Q : A Prop) x : x : P ( y, P y Q y) x : Q. Lemma cmra_updateP_weaken (P Q : A Prop) x : x : P ( y, P y Q y) x : Q.
Proof. eauto using ra_updateP_compose, ra_updateP_id. Qed. Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
Lemma ra_updateP_op (P1 P2 Q : A Prop) x1 x2 : Lemma cmra_updateP_op (P1 P2 Q : A Prop) x1 x2 :
x1 : P1 x2 : P2 ( y1 y2, P1 y1 P2 y2 Q (y1 y2)) x1 x2 : Q. x1 : P1 x2 : P2 ( y1 y2, P1 y1 P2 y2 Q (y1 y2)) x1 x2 : Q.
Proof. Proof.
intros Hx1 Hx2 Hy z n ?. intros Hx1 Hx2 Hy z n ?.
...@@ -337,9 +337,12 @@ Proof. ...@@ -337,9 +337,12 @@ Proof.
first by rewrite associative (commutative _ x2) -associative. first by rewrite associative (commutative _ x2) -associative.
exists (y1 y2); split; last rewrite (commutative _ y1) -associative; auto. exists (y1 y2); split; last rewrite (commutative _ y1) -associative; auto.
Qed. Qed.
Lemma ra_update_op x1 x2 y1 y2 : x1 y1 x2 y2 x1 x2 y1 y2. Lemma cmra_updateP_op' (P1 P2 : A Prop) x1 x2 :
x1 : P1 x2 : P2 x1 x2 : λ y, y1 y2, y = y1 y2 P1 y1 P2 y2.
Proof. eauto 10 using cmra_updateP_op. Qed.
Lemma cmra_update_op x1 x2 y1 y2 : x1 y1 x2 y2 x1 x2 y1 y2.
Proof. Proof.
rewrite !cmra_update_updateP; eauto using ra_updateP_op with congruence. rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed. Qed.
End cmra. End cmra.
...@@ -487,13 +490,16 @@ Section prod. ...@@ -487,13 +490,16 @@ Section prod.
Qed. Qed.
Lemma prod_update x y : x.1 y.1 x.2 y.2 x y. Lemma prod_update x y : x.1 y.1 x.2 y.2 x y.
Proof. intros ?? z n [??]; split; simpl in *; auto. Qed. Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
Lemma prod_updateP (P : A * B Prop) P1 P2 x : Lemma prod_updateP P1 P2 (Q : A * B Prop) x :
x.1 : P1 x.2 : P2 ( a b, P1 a P2 b P (a,b)) x : P. x.1 : P1 x.2 : P2 ( a b, P1 a P2 b Q (a,b)) x : Q.
Proof. Proof.
intros Hx1 Hx2 HP z n [??]; simpl in *. intros Hx1 Hx2 HP z n [??]; simpl in *.
destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto. destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto.
exists (a,b); repeat split; auto. exists (a,b); repeat split; auto.
Qed. Qed.
Lemma prod_updateP' P1 P2 x :
x.1 : P1 x.2 : P2 x : λ y, P1 (y.1) P2 (y.2).
Proof. eauto using prod_updateP. Qed.
End prod. End prod.
Arguments prodRA : clear implicits. Arguments prodRA : clear implicits.
......
...@@ -147,10 +147,12 @@ Proof. ...@@ -147,10 +147,12 @@ Proof.
destruct (Hx (unit x) n) as (y'&?&?); rewrite ?cmra_unit_r; auto. destruct (Hx (unit x) n) as (y'&?&?); rewrite ?cmra_unit_r; auto.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)]. by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
Qed. Qed.
Lemma option_updateP' (P : A Prop) x :
x : P Some x : λ y, default False y P.
Proof. eauto using option_updateP. Qed.
Lemma option_update x y : x y Some x Some y. Lemma option_update x y : x y Some x Some y.
Proof. Proof.
intros; apply cmra_update_updateP, (option_updateP (y=)); [|naive_solver]. rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
by apply cmra_update_updateP.
Qed. Qed.
End cmra. End cmra.
......
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