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

Bump Iris (C→O rename) and remove some dead files.

parent 27f524e0
Pipeline #17961 failed with stage
in 10 minutes and 52 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-06-05.0.ca513824") | (= "dev") }
"coq-iris" { (= "dev.2019-06-18.6.7a983818") | (= "dev") }
]
......@@ -42,7 +42,7 @@ Proof.
* trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
- intros n x y Hxy; split; intros; apply Hxy; auto.
Qed.
Canonical Structure agreeC := OfeT (agree A) agree_cofe_mixin.
Canonical Structure agreeO := OfeT (agree A) agree_cofe_mixin.
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := agree_car x;
......@@ -139,7 +139,7 @@ Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M).
Proof. uPred.unseal; split=> r n ? ? ?; by apply: agree_op_inv. Qed.
End agree.
Arguments agreeC : clear implicits.
Arguments agreeO : clear implicits.
Arguments agreeR : clear implicits.
Program Definition agree_map {A B} (f : A B) (x : agree A) : agree B :=
......@@ -170,33 +170,33 @@ Section agree_map.
Qed.
End agree_map.
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
CofeMor (agree_map f : agreeC A agreeC B).
Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
OfeMor (agree_map f : agreeO A agreeO B).
Instance agreeO_map_ne A B n : Proper (dist n ==> dist n) (@agreeO_map A B).
Proof.
intros f g Hfg x; split; simpl; intros; first done.
by apply dist_le with n; try apply Hfg.
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)
Program Definition agreeRF (F : oFunctor) : rFunctor := {|
rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_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 agreeO_map_ne, oFunctor_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.
apply agree_map_ext=>y. by rewrite oFunctor_id.
Qed.
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.
apply agree_map_ext=>y; apply oFunctor_compose.
Qed.
Instance agreeRF_contractive F :
cFunctorContractive F rFunctorContractive (agreeRF F).
oFunctorContractive F rFunctorContractive (agreeRF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
by apply agreeC_map_ne, cFunctor_contractive.
by apply agreeO_map_ne, oFunctor_contractive.
Qed.
......@@ -48,18 +48,18 @@ Proof.
+ intros ??? [??] [??]; split; etrans; eauto.
- by intros ? [??] [??] [??]; split; apply dist_S.
Qed.
Canonical Structure authC := OfeT (auth A) auth_cofe_mixin.
Canonical Structure authO := OfeT (auth A) auth_cofe_mixin.
Global Instance Auth_timeless a b :
Discrete a Discrete b Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
Global Instance auth_discrete : OfeDiscrete A OfeDiscrete authC.
Global Instance auth_discrete : OfeDiscrete A OfeDiscrete authO.
Proof. intros ? [??]; apply _. Qed.
Global Instance auth_leibniz : LeibnizEquiv A LeibnizEquiv (auth A).
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
End cofe.
Arguments authC : clear implicits.
Arguments authO : clear implicits.
(* CMRA *)
Section cmra.
......@@ -290,17 +290,17 @@ Proof.
intros [??]; split; simpl; try eapply cmra_monotone; eauto.
eapply option_fmap_cmra_monotone; eauto; eapply excl_map_cmra_monotone; apply _.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Definition authO_map {A B} (f : A -n> B) : authO A -n> authO B :=
OfeMor (auth_map f).
Lemma authO_map_ne A B n : Proper (dist n ==> dist n) (@authO_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_map A1 _ A2 _ B1 _ B2 _ fg := authO_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 authO_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
......@@ -314,5 +314,5 @@ 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 authO_map_ne, urFunctor_contractive.
Qed.
......@@ -1115,10 +1115,10 @@ 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)
prodO_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 prodO_map_ne; apply rFunctor_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
Next Obligation.
......@@ -1131,16 +1131,16 @@ Instance prodRF_contractive F1 F2 :
rFunctorContractive (prodRF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodC_map_ne; apply rFunctor_contractive.
by apply prodO_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 :=
prodC_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
prodO_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 prodO_map_ne; apply urFunctor_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
Next Obligation.
......@@ -1153,7 +1153,7 @@ Instance prodURF_contractive F1 F2 :
urFunctorContractive (prodURF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodC_map_ne; apply urFunctor_contractive.
by apply prodO_map_ne; apply urFunctor_contractive.
Qed.
(** ** CMRA for the option type *)
......@@ -1299,10 +1299,10 @@ Proof.
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_map A1 _ A2 _ B1 _ B2 _ fg := optionO_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 optionO_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
......@@ -1316,5 +1316,5 @@ 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 optionO_map_ne, rFunctor_contractive.
Qed.
......@@ -11,7 +11,7 @@ Inductive coPset_disj :=
Section coPset.
Arguments op _ _ !_ !_ /.
Canonical Structure coPset_disjC := leibnizC coPset_disj.
Canonical Structure coPset_disjO := leibnizO coPset_disj.
Instance coPset_disj_valid : Valid coPset_disj := λ X,
match X with CoPset _ => True | CoPsetBot => False end.
......
This diff is collapsed.
......@@ -62,11 +62,11 @@ Proof.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
Qed.
Canonical Structure csumC : ofeT := OfeT (csum A B) csum_cofe_mixin.
Global Instance csum_discrete : OfeDiscrete A OfeDiscrete B OfeDiscrete csumC.
Canonical Structure csumO : ofeT := OfeT (csum A B) csum_cofe_mixin.
Global Instance csum_discrete : OfeDiscrete A OfeDiscrete B OfeDiscrete csumO.
Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
Global Instance csum_leibniz :
LeibnizEquiv A LeibnizEquiv B LeibnizEquiv csumC.
LeibnizEquiv A LeibnizEquiv B LeibnizEquiv csumO.
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
Global Instance Cinl_timeless a : Discrete a Discrete (Cinl a).
......@@ -75,7 +75,7 @@ Global Instance Cinr_timeless b : Discrete b → Discrete (Cinr b).
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
End cofe.
Arguments csumC : clear implicits.
Arguments csumO : clear implicits.
(* Functor on COFEs *)
Definition csum_map {A A' B B'} (fA : A A') (fB : B B')
......@@ -100,11 +100,11 @@ Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
(@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
csumC A B -n> csumC A' B' :=
CofeMor (csum_map f g).
Instance csumC_map_ne A A' B B' n :
Proper (dist n ==> dist n ==> dist n) (@csumC_map A A' B B').
Definition csumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
csumO A B -n> csumO A' B' :=
OfeMor (csum_map f g).
Instance csumO_map_ne A A' B B' n :
Proper (dist n ==> dist n ==> dist n) (@csumO_map A A' B B').
Proof. by intros f f' Hf g g' Hg []; constructor. Qed.
Section cmra.
......@@ -341,10 +341,10 @@ 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_map A1 _ A2 _ B1 _ B2 _ fg := csumO_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 csumO_map_ne; try apply rFunctor_ne.
Qed.
Next Obligation.
intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
......@@ -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 csumO_map_ne; try apply rFunctor_contractive.
Qed.
......@@ -18,7 +18,7 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
Canonical Structure dec_agreeO : ofeT := leibnizO (dec_agree A).
Instance dec_agree_op : Op (dec_agree A) := λ x y,
match x, y with
......@@ -64,5 +64,5 @@ Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
End dec_agree.
Arguments dec_agreeC : clear implicits.
Arguments dec_agreeO : clear implicits.
Arguments dec_agreeR _ {_}.
......@@ -125,7 +125,7 @@ Proof.
- intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
split; [|intros; trans y]; tauto.
Qed.
Canonical Structure validityC : ofeT := discreteC (validity A).
Canonical Structure validityO : ofeT := discreteO (validity A).
Instance dra_valid_proper' : Proper (() ==> iff) (valid : A Prop).
Proof. by split; apply: dra_valid_proper. Qed.
......
......@@ -52,8 +52,8 @@ Proof.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
Qed.
Canonical Structure exclC : ofeT := OfeT (excl A) excl_cofe_mixin.
Global Instance excl_discrete : OfeDiscrete A OfeDiscrete exclC.
Canonical Structure exclO : ofeT := OfeT (excl A) excl_cofe_mixin.
Global Instance excl_discrete : OfeDiscrete A OfeDiscrete exclO.
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
......@@ -136,7 +136,7 @@ Proof.
Qed.
End excl.
Arguments exclC : clear implicits.
Arguments exclO : clear implicits.
Arguments exclR : clear implicits.
(* Functor *)
......@@ -167,33 +167,33 @@ Proof.
- intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n.
move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z.
Qed.
Definition exclC_map (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f).
Instance exclC_map_ne n : Proper (dist n ==> dist n) (exclC_map).
Definition exclO_map (f : A -n> B) : exclO A -n> exclO B :=
OfeMor (excl_map f).
Instance exclO_map_ne n : Proper (dist n ==> dist n) (exclO_map).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
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)
Program Definition exclRF (F : oFunctor) : rFunctor := {|
rFunctor_car A _ B _ := exclR (oFunctor_car F A B) trivial_stepN trivial_stepN_ustep;
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_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 exclO_map_ne, oFunctor_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.
apply excl_map_ext=>y. by rewrite oFunctor_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.
apply excl_map_ext=>y; apply oFunctor_compose.
Qed.
Next Obligation. intros. econstructor; intros; simpl; eapply excl_map_cmra_monotone; eauto with *. Qed.
Instance exclRF_contractive F :
cFunctorContractive F rFunctorContractive (exclRF F).
oFunctorContractive 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 exclO_map_ne, oFunctor_contractive.
Qed.
......@@ -5,7 +5,7 @@ From fri.algebra Require Import upred upred_bi.
Notation frac := Qp (only parsing).
Section frac.
Canonical Structure fracC := leibnizC frac.
Canonical Structure fracO := leibnizO frac.
Instance frac_valid : Valid frac := λ x, (x 1)%Qc.
Instance frac_pcore : PCore frac := λ _, None.
......
......@@ -20,11 +20,11 @@ Proof.
+ by intros m1 m2 m3 ?? k; trans (m2 !! k).
- by intros n m1 m2 ? k; apply dist_S.
Qed.
Canonical Structure gmapC : ofeT := OfeT (gmap K A) gmap_cofe_mixin.
Global Instance gmap_discrete : OfeDiscrete A OfeDiscrete gmapC.
Canonical Structure gmapO : ofeT := OfeT (gmap K A) gmap_cofe_mixin.
Global Instance gmap_discrete : OfeDiscrete A OfeDiscrete gmapO.
Proof. intros ? m m' ? i. by apply (discrete _). Qed.
(* why doesn't this go automatic? *)
Global Instance gmapC_leibniz: LeibnizEquiv A LeibnizEquiv gmapC.
Global Instance gmapO_leibniz: LeibnizEquiv A LeibnizEquiv gmapO.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
Global Instance lookup_ne n k :
......@@ -77,7 +77,7 @@ Global Instance gmap_singleton_timeless i x :
Discrete x Discrete ({[ i := x ]} : gmap K A) := _.
End cofe.
Arguments gmapC _ {_ _} _.
Arguments gmapO _ {_ _} _.
(* CMRA *)
Section cmra.
......@@ -399,42 +399,42 @@ Proof.
- intros m1 m2; rewrite !lookup_included=> Hm i.
by rewrite !lookup_fmap; apply: cmra_monotone.
Qed.
Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A gmapC K B).
Instance gmapC_map_ne `{Countable K} {A B} n :
Proper (dist n ==> dist n) (@gmapC_map K _ _ A B).
Definition gmapO_map `{Countable K} {A B} (f: A -n> B) :
gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A gmapO K B).
Instance gmapO_map_ne `{Countable K} {A B} n :
Proper (dist n ==> dist n) (@gmapO_map K _ _ A B).
Proof.
intros f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
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)
Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
oFunctor_car A _ B _ := gmapO K (oFunctor_car F A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_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 gmapO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
Qed.
Next Obligation.
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.
apply map_fmap_equiv_ext=>y ??; apply oFunctor_compose.
Qed.
Instance gmapCF_contractive K `{Countable K} F :
cFunctorContractive F cFunctorContractive (gmapCF K F).
Instance gmapOF_contractive K `{Countable K} F :
oFunctorContractive F oFunctorContractive (gmapOF 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 gmapO_map_ne, oFunctor_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_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_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 gmapO_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
......@@ -447,5 +447,5 @@ 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 gmapO_map_ne, rFunctor_contractive.
Qed.
......@@ -12,7 +12,7 @@ Section gset.
Context `{Countable K}.
Arguments op _ _ !_ !_ /.
Canonical Structure gset_disjC := leibnizC (gset_disj K).
Canonical Structure gset_disjO := leibnizO (gset_disj K).
Instance gset_disj_valid : Valid (gset_disj K) := λ X,
match X with GSet _ => True | GSetBot => False end.
......
......@@ -286,31 +286,31 @@ Qed.
Definition iprodC_map `{Finite A} {B1 B2 : A ofeT}
(f : iprod (λ x, B1 x -n> B2 x)) :
iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
iprodC B1 -n> iprodC B2 := OfeMor (iprod_map f).
Instance iprodC_map_ne `{Finite A} {B1 B2 : A ofeT} n :
Proper (dist n ==> dist n) (@iprodC_map A _ _ B1 B2).
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)
Program Definition iprodCF `{Finite C} (F : C oFunctor) : oFunctor := {|
oFunctor_car A _ B _ := iprodC (λ c, oFunctor_car (F c) A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := iprodC_map (λ c, oFunctor_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 oFunctor_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.
apply iprod_map_ext=> y; apply oFunctor_id.
Qed.
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.
apply iprod_map_ext=>y; apply oFunctor_compose.
Qed.
Instance iprodCF_contractive `{Finite C} (F : C cFunctor) :
( c, cFunctorContractive (F c)) cFunctorContractive (iprodCF F).
Instance iprodCF_contractive `{Finite C} (F : C oFunctor) :
( c, oFunctorContractive (F c)) oFunctorContractive (iprodCF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply: iprodC_map_ne=>c; apply cFunctor_contractive.
by apply: iprodC_map_ne=>c; apply oFunctor_contractive.
Qed.
Program Definition iprodURF `{Finite C} (F : C urFunctor) : urFunctor := {|
......
......@@ -49,8 +49,8 @@ Proof.
- apply _.
- rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
Qed.
Canonical Structure listC := OfeT (list A) list_cofe_mixin.
Global Instance list_discrete : OfeDiscrete A OfeDiscrete listC.
Canonical Structure listO := OfeT (list A) list_cofe_mixin.
Global Instance list_discrete : OfeDiscrete A OfeDiscrete listO.
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
Global Instance nil_timeless : Discrete (@nil A).
......@@ -59,37 +59,37 @@ Global Instance cons_timeless x l : Discrete x → Discrete l → Discrete (x ::
Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
End cofe.
Arguments listC : clear implicits.
Arguments listO : clear implicits.
(** Functor *)
Instance list_fmap_ne {A B : ofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (fmap (M:=list) f).
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
CofeMor (fmap f : listC A listC B).
Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
OfeMor (fmap f : listO A listO B).
Instance listO_map_ne A B n : Proper (dist n ==> dist n) (@listO_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)
Program Definition listOF (F : oFunctor) : oFunctor := {|
oFunctor_car A _ B _ := listO (oFunctor_car F A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_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 listO_map_ne, oFunctor_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_equiv_ext=>y. apply cFunctor_id.
apply list_fmap_equiv_ext=>y. apply oFunctor_id.
Qed.
Next Obligation.
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.
apply list_fmap_equiv_ext=>y; apply oFunctor_compose.
Qed.
Instance listCF_contractive F :
cFunctorContractive F cFunctorContractive (listCF F).
Instance listOF_contractive F :
oFunctorContractive F oFunctorContractive (listOF 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 listO_map_ne, oFunctor_contractive.
Qed.
(* CMRA *)
......@@ -370,10 +370,10 @@ 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_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
|}.