Commit b936a5ca authored by Robbert Krebbers's avatar Robbert Krebbers

Remove RA from the hierarchy.

Instead, we have just a construction to create a CMRA from a RA. This
construction is also slightly generalized, it now works for RAs over any
timeless COFE instead of just the discrete COFE.

Also:
* Put tactics and big_ops for CMRAs in a separate file.
* Valid is now a derived notion (as the limit of validN), so it does not have
  to be defined by hand for each CMRA.

Todo:
Make the constructions DRA -> CMRA and RA -> CMRA more uniform.
parent f7bbaa2c
......@@ -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
......
Require Export barrier.heap_lang.
Require Import iris.parameter.
Definition Σ := IParamConst heap_lang unitRA.
Definition Σ := iParam_const heap_lang unitRA.
......@@ -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).
......
......@@ -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.
......@@ -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
......@@ -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 (r3rf) 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.
......
......@@ -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} (r1r2) 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.
......@@ -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.
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.
......
......@@ -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).
......
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.
......
This diff is collapsed.
Require Export modures.cmra.
Require Import prelude.fin_maps.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=