WIP: move the later from the resources to the model

iris/model.v

@@ -2,14 +2,14 @@ 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.
+  * intros A B r n ?; rewrite /uPred_holds /= /laterC_map /=. later_map_id 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;

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,16 @@ 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.
+    rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=; done.
+  * rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=; done.
 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.
+    rewrite -agree_map_compose; apply agree_map_ext=> y' /=; done.
+  * rewrite -icmra_map_compose; apply icmra_map_ext=> m /=; 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 +199,3 @@ 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).
-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.
-Qed.