Commit 4f6d4de7 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/functor_diag' into 'master'

Kill `{o,r,ur}Functor_diag` coercions, and rename into `{o,r,ur}Functor_apply`

Closes #240

See merge request iris/iris!413
parents 6b759b62 4326f527
......@@ -81,6 +81,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
* The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
* Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic.
* Make use of `ofe_iso` in the COFE solver.
* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
`{o,r,ur}Functor_apply` to better match their intent.
**Changes in heap_lang:**
......
......@@ -8,8 +8,6 @@
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# We have ambiguous paths, and live with it.
-arg -w -arg -ambiguous-paths
theories/algebra/monoid.v
theories/algebra/cmra.v
......
......@@ -800,9 +800,8 @@ Class rFunctorContractive (F : rFunctor) :=
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) `{!Cofe A} : cmraT :=
Definition rFunctor_apply (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 |}.
......@@ -838,9 +837,8 @@ Class urFunctorContractive (F : urFunctor) :=
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) `{!Cofe A} : ucmraT :=
Definition urFunctor_apply (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 |}.
......
......@@ -4,20 +4,20 @@ Set Default Proof Using "Type".
Record solution (F : oFunctor) := Solution {
solution_car :> ofeT;
solution_cofe : Cofe solution_car;
solution_iso :> ofe_iso (F solution_car _) solution_car;
solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
}.
Existing Instance solution_cofe.
Module solver. Section solver.
Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
Context `{Fcofe : (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
Context `{Finh : Inhabited (F unitO _)}.
Context `{Fcofe : (T : ofeT) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
Notation map := (oFunctor_map F).
Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
match k with
| 0 => existT (P:=Cofe) unitO _
| S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
| S k => existT (P:=Cofe) (@oFunctor_apply 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).
......@@ -176,7 +176,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 (oFunctor_apply F T) :=
{| chain_car n := map (project n,embed' n) (X (S n)) |}.
Next Obligation.
intros X n i Hi.
......@@ -186,14 +186,14 @@ Next Obligation.
rewrite f_S -oFunctor_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) : oFunctor_apply 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 : 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)).
......
......@@ -708,12 +708,10 @@ Class oFunctorContractive (F : oFunctor) :=
Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
Hint Mode oFunctorContractive ! : typeclass_instances.
Definition oFunctor_diag (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
(** Not a coercion due to the [Cofe] type class argument, and to avoid
ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
oFunctor_car F A A.
(** Note that the implicit argument [Cofe A] is not taken into account when
[oFunctor_diag] is used as a coercion. So, given [F : oFunctor] and [A : ofeT]
one has to write [F A _]. *)
Coercion oFunctor_diag : oFunctor >-> Funclass.
Program Definition constOF (B : ofeT) : oFunctor :=
{| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
......@@ -1498,7 +1496,7 @@ Section sigTOF.
Qed.
Program Definition sigTOF (F : A oFunctor) : oFunctor := {|
oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A _ B CB);
oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sigT_map (λ a, oFunctor_map (F a) fg)
|}.
Next Obligation.
......@@ -1584,7 +1582,7 @@ Instance iso_ofe_trans_ne {A B C} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (
Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.
Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
(I : ofe_iso A B) : ofe_iso (F A _) (F B _) :=
(I : ofe_iso A B) : ofe_iso (oFunctor_apply F A) (oFunctor_apply F B) :=
OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
(oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
Next Obligation.
......
......@@ -120,7 +120,8 @@ Module Type iProp_solution_sig.
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
Definition iResUR (Σ : gFunctors) : ucmraT :=
discrete_funUR (λ i, gmapUR gname (gFunctors_lookup Σ i (iPrePropO Σ) _)).
discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
......@@ -142,7 +143,8 @@ Module Export iProp_solution : iProp_solution_sig.
Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT :=
discrete_funUR (λ i, gmapUR gname (gFunctors_lookup Σ i (iPrePropO Σ) _)).
discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
......
......@@ -9,14 +9,15 @@ 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 = gFunctors_lookup Σ inG_id (iPrePropO Σ) _ }.
InG { inG_id : gid Σ; inG_prf :
A = rFunctor_apply (gFunctors_lookup Σ inG_id) (iPrePropO Σ)}.
Arguments inG_id {_ _} _.
(** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
not want Coq to pick one arbitrarily. *)
Hint Mode inG - ! : typeclass_instances.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPrePropO Σ) _).
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (rFunctor_apply F (iPrePropO Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
......
......@@ -9,7 +9,7 @@ Import uPred.
saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (F (iPrePropO Σ) _));
saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPrePropO Σ)));
saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
......@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
Proof. solve_inG. Qed.
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iPropO Σ) _) : iProp Σ :=
(γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
own γ (to_agree $ (oFunctor_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 (iPropO Σ) _.
Implicit Types x y : oFunctor_apply F (iPropO Σ).
Implicit Types γ : gname.
Global Instance saved_anything_persistent γ x :
......
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