Commit 739cc004 authored by Robbert's avatar Robbert

Merge branch 'robbert/oFunctor' into 'master'

Notion of composition on `oFunctor`s, and some renaming

See merge request iris/iris!411
parents 0ccaa796 42c191a8
......@@ -88,6 +88,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
`inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q` and (similar for `na_inv_iff` and
`cinv_iff`), following e.g., `inv_alter` and `wp_wand`.
* Add lemma `is_lock_iff` and show that `is_lock` is contractive.
* Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into
`{o,r,ur}Functor_map_{ne,id,compose,contractive}`.
* Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors.
**Changes in heap_lang:**
......
......@@ -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.
This diff is collapsed.
......@@ -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.
This diff is collapsed.
......@@ -92,7 +92,7 @@ Program Definition vecOF (F : oFunctor) m : oFunctor := {|
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecO_map m (oFunctor_map F fg)
|}.
Next Obligation.
intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_ne.
intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros F m A ? B ? l.
......@@ -103,11 +103,11 @@ Next Obligation.
intros F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
change (vec_to_list (vec_map m (oFunctor_map F (f g, g' f')) l)
vec_map m (oFunctor_map F (g, g')) (vec_map m (oFunctor_map F (f, f')) l)).
rewrite !vec_to_list_map. by apply: (oFunctor_compose (listOF F) f g f' g').
rewrite !vec_to_list_map. by apply: (oFunctor_map_compose (listOF F) f g f' g').
Qed.
Instance vecOF_contractive F m :
oFunctorContractive F oFunctorContractive (vecOF F m).
Proof.
by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_contractive.
by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_map_contractive.
Qed.
......@@ -26,10 +26,10 @@ the agreement CMRA. *)
category of CMRAs with a proof that it is locally contractive. *)
Structure gFunctor := GFunctor {
gFunctor_F :> rFunctor;
gFunctor_contractive : rFunctorContractive gFunctor_F;
gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
Arguments GFunctor _ {_}.
Existing Instance gFunctor_contractive.
Existing Instance gFunctor_map_contractive.
Add Printing Constructor gFunctor.
(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
......
......@@ -60,7 +60,7 @@ Section saved_anything.
set (G1 := oFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := oFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
assert ( z, G2 (G1 z) z) as help.
{ intros z. rewrite /G1 /G2 -oFunctor_compose -{2}[z]oFunctor_id.
{ intros z. rewrite /G1 /G2 -oFunctor_map_compose -{2}[z]oFunctor_map_id.
apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
Qed.
......
......@@ -165,22 +165,22 @@ Program Definition uPredOF (F : urFunctor) : oFunctor := {|
|}.
Next Obligation.
intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
apply uPredO_map_ne, urFunctor_ne; split; by apply HPQ.
apply uPredO_map_ne, urFunctor_map_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 urFunctor_id.
apply uPred_map_ext=>y. by rewrite urFunctor_map_id.
Qed.
Next Obligation.
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.
apply uPred_map_ext=>y; apply urFunctor_map_compose.
Qed.
Instance uPredOF_contractive F :
urFunctorContractive F oFunctorContractive (uPredOF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredO_map_ne, urFunctor_contractive.
destruct n; split; by apply HPQ.
intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
apply uPredO_map_ne, urFunctor_map_contractive. destruct n; split; by apply HPQ.
Qed.
(** logical entailement *)
......
Markdown is supported
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