Commit 2467bf21 authored by Ralf Jung's avatar Ralf Jung

Add both non-expansive and contractive functors, and bundle them for the...

Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.
parent 3d448c5d
Pipeline #273 passed with stage
......@@ -184,10 +184,6 @@ 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 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).
apply agree_map_ext=>y. by rewrite cFunctor_id.
......@@ -196,3 +192,10 @@ Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
apply agree_map_ext=>y; apply cFunctor_compose.
Qed.
Instance agreeRF_contractive F :
cFunctorContractive F rFunctorContractive (agreeRF F).
Proof.
intros ? A1 A2 B1 B2 n ???; simpl.
by apply agreeC_map_ne, cFunctor_contractive.
Qed.
......@@ -244,9 +244,6 @@ 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_contractive.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply rFunctor_id.
......@@ -255,3 +252,9 @@ Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply rFunctor_compose.
Qed.
Instance authRF_contractive F :
rFunctorContractive F rFunctorContractive (authRF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_contractive.
Qed.
......@@ -623,7 +623,6 @@ 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_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 :
......@@ -631,9 +630,21 @@ Structure rFunctor := RFunctor {
rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
CMRAMonotone (rFunctor_map fg)
}.
Existing Instances rFunctor_contractive rFunctor_mono.
Existing Instances 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.
......@@ -641,17 +652,30 @@ Program Definition constRF (B : cmraT) : rFunctor :=
{| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. intros ????. 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.
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.
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).
Proof.
intros ?? A1 A2 B1 B2 n ???;
by apply prodC_map_ne; apply rFunctor_contractive.
Qed.
......@@ -336,16 +336,26 @@ 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_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 (fg, g'f') x cFunctor_map (g,g') (cFunctor_map (f,f') x)
}.
Existing Instances cFunctor_contractive.
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.
......@@ -353,30 +363,46 @@ Program Definition constCF (B : cofeT) : cFunctor :=
{| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
Instance constCF_contractive B : cFunctorContractive (constCF B).
Proof. intros ????. 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.
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.
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).
Proof.
intros ?? A1 A2 B1 B2 n ???;
by apply prodC_map_ne; apply cFunctor_contractive.
Qed.
Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
cFunctor_car A B := cofe_mor (cFunctor_car F1 B A) (cFunctor_car F2 A B);
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_contractive=>i ?; split; by apply Hfg.
Qed.
Next Obligation.
intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
apply (ne_proper f). apply cFunctor_id.
......@@ -386,6 +412,20 @@ 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).
Proof.
intros ?? 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.
(** Discrete cofe *)
Section discrete_cofe.
Context `{Equiv A, @Equivalence A ()}.
......@@ -470,13 +510,22 @@ Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
Program Definition laterCF : cFunctor := {|
cFunctor_car A B := laterC B;
cFunctor_map A1 A2 B1 B2 fg := laterC_map (fg.2)
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 A1 A2 B1 B2 n fg fg' Hfg.
apply laterC_map_contractive=> i ?; by apply Hfg.
intros F A B x; simpl. rewrite -{2}(later_map_id x).
apply later_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 -later_map_compose.
apply later_map_ext=>y; apply cFunctor_compose.
Qed.
Instance laterCF_contractive F :
cFunctorNe F cFunctorContractive (laterCF F).
Proof.
intros ? A1 A2 B1 B2 n fg fg' Hfg.
apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
Qed.
Next Obligation. by intros A B []. Qed.
Next Obligation. by intros A1 A2 A3 B1 B2 B3 f g f' g' []. Qed.
......@@ -11,7 +11,8 @@ Arguments solution_unfold {_} _.
Arguments solution_fold {_} _.
Module solver. Section solver.
Context (F : cFunctor) `{Finhab : Inhabited (F unitC)}.
Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
`{Finhab : Inhabited (F unitC)}.
Notation map := (cFunctor_map F).
Fixpoint A (k : nat) : cofeT :=
......
......@@ -201,14 +201,10 @@ 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 (F : cFunctor) : rFunctor := {|
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 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.
......@@ -217,3 +213,14 @@ 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.
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.
Qed.
......@@ -356,9 +356,6 @@ 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 ?; apply mapC_map_ne, cFunctor_contractive.
Qed.
Next Obligation.
intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
......@@ -368,13 +365,20 @@ Next Obligation.
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.
by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_contractive.
Qed.
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 ?; apply mapC_map_ne, rFunctor_contractive.
Qed.
Next Obligation.
intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
......@@ -383,3 +387,13 @@ 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.
by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_contractive.
Qed.
......@@ -248,9 +248,6 @@ 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_contractive.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(frac_map_id x).
apply frac_map_ext=>y; apply rFunctor_id.
......@@ -259,3 +256,9 @@ Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -frac_map_compose.
apply frac_map_ext=>y; apply rFunctor_compose.
Qed.
Instance fracRF_contractive F :
rFunctorContractive F rFunctorContractive (fracRF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
Qed.
......@@ -292,10 +292,6 @@ 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=>c; apply cFunctor_contractive.
Qed.
Next Obligation.
intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
apply iprod_map_ext=> y; apply cFunctor_id.
......@@ -305,14 +301,23 @@ Next Obligation.
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.
intros ? A1 A2 B1 B2 n ?? g.
by apply iprodC_map_ne=>c; apply cFunctor_contractive.
Qed.
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=>c; apply rFunctor_contractive.
Qed.
Next Obligation.
intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
apply iprod_map_ext=> y; apply rFunctor_id.
......@@ -321,3 +326,16 @@ 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.
intros ? A1 A2 B1 B2 n ?? g.
by apply iprodC_map_ne=>c; apply rFunctor_contractive.
Qed.
......@@ -193,9 +193,6 @@ 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_contractive.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply cFunctor_id.
......@@ -205,13 +202,20 @@ 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.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
Qed.
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_contractive.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply rFunctor_id.
......@@ -220,3 +224,13 @@ Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
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.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
......@@ -101,10 +101,6 @@ 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_contractive=> i ?; 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.
......@@ -114,6 +110,13 @@ Next Obligation.
apply uPred_map_ext=>y; apply rFunctor_compose.
Qed.
Instance uPredCF_contractive F :
rFunctorContractive F cFunctorContractive (uPredCF F).
Proof.
intros ? A1 A2 B1 B2 n P Q HPQ.
apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
Qed.
(** logical entailement *)
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
{ uPred_in_entails : n x, {n} x P n x Q n x }.
......
......@@ -12,7 +12,7 @@ Definition client : expr [] :=
(^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
Section client.
Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Definition y_inv q y : iProp :=
......@@ -33,7 +33,7 @@ Section client.
rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
rewrite comm. apply sep_mono_r. apply wand_intro_l.
rewrite sep_exist_r. apply exist_elim=>f. wp_seq.
(* TODO these aprenthesis are rather surprising. *)
(* TODO these parenthesis are rather surprising. *)
(ewp apply: (wp_load heapN _ _ q f)); eauto with I.
strip_later. (* hu, shouldn't it do that? *)
rewrite -assoc. apply sep_mono_r. apply wand_intro_l.
......@@ -76,7 +76,7 @@ Qed.
End client.
Section ClosedProofs.
Definition Σ : rFunctorG := #[ heapGF ; barrierGF ; spawnGF ].
Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
Notation iProp := (iPropG heap_lang Σ).
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
......
......@@ -10,17 +10,17 @@ 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 Σ laterCF;
barrier_savedPropG :> savedPropG heap_lang Σ (laterCF idCF);
}.
(** The Functors we need. *)
Definition barrierGF : rFunctors := [stsGF sts; agreeRF laterCF].
Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF (laterCF idCF)].
(* Show and register that they match. *)
Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ}.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
......@@ -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:=laterCF) _ (Next P)).
eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF idCF) _ (Next P)).
rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
apply exist_elim=>i.
trans (pvs (heap_ctx heapN
......@@ -182,7 +182,7 @@ Proof.
rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?.
apply exist_elim=>i. rewrite -!(assoc ()%I). apply const_elim_sep_l=>?.
wp_focus (! _)%E.
(* I think some evars here are better than repeating *everything* *)
eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
......@@ -231,7 +231,7 @@ Proof.
rename P1 into R1. rename P2 into R2. intros HN.
rewrite {1}/recv /barrier_ctx.
apply exist_elim=>γ. rewrite sep_exist_r. apply exist_elim=>P.
apply exist_elim=>Q. apply exist_elim=>i. rewrite -!assoc.
apply exist_elim=>Q. apply exist_elim=>i. rewrite -!(assoc ()%I).
apply const_elim_sep_l=>?. rewrite -pvs_trans'.
(* I think some evars here are better than repeating *everything* *)
eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
......
......@@ -4,7 +4,7 @@ From barrier Require Import proof.
Import uPred.
Section spec.
Context {Σ : rFunctorG} `{!heapG Σ} `{!barrierG Σ}.
Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
......
......@@ -12,7 +12,7 @@ Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Section derived.
Context {Σ : rFunctor}.
Context {Σ : iFunctor}.
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val iProp heap_lang Σ.
......
......@@ -15,7 +15,7 @@ Class heapG Σ := HeapG {
heap_name : gname
}.
(** The Functor we need. *)
Definition heapGF : rFunctor := authGF heapR.
Definition heapGF : gFunctor := authGF heapR.
Definition to_heap : state heapR := fmap (λ v, Frac 1 (DecAgree v)).
Definition of_heap : heapR state :=
......@@ -43,7 +43,7 @@ Notation "l ↦{ q } v" := (heap_mapsto l q v)
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : rFunctorG}.
Context {Σ : gFunctors}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val iPropG heap_lang Σ.
......
......@@ -7,7 +7,7 @@ Import uPred.
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
Section lifting.
Context {Σ : rFunctor}.
Context {Σ : iFunctor}.
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val iProp heap_lang Σ.
Implicit Types K : ectx.
......
......@@ -15,7 +15,7 @@ Infix "||" := ParV : expr_scope.
Infix "||" := Par : expr_scope.
Section proof.
Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
......
......@@ -20,15 +20,15 @@ Class spawnG Σ := SpawnG {
spawn_tokG :> inG heap_lang Σ (exclR unitC);
}.
(** The functor we need. *)
Definition spawnGF : rFunctors := [constRF (exclR unitC)].
Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
(* Show and register that they match. *)
Instance inGF_spawnG
`{inGF heap_lang Σ (constRF (exclR unitC))} : spawnG Σ.
Proof. split. apply: inGF_inG. Qed.
`{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
......
......@@ -70,7 +70,7 @@ Section LiftingTests.
End LiftingTests.
Section ClosedProofs.
Definition Σ : rFunctorG := #[ heapGF ].
Definition Σ : gFunctors := #[ heapGF ].
Notation iProp := (iPropG heap_lang Σ).
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
......