Skip to content

GitLab

I
iris
Commit 45d4e2a6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Turn the arguments of functors into COFEs. 

This allows one to make use of recursive ghost state obtained from the
recursive domain equation solver.
parent ccd42ca7
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 212 additions and 192 deletions
theories/algebra/agree.v
View file @ 45d4e2a6
......@@ -306,24 +306,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.
theories/algebra/auth.v
View file @ 45d4e2a6
......@@ -403,13 +403,13 @@ Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_id. Qed.
Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
auth_map (g ∘ f) x = auth_map g (auth_map f x).
Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_compose. Qed.
Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{_ : NonExpansive f} x :
Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{!NonExpansive f} x :
(∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
Proof.
constructor; simpl; auto.
apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Qed.
Instance auth_map_ne {A B : ofeT} (f : A -> B) {Hf : NonExpansive f} :
Instance auth_map_ne {A B : ofeT} (f : A -> B) `{Hf : !NonExpansive f} :
NonExpansive (auth_map f).
Proof.
intros n [??] [??] [??]; split; simpl in *; [|by apply Hf].
......@@ -437,45 +437,45 @@ Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
apply agreeC_map_ne; auto. Qed.
Program Definition authRF (F : urFunctor) : rFunctor := {|
rFunctor_car A B := authR (urFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
rFunctor_car A _ B _ := authR (urFunctor_car F A B);
rFunctor_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).
apply auth_map_ext=>y. apply _. apply urFunctor_id.
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.
apply auth_map_ext=>y. apply _. apply urFunctor_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 authRF_contractive F :
urFunctorContractive F → rFunctorContractive (authRF 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.
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).
apply auth_map_ext=>y. apply _. apply urFunctor_id.
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.
apply auth_map_ext=>y. apply _. apply urFunctor_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.
theories/algebra/cmra.v
View file @ 45d4e2a6
This diff is collapsed.
theories/algebra/cofe_solver.v
View file @ 45d4e2a6
......@@ -4,8 +4,8 @@ Set Default Proof Using "Type".
Record solution (F : cFunctor) := Solution {
solution_car :> ofeT;
solution_cofe : Cofe solution_car;
solution_unfold : solution_car -n> F solution_car;
solution_fold : F solution_car -n> solution_car;
solution_unfold : solution_car -n> F solution_car _;
solution_fold : F solution_car _ -n> solution_car;
solution_fold_unfold X : solution_fold (solution_unfold X) ≡ X;
solution_unfold_fold X : solution_unfold (solution_fold X) ≡ X
}.
......@@ -14,21 +14,25 @@ Arguments solution_fold {_} _.
Existing Instance solution_cofe.
Module solver. Section solver.
Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
`{Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)} `{Finh : Inhabited (F unitC)}.
Context (F : cFunctor) `{Fcontr : cFunctorContractive F}.
Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
Context `{Finh : Inhabited (F unitC _)}.
Notation map := (cFunctor_map F).
Fixpoint A (k : nat) : ofeT :=
match k with 0 => unitC | S k => F (A k) end.
Local Instance: ∀ k, Cofe (A k).
Proof using Fcofe. induction k; apply _. Defined.
Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
match k with
| 0 => existT (P:=Cofe) unitC _
| S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
end.
Notation A k := (projT1 (A' k)).
Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
Arguments A : simpl never.
Arguments f : simpl never.
Arguments g : simpl never.
......@@ -177,7 +181,7 @@ Proof.
- rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
Qed.
Program Definition unfold_chain (X : T) : chain (F T) :=
Program Definition unfold_chain (X : T) : chain (F T _) :=
{| chain_car n := map (project n,embed' n) (X (S n)) |}.
Next Obligation.
intros X n i Hi.
......@@ -187,14 +191,14 @@ Next Obligation.
rewrite f_S -cFunctor_compose.
by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed.
Definition unfold (X : T) : F T := compl (unfold_chain X).
Definition unfold (X : T) : F T _ := compl (unfold_chain X).
Instance unfold_ne : NonExpansive unfold.
Proof.
intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
(conv_compl n (unfold_chain Y)) /= (HXY (S n)).
Qed.
Program Definition fold (X : F T) : T :=
Program Definition fold (X : F T _) : T :=
{| tower_car n := g n (map (embed' n,project n) X) |}.
Next Obligation.
intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
......
theories/algebra/csum.v
View file @ 45d4e2a6
......@@ -100,7 +100,7 @@ Global Instance csum_ofe_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_discrete a : Discrete a → Discrete (Cinl a).
......@@ -367,18 +367,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.
......@@ -386,5 +386,6 @@ 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.
intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
by apply csumC_map_ne; try apply rFunctor_contractive.
Qed.
theories/algebra/excl.v
View file @ 45d4e2a6
......@@ -150,23 +150,23 @@ Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
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)
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.
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.
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.
theories/algebra/gmap.v
View file @ 45d4e2a6
......@@ -558,43 +558,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.
theories/algebra/list.v
View file @ 45d4e2a6
......@@ -113,25 +113,25 @@ Instance listC_map_ne A B : NonExpansive (@listC_map A B).
Proof. intros n f g ? l. by apply list_fmap_ext_ne. 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 *)
......@@ -462,23 +462,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.
theories/algebra/ofe.v
View file @ 45d4e2a6
This diff is collapsed.
theories/algebra/vector.v
View file @ 45d4e2a6
......@@ -88,26 +88,26 @@ Instance vecC_map_ne {A A'} m :
Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
Program Definition vecCF (F : cFunctor) m : cFunctor := {|
cFunctor_car A B := vecC (cFunctor_car F A B) m;
cFunctor_map A1 A2 B1 B2 fg := vecC_map m (cFunctor_map F fg)
cFunctor_car A _ B _ := vecC (cFunctor_car F A B) m;
cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecC_map m (cFunctor_map F fg)
|}.
Next Obligation.
intros F A1 A2 B1 B2 n m f g Hfg. by apply vecC_map_ne, cFunctor_ne.
intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros F m A B l.
intros F m A ? B ? l.
change (vec_to_list (vec_map m (cFunctor_map F (cid, cid)) l) ≡ l).
rewrite vec_to_list_map. apply listCF.
Qed.
Next Obligation.
intros F m A1 A2 A3 B1 B2 B3 f g f' g' l.
intros F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
change (vec_to_list (vec_map m (cFunctor_map F (f ◎ g, g' ◎ f')) l)
≡ vec_map m (cFunctor_map F (g, g')) (vec_map m (cFunctor_map F (f, f')) l)).
rewrite !vec_to_list_map. by apply (cFunctor_compose (listCF F) f g f' g').
rewrite !vec_to_list_map. by apply: (cFunctor_compose (listCF F) f g f' g').
Qed.
Instance vecCF_contractive F m :
cFunctorContractive F → cFunctorContractive (vecCF F m).
Proof.
by intros ?? A1 A2 B1 B2 n ???; apply vecC_map_ne; first apply cFunctor_contractive.
by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecC_map_ne; first apply cFunctor_contractive.
Qed.
theories/base_logic/lib/iprop.v
View file @ 45d4e2a6
......@@ -117,13 +117,14 @@ the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors → ofeT.
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
Definition iResUR (Σ : gFunctors) : ucmraT :=
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
Notation iProp Σ := (uPredC (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
Notation iPropSI Σ := (uPredSI (iResUR Σ)).
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
......@@ -136,13 +137,13 @@ Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
Definition iProp_result (Σ : gFunctors) :
solution (uPredCF (iResF Σ)) := solver.result _.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT :=
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
Notation iProp Σ := (uPredC (iResUR Σ)).
Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
solution_fold (iProp_result Σ).
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
......
theories/base_logic/lib/own.v
View file @ 45d4e2a6
......@@ -10,10 +10,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) :=
InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) }.
InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) _ }.
Arguments inG_id {_ _} _.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ)).
Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ) _).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
......
theories/base_logic/lib/saved_prop.v
View file @ 45d4e2a6
......@@ -9,7 +9,7 @@ Import uPred.
saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : cFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ)));
saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _));
saved_anything_contractive : cFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
......@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
Proof. solve_inG. Qed.
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
(γ : gname) (x : F (iProp Σ) _) : iProp Σ :=
own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
Context `{!savedAnythingG Σ F}.
Implicit Types x y : F (iProp Σ).
Implicit Types x y : F (iProp Σ) _.
Implicit Types γ : gname.
Global Instance saved_anything_persistent γ x :
......
theories/base_logic/upred.v
View file @ 45d4e2a6
......@@ -161,26 +161,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.
......
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