Commit 677aae22 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename cofeMor → cofe_mor and cofe_mor → cofe_morC for consistency.

parent 51eea32e
......@@ -207,13 +207,13 @@ Section fixpoint.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
(** Function space *)
Record cofeMor (A B : cofeT) : Type := CofeMor {
(** Non-expansive function space *)
Record cofe_mor (A B : cofeT) : Type := CofeMor {
cofe_mor_car :> A B;
cofe_mor_ne n : Proper (dist n ==> dist n) cofe_mor_car
}.
Arguments CofeMor {_ _} _ {_}.
Add Printing Constructor cofeMor.
Add Printing Constructor cofe_mor.
Existing Instance cofe_mor_ne.
Notation "'λne' x .. y , t" :=
......@@ -222,20 +222,20 @@ Notation "'λne' x .. y , t" :=
Section cofe_mor.
Context {A B : cofeT}.
Global Instance cofe_mor_proper (f : cofeMor A B) : Proper (() ==> ()) f.
Global Instance cofe_mor_proper (f : cofe_mor A B) : Proper (() ==> ()) f.
Proof. apply ne_proper, cofe_mor_ne. Qed.
Instance cofe_mor_equiv : Equiv (cofeMor A B) := λ f g, x, f x g x.
Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, x, f x {n} g x.
Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
{| chain_car n := c n x |}.
Instance cofe_mor_equiv : Equiv (cofe_mor A B) := λ f g, x, f x g x.
Instance cofe_mor_dist : Dist (cofe_mor A B) := λ n f g, x, f x {n} g x.
Program Definition cofe_mor_chain `(c : chain (cofe_mor A B))
(x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c,
{| cofe_mor_car x := compl (fun_chain c x) |}.
Program Instance cofe_mor_compl : Compl (cofe_mor A B) := λ c,
{| cofe_mor_car x := compl (cofe_mor_chain c x) |}.
Next Obligation.
intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x))
(conv_compl n (fun_chain c y)) /= Hx.
intros c n x y Hx. by rewrite (conv_compl n (cofe_mor_chain c x))
(conv_compl n (cofe_mor_chain c y)) /= Hx.
Qed.
Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
Definition cofe_mor_cofe_mixin : CofeMixin (cofe_mor A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
......@@ -246,22 +246,22 @@ Section cofe_mor.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
- intros n c x; simpl.
by rewrite (conv_compl n (fun_chain c x)) /=.
by rewrite (conv_compl n (cofe_mor_chain c x)) /=.
Qed.
Canonical Structure cofe_mor : cofeT := CofeT (cofeMor A B) cofe_mor_cofe_mixin.
Canonical Structure cofe_morC := CofeT (cofe_mor A B) cofe_mor_cofe_mixin.
Global Instance cofe_mor_car_ne n :
Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
Global Instance cofe_mor_car_proper :
Proper (() ==> () ==> ()) (@cofe_mor_car A B) := ne_proper_2 _.
Lemma cofe_mor_ext (f g : cofeMor A B) : f g x, f x g x.
Lemma cofe_mor_ext (f g : cofe_mor A B) : f g x, f x g x.
Proof. done. Qed.
End cofe_mor.
Arguments cofe_mor : clear implicits.
Arguments cofe_morC : clear implicits.
Notation "A -n> B" :=
(cofe_mor A B) (at level 99, B at level 200, right associativity).
(cofe_morC A B) (at level 99, B at level 200, right associativity).
Instance cofe_mor_inhabited {A B : cofeT} `{Inhabited B} :
Inhabited (A -n> B) := populate (λne _, inhabitant).
......@@ -407,7 +407,7 @@ Proof.
Qed.
Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
cFunctor_car A B := cofe_mor (cFunctor_car F1 B A) (cFunctor_car F2 A B);
cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
cFunctor_map A1 A2 B1 B2 fg :=
cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
|}.
......
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