Commit abe2e507 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into

`{o,r,ur}Functor_map_{ne,id,compose,contractive}`.
parent 0ccaa796
......@@ -310,20 +310,20 @@ Program Definition agreeRF (F : oFunctor) : rFunctor := {|
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
|}.
Next Obligation.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_ne.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
apply (agree_map_ext _)=>y. by rewrite oFunctor_id.
apply (agree_map_ext _)=>y. by rewrite oFunctor_map_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 oFunctor_compose.
apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
Qed.
Instance agreeRF_contractive F :
oFunctorContractive F rFunctorContractive (agreeRF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
by apply agreeO_map_ne, oFunctor_contractive.
by apply agreeO_map_ne, oFunctor_map_contractive.
Qed.
......@@ -455,21 +455,21 @@ Program Definition authRF (F : urFunctor) : rFunctor := {|
rFunctor_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 authO_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
apply (auth_map_ext _ _)=>y; apply urFunctor_id.
apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
Qed.
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 urFunctor_compose.
apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
Qed.
Instance authRF_contractive F :
urFunctorContractive F rFunctorContractive (authRF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
......@@ -477,19 +477,19 @@ Program Definition authURF (F : urFunctor) : urFunctor := {|
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 authO_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
apply (auth_map_ext _ _)=>y; apply urFunctor_id.
apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
Qed.
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 urFunctor_compose.
apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
Qed.
Instance authURF_contractive F :
urFunctorContractive F urFunctorContractive (authURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
Qed.
......@@ -779,25 +779,25 @@ 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 `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
rFunctor_map_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_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}
rFunctor_map_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_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_ne rFunctor_mor.
Existing Instances rFunctor_map_ne rFunctor_mor.
Instance: Params (@rFunctor_map) 9 := {}.
Delimit Scope rFunctor_scope with RF.
Bind Scope rFunctor_scope with rFunctor.
Class rFunctorContractive (F : rFunctor) :=
rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
......@@ -816,25 +816,25 @@ Record urFunctor := URFunctor {
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 `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
urFunctor_map_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_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}
urFunctor_map_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_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_ne urFunctor_mor.
Existing Instances urFunctor_map_ne urFunctor_mor.
Instance: Params (@urFunctor_map) 9 := {}.
Delimit Scope urFunctor_scope with URF.
Bind Scope urFunctor_scope with urFunctor.
Class urFunctorContractive (F : urFunctor) :=
urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
......@@ -1253,12 +1253,12 @@ Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_ne.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_map_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !rFunctor_compose.
by rewrite !rFunctor_map_compose.
Qed.
Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
......@@ -1267,7 +1267,7 @@ Instance prodRF_contractive F1 F2 :
rFunctorContractive (prodRF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodO_map_ne; apply rFunctor_contractive.
by apply prodO_map_ne; apply rFunctor_map_contractive.
Qed.
Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
......@@ -1276,12 +1276,12 @@ Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_ne.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_map_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !urFunctor_compose.
by rewrite !urFunctor_map_compose.
Qed.
Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
......@@ -1290,7 +1290,7 @@ Instance prodURF_contractive F1 F2 :
urFunctorContractive (prodURF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodO_map_ne; apply urFunctor_contractive.
by apply prodO_map_ne; apply urFunctor_map_contractive.
Qed.
(** ** CMRA for the option type *)
......@@ -1527,21 +1527,21 @@ Program Definition optionRF (F : rFunctor) : rFunctor := {|
rFunctor_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 optionO_map_ne, rFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_equiv_ext=>y; apply rFunctor_id.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
Qed.
Next Obligation.
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.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
Qed.
Instance optionRF_contractive F :
rFunctorContractive F rFunctorContractive (optionRF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
Qed.
Program Definition optionURF (F : rFunctor) : urFunctor := {|
......@@ -1549,21 +1549,21 @@ Program Definition optionURF (F : rFunctor) : urFunctor := {|
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 optionO_map_ne, rFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_equiv_ext=>y; apply rFunctor_id.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
Qed.
Next Obligation.
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.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
Qed.
Instance optionURF_contractive F :
rFunctorContractive F urFunctorContractive (optionURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
Qed.
(* Dependently-typed functions over a discrete domain *)
......@@ -1650,19 +1650,19 @@ Program Definition discrete_funURF {C} (F : C → urFunctor) : urFunctor := {|
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_ne.
intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
Qed.
Next Obligation.
intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
apply discrete_fun_map_ext=> y; apply urFunctor_id.
apply discrete_fun_map_ext=> y; apply urFunctor_map_id.
Qed.
Next Obligation.
intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
apply discrete_fun_map_ext=>y; apply urFunctor_compose.
apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
Qed.
Instance discrete_funURF_contractive {C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (discrete_funURF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply discrete_funO_map_ne=>c; apply urFunctor_contractive.
by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
Qed.
......@@ -34,14 +34,15 @@ Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) x.
Proof using Fcontr.
induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -oFunctor_compose -{2}[x]oFunctor_id. by apply (contractive_proper map).
rewrite -oFunctor_map_compose -{2}[x]oFunctor_map_id.
by apply (contractive_proper map).
Qed.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x.
Proof using Fcontr.
induction k as [|k IH]; simpl.
- rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
- rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
apply (contractive_0 map).
- rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
- rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
by apply (contractive_S map).
Qed.
......@@ -183,7 +184,7 @@ Next Obligation.
assert ( k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
induction k as [|k IH]; simpl; first done.
rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
rewrite f_S -oFunctor_compose.
rewrite f_S -oFunctor_map_compose.
by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed.
Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
......@@ -197,7 +198,7 @@ Program Definition fold (X : oFunctor_apply F T) : T :=
{| tower_car n := g n (map (embed' n,project n) X) |}.
Next Obligation.
intros X k. apply (_ : Proper (() ==> ()) (g k)).
rewrite g_S -oFunctor_compose.
rewrite g_S -oFunctor_map_compose.
apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
Qed.
Instance fold_ne : NonExpansive fold.
......@@ -212,7 +213,7 @@ Proof using Type*.
{ rewrite /unfold (conv_compl n (unfold_chain X)).
rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
rewrite f_S -!oFunctor_compose; apply (contractive_ne map); split=> Y.
rewrite f_S -!oFunctor_map_compose; apply (contractive_ne map); split=> Y.
+ rewrite /embed' /= /embed_coerce.
destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
......@@ -222,14 +223,14 @@ Proof using Type*.
assert ( i k (x : A (S i + k)) (H : S i + k = i + S k),
map (ff i, gg i) x gg i (coerce H x)) as map_ff_gg.
{ intros i; induction i as [|i IH]; intros k' x H; simpl.
{ by rewrite coerce_id oFunctor_id. }
rewrite oFunctor_compose g_coerce; apply IH. }
{ by rewrite coerce_id oFunctor_map_id. }
rewrite oFunctor_map_compose g_coerce; apply IH. }
assert (H: S n + k = n + S k) by lia.
rewrite (map_ff_gg _ _ _ H).
apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
- intros X; rewrite equiv_dist=> n /=.
rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=.
rewrite g_S -!oFunctor_compose -{2}[X]oFunctor_id.
rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id.
apply (contractive_ne map); split => Y /=.
+ rewrite f_tower. apply dist_S. by rewrite embed_tower.
+ etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
......
......@@ -375,15 +375,15 @@ Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
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 csumO_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_map_ne.
Qed.
Next Obligation.
intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
apply csum_map_ext=>y; apply rFunctor_id.
apply csum_map_ext=>y; apply rFunctor_map_id.
Qed.
Next Obligation.
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.
apply csum_map_ext=>y; apply rFunctor_map_compose.
Qed.
Instance csumRF_contractive Fa Fb :
......@@ -391,5 +391,5 @@ Instance csumRF_contractive Fa Fb :
rFunctorContractive (csumRF Fa Fb).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
by apply csumO_map_ne; try apply rFunctor_contractive.
by apply csumO_map_ne; try apply rFunctor_map_contractive.
Qed.
......@@ -154,19 +154,19 @@ Program Definition exclRF (F : oFunctor) : rFunctor := {|
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 exclO_map_ne, oFunctor_ne.
intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
apply excl_map_ext=>y. by rewrite oFunctor_id.
apply excl_map_ext=>y. by rewrite oFunctor_map_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 oFunctor_compose.
apply excl_map_ext=>y; apply oFunctor_map_compose.
Qed.
Instance exclRF_contractive F :
oFunctorContractive F rFunctorContractive (exclRF F).
Proof.
intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_contractive.
intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
Qed.
......@@ -628,20 +628,20 @@ Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
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 gmapO_map_ne, oFunctor_ne.
by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_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 oFunctor_compose.
apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
Qed.
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 gmapO_map_ne, oFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_contractive.
Qed.
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
......@@ -649,18 +649,18 @@ Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
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 gmapO_map_ne, rFunctor_ne.
by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_ne.
Qed.
Next Obligation.
intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_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 rFunctor_compose.
apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_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 gmapO_map_ne, rFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
Qed.
......@@ -162,21 +162,21 @@ Program Definition listOF (F : oFunctor) : oFunctor := {|
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 listO_map_ne, oFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_equiv_ext=>y. apply oFunctor_id.
apply list_fmap_equiv_ext=>y. apply oFunctor_map_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 oFunctor_compose.
apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
Qed.
Instance listOF_contractive F :
oFunctorContractive F oFunctorContractive (listOF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
Qed.
(* CMRA *)
......@@ -550,19 +550,19 @@ Program Definition listURF (F : urFunctor) : urFunctor := {|
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_ne.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_equiv_ext=>y. apply urFunctor_id.
apply list_fmap_equiv_ext=>y. apply urFunctor_map_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 urFunctor_compose.
apply list_fmap_equiv_ext=>y; apply urFunctor_map_compose.
Qed.
Instance listURF_contractive F :
urFunctorContractive F urFunctorContractive (listURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_contractive.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
Qed.
......@@ -689,22 +689,22 @@ Record oFunctor := OFunctor {
oFunctor_car : A `{!Cofe A} B `{!Cofe B}, ofeT;
oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
((A2 -n> A1) * (B1 -n> B2)) oFunctor_car A1 B1 -n> oFunctor_car A2 B2;
oFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
oFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
NonExpansive (@oFunctor_map A1 _ A2 _ B1 _ B2 _);
oFunctor_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
oFunctor_map_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
oFunctor_map (cid,cid) x x;
oFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
oFunctor_map_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 :
oFunctor_map (fg, g'f') x oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.
Existing Instance oFunctor_ne.
Existing Instance oFunctor_map_ne.
Instance: Params (@oFunctor_map) 9 := {}.
Delimit Scope oFunctor_scope with OF.
Bind Scope oFunctor_scope with oFunctor.
Class oFunctorContractive (F : oFunctor) :=
oFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
Hint Mode oFunctorContractive ! : typeclass_instances.
......@@ -732,12 +732,12 @@ Program Definition prodOF (F1 F2 : oFunctor) : oFunctor := {|
prodO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
|}.
Next Obligation.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_ne.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_map_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_id. Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_map_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !oFunctor_compose.
by rewrite !oFunctor_map_compose.
Qed.
Notation "F1 * F2" := (prodOF F1%OF F2%OF) : oFunctor_scope.
......@@ -746,7 +746,7 @@ Instance prodOF_contractive F1 F2 :
oFunctorContractive (prodOF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply prodO_map_ne; apply oFunctor_contractive.
by apply prodO_map_ne; apply oFunctor_map_contractive.
Qed.
Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
......@@ -756,15 +756,15 @@ Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
apply ofe_morO_map_ne; apply oFunctor_ne; split; by apply Hfg.
apply ofe_morO_map_ne; apply oFunctor_map_ne; split; by apply Hfg.
Qed.
Next Obligation.
intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_id.
apply (ne_proper f). apply oFunctor_id.
intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_map_id.
apply (ne_proper f). apply oFunctor_map_id.
Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
rewrite -!oFunctor_compose. do 2 apply (ne_proper _). apply oFunctor_compose.
rewrite -!oFunctor_map_compose. do 2 apply (ne_proper _). apply oFunctor_map_compose.
Qed.
Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
......@@ -773,7 +773,7 @@ Instance ofe_morOF_contractive F1 F2 :
oFunctorContractive (ofe_morOF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
apply ofe_morO_map_ne; apply oFunctor_contractive; destruct n, Hfg; by split.
apply ofe_morO_map_ne; apply oFunctor_map_contractive; destruct n, Hfg; by split.
Qed.
(** * Sum type *)
......@@ -848,12 +848,12 @@ Program Definition sumOF (F1 F2 : oFunctor) : oFunctor := {|
sumO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
|}.
Next Obligation.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_ne.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_map_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_id. Qed.
Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_map_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [?|?]; simpl;
by rewrite !oFunctor_compose.
by rewrite !oFunctor_map_compose.
Qed.
Notation "F1 + F2" := (sumOF F1%OF F2%OF) : oFunctor_scope.
......@@ -862,7 +862,7 @@ Instance sumOF_contractive F1 F2 :
oFunctorContractive (sumOF F1 F2).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
by apply sumO_map_ne; apply oFunctor_contractive.
by apply sumO_map_ne; apply oFunctor_map_contractive.