Make cFunctor and rFunctor contractive.

Since functor instances are just used as combinators, there is really
no need for functors that are not contractive.

algebra/agree.v

@@ -185,7 +185,8 @@ Program Definition agreeRF (F : cFunctor) : rFunctor := {|
   rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
+  intros F A1 A2 B1 B2 n ???; simpl.
+  by apply agreeC_map_ne, cFunctor_contractive.
 Qed.
 Next Obligation.
   intros F A B x; simpl. rewrite -{2}(agree_map_id x).

algebra/auth.v

@@ -245,7 +245,7 @@ Program Definition authRF (F : rFunctor) : rFunctor := {|
   rFunctor_map A1 A2 B1 B2 fg := authC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_contractive.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(auth_map_id x).

algebra/cmra.v

@@ -623,8 +623,7 @@ Structure rFunctor := RFunctor {
   rFunctor_car : cofeT → cofeT -> cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne {A1 A2 B1 B2} n :
-    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
+  rFunctor_contractive {A1 A2 B1 B2} : Contractive (@rFunctor_map A1 A2 B1 B2);
   rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
   rFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -632,7 +631,7 @@ Structure rFunctor := RFunctor {
   rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CMRAMonotone (rFunctor_map fg) 
 }.
-Existing Instances rFunctor_ne rFunctor_mono.
+Existing Instances rFunctor_contractive rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
 
 Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
@@ -648,28 +647,11 @@ Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
     prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
 Next Obligation.
-  by intros F1 F2 A1 A2 B1 B2 n ???; apply prodC_map_ne; apply rFunctor_ne.
+  by intros F1 F2 A1 A2 B1 B2 n ???;
+    apply prodC_map_ne; apply rFunctor_contractive.
 Qed.
 Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
 Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !rFunctor_compose.
 Qed.
-
-Program Definition laterRF (F : rFunctor) : rFunctor := {|
-  rFunctor_car A B := rFunctor_car F (laterC A) (laterC B);
-  rFunctor_map A1 A2 B1 B2 fg :=
-    rFunctor_map F (prod_map laterC_map laterC_map fg)
-|}.
-Next Obligation.
-  intros F A1 A2 B1 B2 n x y [??].
-  by apply rFunctor_ne; split; apply (contractive_ne laterC_map).
-Qed.
-Next Obligation.
-  intros F A B x; simpl. rewrite -{2}[x]rFunctor_id.
-  apply (ne_proper (rFunctor_map F)); split; by intros [].
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl in *. rewrite -rFunctor_compose.
-  apply (ne_proper (rFunctor_map F)); split; by intros [].
-Qed.

algebra/cofe.v

@@ -154,6 +154,9 @@ Section cofe.
   Qed.
 End cofe.
 
+Instance const_contractive {A B : cofeT} (x : A) : Contractive (@const A B x).
+Proof. by intros n y1 y2. Qed.
+
 (** Mapping a chain *)
 Program Definition chain_map `{Dist A, Dist B} (f : A → B)
     `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
@@ -164,8 +167,8 @@ Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
 Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
 Next Obligation.
-  intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl;
-                      try reflexivity || omega; [|].
+  intros A ? f ? n.
+  induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega.
   - apply (contractive_0 f).
   - apply (contractive_S f), IH; auto with omega.
 Qed.
@@ -333,24 +336,19 @@ Structure cFunctor := CFunctor {
   cFunctor_car : cofeT → cofeT -> cofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
-  cFunctor_ne {A1 A2 B1 B2} n :
-    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
+  cFunctor_contractive {A1 A2 B1 B2} : Contractive (@cFunctor_map A1 A2 B1 B2);
   cFunctor_id {A B : cofeT} (x : cFunctor_car A B) :
     cFunctor_map (cid,cid) x ≡ x;
   cFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
 }.
-Existing Instances cFunctor_ne.
+Existing Instances cFunctor_contractive.
 Instance: Params (@cFunctor_map) 5.
 
 Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
 Coercion cFunctor_diag : cFunctor >-> Funclass.
 
-Program Definition idCF : cFunctor :=
-  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
-Solve Obligations with done.
-
 Program Definition constCF (B : cofeT) : cFunctor :=
   {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
@@ -361,7 +359,8 @@ Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
     prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
 |}.
 Next Obligation.
-  by intros F1 F2 A1 A2 B1 B2 n ???; apply prodC_map_ne; apply cFunctor_ne.
+  by intros F1 F2 A1 A2 B1 B2 n ???;
+    apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed.
 Next Obligation.
@@ -375,8 +374,8 @@ Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
     cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] [??]; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_ne; by apply pair_ne.
+  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
+  apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
 Qed.
 Next Obligation.
   intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
@@ -476,7 +475,8 @@ Program Definition laterCF : cFunctor := {|
   cFunctor_map A1 A2 B1 B2 fg := laterC_map (fg.2)
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n ? [??]; simpl. by apply (contractive_ne laterC_map).
+  intros A1 A2 B1 B2 n fg fg' Hfg.
+  apply laterC_map_contractive=> i ?; by apply Hfg.
 Qed.
 Next Obligation. by intros A B []. Qed.
 Next Obligation. by intros A1 A2 A3 B1 B2 B3 f g f' g' []. Qed.

algebra/cofe_solver.v

@@ -12,8 +12,6 @@ Arguments solution_fold {_} _.
 
 Module solver. Section solver.
 Context (F : cFunctor) `{Finhab : Inhabited (F unitC)}.
-Context (map_contractive : ∀ {A1 A2 B1 B2},
-  Contractive (@cFunctor_map F A1 A2 B1 B2)).
 Notation map := (cFunctor_map F).
 
 Fixpoint A (k : nat) : cofeT :=

algebra/excl.v

@@ -201,9 +201,19 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
 Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
 Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
 
-Program Definition exclF : rFunctor := {|
-  rFunctor_car A B := exclR B; rFunctor_map A1 A2 B1 B2 fg := exclC_map (fg.2)
+Program Definition exclF (F : cFunctor) : rFunctor := {|
+  rFunctor_car A B := exclR (cFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
 |}.
-Next Obligation. intros A1 A2 B1 B2 n x1 x2 [??]. by apply exclC_map_ne. Qed.
-Next Obligation. by intros A B x; rewrite /= excl_map_id. Qed.
-Next Obligation. by intros A1 A2 A3 B1 B2 B3 *;rewrite /= excl_map_compose. Qed.
+Next Obligation.
+  intros A1 A2 B1 B2 n x1 x2 ??.
+  by apply exclC_map_ne, cFunctor_contractive.
+Qed.
+Next Obligation.
+  intros F A B x; simpl. rewrite -{2}(excl_map_id x).
+  apply excl_map_ext=>y. by rewrite cFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
+  apply excl_map_ext=>y; apply cFunctor_compose.
+Qed.

algebra/fin_maps.v

@@ -357,7 +357,7 @@ Program Definition mapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
   cFunctor_map A1 A2 B1 B2 fg := mapC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_ne.
+  by intros K ?? F A1 A2 B1 B2 n f g ?; apply mapC_map_ne, cFunctor_contractive.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
@@ -373,7 +373,7 @@ Program Definition mapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
   rFunctor_map A1 A2 B1 B2 fg := mapC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_ne.
+  by intros K ?? F A1 A2 B1 B2 n f g ?; apply mapC_map_ne, rFunctor_contractive.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).

algebra/frac.v

@@ -249,7 +249,7 @@ Program Definition fracRF (F : rFunctor) : rFunctor := {|
   rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(frac_map_id x).

algebra/iprod.v

@@ -293,7 +293,8 @@ Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
   cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  by intros C F A1 A2 B1 B2 n ?? g; apply iprodC_map_ne=>c; apply cFunctor_ne.
+  intros C F A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
 Qed.
 Next Obligation.
   intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
@@ -309,7 +310,8 @@ Program Definition iprodRF {C} (F : C → rFunctor) : rFunctor := {|
   rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  by intros C F A1 A2 B1 B2 n ?? g; apply iprodC_map_ne=>c; apply rFunctor_ne.
+  intros C F A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply rFunctor_contractive.
 Qed.
 Next Obligation.
   intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).

algebra/option.v

@@ -194,7 +194,7 @@ Program Definition optionCF (F : cFunctor) : cFunctor := {|
   cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
@@ -210,7 +210,7 @@ Program Definition optionRF (F : rFunctor) : rFunctor := {|
   rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).

algebra/upred.v

@@ -102,7 +102,8 @@ Program Definition uPredCF (F : rFunctor) : cFunctor := {|
   cFunctor_map A1 A2 B1 B2 fg := uPredC_map (rFunctor_map F (fg.2, fg.1))
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n P Q [??]. by apply uPredC_map_ne, rFunctor_ne.
+  intros F A1 A2 B1 B2 n P Q HPQ.
+  apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
 Qed.
 Next Obligation.
   intros F A B P; simpl. rewrite -{2}(uPred_map_id P).

barrier/proof.v

@@ -10,10 +10,10 @@ Import uPred.
 (* Not bundling heapG, as it may be shared with other users. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG heap_lang Σ sts;
-  barrier_savedPropG :> savedPropG heap_lang Σ idCF;
+  barrier_savedPropG :> savedPropG heap_lang Σ laterCF;
 }.
 (** The Functors we need. *)
-Definition barrierGF : rFunctors := [stsGF sts; agreeRF idCF].
+Definition barrierGF : rFunctors := [stsGF sts; agreeRF laterCF].
 (* Show and register that they match. *)
 Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
 Proof. destruct H as (?&?&?). split; apply _. Qed.
@@ -119,7 +119,7 @@ Proof.
   apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
   rewrite !assoc. apply pvs_wand_r.
   (* The core of this proof: Allocating the STS and the saved prop. *)
-  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ (Next P)).
+  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF) _ (Next P)).
   rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
   apply exist_elim=>i.
   trans (pvs ⊤ ⊤ (heap_ctx heapN ★

program_logic/ghost_ownership.v

@@ -18,7 +18,7 @@ Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
 
 Class inG (Λ : language) (Σ : rFunctorG) (A : cmraT) := InG {
   inG_id : gid;
-  inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
+  inG_prf : A = Σ inG_id (iPreProp Λ (globalF Σ))
 }.
 
 Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
@@ -52,9 +52,9 @@ Proof. rewrite /to_globalF; apply _. Qed.
 
 (** * Transport empty *)
 Instance inG_empty `{Empty A} :
-  Empty (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))) := cmra_transport inG_prf ∅.
+  Empty (Σ inG_id (iPreProp Λ (globalF Σ))) := cmra_transport inG_prf ∅.
 Instance inG_empty_spec `{Empty A} :
-  CMRAIdentity A → CMRAIdentity (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))).
+  CMRAIdentity A → CMRAIdentity (Σ inG_id (iPreProp Λ (globalF Σ))).
 Proof.
   split.
   - apply cmra_transport_valid, cmra_empty_valid.

program_logic/global_functor.v

@@ -57,7 +57,7 @@ their first argument to avoid loops. For example, the instances [authGF_inGF]
 and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
 Hint Mode inGF + + - : typeclass_instances.
 
-Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
+Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (iPreProp Λ (globalF Σ))).
 Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
 Instance inGF_here {Λ Σ} (F: rFunctor) : inGF Λ (rFunctorG.cons F Σ) F.
 Proof. by exists 0. Qed.
@@ -76,4 +76,4 @@ Instance inGFs_nil {Λ Σ} : inGFs Λ Σ [].
 Proof. exact tt. Qed.
 Instance inGFs_cons {Λ Σ} F Fs :
   inGF Λ Σ F → inGFs Λ Σ Fs → inGFs Λ Σ (rFunctors.cons F Fs).
-Proof. split; done. Qed.
+Proof. by split. Qed.

program_logic/model.v

@@ -9,8 +9,7 @@ propositions using the agreement CMRA. *)
 
 Module Type iProp_solution_sig.
 Parameter iPreProp : language → rFunctor → cofeT.
-Definition iGst (Λ : language) (Σ : rFunctor) : cmraT :=
-  Σ (laterC (iPreProp Λ Σ)).
+Definition iGst (Λ : language) (Σ : rFunctor) : cmraT := Σ (iPreProp Λ Σ).
 Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
@@ -27,19 +26,10 @@ End iProp_solution_sig.
 
 Module Export iProp_solution : iProp_solution_sig.
 Definition iProp_result (Λ : language) (Σ : rFunctor) :
-  solution (uPredCF (resRF Λ laterCF (laterRF Σ))).
-Proof.
-  (* Contractiveness should be derived from general properties about functors *)
-  apply (solver.result _)=> A1 A2 B1 B2.
-  intros n fg fg' Hf P; split=> n' -[???].
-  apply uPredC_map_ne, resC_map_ne; simpl.
-  - apply laterC_map_contractive=> i ?. by apply Hf.
-  - apply rFunctor_ne; split; apply laterC_map_contractive=> i ?; by apply Hf.
-Qed.
+  solution (uPredCF (resRF Λ laterCF Σ)) := solver.result _.
 
 Definition iPreProp (Λ : language) (Σ : rFunctor) : cofeT := iProp_result Λ Σ.
-Definition iGst (Λ : language) (Σ : rFunctor) : cmraT :=
-  Σ (laterC (iPreProp Λ Σ)).
+Definition iGst (Λ : language) (Σ : rFunctor) : cmraT := Σ (iPreProp Λ Σ).
 Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).

program_logic/resources.v

@@ -232,8 +232,9 @@ Program Definition resRF (Λ : language)
   rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F fg) (rFunctor_map Σ fg)
 |}.
 Next Obligation.
-  intros Λ F Σ A1 A2 B1 B2 n f g Hfg.
-  apply resC_map_ne. by apply cFunctor_ne. by apply rFunctor_ne.
+  intros Λ F Σ A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
+  - by apply cFunctor_contractive.
+  - by apply rFunctor_contractive.
 Qed.
 Next Obligation.
   intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).

program_logic/saved_prop.v

@@ -3,21 +3,20 @@ From program_logic Require Export global_functor.
 Import uPred.
 
 Class savedPropG (Λ : language) (Σ : rFunctorG) (F : cFunctor) :=
-  saved_prop_inG :> inG Λ Σ (agreeR (F (laterC (iPreProp Λ (globalF Σ))))).
+  saved_prop_inG :> inG Λ Σ (agreeR (F (iPreProp Λ (globalF Σ)))).
 
 Instance inGF_savedPropG `{inGF Λ Σ (agreeRF F)} : savedPropG Λ Σ F.
 Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ F}
