diff --git a/CHANGELOG.md b/CHANGELOG.md index 5ab682fcd0fc1dcbd6dac92ed5d2d1e1f56f9245..3b278c5c3dfc50574b1a48eda545c9d81a35d146 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -42,6 +42,8 @@ Changes in and extensions of the theory: describes the postcondition of each forked-off thread (instead of it being True). Additionally, there is a stronger variant of the adequacy theorem that allows to make use of the postconditions of the forked-off threads. +* The user-chosen functor used to instantiate the Iris logic now goes from + COFEs to Cameras (it was OFEs to Cameras). Changes in Coq: diff --git a/ProofGuide.md b/ProofGuide.md index df476850f8b845765c1ea4f11fa196a386e17a93..66a6440fe37feb8f096f4d1f2d28de00255587a4 100644 --- a/ProofGuide.md +++ b/ProofGuide.md @@ -6,16 +6,71 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in the [style guide](StyleGuide.md). +## Combinators for functors + +In Iris, the type of propositions [iProp] is described by the solution to the +recursive domain equation: + + +iProp ≅ uPred (F (iProp)) + + +Here, F is a user-chosen locally contractive bifunctor from COFEs to unital +Camaras (a step-indexed generalization of unital resource algebras). To make it +convenient to construct such functors out of smaller pieces, we provide a number +of abstractions: + +- [cFunctor](theories/algebra/ofe.v): bifunctors from COFEs to OFEs. +- [rFunctor](theories/algebra/cmra.v): bifunctors from COFEs to cameras. +- [urFunctor](theories/algebra/cmra.v): bifunctors from COFEs to unital + cameras. + +Besides, there are the classes cFunctorContractive, rFunctorContractive, and +urFunctorContractive which describe the subset of the above functors that +are contractive. + +To compose these functors, we provide a number of combinators, e.g.: + +- constCF (A : ofeT) : cFunctor := λ (B,B⁻), A  +- idCF : cFunctor := λ (B,B⁻), B +- prodCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻) +- ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻) +- laterCF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻)) +- agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻)) +- gmapURF K (F : rFunctor) : urFunctor := λ (B,B⁻), gmap K (F (B,B⁻)) + +Using these combinators, one can easily construct bigger functors in point-free +style, e.g: + + +F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF))) + + +which effectively defines F := λ (B,B⁻), gmap K (agree (nat * later B)). + +Furthermore, for functors written using these combinators like the functor F +above, Coq can automatically urFunctorContractive F. + +To make it a little bit more convenient to write down such functors, we make +the constant functors (constCF, constRF, and constURF) a coercion, and +provide the usual notation for products, etc. So the above functor can be +written as follows (which is similar to the effective definition of F above): + + +F := gmapURF K (agreeRF (natC * ▶ ∙)) + + ## Resource algebra management When using ghost state in Iris, you have to make sure that the resource algebras you need are actually available. Every Iris proof is carried out using a universally quantified list Σ: gFunctors defining which resource algebras are available. You can think of this as a list of resource algebras, though in -reality it is a list of functors from OFEs to Cameras (where Cameras are a -step-indexed generalization of resource algebras). This is the *global* list of -resources that the entire proof can use. We keep it universally quantified to -enable composition of proofs. The formal side of this is described in §7.4 of +reality it is a list of locally contractive functors from COFEs to Cameras, +which are typically defined using the combinators for functors described above. +The Σ is the *global* list of resources that the entire proof can use. We +keep the Σ universally quantified to enable composition of proofs. The formal +side of this is described in §7.4 of [The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we describe the Coq aspects of this approach. diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex index b8d55d0fd6249636244263d094b789a78286630c..c774af1077f8aaf39a7cfc3ccbc74535f21e2e44 100644 --- a/docs/ghost-state.tex +++ b/docs/ghost-state.tex @@ -174,7 +174,7 @@ The purpose of this section is to describe how we solve these issues. \paragraph{Picking the resources.} The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources. -To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs^\op \times \OFEs \to \CMRAs)_{i \in \mathcal{I}}$. +To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs^\op \times \COFEs \to \CMRAs)_{i \in \mathcal{I}}$. (This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.) From this, we construct the bifunctor defining the overall resources as follows: diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v index 360dc4778c5cab280d9bb560556d69067fb45add..0392aaf6a8d7865765aa33f2a0b8a884e35e829c 100644 --- a/theories/algebra/agree.v +++ b/theories/algebra/agree.v @@ -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. diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v index 927eddaecb9c02f94fc89b49c7df5db59fa6a108..4af018de3c71ef4978c632f70f2f91e3de1f6169 100644 --- a/theories/algebra/auth.v +++ b/theories/algebra/auth.v @@ -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. diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index ed6254f0bee39fef95c92d7abce8d3738bc08965..f44e3f3c423cd7681048541f839c090117237e64 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -766,16 +766,18 @@ End cmra_morphism. (** Functors *) Record rFunctor := RFunctor { - rFunctor_car : ofeT → ofeT → cmraT; - rFunctor_map {A1 A2 B1 B2} : + 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 : - NonExpansive (@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 (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x); - rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) : + 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. @@ -785,13 +787,15 @@ Delimit Scope rFunctor_scope with RF. Bind Scope rFunctor_scope with rFunctor. 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. Coercion constRF : cmraT >-> rFunctor. @@ -799,16 +803,18 @@ Instance constRF_contractive B : rFunctorContractive (constRF B). Proof. rewrite /rFunctorContractive; apply _. Qed. Record 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 : - NonExpansive (@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 (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x); - urFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) : + 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. @@ -818,13 +824,15 @@ Delimit Scope urFunctor_scope with URF. Bind Scope urFunctor_scope with urFunctor. 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. Coercion constURF : ucmraT >-> urFunctor. @@ -1189,16 +1197,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. Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope. @@ -1207,21 +1215,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. Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope. @@ -1230,7 +1238,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. @@ -1450,47 +1458,47 @@ Proof. Qed. Program Definition optionRF (F : rFunctor) : rFunctor := {| - rFunctor_car A B := optionR (rFunctor_car F A B); - rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg) + rFunctor_car A _ B _ := optionR (rFunctor_car F A B); + rFunctor_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 optionRF_contractive F : rFunctorContractive F → rFunctorContractive (optionRF 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. 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. (* Dependently-typed functions over a discrete domain *) @@ -1573,23 +1581,23 @@ Proof. Qed. Program Definition ofe_funURF {C} (F : C → urFunctor) : urFunctor := {| - urFunctor_car A B := ofe_funUR (λ c, urFunctor_car (F c) A B); - urFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, urFunctor_map (F c) fg) + urFunctor_car A _ B _ := ofe_funUR (λ c, urFunctor_car (F c) A B); + urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_funC_map (λ c, urFunctor_map (F c) fg) |}. Next Obligation. - intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne. + intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne. Qed. Next Obligation. - intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g). + intros C F A ? B ? g; simpl. rewrite -{2}(ofe_fun_map_id g). apply ofe_fun_map_ext=> y; apply urFunctor_id. Qed. Next Obligation. - intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose. + intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose. apply ofe_fun_map_ext=>y; apply urFunctor_compose. Qed. Instance ofe_funURF_contractive {C} (F : C → urFunctor) : (∀ c, urFunctorContractive (F c)) → urFunctorContractive (ofe_funURF F). Proof. - intros ? A1 A2 B1 B2 n ?? g. + intros ? A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>c; apply urFunctor_contractive. Qed. diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v index b18a584e96f871943021fa1cac3b0bf847d91c89..33bfebd875ecf222ccbe703d9e653a0a78598f5c 100644 --- a/theories/algebra/cofe_solver.v +++ b/theories/algebra/cofe_solver.v @@ -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)). diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v index de491b25b91ecd6f606337adfe9549938c1b5654..805a9309b1a5947983981265e5939417d03f686e 100644 --- a/theories/algebra/csum.v +++ b/theories/algebra/csum.v @@ -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. diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v index 41956b4412f33d5ea92dbfae4e75186eb47bf569..8d99dec9ddeb8a90009c26a1c98958fca2813f52 100644 --- a/theories/algebra/excl.v +++ b/theories/algebra/excl.v @@ -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. diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index f2bcdfe9919b9710933f370b339cd9c53da12f67..02df4be9695adb0e754b1416c847457b9d526ab2 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -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. diff --git a/theories/algebra/list.v b/theories/algebra/list.v index e15329c51e7c66e223c533af4c9df65778968647..c6d5a137cbeb79448097146b85be0dfe8942c7e3 100644 --- a/theories/algebra/list.v +++ b/theories/algebra/list.v @@ -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. diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 6db8d6e8054f453cc9a078f86ddb4b72e3998485..52bc4c554c43c52e7f998fe34772d916beda83dd 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -664,14 +664,14 @@ Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed. (** Functors *) Record cFunctor := CFunctor { - cFunctor_car : ofeT → ofeT → ofeT; - cFunctor_map {A1 A2 B1 B2} : + cFunctor_car : ∀ A {!Cofe A} B {!Cofe B}, ofeT; + cFunctor_map {!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} : ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2; - cFunctor_ne {A1 A2 B1 B2} : - NonExpansive (@cFunctor_map A1 A2 B1 B2); - cFunctor_id {A B : ofeT} (x : cFunctor_car A B) : + cFunctor_ne {!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} : + NonExpansive (@cFunctor_map A1 _ A2 _ B1 _ B2 _); + cFunctor_id {!Cofe A, !Cofe B} (x : cFunctor_car A B) : cFunctor_map (cid,cid) x ≡ x; - cFunctor_compose {A1 A2 A3 B1 B2 B3} + cFunctor_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 : cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x) }. @@ -682,14 +682,19 @@ Delimit Scope cFunctor_scope with CF. Bind Scope cFunctor_scope with cFunctor. Class cFunctorContractive (F : cFunctor) := - cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). + cFunctor_contractive {!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :> + Contractive (@cFunctor_map F A1 _ A2 _ B1 _ B2 _). Hint Mode cFunctorContractive ! : typeclass_instances. -Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A. +Definition cFunctor_diag (F: cFunctor) (A: ofeT) {!Cofe A} : ofeT := + cFunctor_car F A A. +(** Note that the implicit argument [Cofe A] is not taken into account when +[cFunctor_diag] is used as a coercion. So, given [F : cFunctor] and [A : ofeT] +one has to write [F A _]. *) Coercion cFunctor_diag : cFunctor >-> Funclass. Program Definition constCF (B : ofeT) : cFunctor := - {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}. + {| cFunctor_car A1 A2 _ _ := B; cFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}. Solve Obligations with done. Coercion constCF : ofeT >-> cFunctor. @@ -697,21 +702,21 @@ Instance constCF_contractive B : cFunctorContractive (constCF B). Proof. rewrite /cFunctorContractive; apply _. Qed. Program Definition idCF : cFunctor := - {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}. + {| cFunctor_car A1 _ A2 _ := A2; cFunctor_map A1 _ A2 _ B1 _ B2 _ f := f.2 |}. Solve Obligations with done. Notation "∙" := idCF : cFunctor_scope. Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {| - cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B); - cFunctor_map A1 A2 B1 B2 fg := + cFunctor_car A _ B _ := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B); + cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg) |}. Next Obligation. - intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne. + intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodC_map_ne; apply cFunctor_ne. Qed. -Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed. +Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !cFunctor_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 !cFunctor_compose. Qed. Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope. @@ -720,25 +725,25 @@ Instance prodCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (prodCF F1 F2). Proof. - intros ?? A1 A2 B1 B2 n ???; + intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodC_map_ne; apply cFunctor_contractive. Qed. Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {| - cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B; - cFunctor_map A1 A2 B1 B2 fg := + cFunctor_car A _ B _ := cFunctor_car F1 B A -n> cFunctor_car F2 A B; + cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg) |}. Next Obligation. - intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. + intros F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *. apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg. Qed. Next Obligation. - intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id. + intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !cFunctor_id. apply (ne_proper f). apply cFunctor_id. Qed. Next Obligation. - intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *. + intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *. rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose. Qed. Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope. @@ -747,7 +752,7 @@ Instance ofe_morCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (ofe_morCF F1 F2). Proof. - intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. + intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *. apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split. Qed. @@ -818,16 +823,16 @@ Instance sumC_map_ne {A A' B B'} : Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed. Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {| - cFunctor_car A B := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B); - cFunctor_map A1 A2 B1 B2 fg := + cFunctor_car A _ B _ := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B); + cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sumC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg) |}. Next Obligation. - intros ?? A1 A2 B1 B2 n ???; by apply sumC_map_ne; apply cFunctor_ne. + intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumC_map_ne; apply cFunctor_ne. Qed. -Next Obligation. by intros F1 F2 A B [?|?]; rewrite /= !cFunctor_id. Qed. +Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !cFunctor_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 !cFunctor_compose. Qed. Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope. @@ -836,7 +841,7 @@ Instance sumCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (sumCF F1 F2). Proof. - intros ?? A1 A2 B1 B2 n ???; + intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumC_map_ne; apply cFunctor_contractive. Qed. @@ -973,25 +978,25 @@ Instance optionC_map_ne A B : NonExpansive (@optionC_map A B). Proof. by intros n f f' Hf []; constructor; apply Hf. Qed. Program Definition optionCF (F : cFunctor) : cFunctor := {| - cFunctor_car A B := optionC (cFunctor_car F A B); - cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg) + cFunctor_car A _ B _ := optionC (cFunctor_car F A B); + cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (cFunctor_map F fg) |}. Next Obligation. - by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne. + by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, cFunctor_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 cFunctor_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 cFunctor_compose. Qed. Instance optionCF_contractive F : cFunctorContractive F → cFunctorContractive (optionCF F). Proof. - by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive. + by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, cFunctor_contractive. Qed. (** Later *) @@ -1075,26 +1080,26 @@ Instance laterC_map_contractive (A B : ofeT) : Contractive (@laterC_map A B). Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed. Program Definition laterCF (F : cFunctor) : cFunctor := {| - cFunctor_car A B := laterC (cFunctor_car F A B); - cFunctor_map A1 A2 B1 B2 fg := laterC_map (cFunctor_map F fg) + cFunctor_car A _ B _ := laterC (cFunctor_car F A B); + cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := laterC_map (cFunctor_map F fg) |}. Next Obligation. - intros F A1 A2 B1 B2 n fg fg' ?. + intros F A1 ? A2 ? B1 ? B2 ? n fg fg' ?. by apply (contractive_ne laterC_map), cFunctor_ne. Qed. Next Obligation. - intros F A B x; simpl. rewrite -{2}(later_map_id x). + intros F A ? B ? x; simpl. rewrite -{2}(later_map_id x). apply later_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 -later_map_compose. + intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -later_map_compose. apply later_map_ext=>y; apply cFunctor_compose. Qed. Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope. Instance laterCF_contractive F : cFunctorContractive (laterCF F). Proof. - intros A1 A2 B1 B2 n fg fg' Hfg. apply laterC_map_contractive. + intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterC_map_contractive. destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg. Qed. @@ -1174,18 +1179,19 @@ Instance ofe_funC_map_ne {A} {B1 B2 : A → ofeT} : Proof. intros n f1 f2 Hf g x; apply Hf. Qed. Program Definition ofe_funCF {C} (F : C → cFunctor) : cFunctor := {| - cFunctor_car A B := ofe_funC (λ c, cFunctor_car (F c) A B); - cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, cFunctor_map (F c) fg) + cFunctor_car A _ B _ := ofe_funC (λ c, cFunctor_car (F c) A B); + cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_funC_map (λ c, cFunctor_map (F c) fg) |}. Next Obligation. - intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne. + intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne. Qed. Next Obligation. - intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g). + intros C F A ? B ? g; simpl. rewrite -{2}(ofe_fun_map_id g). apply ofe_fun_map_ext=> y; apply cFunctor_id. Qed. Next Obligation. - intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -ofe_fun_map_compose. + intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. + rewrite /= -ofe_fun_map_compose. apply ofe_fun_map_ext=>y; apply cFunctor_compose. Qed. @@ -1194,7 +1200,7 @@ Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope. Instance ofe_funCF_contractive {C} (F : C → cFunctor) : (∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F). Proof. - intros ? A1 A2 B1 B2 n ?? g. + intros ? A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>c; apply cFunctor_contractive. Qed. diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v index 7250ce400546401f18b69a2a24d32c92b87d0401..f8d073ba13ea447141006d1fffc88308673ca7df 100644 --- a/theories/algebra/vector.v +++ b/theories/algebra/vector.v @@ -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. diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v index 42b53f898bb257242879138deb3ccceeaa2cfc50..34945d66892760632936bbb4ffa197d9d5b2d61a 100644 --- a/theories/base_logic/lib/iprop.v +++ b/theories/base_logic/lib/iprop.v @@ -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 _. diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v index d3475828577f3c2f2050415a2a2530f8b380be35..4540dc68f1946e536437665cd3a7abc37b768590 100644 --- a/theories/base_logic/lib/own.v +++ b/theories/base_logic/lib/own.v @@ -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 ? Σ" *) diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v index 7e3401fd330e7371cf50a4eef8de2a06c3dd7e2d..f844bcc0bb63f6d6e8c150f87a74ab2ad95c6bd2 100644 --- a/theories/base_logic/lib/saved_prop.v +++ b/theories/base_logic/lib/saved_prop.v @@ -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 : diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index b9c90e9708a24cc6dca41d2c45f6a5786ffde16a..df7df317133753818dcaf439eb01f4d8fd17d04e 100644 --- a/theories/base_logic/upred.v +++ b/theories/base_logic/upred.v @@ -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.