put the later into model.v; adjust Iris domain notations

iris/model.v

@@ -2,26 +2,30 @@ Require Export modures.logic iris.resources.
 Require Import modures.cofe_solver.
 
 Module iProp.
-Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ A).
+Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)).
 Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
     (f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
-  uPredC_map (resRA_map (f.1)).
+  uPredC_map (resRA_map (laterC_map (f.1))).
 Definition result Σ : solution (F Σ).
 Proof.
   apply (solver.result _ (@map Σ)).
-  * by intros A B r n ?; rewrite /uPred_holds /= res_map_id.
-  * by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?;
-      rewrite /= /uPred_holds /= res_map_compose.
-  * by intros A1 A2 B1 B2 n f f' [??] r;
-      apply upredC_map_ne, resRA_map_contractive.
+  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=>r {P} /=.
+    rewrite -{2}(res_map_id r). apply res_map_ext=>{r} r /=. by rewrite later_map_id.
+  * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
+    rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
+    rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
+    by rewrite -later_map_compose.
+  * intros A1 A2 B1 B2 n f f' [??] P.
+    by apply upredC_map_ne, resRA_map_ne, laterC_map_contractive.
 Qed.
 End iProp.
 
 (* Solution *)
 Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
-Notation res' Σ := (res Σ (iPreProp Σ)).
-Notation icmra' Σ := (icmra Σ (laterC (iPreProp Σ))).
-Definition iProp (Σ : iParam) : cofeT := uPredC (resRA Σ (iPreProp Σ)).
+Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
+Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
+Notation iCMRA Σ := (icmra Σ (laterC (iPreProp Σ))).
+Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
 Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
 Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
 Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.

iris/ownership.v

@@ -4,7 +4,7 @@ Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
 Arguments inv {_} _ _%I.
 Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Σ} (m : icmra' Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
+Definition ownG {Σ} (m : iCMRA Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
 Instance: Params (@inv) 2.
 Instance: Params (@ownP) 1.
 Instance: Params (@ownG) 1.
@@ -13,10 +13,10 @@ Typeclasses Opaque inv ownG ownP.
 
 Section ownership.
 Context {Σ : iParam}.
-Implicit Types r : res' Σ.
+Implicit Types r : iRes Σ.
 Implicit Types σ : istate Σ.
 Implicit Types P : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iCMRA Σ.
 
 (* Invariants *)
 Global Instance inv_contractive i : Contractive (@inv Σ i).

iris/pviewshifts.v

@@ -29,7 +29,7 @@ Instance: Params (@pvs) 3.
 Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iCMRA Σ.
 Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
@@ -96,7 +96,7 @@ Proof.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
 Qed.
-Lemma pvs_updateP E m (P : icmra' Σ → Prop) :
+Lemma pvs_updateP E m (P : iCMRA Σ → Prop) :
   m ⇝: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.

iris/resources.v

 Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
 
 Record res (Σ : iParam) (A : cofeT) := Res {
-  wld : mapRA positive (agreeRA (laterC A));
+  wld : mapRA positive (agreeRA A);
   pst : exclRA (istateC Σ);
-  gst : icmra Σ (laterC A);
+  gst : icmra Σ A;
 }.
 Add Printing Constructor res.
 Arguments Res {_ _} _ _ _.
@@ -137,7 +137,7 @@ Canonical Structure resRA : cmraT :=
 
 Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
   Res (wld r) (Excl σ) (gst r).
-Definition update_gst (m : icmra Σ (laterC A)) (r : res Σ A) : res Σ A :=
+Definition update_gst (m : icmra Σ A) (r : res Σ A) : res Σ A :=
   Res (wld r) (pst r) m.
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
@@ -167,9 +167,9 @@ End res.
 Arguments resRA : clear implicits.
 
 Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B :=
-  Res (agree_map (later_map f) <$> (wld r))
+  Res (agree_map f <$> (wld r))
       (pst r)
-      (icmra_map Σ (laterC_map f) (gst r)).
+      (icmra_map Σ f (gst r)).
 Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) :
   (∀ n, Proper (dist n ==> dist n) f) →
   ∀ n, Proper (dist n ==> dist n) (@res_map Σ _ _ f).
@@ -178,20 +178,22 @@ Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r.
 Proof.
   constructor; simpl; [|done|].
   * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
-    rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
-    by rewrite later_map_id.
-  * rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
-    by rewrite later_map_id.
+    by rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
+  * by rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
 Qed.
 Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) :
   res_map (g ◎ f) r ≡ res_map g (res_map f r).
 Proof.
   constructor; simpl; [|done|].
   * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
-    rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
-    by rewrite later_map_compose.
-  * rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
-    by rewrite later_map_compose.
+    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.
+Proof.
+  move=>H r. split; simpl;
+    [apply map_fmap_setoid_ext; intros; apply agree_map_ext | | apply icmra_map_ext]; done.
 Qed.
 Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
   CofeMor (res_map f : resRA Σ A → resRA Σ B).
@@ -203,10 +205,10 @@ Proof.
       intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
   * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
 Qed.
-Instance resRA_map_contractive {Σ A B} : Contractive (@resRA_map Σ A B).
+Lemma resRA_map_ne {Σ A B} (f g : A -n> B) n :
+  f ={n}= g → resRA_map (Σ := Σ) f ={n}= resRA_map g.
 Proof.
-  intros n f g ? r; constructor; simpl; [|done|].
-  * by apply (mapRA_map_ne _ (agreeRA_map (laterC_map f))
-      (agreeRA_map (laterC_map g))), agreeRA_map_ne, laterC_map_contractive.
-  * by apply icmra_map_ne, laterC_map_contractive.
+  intros ? r. split; simpl;
+    [apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne
+     | | apply icmra_map_ne]; done.
 Qed.

iris/viewshifts.v

@@ -16,7 +16,7 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I)
 Section vs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iCMRA Σ.
 Import uPred.
 
 Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q.
