diff --git a/_CoqProject b/_CoqProject
index 39a1644d83ddf7e0137f2869f919ea58c0f81a72..3bc088664ebc0c5293bd30f2f4cf0454a7b68b60 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,8 @@ prelude/list.v
prelude/error.v
modures/option.v
modures/cmra.v
+modures/cmra_big_op.v
+modures/cmra_tactics.v
modures/sts.v
modures/auth.v
modures/fin_maps.v
@@ -45,7 +47,6 @@ modures/base.v
modures/dra.v
modures/cofe_solver.v
modures/agree.v
-modures/ra.v
modures/excl.v
iris/model.v
iris/adequacy.v
diff --git a/barrier/parameter.v b/barrier/parameter.v
index c3d21e55241b3108804e13ade1ef59a5bc1d7e1e..36a209edead4520b696db75c52adb784cb698341 100644
--- a/barrier/parameter.v
+++ b/barrier/parameter.v
@@ -1,4 +1,4 @@
Require Export barrier.heap_lang.
Require Import iris.parameter.
-Definition Σ := IParamConst heap_lang unitRA.
+Definition Σ := iParam_const heap_lang unitRA.
diff --git a/iris/adequacy.v b/iris/adequacy.v
index fed684c55fbd145eb1fb5828409bf9ce6f2a17a3..639e09a37cba459ccaff9b26074900ca9d208ae2 100644
--- a/iris/adequacy.v
+++ b/iris/adequacy.v
@@ -46,7 +46,7 @@ Proof.
* apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
{ rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le.
- apply uPred_weaken with r2 (k + n); eauto using @ra_included_l. }
+ apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
@@ -60,7 +60,7 @@ Proof.
intros Hht ????; apply (nsteps_wptp [pvs coPset_all coPset_all ∘ Q] k n
([e1],σ1) (t2,σ2) [r1]); rewrite /big_op ?right_id; auto.
constructor; last constructor.
- apply Hht with r1 (k + n); eauto using @ra_included_unit.
+ apply Hht with r1 (k + n); eauto using cmra_included_unit.
by destruct (k + n).
Qed.
Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
@@ -70,15 +70,16 @@ Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
∃ rs2 Qs', wptp 3 t2 ((λ v, pvs coPset_all coPset_all (Q v)) :: Qs') rs2 ∧
wsat 3 coPset_all σ2 (big_op rs2).
Proof.
- intros Hv ? [k ?]%rtc_nsteps. eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
- - by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN.
- - exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m). split_ands.
- + by rewrite /op /cmra_op /= /res_op /= !ra_empty_l ra_empty_r.
- + by rewrite /uPred_holds /=.
- + by apply ownG_spec.
+ intros Hv ? [k ?]%rtc_nsteps.
+ eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
+ { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
+ exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m); split_ands.
+ * by rewrite Res_op ?left_id ?right_id.
+ * by rewrite /uPred_holds /=.
+ * by apply ownG_spec.
Qed.
Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
- ✓m →
+ ✓ m →
{{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■φ v' }} →
rtc step ([e], σ1) (of_val v :: t2, σ2) →
φ v.
@@ -92,7 +93,7 @@ Proof.
by rewrite right_id_L.
Qed.
Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
- ✓m →
+ ✓ m →
{{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
rtc step ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
@@ -106,7 +107,7 @@ Proof.
rewrite ?right_id_L ?big_op_delete; auto.
Qed.
Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
- ✓m →
+ ✓ m →
{{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
rtc step ([e1], σ1) (t2, σ2) →
Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
diff --git a/iris/ownership.v b/iris/ownership.v
index 2e2c1c3a32773f181660fdc728a571109dfad978..a42e3de4985702d9a2c1a3a8334f1b3a6b69ddb0 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -27,7 +27,8 @@ Proof.
Qed.
Lemma always_inv i P : (□ inv i P)%I ≡ inv i P.
Proof.
- by apply uPred.always_own; rewrite Res_unit !ra_unit_empty map_unit_singleton.
+ apply uPred.always_own.
+ by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
Qed.
Global Instance inv_always_stable i P : AlwaysStable (inv i P).
Proof. by rewrite /AlwaysStable always_inv. Qed.
@@ -51,7 +52,8 @@ Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
Proof.
- by apply uPred.always_own; rewrite Res_unit !ra_unit_empty ra_unit_idempotent.
+ apply uPred.always_own.
+ by rewrite Res_unit !cmra_unit_empty cmra_unit_idempotent.
Qed.
Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
@@ -69,15 +71,15 @@ Proof.
* intros [(P'&Hi&HP) _]; rewrite Hi.
by apply Some_dist, symmetry, agree_valid_includedN,
(cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
- * intros ?; split_ands; try apply cmra_empty_least; eauto.
+ * intros ?; split_ands; try apply cmra_empty_leastN; eauto.
Qed.
Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ={n}= Excl σ.
Proof.
intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
- naive_solver (apply cmra_empty_least).
+ naive_solver (apply cmra_empty_leastN).
Qed.
Lemma ownG_spec r n m : (ownG m) n r ↔ m ≼{n} gst r.
Proof.
- rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_least).
+ rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
Qed.
End ownership.
diff --git a/iris/parameter.v b/iris/parameter.v
index cfbf73ee39c65de9138adace5faa06ee88e87e32..61d12438b426c53639965944b891c268a08514ff 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -7,8 +7,7 @@ Record iParam := IParam {
ilanguage : Language iexpr ival istate;
icmra : cofeT → cmraT;
icmra_empty A : Empty (icmra A);
- icmra_empty_spec A : RAIdentity (icmra A);
- icmra_empty_timeless A : Timeless (∅ : icmra A);
+ icmra_identity A : CMRAIdentity (icmra A);
icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x ≡ x;
@@ -16,10 +15,10 @@ Record iParam := IParam {
icmra_map (g ◎ f) x ≡ icmra_map g (icmra_map f x);
icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
}.
-Arguments IParam {_ _ _} ilanguage icmra {_ _ _} _ {_ _ _ _}.
Existing Instances ilanguage.
-Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
+Existing Instances icmra_empty icmra_identity.
Existing Instances icmra_map_ne icmra_map_mono.
+Canonical Structure istateC Σ := leibnizC (istate Σ).
Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
(∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.
@@ -27,15 +26,12 @@ Proof.
by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
Qed.
-Canonical Structure istateC Σ := leibnizC (istate Σ).
-
-Definition IParamConst {iexpr ival istate : Type}
- (ilanguage : Language iexpr ival istate)
- (icmra : cmraT) {icmra_empty : Empty icmra}
- {icmra_empty_spec : RAIdentity icmra} {icmra_empty_timeless: Timeless (∅ : icmra)}:
- iParam.
-eapply (IParam ilanguage (fun _ => icmra) (fun _ _ _ => cid)).
-Unshelve.
-- by intros.
-- by intros.
-Defined.
+Program Definition iParam_const {iexpr ival istate : Type}
+ (ilanguage : Language iexpr ival istate)
+ (icmra : cmraT)
+ {icmra_empty : Empty icmra} {icmra_identity : CMRAIdentity icmra} : iParam :=
+{|
+ iexpr := iexpr; ival := ival; istate := istate;
+ icmra A := icmra; icmra_map A B f := cid
+|}.
+Solve Obligations with done.
\ No newline at end of file
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index 81ee2f4eec368916dff1dd9f5a644d6597aa6a31..ad3ac04c7110076ff64fdf21421b9fcebb89c26a 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -21,7 +21,7 @@ Next Obligation.
intros Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto.
exists (r' â‹… r3); rewrite -(associative _); split; last done.
- apply uPred_weaken with r' k; eauto using @ra_included_l.
+ apply uPred_weaken with r' k; eauto using cmra_included_l.
Qed.
Arguments pvs {_} _ _ _%I : simpl never.
Instance: Params (@pvs) 3.
@@ -55,7 +55,7 @@ Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ pvs E E P.
Proof.
rewrite uPred.timelessP_spec=> HP r [|n] ? HP' rf k Ef σ ???; first lia.
exists r; split; last done.
- apply HP, uPred_weaken with r n; eauto using cmra_valid_le.
+ apply HP, uPred_weaken with r n; eauto using cmra_validN_le.
Qed.
Lemma pvs_trans E1 E2 E3 P :
E2 ⊆ E1 ∪ E3 → pvs E1 E2 (pvs E2 E3 P) ⊑ pvs E1 E3 P.
@@ -85,7 +85,7 @@ Proof.
destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
exists (rP â‹… r); split; last by rewrite (left_id_L _ _) -(associative _).
- eapply uPred_weaken with rP (S k); eauto using @ra_included_l.
+ eapply uPred_weaken with rP (S k); eauto using cmra_included_l.
Qed.
Lemma pvs_close i P : (inv i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
Proof.
@@ -101,7 +101,7 @@ Lemma pvs_updateP E m (P : iGst Σ → Prop) :
Proof.
intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P)
- as (m'&?&?); eauto using cmra_included_le.
+ as (m'&?&?); eauto using cmra_includedN_le.
by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■(i ∈ E) ∧ inv i P).
@@ -114,6 +114,7 @@ Proof.
Qed.
(* Derived rules *)
+Opaque uPred_holds.
Import uPred.
Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
diff --git a/iris/resources.v b/iris/resources.v
index 067b47e22eb219dccc9386f73c6d5fa2f3132875..a8a37647d5907bf064be6d2df757446e3b8a05d8 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -77,7 +77,6 @@ Instance res_op : Op (res Σ A) := λ r1 r2,
Global Instance res_empty : Empty (res Σ A) := Res ∅ ∅ ∅.
Instance res_unit : Unit (res Σ A) := λ r,
Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
-Instance res_valid : Valid (res Σ A) := λ r, ✓ (wld r) ∧ ✓ (pst r) ∧ ✓ (gst r).
Instance res_validN : ValidN (res Σ A) := λ n r,
✓{n} (wld r) ∧ ✓{n} (pst r) ∧ ✓{n} (gst r).
Instance res_minus : Minus (res Σ A) := λ r1 r2,
@@ -105,25 +104,18 @@ Proof.
* by intros n [???] ? [???] [???] ? [???];
constructor; simpl in *; cofe_subst.
* done.
- * by intros n ? (?&?&?); split_ands'; apply cmra_valid_S.
- * intros r; unfold valid, res_valid, validN, res_validN.
- rewrite !cmra_valid_validN; naive_solver.
+ * by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
* intros ???; constructor; simpl; apply (associative _).
* intros ??; constructor; simpl; apply (commutative _).
- * intros ?; constructor; simpl; apply ra_unit_l.
- * intros ?; constructor; simpl; apply ra_unit_idempotent.
+ * intros ?; constructor; simpl; apply cmra_unit_l.
+ * intros ?; constructor; simpl; apply cmra_unit_idempotent.
* intros n r1 r2; rewrite !res_includedN.
- by intros (?&?&?); split_ands'; apply cmra_unit_preserving.
+ by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
* intros n r1 r2 (?&?&?);
- split_ands'; simpl in *; eapply cmra_valid_op_l; eauto.
+ split_ands'; simpl in *; eapply cmra_validN_op_l; eauto.
* intros n r1 r2; rewrite res_includedN; intros (?&?&?).
by constructor; apply cmra_op_minus.
Qed.
-Global Instance res_ra_empty : RAIdentity (res Σ A).
-Proof.
- by repeat split; simpl; repeat apply ra_empty_valid; rewrite (left_id _ _).
-Qed.
-
Definition res_cmra_extend_mixin : CMRAExtendMixin (res Σ A).
Proof.
intros n r r1 r2 (?&?&?) [???]; simpl in *.
@@ -134,6 +126,13 @@ Proof.
Qed.
Canonical Structure resRA : cmraT :=
CMRAT res_cofe_mixin res_cmra_mixin res_cmra_extend_mixin.
+Global Instance res_cmra_identity : CMRAIdentity resRA.
+Proof.
+ split.
+ * intros n; split_ands'; apply cmra_empty_valid.
+ * by split; rewrite /= (left_id _ _).
+ * apply _.
+Qed.
Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
Res (wld r) (Excl σ) (gst r).
@@ -153,7 +152,7 @@ Lemma lookup_wld_op_l n r1 r2 i P :
✓{n} (r1⋅r2) → wld r1 !! i ={n}= Some P → (wld r1 ⋅ wld r2) !! i ={n}= Some P.
Proof.
move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
- destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?(right_id _ _) // =>-> ?.
+ destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
by constructor; rewrite (agree_op_inv P P') // agree_idempotent.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
@@ -189,11 +188,12 @@ Proof.
by rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
* by rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
Qed.
-Lemma res_map_ext {Σ A B} (f g : A -n> B) :
- (∀ r, f r ≡ g r) -> ∀ r : res Σ A, res_map f r ≡ res_map g r.
+Lemma res_map_ext {Σ A B} (f g : A -n> B) (r : res Σ A) :
+ (∀ x, f x ≡ g x) → res_map f r ≡ res_map g r.
Proof.
- move=>H r. split; simpl;
- [apply map_fmap_setoid_ext; intros; apply agree_map_ext | | apply icmra_map_ext]; done.
+ intros Hfg; split; simpl; auto.
+ * by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
+ * by apply icmra_map_ext.
Qed.
Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
CofeMor (res_map f : resRA Σ A → resRA Σ B).
@@ -205,10 +205,9 @@ Proof.
intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
* by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
Qed.
-Lemma resRA_map_ne {Σ A B} (f g : A -n> B) n :
- f ={n}= g → resRA_map (Σ := Σ) f ={n}= resRA_map g.
+Instance resRA_map_ne {Σ A B} n : Proper (dist n ==> dist n) (@resRA_map Σ A B).
Proof.
- intros ? r. split; simpl;
- [apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne
- | | apply icmra_map_ne]; done.
+ intros f g Hfg r; split; simpl; auto.
+ * by apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne.
+ * by apply icmra_map_ne.
Qed.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 6c7d9a87f6567692b1396f079190a97ff2601264..b898dd059a91d701bb6c822b8e879b599863a8b8 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -47,10 +47,10 @@ Next Obligation.
* constructor; eauto using uPred_weaken.
* intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep];
- rewrite ?(associative _) -?Hr; auto; constructor; [done|].
+ rewrite ?associative -?Hr; auto; constructor; [done|].
intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
- exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), @ra_included_l.
- by rewrite -!(associative _) (associative _ r2).
+ exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), cmra_included_l.
+ by rewrite -!associative (associative _ r2).
Qed.
Instance: Params (@wp) 3.
@@ -70,7 +70,7 @@ Proof.
destruct 3 as [|n' r e1 ? Hgo]; constructor; eauto.
intros rf k Ef σ1 ???.
assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
- { by rewrite (associative_L _) -union_difference_L. }
+ { by rewrite associative_L -union_difference_L. }
destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
@@ -143,7 +143,7 @@ Proof.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_ands; auto.
* by rewrite -(associative _ r2)
- (commutative _ rR) !(associative _) -(associative _ _ rR).
+ (commutative _ rR) !associative -(associative _ _ rR).
* apply IH; eauto using uPred_weaken.
Qed.
Lemma wp_frame_later_r E e Q R :
@@ -157,7 +157,7 @@ Proof.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_ands; auto.
* by rewrite -(associative _ r2)
- (commutative _ rR) !(associative _) -(associative _ _ rR).
+ (commutative _ rR) !associative -(associative _ _ rR).
* apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
eapply uPred_weaken with rR n; eauto.
Qed.
@@ -182,13 +182,8 @@ Import uPred.
Global Instance wp_mono' E e :
Proper (pointwise_relation _ (⊑) ==> (⊑)) (wp E e).
Proof. by intros Q Q' ?; apply wp_mono. Qed.
-Lemma wp_value' E Q e v :
- to_val e = Some v →
- Q v ⊑ wp E e Q.
-Proof.
- intros Hv. apply of_to_val in Hv.
- rewrite -Hv. by apply wp_value.
-Qed.
+Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
+Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
Lemma wp_frame_later_l E e Q R :
@@ -209,5 +204,5 @@ Proof.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2.
-Proof. by rewrite (commutative _) wp_impl_l. Qed.
+Proof. by rewrite commutative wp_impl_l. Qed.
End wp.
diff --git a/iris/wsat.v b/iris/wsat.v
index 7a8a38e5181da22e371aef8ca5f229de41ccc52a..69e82df1cf007c2d4bdf1f2fc8b2d55833c6e6f7 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -1,4 +1,5 @@
Require Export iris.model prelude.co_pset.
+Require Export modures.cmra_big_op modures.cmra_tactics.
Local Hint Extern 10 (_ ≤ _) => omega.
Local Hint Extern 10 (✓{_} _) => solve_validN.
Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
@@ -60,8 +61,8 @@ Proof.
Qed.
Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r.
Proof.
- destruct n; [intros; apply cmra_valid_0|intros [rs ?]].
- eapply cmra_valid_op_l, wsat_pre_valid; eauto.
+ destruct n; [done|intros [rs ?]].
+ eapply cmra_validN_op_l, wsat_pre_valid; eauto.
Qed.
Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl σ) m).
Proof.
@@ -70,7 +71,7 @@ Proof.
split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
constructor || apply Hv.
* by intros i; rewrite lookup_empty=>-[??].
- * intros i P ?; rewrite /= (left_id _ _) lookup_empty; inversion_clear 1.
+ * intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Qed.
Lemma wsat_open n E σ r i P :
wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
@@ -79,7 +80,7 @@ Proof.
intros HiP Hi [rs [Hval Hσ HE Hwld]].
destruct (Hwld i P) as (rP&?&?); [solve_elem_of +|by apply lookup_wld_op_l|].
assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
- { by rewrite (commutative _ rP) -(associative _) big_opM_delete. }
+ { by rewrite (commutative _ rP) -associative big_opM_delete. }
exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto.
* intros j; rewrite lookup_delete_is_Some Hr.
generalize (HE j); solve_elem_of +Hi.
@@ -94,7 +95,7 @@ Proof.
intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver).
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
- { by rewrite (commutative _ rP) -(associative _) big_opM_insert. }
+ { by rewrite (commutative _ rP) -associative big_opM_insert. }
exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
* intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ rewrite !lookup_op HiP !op_is_Some; solve_elem_of -.
@@ -113,13 +114,13 @@ Lemma wsat_update_pst n E σ1 σ1' r rf :
Proof.
intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
- { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r (associative _). }
+ { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r associative. }
assert (σ1' = σ1) as ->.
{ apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
apply (injective Excl).
- by rewrite -Hpst_r -Hpst -(associative _) Hpst' (right_id _). }
+ by rewrite -Hpst_r -Hpst -associative Hpst' (right_id _). }
split; [done|exists rs].
- by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
+ by constructor; split_ands'; try (rewrite /= -associative Hpst').
Qed.
Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) :
m1 ≼{S n} gst r → m1 â‡: P →
@@ -148,24 +149,24 @@ Proof.
{ apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'.
rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
- { by rewrite (commutative _ rP) -(associative _) big_opM_insert. }
+ { by rewrite (commutative _ rP) -associative big_opM_insert. }
exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
- * destruct Hval as (?&?&?); rewrite -(associative _) Hr.
- split_ands'; rewrite /= ?(left_id _ _); [|eauto|eauto].
+ * destruct Hval as (?&?&?); rewrite -associative Hr.
+ split_ands'; rewrite /= ?left_id; [|eauto|eauto].
intros j; destruct (decide (j = i)) as [->|].
+ by rewrite !lookup_op Hri HrPi Hrsi !(right_id _ _) lookup_singleton.
+ by rewrite lookup_op lookup_singleton_ne // (left_id _ _).
- * by rewrite -(associative _) Hr /= (left_id _ _).
- * intros j; rewrite -(associative _) Hr; destruct (decide (j = i)) as [->|].
+ * by rewrite -associative Hr /= left_id.
+ * intros j; rewrite -associative Hr; destruct (decide (j = i)) as [->|].
+ rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi.
+ rewrite lookup_insert_ne //.
- rewrite lookup_op lookup_singleton_ne // (left_id _ _); eauto.
- * intros j P'; rewrite -(associative _) Hr; destruct (decide (j=i)) as [->|].
- + rewrite /= !lookup_op Hri HrPi Hrsi (right_id _ _) lookup_singleton=>? HP.
+ rewrite lookup_op lookup_singleton_ne // left_id; eauto.
+ * intros j P'; rewrite -associative Hr; destruct (decide (j=i)) as [->|].
+ + rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
apply (injective Some), (injective to_agree),
(injective Later), (injective iProp_unfold) in HP.
exists rP; rewrite lookup_insert; split; [|apply HP]; auto.
- + rewrite /= lookup_op lookup_singleton_ne // (left_id _ _)=> ??.
+ + rewrite /= lookup_op lookup_singleton_ne // left_id=> ??.
destruct (Hwld j P') as [r' ?]; auto.
by exists r'; rewrite lookup_insert_ne.
Qed.
diff --git a/modures/agree.v b/modures/agree.v
index 212be59d339a148b11c1dc3c4f0392cec6fa5bc5..bceadd5189d4bc01d34855af417e1727f20a3fbc 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -19,7 +19,6 @@ Instance agree_validN : ValidN (agree A) := λ n x,
Lemma agree_valid_le (x : agree A) n n' :
agree_is_valid x n → n' ≤ n → agree_is_valid x n'.
Proof. induction 2; eauto using agree_valid_S. Qed.
-Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Instance agree_equiv : Equiv (agree A) := λ x y,
(∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
(∀ n, agree_is_valid x n → x n ={n}= y n).
diff --git a/modures/auth.v b/modures/auth.v
index a860a0b9b9ef63475de6e81c9c0dc51cf893e4f7..9096b46a9ad3efc112a4491c22603626c0ba7ad8 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -1,5 +1,4 @@
Require Export modures.excl.
-Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -57,13 +56,6 @@ Section cmra.
Context {A : cmraT}.
Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
-Instance auth_valid : Valid (auth A) := λ x,
- match authoritative x with
- | Excl a => own x ≼ a ∧ ✓ a
- | ExclUnit => ✓ (own x)
- | ExclBot => False
- end.
-Global Arguments auth_valid !_ /.
Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
| Excl a => own x ≼{n} a ∧ ✓{n} a
@@ -92,7 +84,7 @@ Qed.
Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} (authoritative x).
Proof. by destruct x as [[]]. Qed.
Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} (own x).
-Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
+Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
Definition auth_cmra_mixin : CMRAMixin (auth A).
Proof.
@@ -104,20 +96,17 @@ Proof.
* by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
* by intros [[] ?]; simpl.
- * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
- * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN
- ?cmra_valid_validN; [naive_solver|naive_solver|].
- split; [done|intros Hn; discriminate (Hn 1)].
- * by split; simpl; rewrite (associative _).
- * by split; simpl; rewrite (commutative _).
- * by split; simpl; rewrite ?(ra_unit_l _).
- * by split; simpl; rewrite ?(ra_unit_idempotent _).
+ * intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
+ * by split; simpl; rewrite associative.
+ * by split; simpl; rewrite commutative.
+ * by split; simpl; rewrite ?cmra_unit_l.
+ * by split; simpl; rewrite ?cmra_unit_idempotent.
* intros n ??; rewrite! auth_includedN; intros [??].
- by split; simpl; apply cmra_unit_preserving.
+ by split; simpl; apply cmra_unit_preservingN.
* assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
- { intros n a b1 b2 <-; apply cmra_included_l. }
+ { intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[a1| |] b1] [[a2| |] b2];
- naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
+ naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
* by intros n ??; rewrite auth_includedN;
intros [??]; split; simpl; apply cmra_op_minus.
Qed.
@@ -132,10 +121,12 @@ Proof.
Qed.
Canonical Structure authRA : cmraT :=
CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
-Instance auth_ra_empty `{Empty A} : RAIdentity A → RAIdentity (auth A).
+Instance auth_cmra_identity `{Empty A} : CMRAIdentity A → CMRAIdentity authRA.
Proof.
- split; simpl; [apply ra_empty_valid|].
- by intros x; constructor; simpl; rewrite (left_id _ _).
+ split; simpl.
+ * by apply (@cmra_empty_valid A _).
+ * by intros x; constructor; rewrite /= left_id.
+ * apply Auth_timeless; apply _.
Qed.
Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
diff --git a/modures/cmra.v b/modures/cmra.v
index 39ea086c82a135ef625896f8088e57e78a7fbc1b..ed96b1f5894667589fc129f3a1ea1fb8d2586d62 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -1,33 +1,54 @@
-Require Export modures.ra modures.cofe.
+Require Export modures.cofe.
+
+Class Unit (A : Type) := unit : A → A.
+Instance: Params (@unit) 2.
+
+Class Op (A : Type) := op : A → A → A.
+Instance: Params (@op) 2.
+Infix "â‹…" := op (at level 50, left associativity) : C_scope.
+Notation "(â‹…)" := op (only parsing) : C_scope.
+
+Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
+Infix "≼" := included (at level 70) : C_scope.
+Notation "(≼)" := included (only parsing) : C_scope.
+Hint Extern 0 (?x ≼ ?y) => reflexivity.
+Instance: Params (@included) 3.
+
+Class Minus (A : Type) := minus : A → A → A.
+Instance: Params (@minus) 2.
+Infix "⩪" := minus (at level 40) : C_scope.
Class ValidN (A : Type) := validN : nat → A → Prop.
Instance: Params (@validN) 3.
Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
+Class Valid (A : Type) := valid : A → Prop.
+Instance: Params (@valid) 2.
+Notation "✓" := valid (at level 1).
+Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
+
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, format "x ≼{ n } y") : C_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (?x ≼{_} ?y) => reflexivity.
-Record CMRAMixin A
- `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
+Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
(* setoids *)
mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
- mixin_cmra_valid_ne n : Proper (dist n ==> impl) (✓{n});
+ mixin_cmra_validN_ne n : Proper (dist n ==> impl) (✓{n});
mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
(* valid *)
- mixin_cmra_valid_0 x : ✓{0} x;
- mixin_cmra_valid_S n x : ✓{S n} x → ✓{n} x;
- mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
+ mixin_cmra_validN_0 x : ✓{0} x;
+ mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
(* monoid *)
mixin_cmra_associative : Associative (≡) (⋅);
mixin_cmra_commutative : Commutative (≡) (⋅);
mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit x;
- mixin_cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y;
- mixin_cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
+ mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
+ mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y
}.
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2,
@@ -42,28 +63,26 @@ Structure cmraT := CMRAT {
cmra_compl : Compl cmra_car;
cmra_unit : Unit cmra_car;
cmra_op : Op cmra_car;
- cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_minus : Minus cmra_car;
cmra_cofe_mixin : CofeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car;
cmra_extend_mixin : CMRAExtendMixin cmra_car
}.
-Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _ _.
+Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _.
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_compl : simpl never.
Arguments cmra_unit : simpl never.
Arguments cmra_op : simpl never.
-Arguments cmra_valid : simpl never.
Arguments cmra_validN : simpl never.
Arguments cmra_minus : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Arguments cmra_extend_mixin : simpl never.
Add Printing Constructor cmraT.
-Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus.
+Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
@@ -75,21 +94,27 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _).
Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
- Global Instance cmra_valid_ne n : Proper (dist n ==> impl) (@validN A _ n).
- Proof. apply (mixin_cmra_valid_ne _ (cmra_mixin A)). Qed.
+ Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
+ Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
Global Instance cmra_minus_ne n :
Proper (dist n ==> dist n ==> dist n) (@minus A _).
Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
- Lemma cmra_valid_0 x : ✓{0} x.
- Proof. apply (mixin_cmra_valid_0 _ (cmra_mixin A)). Qed.
- Lemma cmra_valid_S n x : ✓{S n} x → ✓{n} x.
- Proof. apply (mixin_cmra_valid_S _ (cmra_mixin A)). Qed.
- Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
- Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
- Lemma cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y.
- Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
- Lemma cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
- Proof. apply (mixin_cmra_valid_op_l _ (cmra_mixin A)). Qed.
+ Lemma cmra_validN_0 x : ✓{0} x.
+ Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed.
+ Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
+ Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
+ Global Instance cmra_associative : Associative (≡) (@op A _).
+ Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed.
+ Global Instance cmra_commutative : Commutative (≡) (@op A _).
+ Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed.
+ Lemma cmra_unit_l x : unit x ⋅ x ≡ x.
+ Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
+ Lemma cmra_unit_idempotent x : unit (unit x) ≡ unit x.
+ Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed.
+ Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
+ Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed.
+ Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
+ Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y.
Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
Lemma cmra_extend_op n x y1 y2 :
@@ -98,22 +123,24 @@ Section cmra_mixin.
Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.
-Hint Extern 0 (✓{0} _) => apply cmra_valid_0.
+Hint Extern 0 (✓{0} _) => apply cmra_validN_0.
+
+(** * CMRAs with a global identity element *)
+(** We use the notation ∅ because for most instances (maps, sets, etc) the
+`empty' element is the global identity. *)
+Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
+ cmra_empty_valid : ✓ ∅;
+ cmra_empty_left_id :> LeftId (≡) ∅ (⋅);
+ cmra_empty_timeless :> Timeless ∅
+}.
(** * Morphisms *)
Class CMRAMonotone {A B : cmraT} (f : A → B) := {
includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
validN_preserving n x : ✓{n} x → ✓{n} (f x)
}.
-Instance compose_cmra_monotone {A B C : cmraT} (f : A -n> B) (g : B -n> C) :
- CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ◎ f).
-Proof.
- split.
- - move=> n x y Hxy /=. eapply includedN_preserving, includedN_preserving; done.
- - move=> n x Hx /=. eapply validN_preserving, validN_preserving; done.
-Qed.
-(** * Updates *)
+(** * Frame preserving updates *)
Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
Instance: Params (@cmra_updateP) 3.
@@ -127,41 +154,129 @@ Instance: Params (@cmra_update) 3.
Section cmra.
Context {A : cmraT}.
Implicit Types x y z : A.
+Implicit Types xs ys zs : list A.
+(** ** Setoids *)
+Global Instance cmra_unit_proper : Proper ((≡) ==> (≡)) (@unit A _).
+Proof. apply (ne_proper _). Qed.
+Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
+Proof.
+ intros x1 x2 Hx y1 y2 Hy.
+ by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
+Qed.
+Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
+Proof. apply (ne_proper_2 _). Qed.
+Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
+Proof. by split; apply cmra_validN_ne. Qed.
+Global Instance cmra_validN_proper : Proper ((≡) ==> iff) (@validN A _ n) | 1.
+Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
+Global Instance cmra_minus_proper : Proper ((≡) ==> (≡) ==> (≡)) (@minus A _).
+Proof. apply (ne_proper_2 _). Qed.
+
+Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
+Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed.
+Global Instance cmra_includedN_ne n :
+ Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
+Proof.
+ intros x x' Hx y y' Hy.
+ by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
+Qed.
+Global Instance cmra_includedN_proper n :
+ Proper ((≡) ==> (≡) ==> iff) (@includedN A _ _ n) | 1.
+Proof.
+ intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
+ by rewrite (Hx n) (Hy n).
+Qed.
+Global Instance cmra_included_proper :
+ Proper ((≡) ==> (≡) ==> iff) (@included A _ _) | 1.
+Proof.
+ intros x x' Hx y y' Hy.
+ by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
+Qed.
+
+(** ** Validity *)
+Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
+Proof. done. Qed.
+Lemma cmra_validN_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x.
+Proof. induction 2; eauto using cmra_validN_S. Qed.
+Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
+Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
+Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
+Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed.
+Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
+Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
+
+(** ** Units *)
+Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
+Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
+Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x.
+Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed.
+Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} (unit x).
+Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
+Lemma cmra_unit_valid x : ✓ x → ✓ (unit x).
+Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
+
+(** ** Order *)
Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
Proof.
split; [by intros [z Hz] n; exists z; rewrite Hz|].
intros Hxy; exists (y ⩪ x); apply equiv_dist; intros n.
symmetry; apply cmra_op_minus, Hxy.
Qed.
+Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
+Proof.
+ split.
+ * by intros x; exists (unit x); rewrite cmra_unit_r.
+ * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+ by rewrite (associative _) -Hy -Hz.
+Qed.
+Global Instance cmra_included_preorder: PreOrder (@included A _ _).
+Proof.
+ split; red; intros until 0; rewrite !cmra_included_includedN; first done.
+ intros; etransitivity; eauto.
+Qed.
+Lemma cmra_validN_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
+Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
+Lemma cmra_validN_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
+Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
+
+Lemma cmra_includedN_0 x y : x ≼{0} y.
+Proof. by exists (unit x). Qed.
+Lemma cmra_includedN_S x y n : x ≼{S n} y → x ≼{n} y.
+Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
+Lemma cmra_includedN_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y.
+Proof. induction 2; auto using cmra_includedN_S. Qed.
+
+Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y.
+Proof. by exists y. Qed.
+Lemma cmra_included_l x y : x ≼ x ⋅ y.
+Proof. by exists y. Qed.
+Lemma cmra_includedN_r n x y : y ≼{n} x ⋅ y.
+Proof. rewrite (commutative op); apply cmra_includedN_l. Qed.
+Lemma cmra_included_r x y : y ≼ x ⋅ y.
+Proof. rewrite (commutative op); apply cmra_included_l. Qed.
-Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (✓{n} : A → _) | 1.
-Proof. by split; apply cmra_valid_ne. Qed.
-Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (✓{n} : A → _) | 1.
-Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
-Global Instance cmra_ra : RA A.
+Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
+Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
+Lemma cmra_included_unit x : unit x ≼ x.
+Proof. by exists x; rewrite cmra_unit_l. Qed.
+Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
+Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.
+
+Lemma cmra_included_dist_l x1 x2 x1' n :
+ x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
Proof.
- split; try by (destruct (@cmra_mixin A);
- eauto using ne_proper, ne_proper_2 with typeclass_instances).
- * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
- * intros x y; rewrite !cmra_included_includedN.
- eauto using @cmra_unit_preserving.
- * intros x y; rewrite !cmra_valid_validN; intros ? n.
- by apply cmra_valid_op_l with y.
- * intros x y [z Hz]; apply equiv_dist; intros n.
- by apply cmra_op_minus; exists z; rewrite Hz.
+ intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using cmra_included_l.
+ by rewrite Hx1 Hx2.
Qed.
-Lemma cmra_valid_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
-Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
-Lemma cmra_valid_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x.
-Proof. induction 2; eauto using cmra_valid_S. Qed.
-Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (@op A _).
+
+(** ** Minus *)
+Lemma cmra_op_minus' x y : x ≼ y → x ⋅ y ⩪ x ≡ y.
Proof.
- intros x1 x2 Hx y1 y2 Hy.
- by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
+ rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
Qed.
-Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x).
-Proof. rewrite -{1}(ra_unit_l x); apply cmra_valid_op_l. Qed.
(** ** Timeless *)
Lemma cmra_timeless_included_l x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
@@ -177,68 +292,24 @@ Lemma cmra_op_timeless x1 x2 :
Proof.
intros ??? z Hz.
destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
- { by rewrite -?Hz; apply cmra_valid_validN. }
+ { by rewrite -?Hz. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
-(** ** Order *)
-Global Instance cmra_included_ne n :
- Proper (dist n ==> dist n ==> iff) (includedN n : relation A) | 1.
-Proof.
- intros x x' Hx y y' Hy; unfold includedN.
- by setoid_rewrite Hx; setoid_rewrite Hy.
-Qed.
-Global Instance cmra_included_proper :
- Proper ((≡) ==> (≡) ==> iff) (includedN n : relation A) | 1.
-Proof.
- intros n x x' Hx y y' Hy; unfold includedN.
- by setoid_rewrite Hx; setoid_rewrite Hy.
-Qed.
-Lemma cmra_included_0 x y : x ≼{0} y.
-Proof. by exists (unit x). Qed.
-Lemma cmra_included_S x y n : x ≼{S n} y → x ≼{n} y.
-Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
-Lemma cmra_included_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y.
-Proof. induction 2; auto using cmra_included_S. Qed.
+(** ** RAs with an empty element *)
+Section identity.
+ Context `{Empty A, !CMRAIdentity A}.
+ Lemma cmra_empty_leastN n x : ∅ ≼{n} x.
+ Proof. by exists x; rewrite left_id. Qed.
+ Lemma cmra_empty_least x : ∅ ≼ x.
+ Proof. by exists x; rewrite left_id. Qed.
+ Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅).
+ Proof. by intros x; rewrite (commutative op) left_id. Qed.
+ Lemma cmra_unit_empty : unit ∅ ≡ ∅.
+ Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
+End identity.
-Lemma cmra_included_l n x y : x ≼{n} x ⋅ y.
-Proof. by exists y. Qed.
-Lemma cmra_included_r n x y : y ≼{n} x ⋅ y.
-Proof. rewrite (commutative op); apply cmra_included_l. Qed.
-Global Instance cmra_included_ord n : PreOrder (includedN n : relation A).
-Proof.
- split.
- * by intros x; exists (unit x); rewrite ra_unit_r.
- * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite (associative _) -Hy -Hz.
-Qed.
-Lemma cmra_valid_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
-Proof. intros Hyv [z ?]; cofe_subst y; eauto using @cmra_valid_op_l. Qed.
-Lemma cmra_valid_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
-Proof. rewrite cmra_included_includedN; eauto using @cmra_valid_includedN. Qed.
-Lemma cmra_included_dist_l x1 x2 x1' n :
- x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
-Proof.
- intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using ra_included_l.
- by rewrite Hx1 Hx2.
-Qed.
-
-(** ** RAs with empty element *)
-Lemma cmra_empty_least `{Empty A, !RAIdentity A} n x : ∅ ≼{n} x.
-Proof. by exists x; rewrite (left_id _ _). Qed.
-
-(** ** big ops *)
-Section bigop.
- Context `{Empty A, !RAIdentity A, FinMap K M}.
- Lemma big_opM_lookup_valid n m i x :
- ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
- Proof.
- intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
- apply cmra_valid_op_l.
- Qed.
-End bigop.
-
-(** ** Properties of [(â‡)] relation *)
+(** ** Updates *)
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
Lemma cmra_update_updateP x y : x ⇠y ↔ x â‡: (y =).
@@ -249,59 +320,70 @@ Proof.
Qed.
End cmra.
-Hint Resolve cmra_ra.
-Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0.
-(* Also via [cmra_cofe; cofe_equivalence] *)
-Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
-
-(* Solver for validity *)
-Ltac solve_validN :=
- match goal with
- | H : ✓{?n} ?y |- ✓{?n'} ?x =>
- let Hn := fresh in let Hx := fresh in
- assert (n' ≤ n) as Hn by omega;
- assert (x ≼ y) as Hx by solve_included;
- eapply cmra_valid_le, Hn; eapply cmra_valid_included, Hx; apply H
- end.
+Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.
+(** * Properties about monotone functions *)
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Proof. by split. Qed.
-Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A → B) :
- CMRAMonotone f → RAMonotone f.
+Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
+ CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f).
Proof.
split.
- * intros x y; rewrite !cmra_included_includedN.
- by intros ? n; apply includedN_preserving.
- * intros x; rewrite !cmra_valid_validN.
- by intros ? n; apply validN_preserving.
+ * move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
+ * move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Qed.
-(** Discrete *)
+Section cmra_monotone.
+ Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}.
+ Lemma included_preserving x y : x ≼ y → f x ≼ f y.
+ Proof.
+ rewrite !cmra_included_includedN; eauto using includedN_preserving.
+ Qed.
+ Lemma valid_preserving x : ✓ x → ✓ (f x).
+ Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
+End cmra_monotone.
+
+(** * Instances *)
+(** ** Discrete CMRA *)
+Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
+ (* setoids *)
+ ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
+ ra_unit_ne :> Proper ((≡) ==> (≡)) unit;
+ ra_validN_ne :> Proper ((≡) ==> impl) ✓;
+ ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus;
+ (* monoid *)
+ ra_associative :> Associative (≡) (⋅);
+ ra_commutative :> Commutative (≡) (⋅);
+ ra_unit_l x : unit x ⋅ x ≡ x;
+ ra_unit_idempotent x : unit (unit x) ≡ unit x;
+ ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
+ ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
+ ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+}.
+
Section discrete.
- Context `{ra : RA A}.
- Existing Instances discrete_dist discrete_compl.
+ Context {A : cofeT} `{∀ x : A, Timeless x}.
+ Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
+
Instance discrete_validN : ValidN A := λ n x,
match n with 0 => True | S n => ✓ x end.
Definition discrete_cmra_mixin : CMRAMixin A.
Proof.
- split; try by (destruct ra; auto).
- * by intros [|n]; try apply ra_op_proper.
- * by intros [|n]; try apply ra_unit_proper.
- * by intros [|n]; try apply ra_valid_proper.
- * by intros [|n]; try apply ra_minus_proper.
- * by intros [|n].
- * intros x; split; intros Hvalid. by intros [|n]. apply (Hvalid 1).
- * by intros [|n]; try apply ra_unit_preserving.
- * by intros [|n]; try apply ra_valid_op_l.
- * by intros [|n] x y; try apply ra_op_minus.
+ destruct ra; split; unfold Proper, respectful, includedN;
+ repeat match goal with
+ | |- ∀ n : nat, _ => intros [|?]
+ end; try setoid_rewrite <-(timeless_S _ _ _ _); try done.
+ by intros x y ?; exists x.
Qed.
Definition discrete_extend_mixin : CMRAExtendMixin A.
Proof.
- intros [|n] x y1 y2 ??; [|by exists (y1,y2); rewrite /dist /discrete_dist].
- by exists (x,unit x); simpl; rewrite ra_unit_r.
+ intros [|n] x y1 y2 ??.
+ * by exists (unit x, x); rewrite /= ra_unit_l.
+ * exists (y1,y2); split_ands; auto.
+ apply (timeless _), dist_le with (S n); auto with lia.
Qed.
Definition discreteRA : cmraT :=
- CMRAT discrete_cofe_mixin discrete_cmra_mixin discrete_extend_mixin.
+ CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} :
(∀ z, ✓ (x â‹… z) → ∃ y, P y ∧ ✓ (y â‹… z)) → (x : discreteRA) â‡: P.
Proof.
@@ -312,18 +394,28 @@ Section discrete.
(∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → (x : discreteRA) ⇠y.
Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
End discrete.
-Arguments discreteRA _ {_ _ _ _ _ _}.
-(** CMRA for the unit type *)
-Canonical Structure unitRA : cmraT := discreteRA ().
+(** ** CMRA for the unit type *)
+Section unit.
+ Instance unit_valid : Valid () := λ x, True.
+ Instance unit_unit : Unit () := λ x, x.
+ Instance unit_op : Op () := λ x y, ().
+ Instance unit_minus : Minus () := λ x y, ().
+ Global Instance unit_empty : Empty () := ().
+ Definition unit_ra : RA ().
+ Proof. by split. Qed.
+ Canonical Structure unitRA : cmraT :=
+ Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
+ Global Instance unit_cmra_identity : CMRAIdentity unitRA.
+ Proof. by split; intros []. Qed.
+End unit.
-(** Product *)
+(** ** Product *)
Section prod.
Context {A B : cmraT}.
Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
- Instance prod_valid : Valid (A * B) := λ x, ✓ (x.1) ∧ ✓ (x.2).
Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} (x.1) ∧ ✓{n} (x.2).
Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2).
Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
@@ -344,25 +436,18 @@ Section prod.
* by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
* by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
- * split; apply cmra_valid_0.
- * by intros n x [??]; split; apply cmra_valid_S.
- * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
- intros Hvalid; split; apply cmra_valid_validN; intros n; apply Hvalid.
+ * by split.
+ * by intros n x [??]; split; apply cmra_validN_S.
* split; simpl; apply (associative _).
* split; simpl; apply (commutative _).
- * split; simpl; apply ra_unit_l.
- * split; simpl; apply ra_unit_idempotent.
+ * split; simpl; apply cmra_unit_l.
+ * split; simpl; apply cmra_unit_idempotent.
* intros n x y; rewrite !prod_includedN.
- by intros [??]; split; apply cmra_unit_preserving.
- * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
+ by intros [??]; split; apply cmra_unit_preservingN.
+ * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
* intros x y n; rewrite prod_includedN; intros [??].
by split; apply cmra_op_minus.
Qed.
- Global Instance prod_ra_empty `{Empty A, Empty B} :
- RAIdentity A → RAIdentity B → RAIdentity (A * B).
- Proof.
- repeat split; simpl; repeat (apply ra_empty_valid || apply (left_id _ _)).
- Qed.
Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
Proof.
intros n x y1 y2 [??] [??]; simpl in *.
@@ -372,6 +457,14 @@ Section prod.
Qed.
Canonical Structure prodRA : cmraT :=
CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin.
+ Global Instance prod_cmra_identity `{Empty A, Empty B} :
+ CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodRA.
+ Proof.
+ split.
+ * split; apply cmra_empty_valid.
+ * by split; rewrite /=left_id.
+ * by intros ? [??]; split; apply (timeless _).
+ Qed.
End prod.
Arguments prodRA : clear implicits.
diff --git a/modures/cmra_big_op.v b/modures/cmra_big_op.v
new file mode 100644
index 0000000000000000000000000000000000000000..c96118a095d009aa0644004294360c23c4392691
--- /dev/null
+++ b/modures/cmra_big_op.v
@@ -0,0 +1,80 @@
+Require Export modures.cmra.
+Require Import prelude.fin_maps.
+
+Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
+ match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
+Arguments big_op _ _ !_ /.
+Instance: Params (@big_op) 2.
+Definition big_opM {A : cmraT} `{FinMapToList K A M, Empty A} (m : M) : A :=
+ big_op (snd <$> map_to_list m).
+Instance: Params (@big_opM) 5.
+
+(** * Properties about big ops *)
+Section big_op.
+Context `{CMRAIdentity A}.
+
+(** * Big ops *)
+Lemma big_op_nil : big_op (@nil A) = ∅.
+Proof. done. Qed.
+Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
+Proof. done. Qed.
+Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
+Proof.
+ induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
+ * by rewrite IH.
+ * by rewrite !(associative _) (commutative _ x).
+ * by transitivity (big_op xs2).
+Qed.
+Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
+Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
+Proof.
+ induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
+ by rewrite IH (associative _).
+Qed.
+Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
+Proof.
+ induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
+ * by apply cmra_preserving_l.
+ * by rewrite !associative (commutative _ y).
+ * by transitivity (big_op ys); last apply cmra_included_r.
+ * by transitivity (big_op ys).
+Qed.
+Lemma big_op_delete xs i x :
+ xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
+Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
+
+Context `{FinMap K M}.
+Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
+Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
+Lemma big_opM_insert (m : M A) i x :
+ m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
+Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
+Lemma big_opM_delete (m : M A) i x :
+ m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
+Proof.
+ intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
+Qed.
+Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
+Proof.
+ rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
+ by rewrite big_opM_empty (right_id _ _).
+Qed.
+Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
+Proof.
+ intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
+ { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
+ intros m2 Hm2; rewrite big_opM_insert //.
+ rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
+ destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
+ as (y&?&Hxy); auto using lookup_insert.
+ rewrite Hxy -big_opM_insert; last auto using lookup_delete.
+ by rewrite insert_delete.
+Qed.
+Lemma big_opM_lookup_valid n m i x :
+ ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
+Proof.
+ intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
+ apply cmra_validN_op_l.
+Qed.
+End big_op.
diff --git a/modures/cmra_tactics.v b/modures/cmra_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..c2cce946a58e44e8b5fc5b43248471872fc56019
--- /dev/null
+++ b/modures/cmra_tactics.v
@@ -0,0 +1,66 @@
+Require Export modures.cmra.
+Require Import modures.cmra_big_op.
+
+(** * Simple solver for validity and inclusion by reflection *)
+Module ra_reflection. Section ra_reflection.
+ Context `{CMRAIdentity A}.
+
+ Inductive expr :=
+ | EVar : nat → expr
+ | EEmpty : expr
+ | EOp : expr → expr → expr.
+ Fixpoint eval (Σ : list A) (e : expr) : A :=
+ match e with
+ | EVar n => from_option ∅ (Σ !! n)
+ | EEmpty => ∅
+ | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
+ end.
+ Fixpoint flatten (e : expr) : list nat :=
+ match e with
+ | EVar n => [n]
+ | EEmpty => []
+ | EOp e1 e2 => flatten e1 ++ flatten e2
+ end.
+ Lemma eval_flatten Σ e :
+ eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
+ Proof.
+ by induction e as [| |e1 IH1 e2 IH2];
+ rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
+ Qed.
+ Lemma flatten_correct Σ e1 e2 :
+ flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
+ Proof.
+ by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
+ Qed.
+
+ Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
+ Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
+ Global Instance quote_var Σ1 Σ2 e i:
+ rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
+ Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
+ Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
+ End ra_reflection.
+
+ Ltac quote :=
+ match goal with
+ | |- @included _ _ _ ?x ?y =>
+ lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
+ lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
+ change (eval Σ3 e1 ≼ eval Σ3 e2)
+ end end
+ end.
+End ra_reflection.
+
+Ltac solve_included :=
+ ra_reflection.quote;
+ apply ra_reflection.flatten_correct, (bool_decide_unpack _);
+ vm_compute; apply I.
+
+Ltac solve_validN :=
+ match goal with
+ | H : ✓{?n} ?y |- ✓{?n'} ?x =>
+ let Hn := fresh in let Hx := fresh in
+ assert (n' ≤ n) as Hn by omega;
+ assert (x ≼ y) as Hx by solve_included;
+ eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
+ end.
diff --git a/modures/cofe.v b/modures/cofe.v
index b2c214a1e6f51762f2332220e37e10d5db7877d3..becd4395a9c335cf840a67d3365a311185d4ed1a 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -129,6 +129,11 @@ Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y → x ≡ y.
Arguments timeless {_} _ {_} _ _.
+Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ={S n}= y.
+Proof.
+ split; intros; [by apply equiv_dist|].
+ apply (timeless _), dist_le with (S n); auto with lia.
+Qed.
(** Fixpoint *)
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
diff --git a/modures/cofe_solver.v b/modures/cofe_solver.v
index 3ba4f641e7cb8b465acf81801c9614878596d269..977a6fdc5d6852f4986d93c370aa9cf12ad53bf8 100644
--- a/modures/cofe_solver.v
+++ b/modures/cofe_solver.v
@@ -34,7 +34,7 @@ Fixpoint A (k : nat) : cofeT :=
Fixpoint f {k} : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
with g {k} : A (S k) -n> A k :=
- match k with 0 => CofeMor (λ _, () : unitC) | S k => map (f,g) end.
+ match k with 0 => CofeMor (λ _, ()) | S k => map (f,g) end.
Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
Lemma gf {k} (x : A k) : g (f x) ≡ x.
diff --git a/modures/dra.v b/modures/dra.v
index 3bf9e306a24135b777f5d026cbf55373b9ed4510..4965a1264c755c7d96c8e9cb6e30ab6888165ff1 100644
--- a/modures/dra.v
+++ b/modures/dra.v
@@ -1,4 +1,4 @@
-Require Export modures.ra modures.cmra.
+Require Export modures.cmra.
(** From disjoint pcm *)
Record validity {A} (P : A → Prop) : Type := Validity {
@@ -99,10 +99,9 @@ Program Instance validity_minus : Minus T := λ x y,
(✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _.
Solve Obligations with naive_solver auto using dra_minus_valid.
-Instance validity_ra : RA T.
+Definition validity_ra : RA (discreteC T).
Proof.
split.
- * apply _.
* intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_ands';
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
@@ -130,11 +129,11 @@ Proof.
* intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
Qed.
-Definition validityRA : cmraT := discreteRA T.
+Definition validityRA : cmraT := discreteRA validity_ra.
Definition validity_update (x y : validityRA) :
(∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ⇠y.
Proof.
- intros Hxy; apply discrete_update.
+ intros Hxy. apply discrete_update.
intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
Qed.
End dra.
diff --git a/modures/excl.v b/modures/excl.v
index fdb667dcf84b9ea09b76d2e150f5fac09c83868e..795c2840d1b42fcae5f20fbad07c8f8fb84a71af 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -83,8 +83,6 @@ Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
(* CMRA *)
-Instance excl_valid : Valid (excl A) := λ x,
- match x with Excl _ | ExclUnit => True | ExclBot => False end.
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
Global Instance excl_empty : Empty (excl A) := ExclUnit.
@@ -110,8 +108,6 @@ Proof.
* by destruct 1; inversion_clear 1; constructor.
* by intros [].
* intros n [?| |]; simpl; auto with lia.
- * intros x; split; [by intros ? [|n]; destruct x|].
- by intros Hx; specialize (Hx 1); destruct x.
* by intros [?| |] [?| |] [?| |]; constructor.
* by intros [?| |] [?| |]; constructor.
* by intros [?| |]; constructor.
@@ -120,8 +116,6 @@ Proof.
* by intros n [?| |] [?| |].
* by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Qed.
-Global Instance excl_empty_ra : RAIdentity (excl A).
-Proof. split. done. by intros []. Qed.
Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Proof.
intros [|n] x y1 y2 ? Hx; [by exists (x,∅); destruct x|].
@@ -133,6 +127,8 @@ Proof.
Qed.
Canonical Structure exclRA : cmraT :=
CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
+Global Instance excl_cmra_identity : CMRAIdentity exclRA.
+Proof. split. done. by intros []. apply _. Qed.
Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
Proof. by destruct y. Qed.
Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index 9cefea9046d7621830f881f8a96e17bae2d11385..bf289e28999a641a71b013b036ff87ea653e799f 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -50,7 +50,7 @@ Proof.
intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
[by constructor|by apply lookup_ne].
Qed.
-Global Instance map_empty_timeless : Timeless (∅ : gmap K A).
+Instance map_empty_timeless : Timeless (∅ : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
inversion_clear Hm; constructor.
@@ -81,7 +81,6 @@ Context `{Countable K} {A : cmraT}.
Instance map_op : Op (gmap K A) := merge op.
Instance map_unit : Unit (gmap K A) := fmap unit.
-Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m!!i).
Instance map_minus : Minus (gmap K A) := merge minus.
Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
@@ -95,7 +94,7 @@ Proof.
split.
* by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
* intros Hm; exists (m2 ⩪ m1); intros i.
- by rewrite lookup_op lookup_minus ra_op_minus.
+ by rewrite lookup_op lookup_minus cmra_op_minus'.
Qed.
Lemma map_includedN_spec (m1 m2 : gmap K A) n :
m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
@@ -113,26 +112,18 @@ Proof.
* by intros n m1 m2 Hm ? i; rewrite -(Hm i).
* by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
* by intros m i.
- * intros n m Hm i; apply cmra_valid_S, Hm.
- * intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
- intros Hm i; apply cmra_valid_validN; intros n; apply Hm.
- * by intros m1 m2 m3 i; rewrite !lookup_op (associative _).
- * by intros m1 m2 i; rewrite !lookup_op (commutative _).
- * by intros m i; rewrite lookup_op !lookup_unit ra_unit_l.
- * by intros m i; rewrite !lookup_unit ra_unit_idempotent.
+ * intros n m Hm i; apply cmra_validN_S, Hm.
+ * by intros m1 m2 m3 i; rewrite !lookup_op associative.
+ * by intros m1 m2 i; rewrite !lookup_op commutative.
+ * by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
+ * by intros m i; rewrite !lookup_unit cmra_unit_idempotent.
* intros n x y; rewrite !map_includedN_spec; intros Hm i.
- by rewrite !lookup_unit; apply cmra_unit_preserving.
- * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
+ by rewrite !lookup_unit; apply cmra_unit_preservingN.
+ * intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- * intros x y n; rewrite map_includedN_spec; intros ? i.
+ * intros x y n; rewrite map_includedN_spec=> ? i.
by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
-Global Instance map_ra_empty : RAIdentity (gmap K A).
-Proof.
- split.
- * by intros ?; rewrite lookup_empty.
- * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
-Qed.
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
Proof.
intros n m m1 m2 Hm Hm12.
@@ -153,6 +144,14 @@ Proof.
Qed.
Canonical Structure mapRA : cmraT :=
CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
+Global Instance map_cmra_identity : CMRAIdentity mapRA.
+Proof.
+ split.
+ * by intros ? n; rewrite lookup_empty.
+ * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
+ * apply map_empty_timeless.
+Qed.
+
End cmra.
Arguments mapRA _ {_ _} _.
@@ -180,7 +179,7 @@ Proof.
split.
* move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
destruct (m' !! i) as [y|];
- [exists (x â‹… y)|exists x]; eauto using @ra_included_l.
+ [exists (x â‹… y)|exists x]; eauto using cmra_included_l.
* intros (y&Hi&?); rewrite map_includedN_spec=>j.
destruct (decide (i = j)); simplify_map_equality.
+ by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
diff --git a/modures/logic.v b/modures/logic.v
index feaf66ebb697bf4b7d832fe0bc85cd8048cad92c..f14b3da45bcddbe047795b83f633f7ae954c549f 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -152,11 +152,11 @@ Next Obligation. by intros M P Q x; exists x, x. Qed.
Next Obligation.
intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
- { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using @ra_included_l.
+ { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using cmra_included_l.
apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
- * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
- * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
+ * apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l.
+ * apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r.
Qed.
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
@@ -171,7 +171,7 @@ Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Next Obligation.
intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
apply uPred_weaken with (x1 â‹… x3) n3;
- eauto using cmra_valid_included, @ra_preserving_r.
+ eauto using cmra_validN_included, cmra_preserving_r.
Qed.
Program Definition uPred_later {M} (P : uPred M) : uPred M :=
@@ -179,7 +179,7 @@ Program Definition uPred_later {M} (P : uPred M) : uPred M :=
Next Obligation. intros M P ?? [|n]; eauto using uPred_ne,(dist_le (A:=M)). Qed.
Next Obligation. done. Qed.
Next Obligation.
- intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_valid_S.
+ intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_validN_S.
Qed.
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (unit x) |}.
@@ -187,7 +187,7 @@ Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Next Obligation. by intros; simpl. Qed.
Next Obligation.
intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
- eauto using @ra_unit_preserving, cmra_unit_valid.
+ eauto using cmra_unit_preserving, cmra_unit_validN.
Qed.
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
@@ -200,7 +200,7 @@ Next Obligation.
Qed.
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_valid_le, cmra_valid_0.
+Solve Obligations with naive_solver eauto 2 using cmra_validN_le, cmra_validN_0.
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
@@ -299,7 +299,7 @@ Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Proof.
intros P P' HP Q Q' HQ x n' ??; split; intros (x1&x2&?&?&?); cofe_subst x;
exists x1, x2; split_ands; try (apply HP || apply HQ);
- eauto using cmra_valid_op_l, cmra_valid_op_r.
+ eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Global Instance sep_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_sep M) := ne_proper_2 _.
@@ -307,7 +307,7 @@ Global Instance wand_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Proof.
intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
- apply HQ, HPQ, HP; eauto using cmra_valid_op_r.
+ apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
Global Instance wand_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_wand M) := ne_proper_2 _.
@@ -339,12 +339,12 @@ Qed.
Global Instance later_contractive : Contractive (@uPred_later M).
Proof.
intros n P Q HPQ x [|n'] ??; simpl; [done|].
- apply HPQ; eauto using cmra_valid_S.
+ apply HPQ; eauto using cmra_validN_S.
Qed.
Global Instance later_proper :
Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
-Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_valid. Qed.
+Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed.
Global Instance always_proper :
Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_own M).
@@ -404,11 +404,11 @@ Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
Proof.
intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
-Lemma eq_equiv `{Empty M, !RAIdentity M} {A : cofeT} (a b : A) :
+Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
True ⊑ (a ≡ b) → a ≡ b.
Proof.
intros Hab; apply equiv_dist; intros n; apply Hab with ∅.
- * apply cmra_valid_validN, ra_empty_valid.
+ * apply cmra_valid_validN, cmra_empty_valid.
* by destruct n.
Qed.
Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
@@ -543,13 +543,13 @@ Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
Proof.
intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
- eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
+ eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
intros P x n Hvalid; split.
- * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
- * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
+ * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
+ * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite cmra_unit_l].
Qed.
Global Instance sep_commutative : Commutative (≡) (@uPred_sep M).
Proof.
@@ -570,7 +570,7 @@ Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
Proof.
intros HPQR x n ?? x' n' ???; apply HPQR; auto.
exists x, x'; split_ands; auto.
- eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
+ eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
Qed.
Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
@@ -643,16 +643,16 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Later *)
Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
-Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_valid_S]. Qed.
+Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
Lemma later_intro P : P ⊑ ▷ P.
Proof.
intros x [|n] ??; simpl in *; [done|].
- apply uPred_weaken with x (S n); eauto using cmra_valid_S.
+ apply uPred_weaken with x (S n); eauto using cmra_validN_S.
Qed.
Lemma löb P : (▷ P → P) ⊑ P.
Proof.
intros x n ? HP; induction n as [|n IH]; [by apply HP|].
- apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
+ apply HP, IH, uPred_weaken with x (S n); eauto using cmra_validN_S.
Qed.
Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
Proof. by intros x [|n]; split. Qed.
@@ -670,7 +670,7 @@ Proof.
intros x n ?; split.
* destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
destruct (cmra_extend_op n x x1 x2)
- as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_valid_S; simpl in *.
+ as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
* destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S.
@@ -701,12 +701,12 @@ Proof. done. Qed.
Lemma always_elim P : □ P ⊑ P.
Proof.
intros x n ??; apply uPred_weaken with (unit x) n;
- eauto using @ra_included_unit.
+ eauto using cmra_included_unit.
Qed.
Lemma always_intro P Q : □ P ⊑ Q → □ P ⊑ □ Q.
Proof.
- intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_valid.
- by rewrite ra_unit_idempotent.
+ intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
+ by rewrite cmra_unit_idempotent.
Qed.
Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
Proof. done. Qed.
@@ -718,12 +718,12 @@ Lemma always_exist {A} (P : A → uPred M) : (□ ∃ a, P a)%I ≡ (∃ a, □
Proof. done. Qed.
Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
Proof.
- intros x n ? [??]; exists (unit x), (unit x); rewrite ra_unit_unit; auto.
+ intros x n ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
Qed.
Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
Proof.
intros x n ? [??]; exists (unit x), x; simpl in *.
- by rewrite ra_unit_l ra_unit_idempotent.
+ by rewrite cmra_unit_l cmra_unit_idempotent.
Qed.
Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
Proof. done. Qed.
@@ -775,7 +775,7 @@ Lemma own_op (a1 a2 : M) :
Proof.
intros x n ?; split.
* intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (associative op)|].
- split. by exists (unit a1); rewrite ra_unit_r. by exists z.
+ split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
* intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
by rewrite (associative op _ z1) -(commutative op z1) (associative op z1)
-(associative op _ a2) (commutative op z1) -Hy1 -Hy2.
@@ -783,20 +783,20 @@ Qed.
Lemma always_own_unit (a : M) : (□ uPred_own (unit a))%I ≡ uPred_own (unit a).
Proof.
intros x n; split; [by apply always_elim|intros [a' Hx]]; simpl.
- rewrite -(ra_unit_idempotent a) Hx.
- apply cmra_unit_preserving, cmra_included_l.
+ rewrite -(cmra_unit_idempotent a) Hx.
+ apply cmra_unit_preservingN, cmra_includedN_l.
Qed.
Lemma always_own (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
Proof. by intros <-; rewrite always_own_unit. Qed.
-Lemma own_empty `{Empty M, !RAIdentity M} : True ⊑ uPred_own ∅.
+Lemma own_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_own ∅.
Proof. intros x [|n] ??; [done|]. by exists x; rewrite (left_id _ _). Qed.
Lemma own_valid (a : M) : uPred_own a ⊑ (✓ a).
-Proof. move => x n Hv [a' ?]; cofe_subst; eauto using cmra_valid_op_l. Qed.
+Proof. move => x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ (✓ a).
Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{1} a → (✓ a) ⊑ False.
Proof.
- intros Ha x [|n] ??; [|apply Ha, cmra_valid_le with (S n)]; auto with lia.
+ intros Ha x [|n] ??; [|apply Ha, cmra_validN_le with (S n)]; auto with lia.
Qed.
Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
(∀ n, ✓{n} a → ✓{n} b) → (✓ a) ⊑ (✓ b).
@@ -847,9 +847,9 @@ Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 1 x → P n x.
Proof.
split.
* intros HP x n ??; induction n as [|[|n]]; auto.
- by destruct (HP x (S (S n))); auto using cmra_valid_S.
+ by destruct (HP x (S (S n))); auto using cmra_validN_S.
* move=> HP x [|[|n]] /=; auto; left.
- apply HP, uPred_weaken with x (S n); eauto using cmra_valid_le.
+ apply HP, uPred_weaken with x (S n); eauto using cmra_validN_le.
Qed.
Global Instance const_timeless φ : TimelessP (■φ : uPred M)%I.
Proof. by apply timelessP_spec=> x [|n]. Qed.
@@ -862,7 +862,7 @@ Qed.
Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
Proof.
rewrite !timelessP_spec=> HP x [|n] ? HPQ x' [|n'] ????; auto.
- apply HP, HPQ, uPred_weaken with x' (S n'); eauto using cmra_valid_le.
+ apply HP, HPQ, uPred_weaken with x' (S n'); eauto using cmra_validN_le.
Qed.
Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
Proof.
@@ -875,7 +875,7 @@ Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
rewrite !timelessP_spec=> HP x [|n] ? HPQ x' [|n'] ???; auto.
apply HP, HPQ, uPred_weaken with x' (S n');
- eauto 3 using cmra_valid_le, cmra_valid_op_r.
+ eauto 3 using cmra_validN_le, cmra_validN_op_r.
Qed.
Global Instance forall_timeless {A} (P : A → uPred M) :
(∀ x, TimelessP (P x)) → TimelessP (∀ x, P x).
@@ -894,10 +894,10 @@ Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
Timeless a → TimelessP (a ≡ b : uPred M)%I.
Proof. by intro; apply timelessP_spec=> x n ??; apply equiv_dist, timeless. Qed.
-Global Instance own_timeless (a : M): Timeless a → TimelessP (uPred_own a).
+Global Instance own_timeless (a : M) : Timeless a → TimelessP (uPred_own a).
Proof.
- intro; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
- cmra_timeless_included_l; eauto using cmra_valid_le.
+ intros ?; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
+ cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.
(* Always stable *)
diff --git a/modures/option.v b/modures/option.v
index 256331bfad728d80eec71313f8d0e6743be0a142..0b32c1180a2c088c1812e631aafd9d933b401dca 100644
--- a/modures/option.v
+++ b/modures/option.v
@@ -66,25 +66,12 @@ Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
Section cmra.
Context {A : cmraT}.
-Instance option_valid : Valid (option A) := λ mx,
- match mx with Some x => ✓ x | None => True end.
Instance option_validN : ValidN (option A) := λ n mx,
match mx with Some x => ✓{n} x | None => True end.
Instance option_unit : Unit (option A) := fmap unit.
Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
Instance option_minus : Minus (option A) :=
difference_with (λ x y, Some (x ⩪ y)).
-Lemma option_included mx my :
- mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
-Proof.
- split.
- * intros [mz Hmz]; destruct mx as [x|]; [right|by left].
- destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
- destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
- setoid_subst; eauto using ra_included_l.
- * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
- by exists (Some z); constructor.
-Qed.
Lemma option_includedN n (mx my : option A) :
mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
Proof.
@@ -93,7 +80,7 @@ Proof.
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
- cofe_subst; eauto using @cmra_included_l.
+ cofe_subst; eauto using cmra_includedN_l.
* intros [->|[->|(x&y&->&->&z&Hz)]];
try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
@@ -110,22 +97,20 @@ Proof.
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
* destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl;
- intros ?; auto using cmra_valid_0;
+ intros ?; auto using cmra_validN_0;
eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
* by destruct 1; inversion_clear 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
- * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0.
- * intros n [x|]; unfold validN, option_validN; eauto using @cmra_valid_S.
- * by intros [x|]; unfold valid, validN, option_validN, option_valid;
- eauto using cmra_valid_validN.
- * intros [x|] [y|] [z|]; constructor; rewrite ?(associative _); auto.
- * intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto.
- * by intros [x|]; constructor; rewrite ra_unit_l.
- * by intros [x|]; constructor; rewrite ra_unit_idempotent.
+ * intros [x|]; unfold validN, option_validN; auto using cmra_validN_0.
+ * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
+ * intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto.
+ * intros [x|] [y|]; constructor; rewrite 1?commutative; auto.
+ * by intros [x|]; constructor; rewrite cmra_unit_l.
+ * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
* intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
- do 2 right; exists (unit x), (unit y); eauto using @cmra_unit_preserving.
- * intros n [x|] [y|]; unfold validN, option_validN; simpl;
- eauto using @cmra_valid_op_l.
+ do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
+ * intros n [x|] [y|]; rewrite /validN /option_validN /=;
+ eauto using cmra_validN_op_l.
* intros n mx my; rewrite option_includedN.
intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
by constructor; apply cmra_op_minus.
diff --git a/modures/ra.v b/modures/ra.v
deleted file mode 100644
index 4401556a103147cac4987d9922a35fda7972e785..0000000000000000000000000000000000000000
--- a/modures/ra.v
+++ /dev/null
@@ -1,258 +0,0 @@
-Require Export prelude.collections prelude.relations prelude.fin_maps.
-Require Export modures.base.
-
-Class Valid (A : Type) := valid : A → Prop.
-Instance: Params (@valid) 2.
-Notation "✓" := valid (at level 1).
-
-Class Unit (A : Type) := unit : A → A.
-Instance: Params (@unit) 2.
-
-Class Op (A : Type) := op : A → A → A.
-Instance: Params (@op) 2.
-Infix "â‹…" := op (at level 50, left associativity) : C_scope.
-Notation "(â‹…)" := op (only parsing) : C_scope.
-
-Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
-Infix "≼" := included (at level 70) : C_scope.
-Notation "(≼)" := included (only parsing) : C_scope.
-Hint Extern 0 (?x ≼ ?y) => reflexivity.
-Instance: Params (@included) 3.
-
-Class Minus (A : Type) := minus : A → A → A.
-Instance: Params (@minus) 2.
-Infix "⩪" := minus (at level 40) : C_scope.
-
-Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := {
- (* setoids *)
- ra_equivalence :> Equivalence ((≡) : relation A);
- ra_op_proper x :> Proper ((≡) ==> (≡)) (op x);
- ra_unit_proper :> Proper ((≡) ==> (≡)) unit;
- ra_valid_proper :> Proper ((≡) ==> impl) ✓;
- ra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
- (* monoid *)
- ra_associative :> Associative (≡) (⋅);
- ra_commutative :> Commutative (≡) (⋅);
- ra_unit_l x : unit x ⋅ x ≡ x;
- ra_unit_idempotent x : unit (unit x) ≡ unit x;
- ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
- ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
- ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
-}.
-Class RAIdentity A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
- ra_empty_valid : ✓ ∅;
- ra_empty_l :> LeftId (≡) ∅ (⋅)
-}.
-
-Class RAMonotone
- `{Equiv A, Op A, Valid A, Equiv B, Op B, Valid B} (f : A → B) := {
- included_preserving x y : x ≼ y → f x ≼ f y;
- valid_preserving x : ✓ x → ✓ (f x)
-}.
-
-(** Big ops *)
-Fixpoint big_op `{Op A, Empty A} (xs : list A) : A :=
- match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
-Arguments big_op _ _ _ !_ /.
-Instance: Params (@big_op) 3.
-
-Definition big_opM `{FinMapToList K A M, Op A, Empty A} (m : M) : A :=
- big_op (snd <$> map_to_list m).
-Instance: Params (@big_opM) 6.
-
-(** Updates *)
-Definition ra_update_set `{Op A, Valid A} (x : A) (P : A → Prop) :=
- ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
-Instance: Params (@ra_update_set) 3.
-Infix "â‡:" := ra_update_set (at level 70).
-Definition ra_update `{Op A, Valid A} (x y : A) := ∀ z,
- ✓ (x ⋅ z) → ✓ (y ⋅ z).
-Infix "â‡" := ra_update (at level 70).
-Instance: Params (@ra_update) 3.
-
-(** Properties **)
-Section ra.
-Context `{RA A}.
-Implicit Types x y z : A.
-Implicit Types xs ys zs : list A.
-
-Global Instance ra_valid_proper' : Proper ((≡) ==> iff) ✓.
-Proof. by intros ???; split; apply ra_valid_proper. Qed.
-Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (⋅).
-Proof.
- intros x1 x2 Hx y1 y2 Hy.
- by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
-Qed.
-Lemma ra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
-Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed.
-
-(** ** Units *)
-Lemma ra_unit_r x : x ⋅ unit x ≡ x.
-Proof. by rewrite (commutative _ x) ra_unit_l. Qed.
-Lemma ra_unit_unit x : unit x ⋅ unit x ≡ unit x.
-Proof. by rewrite -{2}(ra_unit_idempotent x) ra_unit_r. Qed.
-
-(** ** Order *)
-Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> impl) (≼).
-Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite -Hy Hz Hx. Qed.
-Global Instance ra_included_proper : Proper ((≡) ==> (≡) ==> iff) (≼).
-Proof. by split; apply ra_included_proper'. Qed.
-Lemma ra_included_l x y : x ≼ x ⋅ y.
-Proof. by exists y. Qed.
-Lemma ra_included_r x y : y ≼ x ⋅ y.
-Proof. rewrite (commutative op); apply ra_included_l. Qed.
-Global Instance: PreOrder included.
-Proof.
- split; first by intros x; exists (unit x); rewrite ra_unit_r.
- intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite (associative _) -Hy -Hz.
-Qed.
-Lemma ra_included_unit x : unit x ≼ x.
-Proof. by exists x; rewrite ra_unit_l. Qed.
-Lemma ra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative (â‹…)). Qed.
-Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
-Proof. by intros; rewrite -!(commutative _ z); apply ra_preserving_l. Qed.
-
-(** ** RAs with empty element *)
-Context `{Empty A, !RAIdentity A}.
-
-Global Instance ra_empty_r : RightId (≡) ∅ (⋅).
-Proof. by intros x; rewrite (commutative op) (left_id _ _). Qed.
-Lemma ra_unit_empty : unit ∅ ≡ ∅.
-Proof. by rewrite -{2}(ra_unit_l ∅) (right_id _ _). Qed.
-Lemma ra_empty_least x : ∅ ≼ x.
-Proof. by exists x; rewrite (left_id _ _). Qed.
-
-(** * Big ops *)
-Lemma big_op_nil : big_op (@nil A) = ∅.
-Proof. done. Qed.
-Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
-Proof. done. Qed.
-Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
-Proof.
- induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
- * by rewrite IH.
- * by rewrite !(associative _) (commutative _ x).
- * by transitivity (big_op xs2).
-Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
-Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
-Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
-Proof.
- induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
- by rewrite IH (associative _).
-Qed.
-Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
-Proof.
- induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
- * by apply ra_preserving_l.
- * by rewrite !(associative _) (commutative _ y); apply ra_preserving_r.
- * by transitivity (big_op ys); [|apply ra_included_r].
- * by transitivity (big_op ys).
-Qed.
-Lemma big_op_delete xs i x :
- xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
-Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
-
-Context `{FinMap K M}.
-Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
-Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
-Lemma big_opM_insert (m : M A) i x :
- m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
-Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
-Lemma big_opM_delete (m : M A) i x :
- m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
-Proof.
- intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
-Qed.
-Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
-Proof.
- rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
- by rewrite big_opM_empty (right_id _ _).
-Qed.
-Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
-Proof.
- intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
- { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
- intros m2 Hm2; rewrite big_opM_insert //.
- rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
- destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
- as (y&?&Hxy); auto using lookup_insert.
- rewrite Hxy -big_opM_insert; last auto using lookup_delete.
- by rewrite insert_delete.
-Qed.
-End ra.
-
-(* Simple solver for inclusion by reflection *)
-Module ra_reflection. Section ra_reflection.
- Context `{RA A, Empty A, !RAIdentity A}.
-
- Inductive expr :=
- | EVar : nat → expr
- | EEmpty : expr
- | EOp : expr → expr → expr.
- Fixpoint eval (Σ : list A) (e : expr) : A :=
- match e with
- | EVar n => from_option ∅ (Σ !! n)
- | EEmpty => ∅
- | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
- end.
- Fixpoint flatten (e : expr) : list nat :=
- match e with
- | EVar n => [n]
- | EEmpty => []
- | EOp e1 e2 => flatten e1 ++ flatten e2
- end.
- Lemma eval_flatten Σ e :
- eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
- Proof.
- by induction e as [| |e1 IH1 e2 IH2];
- rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
- Qed.
- Lemma flatten_correct Σ e1 e2 :
- flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
- Proof.
- by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
- Qed.
-
- Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
- Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
- Global Instance quote_var Σ1 Σ2 e i:
- rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
- Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
- Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
- End ra_reflection.
-
- Ltac quote :=
- match goal with
- | |- @included _ _ _ ?x ?y =>
- lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
- lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
- change (eval Σ3 e1 ≼ eval Σ3 e2)
- end end
- end.
-End ra_reflection.
-
-Ltac solve_included :=
- ra_reflection.quote;
- apply ra_reflection.flatten_correct, (bool_decide_unpack _);
- vm_compute; apply I.
-
-(** An RA for the unit type *)
-Instance unit_valid : Valid () := λ x, True.
-Instance unit_unit : Unit () := λ x, x.
-Instance unit_op : Op () := λ x y, tt.
-Instance unit_minus : Minus () := λ x y, tt.
-
-Instance unit_ra : RA ().
-Proof.
- split; done.
-Qed.
-
-
-Instance unit_empty : Empty () := tt.
-Instance unit_empty_ra : RAIdentity().
-Proof.
- split; done.
-Qed.
diff --git a/modures/sts.v b/modures/sts.v
index e4977886b5b20def0d147d4f98ac58d79617a94d..4697c82c0e85895637d663873caa72d58626786d 100644
--- a/modures/sts.v
+++ b/modures/sts.v
@@ -1,21 +1,21 @@
-Require Export modures.ra.
+Require Export modures.cmra.
Require Import prelude.sets modures.dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.
-Module sts.
-Inductive t {A B} (R : relation A) (tok : A → set B) :=
- | auth : A → set B → t R tok
- | frag : set A → set B → t R tok.
+Inductive sts {A B} (R : relation A) (tok : A → set B) :=
+ | auth : A → set B → sts R tok
+ | frag : set A → set B → sts R tok.
Arguments auth {_ _ _ _} _ _.
Arguments frag {_ _ _ _} _ _.
+Module sts.
Section sts_core.
Context {A B : Type} (R : relation A) (tok : A → set B).
Infix "≼" := dra_included.
-Inductive sts_equiv : Equiv (t R tok) :=
+Inductive sts_equiv : Equiv (sts R tok) :=
| auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
| frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
Global Existing Instance sts_equiv.
@@ -36,28 +36,28 @@ Record closed (T : set B) (S : set A) : Prop := Closed {
Lemma closed_steps S T s1 s2 :
closed T S → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
Proof. induction 3; eauto using closed_step. Qed.
-Global Instance sts_valid : Valid (t R tok) := λ x,
+Global Instance sts_valid : Valid (sts R tok) := λ x,
match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed T S' end.
Definition up (T : set B) (s : A) : set A := mkSet (rtc (frame_step T) s).
Definition up_set (T : set B) (S : set A) : set A := S ≫= up T.
-Global Instance sts_unit : Unit (t R tok) := λ x,
+Global Instance sts_unit : Unit (sts R tok) := λ x,
match x with
| frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅
end.
-Inductive sts_disjoint : Disjoint (t R tok) :=
+Inductive sts_disjoint : Disjoint (sts R tok) :=
| frag_frag_disjoint S1 S2 T1 T2 :
S1 ∩ S2 ≢ ∅ → T1 ∩ T2 ≡ ∅ → frag S1 T1 ⊥ frag S2 T2
| auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → auth s T1 ⊥ frag S T2
| frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → frag S T1 ⊥ auth s T2.
Global Existing Instance sts_disjoint.
-Global Instance sts_op : Op (t R tok) := λ x1 x2,
+Global Instance sts_op : Op (sts R tok) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
| auth s T1, frag _ T2 => auth s (T1 ∪ T2)
| frag _ T1, auth s T2 => auth s (T1 ∪ T2)
| auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *)
end.
-Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
+Global Instance sts_minus : Minus (sts R tok) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (up_set (T1 ∖ T2) S1) (T1 ∖ T2)
| auth s T1, frag _ T2 => auth s (T1 ∖ T2)
@@ -69,7 +69,7 @@ Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬(equiv (A:=set _) _ _)) => solve_elem_of : sts.
Hint Extern 10 (_ ∈ _) => solve_elem_of : sts.
Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts.
-Instance: Equivalence ((≡) : relation (t R tok)).
+Instance: Equivalence ((≡) : relation (sts R tok)).
Proof.
split.
* by intros []; constructor.
@@ -135,7 +135,7 @@ Proof.
unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
induction Hstep; eauto using closed_step.
Qed.
-Global Instance sts_dra : DRA (t R tok).
+Global Instance sts_dra : DRA (sts R tok).
Proof.
split.
* apply _.
@@ -203,18 +203,12 @@ Qed.
End sts_core.
End sts.
-Section sts_ra.
+Section stsRA.
Context {A B : Type} (R : relation A) (tok : A → set B).
-Definition sts := validity (✓ : sts.t R tok → Prop).
-Global Instance sts_equiv : Equiv sts := validity_equiv _.
-Global Instance sts_unit : Unit sts := validity_unit _.
-Global Instance sts_op : Op sts := validity_op _.
-Global Instance sts_minus : Minus sts := validity_minus _.
-Global Instance sts_ra : RA sts := validity_ra _.
-Definition sts_auth (s : A) (T : set B) : sts := to_validity (sts.auth s T).
-Definition sts_frag (S : set A) (T : set B) : sts := to_validity (sts.frag S T).
-Canonical Structure stsRA := validityRA (sts.t R tok).
+Canonical Structure stsRA := validityRA (sts R tok).
+Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
+Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
Lemma sts_update s1 s2 T1 T2 :
sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇠sts_auth s2 T2.
Proof.
@@ -222,4 +216,4 @@ Proof.
destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
repeat (done || constructor).
Qed.
-End sts_ra.
+End stsRA.