From 2d9c59ace0ab98826eacf1f81457fe6cc23ba3ce Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 21 Jan 2016 19:39:13 +0100
Subject: [PATCH] Revert accidentally pushed "WIP: move the later from the
 resources to the model"

This reverts commit 5161e4634554152026249bc05e5eada4c128629d.
---
 iris/model.v     |  6 +++---
 iris/resources.v | 29 ++++++++++++++++++++---------
 2 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/iris/model.v b/iris/model.v
index f895c3c8c..6097d1915 100644
--- a/iris/model.v
+++ b/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 Σ (laterC A)).
+Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ 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 (laterC_map (f.1))).
+  uPredC_map (resRA_map (f.1)).
 Definition result Σ : solution (F Σ).
 Proof.
   apply (solver.result _ (@map Σ)).
-  * intros A B r n ?; rewrite /uPred_holds /= /laterC_map /=. later_map_id res_map_id.
+  * 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;
diff --git a/iris/resources.v b/iris/resources.v
index caac93946..73996b11c 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -1,9 +1,9 @@
 Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
 
 Record res (Σ : iParam) (A : cofeT) := Res {
-  wld : mapRA positive (agreeRA A);
+  wld : mapRA positive (agreeRA (laterC A));
   pst : exclRA (istateC Σ);
-  gst : icmra Σ A;
+  gst : icmra Σ (laterC 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 Σ A) (r : res Σ A) : res Σ A :=
+Definition update_gst (m : icmra Σ (laterC 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 f <$> (wld r))
+  Res (agree_map (later_map f) <$> (wld r))
       (pst r)
-      (icmra_map Σ f (gst r)).
+      (icmra_map Σ (laterC_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,16 +178,20 @@ 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' /=; done.
-  * rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=; done.
+    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.
 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' /=; done.
-  * rewrite -icmra_map_compose; apply icmra_map_ext=> m /=; done.
+    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.
 Qed.
 Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
   CofeMor (res_map f : resRA Σ A → resRA Σ B).
@@ -199,3 +203,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).
+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.
-- 
GitLab