Commit e30e19b2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent c0c61da9
Pipeline #17668 canceled with stage
in 6 minutes and 8 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2019-05-20.1.eb3117bd") | (= "dev") }
"coq-iris" { (= "dev.2019-06-05.0.ca513824") | (= "dev") }
]
......@@ -179,24 +179,24 @@ Proof.
Qed.
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)
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.
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).
intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
apply agree_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 -agree_map_compose.
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.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
by apply agreeC_map_ne, cFunctor_contractive.
Qed.
......@@ -296,23 +296,23 @@ Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := authUR (urFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply urFunctor_compose.
Qed.
Instance authURF_contractive F :
urFunctorContractive F urFunctorContractive (authURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.
......@@ -692,58 +692,66 @@ Section cmra_monotone.
End cmra_monotone.
(** Functors *)
Structure rFunctor := RFunctor {
rFunctor_car : ofeT ofeT cmraT;
rFunctor_map {A1 A2 B1 B2} :
Record rFunctor := RFunctor {
rFunctor_car : A `{!Cofe A} B `{!Cofe B}, cmraT;
rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe 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}
rFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
rFunctor_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
rFunctor_map (cid,cid) x x;
rFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
rFunctor_map (fg, g'◎f') x rFunctor_map (g,g') (rFunctor_map (f,f') x);
rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
rFunctor_mono `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CMRAMonotone (rFunctor_map fg)
}.
Existing Instances rFunctor_ne rFunctor_mono.
Instance: Params (@rFunctor_map) 5 := {}.
Instance: Params (@rFunctor_map) 9 := {}.
Class rFunctorContractive (F : rFunctor) :=
rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
Definition rFunctor_diag (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
rFunctor_car F A A.
Coercion rFunctor_diag : rFunctor >-> Funclass.
Program Definition constRF (B : cmraT) : rFunctor :=
{| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
{| 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. rewrite /rFunctorContractive; apply _. Qed.
Structure urFunctor := URFunctor {
urFunctor_car : ofeT ofeT ucmraT;
urFunctor_map {A1 A2 B1 B2} :
urFunctor_car : A `{!Cofe A} B `{!Cofe B}, ucmraT;
urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
((A2 -n> A1) * (B1 -n> B2)) urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
urFunctor_ne A1 A2 B1 B2 n :
Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2);
urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x x;
urFunctor_compose {A1 A2 A3 B1 B2 B3}
urFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
urFunctor_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
urFunctor_map (cid,cid) x x;
urFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
urFunctor_map (fg, g'◎f') x urFunctor_map (g,g') (urFunctor_map (f,f') x);
urFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
urFunctor_mono `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CMRAMonotone (urFunctor_map fg)
}.
Existing Instances urFunctor_ne urFunctor_mono.
Instance: Params (@urFunctor_map) 5 := {}.
Instance: Params (@urFunctor_map) 9 := {}.
Class urFunctorContractive (F : urFunctor) :=
urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
Definition urFunctor_diag (F: urFunctor) (A: ofeT) : ucmraT := urFunctor_car F A A.
Definition urFunctor_diag (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
urFunctor_car F A A.
Coercion urFunctor_diag : urFunctor >-> Funclass.
Program Definition constURF (B : ucmraT) : urFunctor :=
{| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
{| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
Instance constURF_contractive B : urFunctorContractive (constURF B).
......@@ -1105,16 +1113,16 @@ Proof.
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 :=
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.
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. 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.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !rFunctor_compose.
Qed.
......@@ -1122,21 +1130,21 @@ Instance prodRF_contractive F1 F2 :
rFunctorContractive F1 rFunctorContractive F2
rFunctorContractive (prodRF F1 F2).
Proof.
intros ?? A1 A2 B1 B2 n ???;
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodC_map_ne; apply rFunctor_contractive.
Qed.
Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
urFunctor_car A B := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 A2 B1 B2 fg :=
urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
prodC_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply urFunctor_ne.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply urFunctor_ne.
Qed.
Next Obligation. by intros F1 F2 A B [??]; rewrite /= !urFunctor_id. Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
Next Obligation.
intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !urFunctor_compose.
Qed.
......@@ -1144,7 +1152,7 @@ Instance prodURF_contractive F1 F2 :
urFunctorContractive F1 urFunctorContractive F2
urFunctorContractive (prodURF F1 F2).
Proof.
intros ?? A1 A2 B1 B2 n ???;
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodC_map_ne; apply urFunctor_contractive.
Qed.
......@@ -1290,23 +1298,23 @@ Proof.
right; exists (f x), (f y). by rewrite {4}Hxy; eauto.
Qed.
Program Definition optionURF (F : rFunctor) : urFunctor := {|
urFunctor_car A B := optionUR (rFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
urFunctor_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_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x).
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_equiv_ext=>y; apply rFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
Qed.
Instance optionURF_contractive F :
rFunctorContractive F urFunctorContractive (optionURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
......@@ -66,7 +66,7 @@ Canonical Structure csumC : ofeT := OfeT (csum A B) csum_cofe_mixin.
Global Instance csum_discrete : OfeDiscrete A OfeDiscrete B OfeDiscrete csumC.
Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
Global Instance csum_leibniz :
LeibnizEquiv A LeibnizEquiv B LeibnizEquiv (csumC A B).
LeibnizEquiv A LeibnizEquiv B LeibnizEquiv csumC.
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
Global Instance Cinl_timeless a : Discrete a Discrete (Cinl a).
......@@ -340,18 +340,18 @@ Proof.
Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
|}.
Next Obligation.
by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
Qed.
Next Obligation.
intros Fa Fb A B x. rewrite /= -{2}(csum_map_id x).
intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
apply csum_map_ext=>y; apply rFunctor_id.
Qed.
Next Obligation.
intros Fa Fb A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -csum_map_compose.
intros Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -csum_map_compose.
apply csum_map_ext=>y; apply rFunctor_compose.
Qed.
......@@ -359,5 +359,5 @@ Instance csumRF_contractive Fa Fb :
rFunctorContractive Fa rFunctorContractive Fb
rFunctorContractive (csumRF Fa Fb).
Proof.
by intros ?? A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive.
by intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive.
Qed.
......@@ -176,18 +176,18 @@ End functor.
Definition exclRADS (A: ofeT) := exclR A trivial_stepN trivial_stepN_ustep.
Program Definition exclRF (F : cFunctor) : rFunctor := {|
rFunctor_car A B := exclR (cFunctor_car F A B) trivial_stepN trivial_stepN_ustep;
rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
rFunctor_car A _ B _ := exclR (cFunctor_car F A B) trivial_stepN trivial_stepN_ustep;
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.
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).
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.
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.
Next Obligation. intros. econstructor; intros; simpl; eapply excl_map_cmra_monotone; eauto with *. Qed.
......@@ -195,5 +195,5 @@ Next Obligation. intros. econstructor; intros; simpl; eapply excl_map_cmra_monot
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.
......@@ -409,43 +409,43 @@ Proof.
Qed.
Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
cFunctor_car A B := gmapC K (cFunctor_car F A B);
cFunctor_map A1 A2 B1 B2 fg := gmapC_map (cFunctor_map F fg)
cFunctor_car A _ B _ := gmapC K (cFunctor_car F A B);
cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapC_map (cFunctor_map F fg)
|}.
Next Obligation.
by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
Qed.
Next Obligation.
intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
Qed.
Instance gmapCF_contractive K `{Countable K} F :
cFunctorContractive F cFunctorContractive (gmapCF K F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
Qed.
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
urFunctor_car A B := gmapUR K (rFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
Qed.
Next Obligation.
intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
Qed.
Instance gmapRF_contractive K `{Countable K} F :
rFunctorContractive F urFunctorContractive (gmapURF K F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
Qed.
......@@ -292,46 +292,46 @@ Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} n :
Proof. intros f1 f2 Hf g x; apply Hf. Qed.
Program Definition iprodCF `{Finite 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)
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.
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).
intros C ?? F A ? B ? g; simpl. rewrite -{2}(iprod_map_id g).
apply iprod_map_ext=> y; apply cFunctor_id.
Qed.
Next Obligation.
intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
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_contractive `{Finite C} (F : C cFunctor) :
( c, cFunctorContractive (F c)) cFunctorContractive (iprodCF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply: iprodC_map_ne=>c; apply cFunctor_contractive.
Qed.
Program Definition iprodURF `{Finite C} (F : C urFunctor) : urFunctor := {|
urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
urFunctor_car A _ B _ := iprodUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := iprodC_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
intros C ?? F A1 A2 B1 B2 n ?? g.
intros C ?? F A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply iprodC_map_ne=>?; apply urFunctor_ne.
Qed.
Next Obligation.
intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
intros C ?? F A ? B ? g; simpl. rewrite -{2}(iprod_map_id g).
apply iprod_map_ext=> y; apply urFunctor_id.
Qed.
Next Obligation.
intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
intros C ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
apply iprod_map_ext=>y; apply urFunctor_compose.
Qed.
Instance iprodURF_contractive `{Finite C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (iprodURF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply iprodC_map_ne=>c; apply urFunctor_contractive.
Qed.
......@@ -71,25 +71,25 @@ Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
Program Definition listCF (F : cFunctor) : cFunctor := {|
cFunctor_car A B := listC (cFunctor_car F A B);
cFunctor_map A1 A2 B1 B2 fg := listC_map (cFunctor_map F fg)
cFunctor_car A _ B _ := listC (cFunctor_car F A B);
cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listC_map (cFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(list_fmap_id x).
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_equiv_ext=>y. apply cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
Qed.
Instance listCF_contractive F :
cFunctorContractive F cFunctorContractive (listCF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, cFunctor_contractive.
Qed.
(* CMRA *)
......@@ -369,23 +369,23 @@ Proof.
Qed.
Program Definition listURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := listUR (urFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := listC_map (urFunctor_map F fg)
urFunctor_car A _ B _ := listUR (urFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listC_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(list_fmap_id x).
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_equiv_ext=>y. apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
Qed.
Instance listURF_contractive F :
urFunctorContractive F urFunctorContractive (listURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, urFunctor_contractive.
Qed.
......@@ -109,26 +109,26 @@ Proof.
Qed.
Program Definition uPredCF (F : urFunctor) : cFunctor := {|
cFunctor_car A B := uPredC (urFunctor_car F B A);
cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
cFunctor_car A _ B _ := uPredC (urFunctor_car F B A);
cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
intros F A1 A2 B1 B2 n P Q HPQ.
intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
Qed.
Next Obligation.
intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
apply uPred_map_ext=>y. by rewrite urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' P; simpl. rewrite -uPred_map_compose.
apply uPred_map_ext=>y; apply urFunctor_compose.
Qed.
Instance uPredCF_contractive F :
urFunctorContractive F cFunctorContractive (uPredCF F).
Proof.
intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
destruct n; split; by apply HPQ.
Qed.
......
......@@ -247,7 +247,7 @@ Section globale_step.
(a a': A) n, a _(n) a'.