Commit 5b8186e2 by Robbert Krebbers

### Kill `{o,r,ur}Functor_diag` coercions.

parent 6b759b62
 ... ... @@ -802,7 +802,6 @@ Class rFunctorContractive (F : rFunctor) := 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 |}. ... ... @@ -840,7 +839,6 @@ Class urFunctorContractive (F : urFunctor) := 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 |}. ... ...
 ... ... @@ -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_diag 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_diag F T)}. Context `{Finh : Inhabited (oFunctor_diag 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_diag 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_diag 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_diag 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_diag F T) : T := {| tower_car n := g n (map (embed' n,project n) X) |}. Next Obligation. intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)). ... ...
 ... ... @@ -710,10 +710,6 @@ Hint Mode oFunctorContractive ! : typeclass_instances. Definition oFunctor_diag (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 +1494,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 +1580,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_diag F A) (oFunctor_diag 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_diag (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_diag (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_diag (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_diag 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_diag 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_diag 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_diag 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!