@@ -85,7 +85,7 @@ Proof.
   intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_close.
 Qed.
-Lemma vs_updateP E m (P : icmra' Σ → Prop) :
+Lemma vs_updateP E m (P : iCMRA Σ → Prop) :
   m ⇝: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
 Lemma vs_update E m m' : m ⇝ m' → ownG m >{E}> ownG m'.

iris/weakestpre.v

@@ -7,8 +7,8 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
-    (k : nat) (rf : res' Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
+Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
+    (k : nat) (rf : iRes Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
   wf_safe : reducible e1 σ1;
   wp_step e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
@@ -18,7 +18,7 @@ Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
       ∀ e', ef = Some e' → Qfork e' k r2'
 }.
 CoInductive wp_pre {Σ} (E : coPset)
-     (Q : ival Σ → iProp Σ) : iexpr Σ → nat → res' Σ → Prop :=
+     (Q : ival Σ → iProp Σ) : iexpr Σ → nat → iRes Σ → Prop :=
   | wp_pre_0 e r : wp_pre E Q e 0 r
   | wp_pre_value n r v : Q v n r → wp_pre E Q (of_val v) n r
   | wp_pre_step n r1 e1 :

iris/wsat.v

@@ -5,7 +5,7 @@ Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
 Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
 
 Record wsat_pre {Σ} (n : nat) (E : coPset)
-    (σ : istate Σ) (rs : gmap positive (res' Σ)) (r : res' Σ) := {
+    (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := {
   wsat_pre_valid : ✓{S n} r;
   wsat_pre_state : pst r ≡ Excl σ;
   wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
@@ -19,7 +19,7 @@ Arguments wsat_pre_state {_ _ _ _ _ _} _.
 Arguments wsat_pre_dom {_ _ _ _ _ _} _ _ _.
 Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
 
-Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : res' Σ) : Prop :=
+Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : Prop :=
   match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end.
 Instance: Params (@wsat) 4.
 Arguments wsat : simpl never.
@@ -27,8 +27,8 @@ Arguments wsat : simpl never.
 Section wsat.
 Context {Σ : iParam}.
 Implicit Types σ : istate Σ.
-Implicit Types r : res' Σ.
-Implicit Types rs : gmap positive (res' Σ).
+Implicit Types r : iRes Σ.
+Implicit Types rs : gmap positive (iRes Σ).
 Implicit Types P : iProp Σ.
 
 Instance wsat_ne' : Proper (dist n ==> impl) (wsat (Σ:=Σ) n E σ).
@@ -120,7 +120,7 @@ Proof.
   split; [done|exists rs].
   by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
 Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : icmra' Σ → Prop) :
+Lemma wsat_update_gst n E σ r rf m1 (P : iCMRA Σ → Prop) :
   m1 ≼{S n} gst r → m1 ⇝: P →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.

modures/cmra.v

@@ -105,6 +105,13 @@ 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 *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,

modures/logic.v

@@ -54,20 +54,31 @@ Instance uPred_holds_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
 Proof. by intros x1 x2 Hx; apply uPred_holds_ne, equiv_dist. Qed.
 
 (** functor *)
-Program Definition uPred_map {M1 M2 : cmraT} (f : M2 → M1)
-  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
-  (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
-Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
+Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} (P : uPred M1) :
+  uPred M2 := {| uPred_holds n x := P n (f x) |}.
+Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
+Next Obligation. intros M1 M2 f _ P x; apply uPred_0. Qed.
 Next Obligation.
   naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
 Qed.
-Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 → M1)
-  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f} :
+Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} :
   Proper (dist n ==> dist n) (uPred_map f).
 Proof.
   by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
 Qed.
+Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
+Proof. by intros x n ?. Qed.
+Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+      `{!CMRAMonotone f} `{!CMRAMonotone g}
+      (P : uPred M3):
+  uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
+Proof. by intros x n Hx. Qed.
+Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
+      `{!CMRAMonotone f} `{!CMRAMonotone g}:
+  (∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
+Proof. move=> H x P n Hx /=. by rewrite /uPred_holds /= H. Qed.
 Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
   uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
 Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)