-    (γ : gname) (x : F (laterC (iPropG Λ Σ))) : iPropG Λ Σ :=
-  own γ (to_agree
-    (cFunctor_map F (laterC_map iProp_fold, laterC_map iProp_unfold) x)).
+    (γ : gname) (x : F (iPropG Λ Σ)) : iPropG Λ Σ :=
+  own γ (to_agree (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_prop_own.
 Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.
   Context `{savedPropG Λ Σ F}.
-  Implicit Types x y : F (laterC (iPropG Λ Σ)).
+  Implicit Types x y : F (iPropG Λ Σ).
   Implicit Types γ : gname.
 
   Global Instance saved_prop_always_stable γ x :
@@ -35,14 +34,12 @@ Section saved_prop.
     (saved_prop_own γ x ★ saved_prop_own γ y) ⊑ (x ≡ y).
   Proof.
     rewrite -own_op own_valid agree_validI agree_equivI.
-    set (G1 := cFunctor_map F (laterC_map iProp_fold, laterC_map iProp_unfold)).
-    set (G2 := cFunctor_map F (laterC_map (@iProp_unfold Λ (globalF Σ)),
-                               laterC_map (@iProp_fold Λ (globalF Σ)))).
+    set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
+    set (G2 := cFunctor_map F (@iProp_unfold Λ (globalF Σ),
+                               @iProp_fold Λ (globalF Σ))).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
-      apply (ne_proper (cFunctor_map F)); split=> P /=;
-        rewrite -later_map_compose -{2}[P]later_map_id;
-        apply later_map_ext=>?; apply iProp_fold_unfold. }
+      apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
     rewrite -{2}[x]help -{2}[y]help.
     apply (eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I;
       first solve_proper; auto with I.

program_logic/tests.v

@@ -9,11 +9,11 @@ End ModelTest.
 Module SavedPropTest.
   (* Test if we can really go "crazy higher order" *)
   Section sec.
-    Definition Σ : rFunctorG := #[ agreeRF (cofe_morCF idCF idCF) ].
+    Definition Σ : rFunctorG := #[ agreeRF (cofe_morCF laterCF laterCF) ].
     Context {Λ : language}.
     Notation iProp := (iPropG Λ Σ).
 
-    Local Instance : savedPropG Λ Σ (cofe_morCF idCF idCF) := _.
+    Local Instance : savedPropG Λ Σ (cofe_morCF laterCF laterCF) := _.
 
     Definition own_pred γ (φ : laterC iProp -n> laterC iProp) : iProp :=
       saved_prop_own γ φ.