Skip to content
Snippets Groups Projects
Commit 0a279595 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 843905d8 5f20821b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 69 additions and 92 deletions
algebra/agree.v
+ 3
− 0
View file @ 0a279595
......@@ -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
+ 3
− 0
View file @ 0a279595
......@@ -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
+ 7
− 17
View file @ 0a279595
......@@ -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
+ 17
− 28
View file @ 0a279595
......@@ -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
+ 4
− 6
View file @ 0a279595
......@@ -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
+ 6
− 10
View file @ 0a279595
......@@ -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
+ 3
− 0
View file @ 0a279595
......@@ -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
+ 6
− 14
View file @ 0a279595
......@@ -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
+ 6
− 8
View file @ 0a279595
......@@ -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
+ 4
− 0
View file @ 0a279595
......@@ -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
+ 5
− 0
View file @ 0a279595
......@@ -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
+ 5
− 9
View file @ 0a279595
......@@ -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 Λ Σ :=
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment