Commit 22b68d48 by Robbert Krebbers

### Rename `{o,r,ur}Functor_diag` into `{o,r,ur}Functor_apply`.

parent 5b8186e2
 ... ... @@ -800,7 +800,7 @@ 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. Program Definition constRF (B : cmraT) : rFunctor := ... ... @@ -837,7 +837,7 @@ 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. Program Definition constURF (B : ucmraT) : urFunctor := ... ...
 ... ... @@ -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 (oFunctor_diag 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 (oFunctor_diag F T)}. Context `{Finh : Inhabited (oFunctor_diag 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) (@oFunctor_diag 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 (oFunctor_diag 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) : oFunctor_diag 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 : oFunctor_diag 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,7 +708,7 @@ 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 := Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT := oFunctor_car F A A. Program Definition constOF (B : ofeT) : oFunctor := ... ... @@ -1580,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 (oFunctor_diag F A) (oFunctor_diag 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. ... ...
 ... ... @@ -121,7 +121,7 @@ Module Type iProp_solution_sig. Definition iResUR (Σ : gFunctors) : ucmraT := discrete_funUR (λ i, gmapUR gname (rFunctor_diag (gFunctors_lookup Σ i) (iPrePropO Σ))). gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))). Notation iProp Σ := (uPred (iResUR Σ)). Notation iPropO Σ := (uPredO (iResUR Σ)). Notation iPropI Σ := (uPredI (iResUR Σ)). ... ... @@ -144,7 +144,7 @@ Module Export iProp_solution : iProp_solution_sig. Definition iResUR (Σ : gFunctors) : ucmraT := discrete_funUR (λ i, gmapUR gname (rFunctor_diag (gFunctors_lookup Σ i) (iPrePropO Σ))). gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))). Notation iProp Σ := (uPred (iResUR Σ)). Notation iPropO Σ := (uPredO (iResUR Σ)). ... ...
 ... ... @@ -10,14 +10,14 @@ 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 = rFunctor_diag (gFunctors_lookup Σ inG_id) (iPrePropO Σ)}. 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 Σ (rFunctor_diag 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 (oFunctor_diag 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 : oFunctor_diag 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 : oFunctor_diag 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!