Bundle non-expansiveness with functors.

So, only use the type class for contractive functors.

algebra/agree.v

@@ -184,6 +184,9 @@ Program Definition agreeRF (F : cFunctor) : rFunctor := {|
   rFunctor_car A B := agreeR (cFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
 |}.
+Next Obligation.
+  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
+Qed.
 Next Obligation.
   intros F A B x; simpl. rewrite -{2}(agree_map_id x).
   apply agree_map_ext=>y. by rewrite cFunctor_id.

algebra/auth.v

@@ -244,6 +244,9 @@ Program Definition authRF (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := authR (rFunctor_car F A B);
   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.
+Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(auth_map_id x).
   apply auth_map_ext=>y; apply rFunctor_id.

algebra/cmra.v

@@ -623,6 +623,8 @@ 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_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 :
@@ -630,21 +632,12 @@ Structure rFunctor := RFunctor {
   rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CMRAMonotone (rFunctor_map fg) 
 }.
-Existing Instances rFunctor_mono.
+Existing Instances rFunctor_ne rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
 
-Class rFunctorNe (F : rFunctor) :=
-  rFunctor_ne A1 A2 B1 B2 n :> Proper (dist n ==> dist n) (@rFunctor_map F A1 A2 B1 B2).
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
 
-(* TODO: Check if this instance hurts us. We don't have such a large search space
-   overall, and because of the priority constCF and laterCF should be the only
-   users of this. *)
-Instance rFunctorContractive_Ne F :
-  rFunctorContractive F → rFunctorNe F.
-Proof. intros ?????. apply contractive_ne, _. Qed.
-
 Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
 Coercion rFunctor_diag : rFunctor >-> Funclass.
 
@@ -653,25 +646,22 @@ Program Definition constRF (B : cmraT) : rFunctor :=
 Solve Obligations with done.
 
 Instance constRF_contractive B : rFunctorContractive (constRF B).
-Proof. intros ????. apply _. Qed.
+Proof. rewrite /rFunctorContractive; apply _. Qed.
 
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
   rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
   rFunctor_map A1 A2 B1 B2 fg :=
     prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
+Next Obligation.
+  intros F1 F2 A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_ne.
+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.
 
-Instance prodRF_ne F1 F2 :
-  rFunctorNe F1 → rFunctorNe F2 → rFunctorNe (prodRF F1 F2).
-Proof.
-  intros ?? A1 A2 B1 B2 n ???;
-    by apply prodC_map_ne; apply rFunctor_ne.
-Qed.
 Instance prodRF_contractive F1 F2 :
   rFunctorContractive F1 → rFunctorContractive F2 →
   rFunctorContractive (prodRF F1 F2).

algebra/cofe.v

@@ -336,26 +336,20 @@ 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_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 Instance cFunctor_ne.
 Instance: Params (@cFunctor_map) 5.
 
-Class cFunctorNe (F : cFunctor) :=
-  cFunctor_ne A1 A2 B1 B2 n :> Proper (dist n ==> dist n) (@cFunctor_map F A1 A2 B1 B2).
 Class cFunctorContractive (F : cFunctor) :=
   cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
 
-(* TODO: Check if this instance hurts us. We don't have such a large search space
-   overall, and because of the priority constCF and laterCF should be the only
-   users of this. *)
-Instance cFunctorContractive_Ne F :
-  cFunctorContractive F → cFunctorNe F.
-Proof. intros ?????. apply contractive_ne, _. Qed.
-
 Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
 Coercion cFunctor_diag : cFunctor >-> Funclass.
 
@@ -364,32 +358,26 @@ Program Definition constCF (B : cofeT) : cFunctor :=
 Solve Obligations with done.
 
 Instance constCF_contractive B : cFunctorContractive (constCF B).
-Proof. intros ????. apply _. Qed.
+Proof. rewrite /cFunctorContractive; apply _. Qed.
 
 Program Definition idCF : cFunctor :=
   {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
 Solve Obligations with done.
 
-Instance idCF_ne : cFunctorNe idCF.
-Proof. intros ????. solve_proper. Qed.
-
 Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
   cFunctor_map A1 A2 B1 B2 fg :=
     prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
 |}.
+Next Obligation.
+  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
+Qed.
 Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed.
 Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !cFunctor_compose.
 Qed.
 
-Instance prodCF_ne F1 F2 :
-  cFunctorNe F1 → cFunctorNe F2 → cFunctorNe (prodCF F1 F2).
-Proof.
-  intros ?? A1 A2 B1 B2 n ???;
-    by apply prodC_map_ne; apply cFunctor_ne.
-Qed.
 Instance prodCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
   cFunctorContractive (prodCF F1 F2).
@@ -403,6 +391,10 @@ Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_map A1 A2 B1 B2 fg :=
     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'] Hfg; simpl in *.
+  apply cofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
+Qed.
 Next Obligation.
   intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
   apply (ne_proper f). apply cFunctor_id.
@@ -412,12 +404,6 @@ Next Obligation.
   rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
 Qed.
 
-Instance cofe_morCF_ne F1 F2 :
-  cFunctorNe F1 → cFunctorNe F2 → cFunctorNe (cofe_morCF F1 F2).
-Proof.
-  intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
-Qed.
 Instance cofe_morCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
   cFunctorContractive (cofe_morCF F1 F2).
@@ -514,6 +500,10 @@ Program Definition laterCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := laterC (cFunctor_car F A B);
   cFunctor_map A1 A2 B1 B2 fg := laterC_map (cFunctor_map F fg)
 |}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n fg fg' ?.
+  by apply (contractive_ne laterC_map), cFunctor_ne.
+Qed.
 Next Obligation.
   intros F A B x; simpl. rewrite -{2}(later_map_id x).
   apply later_map_ext=>y. by rewrite cFunctor_id.
@@ -523,9 +513,8 @@ Next Obligation.
   apply later_map_ext=>y; apply cFunctor_compose.
 Qed.
 
-Instance laterCF_contractive F : 
-  cFunctorNe F → cFunctorContractive (laterCF F).
+Instance laterCF_contractive F : cFunctorContractive (laterCF F).
 Proof.
-  intros ? A1 A2 B1 B2 n fg fg' Hfg.
+  intros A1 A2 B1 B2 n fg fg' Hfg.
   apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
 Qed.

algebra/excl.v

@@ -205,6 +205,9 @@ Program Definition exclRF (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 F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
+Qed.
 Next Obligation.
   intros F A B x; simpl. rewrite -{2}(excl_map_id x).
   apply excl_map_ext=>y. by rewrite cFunctor_id.
@@ -214,13 +217,8 @@ Next Obligation.
   apply excl_map_ext=>y; apply cFunctor_compose.
 Qed.
 
-Instance exclRF_ne F : cFunctorNe F → rFunctorNe (exclRF F).
-Proof.
-  intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
-Qed.
 Instance exclRF_contractive F :
   cFunctorContractive F → rFunctorContractive (exclRF F).
 Proof.
-  intros A1 A2 B1 B2 n x1 x2 ??.
-  by apply exclC_map_ne, cFunctor_contractive.
+  intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
 Qed.

algebra/fin_maps.v

@@ -356,6 +356,9 @@ Program Definition mapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := mapC K (cFunctor_car F A B);
   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.
+Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
   apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
@@ -364,11 +367,6 @@ Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
 Qed.
-
-Instance mapCF_ne K `{Countable K} F : cFunctorNe F → cFunctorNe (mapCF K F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_ne.
-Qed.
 Instance mapCF_contractive K `{Countable K} F :
   cFunctorContractive F → cFunctorContractive (mapCF K F).
 Proof.
@@ -379,6 +377,9 @@ Program Definition mapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := mapR K (rFunctor_car F A B);
   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.
+Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
   apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
@@ -387,11 +388,6 @@ Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
 Qed.
-
-Instance mapRF_ne K `{Countable K} F : rFunctorNe F → rFunctorNe (mapRF K F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_ne.
-Qed.
 Instance mapRF_contractive K `{Countable K} F :
   rFunctorContractive F → rFunctorContractive (mapRF K F).
 Proof.

algebra/frac.v

@@ -248,6 +248,9 @@ Program Definition fracRF (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := fracR (rFunctor_car F A B);
   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.
+Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(frac_map_id x).
   apply frac_map_ext=>y; apply rFunctor_id.

algebra/iprod.v

@@ -292,6 +292,9 @@ Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
   cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
   cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
 |}.
+Next Obligation.
+  intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
+Qed.
 Next Obligation.
   intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
   apply iprod_map_ext=> y; apply cFunctor_id.
@@ -300,13 +303,6 @@ Next Obligation.
   intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
   apply iprod_map_ext=>y; apply cFunctor_compose.
 Qed.
-
-Instance iprodCF_ne {C} (F : C → cFunctor) :
-  (∀ c, cFunctorNe (F c)) → cFunctorNe (iprodCF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply cFunctor_ne.
-Qed.
 Instance iprodCF_contractive {C} (F : C → cFunctor) :
   (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
 Proof.
@@ -318,6 +314,9 @@ Program Definition iprodRF {C} (F : C → rFunctor) : rFunctor := {|
   rFunctor_car A B := iprodR (λ c, rFunctor_car (F c) A B);
   rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg)
 |}.
+Next Obligation.
+  intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply rFunctor_ne.
+Qed.
 Next Obligation.
   intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
   apply iprod_map_ext=> y; apply rFunctor_id.
@@ -326,13 +325,6 @@ Next Obligation.
   intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
   apply iprod_map_ext=>y; apply rFunctor_compose.
 Qed.
-
-Instance iprodRF_ne {C} (F : C → rFunctor) :
-  (∀ c, rFunctorNe (F c)) → rFunctorNe (iprodRF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply rFunctor_ne.
-Qed.
 Instance iprodRF_contractive {C} (F : C → rFunctor) :
   (∀ c, rFunctorContractive (F c)) → rFunctorContractive (iprodRF F).
 Proof.

algebra/option.v

@@ -193,6 +193,9 @@ Program Definition optionCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := optionC (cFunctor_car F A B);
   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.
+Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_setoid_ext=>y; apply cFunctor_id.
@@ -202,10 +205,6 @@ Next Obligation.
   apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
 Qed.
 
-Instance optionCF_ne F : cFunctorNe F → cFunctorNe (optionCF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
-Qed.
 Instance optionCF_contractive F :
   cFunctorContractive F → cFunctorContractive (optionCF F).
 Proof.
@@ -216,6 +215,9 @@ Program Definition optionRF (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := optionR (rFunctor_car F A B);
   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.
+Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_setoid_ext=>y; apply rFunctor_id.
@@ -225,10 +227,6 @@ Next Obligation.
   apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
 Qed.
 
-Instance optionRF_ne F : rFunctorNe F → rFunctorNe (optionRF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
-Qed.
 Instance optionRF_contractive F :
   rFunctorContractive F → rFunctorContractive (optionRF F).
 Proof.

algebra/upred.v

@@ -101,6 +101,10 @@ Program Definition uPredCF (F : rFunctor) : cFunctor := {|
   cFunctor_car A B := uPredC (rFunctor_car F B A);
   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 HPQ.
+  apply uPredC_map_ne, rFunctor_ne; split; by apply HPQ.
+Qed.
 Next Obligation.
   intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
   apply uPred_map_ext=>y. by rewrite rFunctor_id.

program_logic/resources.v

@@ -227,6 +227,11 @@ Program Definition resRF (Λ : language)
   rFunctor_car A B := resR Λ (cFunctor_car F1 A B) (rFunctor_car F2 A B);
   rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
+Next Obligation.
+  intros Λ F1 F2 A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
+  - by apply cFunctor_ne.
+  - by apply rFunctor_ne.
+Qed.
 Next Obligation.
   intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
   apply res_map_ext=>y. apply cFunctor_id. apply rFunctor_id.

program_logic/saved_prop.v

@@ -3,15 +3,11 @@ From program_logic Require Export ghost_ownership.
 Import uPred.
 
 Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
-  SavedPropG {
-    saved_prop_F_contractive :> cFunctorNe F;
-    saved_prop_inG :> inG Λ Σ (agreeR $ laterC (F (iPreProp Λ (globalF Σ))));
-  }.
-Definition savedPropGF (F : cFunctor) `{cFunctorNe F} :
-  gFunctor := GFunctor (agreeRF $ laterCF F).
-Instance inGF_savedPropG `{cFunctorNe F}
-         `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
-Proof. split; try apply _; apply: inGF_inG. Qed.
+  saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))).
+Definition savedPropGF (F : cFunctor) : gFunctor :=
+  GFunctor (agreeRF (laterCF F)).
+Instance inGF_savedPropG  `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
+Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ F}
     (γ : gname) (x : F (iPropG Λ Σ)) : iPropG Λ Σ :=