ofe.v 39.8 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.algebra Require Export base. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Nov 11, 2015 3 `````` `````` Ralf Jung committed Nov 22, 2016 4 ``````(** This files defines (a shallow embedding of) the category of OFEs: `````` Ralf Jung committed Feb 16, 2016 5 6 7 8 9 10 11 12 `````` Complete ordered families of equivalences. This is a cartesian closed category, and mathematically speaking, the entire development lives in this category. However, we will generally prefer to work with raw Coq functions plus some registered Proper instances for non-expansiveness. This makes writing such functions much easier. It turns out that it many cases, we do not even need non-expansiveness. *) `````` Robbert Krebbers committed Nov 11, 2015 13 14 ``````(** Unbundeled version *) Class Dist A := dist : nat → relation A. `````` Robbert Krebbers committed Nov 12, 2015 15 ``````Instance: Params (@dist) 3. `````` Ralf Jung committed Feb 10, 2016 16 17 ``````Notation "x ≡{ n }≡ y" := (dist n x y) (at level 70, n at next level, format "x ≡{ n }≡ y"). `````` Robbert Krebbers committed Feb 13, 2016 18 ``````Hint Extern 0 (_ ≡{_}≡ _) => reflexivity. `````` Ralf Jung committed Feb 10, 2016 19 ``````Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption. `````` Robbert Krebbers committed Jan 13, 2016 20 21 22 `````` Tactic Notation "cofe_subst" ident(x) := repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 23 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Jan 13, 2016 24 25 26 27 `````` | H:@dist ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x end. Tactic Notation "cofe_subst" := `````` Robbert Krebbers committed Nov 17, 2015 28 `````` repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 29 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Dec 21, 2015 30 31 `````` | H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x `````` Robbert Krebbers committed Nov 17, 2015 32 `````` end. `````` Robbert Krebbers committed Nov 11, 2015 33 `````` `````` Ralf Jung committed Nov 22, 2016 34 ``````Record OfeMixin A `{Equiv A, Dist A} := { `````` Ralf Jung committed Feb 10, 2016 35 `````` mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; `````` Robbert Krebbers committed Jan 14, 2016 36 `````` mixin_dist_equivalence n : Equivalence (dist n); `````` Ralf Jung committed Nov 22, 2016 37 `````` mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y `````` Robbert Krebbers committed Nov 11, 2015 38 39 40 ``````}. (** Bundeled version *) `````` Ralf Jung committed Nov 22, 2016 41 42 43 44 45 ``````Structure ofeT := OfeT' { ofe_car :> Type; ofe_equiv : Equiv ofe_car; ofe_dist : Dist ofe_car; ofe_mixin : OfeMixin ofe_car; `````` Robbert Krebbers committed Jun 15, 2016 46 `````` _ : Type `````` Robbert Krebbers committed Nov 11, 2015 47 ``````}. `````` Ralf Jung committed Nov 22, 2016 48 49 50 51 52 53 54 55 56 ``````Arguments OfeT' _ {_ _} _ _. Notation OfeT A m := (OfeT' A m A). Add Printing Constructor ofeT. Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances. Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances. Arguments ofe_car : simpl never. Arguments ofe_equiv : simpl never. Arguments ofe_dist : simpl never. Arguments ofe_mixin : simpl never. `````` Robbert Krebbers committed Jan 14, 2016 57 58 `````` (** Lifting properties from the mixin *) `````` Ralf Jung committed Nov 22, 2016 59 60 ``````Section ofe_mixin. Context {A : ofeT}. `````` Robbert Krebbers committed Jan 14, 2016 61 `````` Implicit Types x y : A. `````` Ralf Jung committed Feb 10, 2016 62 `````` Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y. `````` Ralf Jung committed Nov 22, 2016 63 `````` Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed. `````` Robbert Krebbers committed Jan 14, 2016 64 `````` Global Instance dist_equivalence n : Equivalence (@dist A _ n). `````` Ralf Jung committed Nov 22, 2016 65 `````` Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed. `````` Ralf Jung committed Feb 10, 2016 66 `````` Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y. `````` Ralf Jung committed Nov 22, 2016 67 68 `````` Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed. End ofe_mixin. `````` Robbert Krebbers committed Jan 14, 2016 69 `````` `````` Robbert Krebbers committed May 28, 2016 70 71 ``````Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption. `````` Ralf Jung committed Dec 21, 2016 72 ``````(** Discrete OFEs and Timeless elements *) `````` Ralf Jung committed Mar 15, 2016 73 ``````(* TODO: On paper, We called these "discrete elements". I think that makes `````` Ralf Jung committed Mar 07, 2016 74 `````` more sense. *) `````` Robbert Krebbers committed May 27, 2016 75 76 ``````Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_ _ _} _ {_} _ _. `````` Ralf Jung committed Nov 22, 2016 77 78 79 80 81 82 83 84 85 86 ``````Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x. (** OFEs with a completion *) Record chain (A : ofeT) := { chain_car :> nat → A; chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n }. Arguments chain_car {_} _ _. Arguments chain_cauchy {_} _ _ _ _. `````` Robbert Krebbers committed Dec 05, 2016 87 88 89 90 91 ``````Program Definition chain_map {A B : ofeT} (f : A → B) `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B := {| chain_car n := f (c n) |}. Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed. `````` Ralf Jung committed Nov 22, 2016 92 93 94 95 96 97 ``````Notation Compl A := (chain A%type → A). Class Cofe (A : ofeT) := { compl : Compl A; conv_compl n c : compl c ≡{n}≡ c n; }. Arguments compl : simpl never. `````` Robbert Krebbers committed Feb 24, 2016 98 `````` `````` Robbert Krebbers committed Nov 11, 2015 99 100 ``````(** General properties *) Section cofe. `````` Ralf Jung committed Nov 22, 2016 101 `````` Context {A : ofeT}. `````` Robbert Krebbers committed Jan 14, 2016 102 `````` Implicit Types x y : A. `````` Robbert Krebbers committed Nov 11, 2015 103 104 105 `````` Global Instance cofe_equivalence : Equivalence ((≡) : relation A). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 106 107 `````` - by intros x; rewrite equiv_dist. - by intros x y; rewrite !equiv_dist. `````` Ralf Jung committed Feb 20, 2016 108 `````` - by intros x y z; rewrite !equiv_dist; intros; trans y. `````` Robbert Krebbers committed Nov 11, 2015 109 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 110 `````` Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 111 112 `````` Proof. intros x1 x2 ? y1 y2 ?; split; intros. `````` Ralf Jung committed Feb 20, 2016 113 114 `````` - by trans x1; [|trans y1]. - by trans x2; [|trans y2]. `````` Robbert Krebbers committed Nov 11, 2015 115 `````` Qed. `````` Robbert Krebbers committed Jan 14, 2016 116 `````` Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n). `````` Robbert Krebbers committed Nov 11, 2015 117 `````` Proof. `````` Robbert Krebbers committed Jan 13, 2016 118 `````` by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 119 120 121 `````` Qed. Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x). Proof. by apply dist_proper. Qed. `````` Robbert Krebbers committed Feb 18, 2016 122 `````` Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. `````` Robbert Krebbers committed Nov 11, 2015 123 `````` Proof. induction 2; eauto using dist_S. Qed. `````` Ralf Jung committed Feb 29, 2016 124 125 `````` Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y. Proof. intros; eauto using dist_le. Qed. `````` Ralf Jung committed Nov 22, 2016 126 `````` Instance ne_proper {B : ofeT} (f : A → B) `````` Robbert Krebbers committed Nov 11, 2015 127 128 `````` `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100. Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed. `````` Ralf Jung committed Nov 22, 2016 129 `````` Instance ne_proper_2 {B C : ofeT} (f : A → B → C) `````` Robbert Krebbers committed Nov 11, 2015 130 131 132 133 `````` `{!∀ n, Proper (dist n ==> dist n ==> dist n) f} : Proper ((≡) ==> (≡) ==> (≡)) f | 100. Proof. unfold Proper, respectful; setoid_rewrite equiv_dist. `````` Robbert Krebbers committed Jan 13, 2016 134 `````` by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n). `````` Robbert Krebbers committed Nov 11, 2015 135 `````` Qed. `````` Robbert Krebbers committed Feb 24, 2016 136 `````` `````` Ralf Jung committed Nov 22, 2016 137 `````` Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n). `````` Ralf Jung committed Feb 29, 2016 138 139 140 141 `````` Proof. transitivity (c n); first by apply conv_compl. symmetry. apply chain_cauchy. omega. Qed. `````` Robbert Krebbers committed Feb 24, 2016 142 143 `````` Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y. Proof. `````` Robbert Krebbers committed May 28, 2016 144 `````` split; intros; auto. apply (timeless _), dist_le with n; auto with lia. `````` Robbert Krebbers committed Feb 24, 2016 145 `````` Qed. `````` Robbert Krebbers committed Nov 11, 2015 146 147 ``````End cofe. `````` Robbert Krebbers committed Dec 02, 2016 148 ``````(** Contractive functions *) `````` Robbert Krebbers committed Dec 05, 2016 149 150 151 152 153 154 155 156 ``````Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop := match n with 0 => True | S n => x ≡{n}≡ y end. Arguments dist_later _ !_ _ _ /. Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n). Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed. Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f). `````` Robbert Krebbers committed Dec 02, 2016 157 `````` `````` Ralf Jung committed Nov 22, 2016 158 ``````Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x). `````` Robbert Krebbers committed Mar 06, 2016 159 160 ``````Proof. by intros n y1 y2. Qed. `````` Robbert Krebbers committed Dec 02, 2016 161 ``````Section contractive. `````` Ralf Jung committed Jan 05, 2017 162 `````` Set Default Proof Using "Type*". `````` Robbert Krebbers committed Dec 02, 2016 163 164 165 166 `````` Context {A B : ofeT} (f : A → B) `{!Contractive f}. Implicit Types x y : A. Lemma contractive_0 x y : f x ≡{0}≡ f y. `````` Robbert Krebbers committed Dec 05, 2016 167 `````` Proof. by apply (_ : Contractive f). Qed. `````` Robbert Krebbers committed Dec 02, 2016 168 `````` Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y. `````` Robbert Krebbers committed Dec 05, 2016 169 `````` Proof. intros. by apply (_ : Contractive f). Qed. `````` Robbert Krebbers committed Dec 02, 2016 170 171 172 173 174 175 176 `````` Global Instance contractive_ne n : Proper (dist n ==> dist n) f | 100. Proof. by intros x y ?; apply dist_S, contractive_S. Qed. Global Instance contractive_proper : Proper ((≡) ==> (≡)) f | 100. Proof. apply (ne_proper _). Qed. End contractive. `````` Robbert Krebbers committed Dec 05, 2016 177 178 179 180 181 182 183 ``````Ltac f_contractive := match goal with | |- ?f _ ≡{_}≡ ?f _ => apply (_ : Proper (dist_later _ ==> _) f) | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (dist_later _ ==> _ ==> _) f) | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f) end; try match goal with `````` Jacques-Henri Jourdan committed Dec 26, 2016 184 185 `````` | |- @dist_later ?A ?n ?x ?y => destruct n as [|n]; [done|change (@dist A _ n x y)] `````` Robbert Krebbers committed Dec 05, 2016 186 187 188 189 190 191 `````` end; try reflexivity. Ltac solve_contractive := preprocess_solve_proper; solve [repeat (first [f_contractive|f_equiv]; try eassumption)]. `````` Robbert Krebbers committed Nov 22, 2015 192 `````` `````` Robbert Krebbers committed Nov 11, 2015 193 ``````(** Fixpoint *) `````` Ralf Jung committed Nov 22, 2016 194 ``````Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 195 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 196 ``````Next Obligation. `````` Robbert Krebbers committed Mar 06, 2016 197 `````` intros A ? f ? n. `````` Robbert Krebbers committed Dec 05, 2016 198 `````` induction n as [|n IH]=> -[|i] //= ?; try omega. `````` Robbert Krebbers committed Feb 17, 2016 199 200 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 201 ``````Qed. `````` Robbert Krebbers committed Mar 18, 2016 202 `````` `````` Ralf Jung committed Nov 22, 2016 203 ``````Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 204 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Mar 18, 2016 205 ``````Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed. `````` Ralf Jung committed Nov 22, 2016 206 ``````Definition fixpoint {A AC AiH} f {Hf} := proj1_sig fixpoint_aux A AC AiH f Hf. `````` Robbert Krebbers committed Mar 18, 2016 207 ``````Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux. `````` Robbert Krebbers committed Nov 11, 2015 208 209 `````` Section fixpoint. `````` Ralf Jung committed Nov 22, 2016 210 `````` Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Aug 21, 2016 211 `````` `````` Robbert Krebbers committed Nov 17, 2015 212 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 213 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 214 215 `````` apply equiv_dist=>n. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 216 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 217 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2016 218 219 220 `````` Lemma fixpoint_unique (x : A) : x ≡ f x → x ≡ fixpoint f. Proof. `````` Robbert Krebbers committed Aug 22, 2016 221 222 223 `````` rewrite !equiv_dist=> Hx n. induction n as [|n IH]; simpl in *. - rewrite Hx fixpoint_unfold; eauto using contractive_0. - rewrite Hx fixpoint_unfold. apply (contractive_S _), IH. `````` Robbert Krebbers committed Aug 21, 2016 224 225 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 226 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 227 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 228 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 229 `````` intros Hfg. rewrite fixpoint_eq /fixpoint_def `````` Robbert Krebbers committed Feb 18, 2016 230 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 231 232 `````` induction n as [|n IH]; simpl in *; [by rewrite !Hfg|]. rewrite Hfg; apply contractive_S, IH; auto using dist_S. `````` Robbert Krebbers committed Nov 11, 2015 233 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 234 235 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 236 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. `````` Jacques-Henri Jourdan committed Dec 23, 2016 237 238 `````` Lemma fixpoint_ind (P : A → Prop) : `````` Jacques-Henri Jourdan committed Dec 23, 2016 239 `````` Proper ((≡) ==> impl) P → `````` Jacques-Henri Jourdan committed Dec 23, 2016 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 `````` (∃ x, P x) → (∀ x, P x → P (f x)) → (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) → P (fixpoint f). Proof. intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x). assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n). { intros n. induction n as [|n IH]=> -[|i] //= ?; try omega. - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. } set (fp2 := compl {| chain_cauchy := Hcauch |}). rewrite -(fixpoint_unique fp2); first by apply Hlim; induction n; apply Hincr. apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar. induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. Qed. `````` Robbert Krebbers committed Nov 11, 2015 255 256 ``````End fixpoint. `````` Robbert Krebbers committed Dec 05, 2016 257 258 ``````(** Mutual fixpoints *) Section fixpoint2. `````` 259 260 `````` Local Unset Default Proof Using. `````` Robbert Krebbers committed Dec 05, 2016 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 `````` Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}. Context (fA : A → B → A). Context (fB : A → B → B). Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}. Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}. Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x). Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB. Proof. intros n x x' Hx; rewrite /fixpoint_AB. apply fixpoint_ne=> y. by f_contractive. Qed. Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x). Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA. Proof. solve_contractive. Qed. Definition fixpoint_A : A := fixpoint fixpoint_AA. Definition fixpoint_B : B := fixpoint_AB fixpoint_A. Lemma fixpoint_A_unfold : fA fixpoint_A fixpoint_B ≡ fixpoint_A. Proof. by rewrite {2}/fixpoint_A (fixpoint_unfold _). Qed. Lemma fixpoint_B_unfold : fB fixpoint_A fixpoint_B ≡ fixpoint_B. Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed. Instance: Proper ((≡) ==> (≡) ==> (≡)) fA. Proof. apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S. Qed. Instance: Proper ((≡) ==> (≡) ==> (≡)) fB. Proof. apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S. Qed. Lemma fixpoint_A_unique p q : fA p q ≡ p → fB p q ≡ q → p ≡ fixpoint_A. Proof. intros HfA HfB. rewrite -HfA. apply fixpoint_unique. rewrite /fixpoint_AA. f_equiv=> //. apply fixpoint_unique. by rewrite HfA HfB. Qed. Lemma fixpoint_B_unique p q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B. Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed. End fixpoint2. Section fixpoint2_ne. Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}. Context (fA fA' : A → B → A). Context (fB fB' : A → B → B). Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}. Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA'}. Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}. Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB'}. Lemma fixpoint_A_ne n : (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) → fixpoint_A fA fB ≡{n}≡ fixpoint_A fA' fB'. Proof. intros HfA HfB. apply fixpoint_ne=> z. rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv. by apply fixpoint_ne. Qed. Lemma fixpoint_B_ne n : (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) → fixpoint_B fA fB ≡{n}≡ fixpoint_B fA' fB'. Proof. intros HfA HfB. apply fixpoint_ne=> z. rewrite HfB. f_contractive. apply fixpoint_A_ne; auto using dist_S. Qed. Lemma fixpoint_A_proper : (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) → fixpoint_A fA fB ≡ fixpoint_A fA' fB'. Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_A_ne. Qed. Lemma fixpoint_B_proper : (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) → fixpoint_B fA fB ≡ fixpoint_B fA' fB'. Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed. End fixpoint2_ne. `````` Robbert Krebbers committed Jul 25, 2016 338 ``````(** Function space *) `````` Ralf Jung committed Nov 22, 2016 339 ``````(* We make [ofe_fun] a definition so that we can register it as a canonical `````` Robbert Krebbers committed Aug 05, 2016 340 ``````structure. *) `````` Ralf Jung committed Nov 22, 2016 341 ``````Definition ofe_fun (A : Type) (B : ofeT) := A → B. `````` Robbert Krebbers committed Jul 25, 2016 342 `````` `````` Ralf Jung committed Nov 22, 2016 343 344 345 346 347 ``````Section ofe_fun. Context {A : Type} {B : ofeT}. Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, ∀ x, f x ≡ g x. Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B). `````` Robbert Krebbers committed Jul 25, 2016 348 349 350 351 352 353 354 355 356 357 `````` Proof. split. - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. intros Hfg k; apply equiv_dist=> n; apply Hfg. - intros n; split. + by intros f x. + by intros f g ? x. + by intros f g h ?? x; trans (g x). - by intros n f g ? x; apply dist_S. Qed. `````` Ralf Jung committed Nov 22, 2016 358 `````` Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin. `````` Robbert Krebbers committed Jul 25, 2016 359 `````` `````` Ralf Jung committed Nov 22, 2016 360 361 362 363 364 365 366 367 368 `````` Program Definition ofe_fun_chain `(c : chain ofe_funC) (x : A) : chain B := {| chain_car n := c n x |}. Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed. Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC := { compl c x := compl (ofe_fun_chain c x) }. Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed. End ofe_fun. Arguments ofe_funC : clear implicits. `````` Robbert Krebbers committed Jul 25, 2016 369 ``````Notation "A -c> B" := `````` Ralf Jung committed Nov 22, 2016 370 371 `````` (ofe_funC A B) (at level 99, B at level 200, right associativity). Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} : `````` Robbert Krebbers committed Jul 25, 2016 372 373 `````` Inhabited (A -c> B) := populate (λ _, inhabitant). `````` Robbert Krebbers committed Jul 25, 2016 374 ``````(** Non-expansive function space *) `````` Ralf Jung committed Nov 22, 2016 375 376 377 ``````Record ofe_mor (A B : ofeT) : Type := CofeMor { ofe_mor_car :> A → B; ofe_mor_ne n : Proper (dist n ==> dist n) ofe_mor_car `````` Robbert Krebbers committed Nov 11, 2015 378 379 ``````}. Arguments CofeMor {_ _} _ {_}. `````` Ralf Jung committed Nov 22, 2016 380 381 ``````Add Printing Constructor ofe_mor. Existing Instance ofe_mor_ne. `````` Robbert Krebbers committed Nov 11, 2015 382 `````` `````` Robbert Krebbers committed Jun 17, 2016 383 384 385 386 ``````Notation "'λne' x .. y , t" := (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _) (at level 200, x binder, y binder, right associativity). `````` Ralf Jung committed Nov 22, 2016 387 388 389 390 391 392 393 ``````Section ofe_mor. Context {A B : ofeT}. Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f. Proof. apply ne_proper, ofe_mor_ne. Qed. Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x. Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x. Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B). `````` Robbert Krebbers committed Jan 14, 2016 394 395 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 396 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 397 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 398 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 399 400 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 401 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 402 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Jan 14, 2016 403 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 `````` Canonical Structure ofe_morC := OfeT (ofe_mor A B) ofe_mor_ofe_mixin. Program Definition ofe_mor_chain (c : chain ofe_morC) (x : A) : chain B := {| chain_car n := c n x |}. Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed. Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morC := λ c, {| ofe_mor_car x := compl (ofe_mor_chain c x) |}. Next Obligation. intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x)) (conv_compl n (ofe_mor_chain c y)) /= Hx. Qed. Global Program Instance ofe_more_cofe `{Cofe B} : Cofe ofe_morC := {| compl := ofe_mor_compl |}. Next Obligation. intros ? n c x; simpl. by rewrite (conv_compl n (ofe_mor_chain c x)) /=. Qed. `````` Robbert Krebbers committed Jan 14, 2016 421 `````` `````` Ralf Jung committed Nov 22, 2016 422 423 `````` Global Instance ofe_mor_car_ne n : Proper (dist n ==> dist n ==> dist n) (@ofe_mor_car A B). `````` Robbert Krebbers committed Jan 14, 2016 424 `````` Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed. `````` Ralf Jung committed Nov 22, 2016 425 426 427 `````` Global Instance ofe_mor_car_proper : Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car A B) := ne_proper_2 _. Lemma ofe_mor_ext (f g : ofe_mor A B) : f ≡ g ↔ ∀ x, f x ≡ g x. `````` Robbert Krebbers committed Jan 14, 2016 428 `````` Proof. done. Qed. `````` Ralf Jung committed Nov 22, 2016 429 ``````End ofe_mor. `````` Robbert Krebbers committed Jan 14, 2016 430 `````` `````` Ralf Jung committed Nov 22, 2016 431 ``````Arguments ofe_morC : clear implicits. `````` Robbert Krebbers committed Jul 25, 2016 432 ``````Notation "A -n> B" := `````` Ralf Jung committed Nov 22, 2016 433 434 `````` (ofe_morC A B) (at level 99, B at level 200, right associativity). Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} : `````` Robbert Krebbers committed Jul 25, 2016 435 `````` Inhabited (A -n> B) := populate (λne _, inhabitant). `````` Robbert Krebbers committed Nov 11, 2015 436 `````` `````` Ralf Jung committed Mar 17, 2016 437 ``````(** Identity and composition and constant function *) `````` Robbert Krebbers committed Nov 11, 2015 438 439 ``````Definition cid {A} : A -n> A := CofeMor id. Instance: Params (@cid) 1. `````` Ralf Jung committed Nov 22, 2016 440 ``````Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x). `````` Ralf Jung committed Mar 17, 2016 441 ``````Instance: Params (@cconst) 2. `````` Robbert Krebbers committed Mar 02, 2016 442 `````` `````` Robbert Krebbers committed Nov 11, 2015 443 444 445 446 447 ``````Definition ccompose {A B C} (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g). Instance: Params (@ccompose) 3. Infix "◎" := ccompose (at level 40, left associativity). Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n : `````` Ralf Jung committed Feb 10, 2016 448 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 449 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 450 `````` `````` Ralf Jung committed Mar 02, 2016 451 ``````(* Function space maps *) `````` Ralf Jung committed Nov 22, 2016 452 ``````Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') `````` Ralf Jung committed Mar 02, 2016 453 `````` (h : A -n> B) : A' -n> B' := g ◎ h ◎ f. `````` Ralf Jung committed Nov 22, 2016 454 455 ``````Instance ofe_mor_map_ne {A A' B B'} n : Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B'). `````` Robbert Krebbers committed Mar 02, 2016 456 ``````Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed. `````` Ralf Jung committed Mar 02, 2016 457 `````` `````` Ralf Jung committed Nov 22, 2016 458 459 460 461 ``````Definition ofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') : (A -n> B) -n> (A' -n> B') := CofeMor (ofe_mor_map f g). Instance ofe_morC_map_ne {A A' B B'} n : Proper (dist n ==> dist n ==> dist n) (@ofe_morC_map A A' B B'). `````` Ralf Jung committed Mar 02, 2016 462 ``````Proof. `````` Ralf Jung committed Nov 22, 2016 463 `````` intros f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map. `````` Robbert Krebbers committed Mar 02, 2016 464 `````` by repeat apply ccompose_ne. `````` Ralf Jung committed Mar 02, 2016 465 466 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 467 ``````(** unit *) `````` Robbert Krebbers committed Jan 14, 2016 468 469 ``````Section unit. Instance unit_dist : Dist unit := λ _ _ _, True. `````` Ralf Jung committed Nov 22, 2016 470 `````` Definition unit_ofe_mixin : OfeMixin unit. `````` Robbert Krebbers committed Jan 14, 2016 471 `````` Proof. by repeat split; try exists 0. Qed. `````` Ralf Jung committed Nov 22, 2016 472 `````` Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin. `````` Robbert Krebbers committed Nov 28, 2016 473 `````` `````` Ralf Jung committed Nov 22, 2016 474 475 `````` Global Program Instance unit_cofe : Cofe unitC := { compl x := () }. Next Obligation. by repeat split; try exists 0. Qed. `````` Robbert Krebbers committed Nov 28, 2016 476 477 `````` Global Instance unit_discrete_cofe : Discrete unitC. `````` Robbert Krebbers committed Jan 31, 2016 478 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 479 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 480 481 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 482 ``````Section product. `````` Ralf Jung committed Nov 22, 2016 483 `````` Context {A B : ofeT}. `````` Robbert Krebbers committed Jan 14, 2016 484 485 486 487 488 489 `````` Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n). Global Instance pair_ne : Proper (dist n ==> dist n ==> dist n) (@pair A B) := _. Global Instance fst_ne : Proper (dist n ==> dist n) (@fst A B) := _. Global Instance snd_ne : Proper (dist n ==> dist n) (@snd A B) := _. `````` Ralf Jung committed Nov 22, 2016 490 `````` Definition prod_ofe_mixin : OfeMixin (A * B). `````` Robbert Krebbers committed Jan 14, 2016 491 492 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 493 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 494 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 495 496 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Jan 14, 2016 497 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 498 499 500 501 502 503 504 505 506 `````` Canonical Structure prodC : ofeT := OfeT (A * B) prod_ofe_mixin. Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodC := { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }. Next Obligation. intros ?? n c; split. apply (conv_compl n (chain_map fst c)). apply (conv_compl n (chain_map snd c)). Qed. `````` Jacques-Henri Jourdan committed Jun 15, 2016 507 508 509 `````` Global Instance prod_timeless (x : A * B) : Timeless (x.1) → Timeless (x.2) → Timeless x. Proof. by intros ???[??]; split; apply (timeless _). Qed. `````` Robbert Krebbers committed Feb 24, 2016 510 511 `````` Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC. Proof. intros ?? [??]; apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 512 513 514 515 516 ``````End product. Arguments prodC : clear implicits. Typeclasses Opaque prod_dist. `````` Ralf Jung committed Nov 22, 2016 517 ``````Instance prod_map_ne {A A' B B' : ofeT} n : `````` Robbert Krebbers committed Nov 11, 2015 518 519 520 521 522 523 524 525 526 `````` Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n) (@prod_map A A' B B'). Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed. Definition prodC_map {A A' B B'} (f : A -n> A') (g : B -n> B') : prodC A B -n> prodC A' B' := CofeMor (prod_map f g). Instance prodC_map_ne {A A' B B'} n : Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B'). Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed. `````` Robbert Krebbers committed Mar 02, 2016 527 528 ``````(** Functors *) Structure cFunctor := CFunctor { `````` Ralf Jung committed Nov 22, 2016 529 `````` cFunctor_car : ofeT → ofeT → ofeT; `````` Robbert Krebbers committed Mar 02, 2016 530 531 `````` cFunctor_map {A1 A2 B1 B2} : ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2; `````` Robbert Krebbers committed Mar 07, 2016 532 533 `````` cFunctor_ne {A1 A2 B1 B2} n : Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2); `````` Ralf Jung committed Nov 22, 2016 534 `````` cFunctor_id {A B : ofeT} (x : cFunctor_car A B) : `````` Robbert Krebbers committed Mar 02, 2016 535 536 537 538 539 `````` cFunctor_map (cid,cid) x ≡ x; cFunctor_compose {A1 A2 A3 B1 B2 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) }. `````` Robbert Krebbers committed Mar 07, 2016 540 ``````Existing Instance cFunctor_ne. `````` Robbert Krebbers committed Mar 02, 2016 541 542 ``````Instance: Params (@cFunctor_map) 5. `````` Ralf Jung committed Mar 07, 2016 543 544 545 ``````Delimit Scope cFunctor_scope with CF. Bind Scope cFunctor_scope with cFunctor. `````` Ralf Jung committed Mar 07, 2016 546 547 548 ``````Class cFunctorContractive (F : cFunctor) := cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). `````` Ralf Jung committed Nov 22, 2016 549 ``````Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A. `````` Robbert Krebbers committed Mar 02, 2016 550 551 ``````Coercion cFunctor_diag : cFunctor >-> Funclass. `````` Ralf Jung committed Nov 22, 2016 552 ``````Program Definition constCF (B : ofeT) : cFunctor := `````` Robbert Krebbers committed Mar 02, 2016 553 554 `````` {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}. Solve Obligations with done. `````` Ralf Jung committed Jan 06, 2017 555 ``````Coercion constCF : ofeT >-> cFunctor. `````` Robbert Krebbers committed Mar 02, 2016 556 `````` `````` Ralf Jung committed Mar 07, 2016 557 ``````Instance constCF_contractive B : cFunctorContractive (constCF B). `````` Robbert Krebbers committed Mar 07, 2016 558 ``````Proof. rewrite /cFunctorContractive; apply _. Qed. `````` Ralf Jung committed Mar 07, 2016 559 560 561 562 `````` Program Definition idCF : cFunctor := {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}. Solve Obligations with done. `````` Ralf Jung committed Jan 06, 2017 563 ``````Notation "∙" := idCF : cFunctor_scope. `````` Ralf Jung committed Mar 07, 2016 564 `````` `````` Robbert Krebbers committed Mar 02, 2016 565 566 567 568 569 ``````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 := prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg) |}. `````` Robbert Krebbers committed Mar 07, 2016 570 571 572 ``````Next Obligation. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 573 574 575 576 577 ``````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. by rewrite !cFunctor_compose. Qed. `````` Ralf Jung committed Jan 06, 2017 578 ``````Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope. `````` Robbert Krebbers committed Mar 02, 2016 579 `````` `````` Ralf Jung committed Mar 07, 2016 580 581 582 583 584 585 586 587 ``````Instance prodCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (prodCF F1 F2). Proof. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_contractive. Qed. `````` Ralf Jung committed Nov 22, 2016 588 ``````Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') n : `````` Jacques-Henri Jourdan committed Oct 05, 2016 589 590 591 `````` Proper (dist n ==> dist n) (compose f : (A -c> B) → A -c> B'). Proof. intros g g' Hf x; simpl. by rewrite (Hf x). Qed. `````` Ralf Jung committed Nov 22, 2016 592 ``````Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') := `````` Jacques-Henri Jourdan committed Oct 05, 2016 593 `````` @CofeMor (_ -c> _) (_ -c> _) (compose f) _. `````` Ralf Jung committed Nov 22, 2016 594 595 ``````Instance ofe_funC_map_ne {A B B'} n : Proper (dist n ==> dist n) (@ofe_funC_map A B B'). `````` Jacques-Henri Jourdan committed Oct 05, 2016 596 597 ``````Proof. intros f f' Hf g x. apply Hf. Qed. `````` Ralf Jung committed Nov 22, 2016 598 599 600 ``````Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {| cFunctor_car A B := ofe_funC T (cFunctor_car F A B); cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (cFunctor_map F fg) `````` Jacques-Henri Jourdan committed Oct 05, 2016 601 602 ``````|}. Next Obligation. `````` Ralf Jung committed Nov 22, 2016 603 `````` intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne. `````` Jacques-Henri Jourdan committed Oct 05, 2016 604 605 606 607 608 609 ``````Qed. Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed. Next Obligation. intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl. by rewrite !cFunctor_compose. Qed. `````` Ralf Jung committed Jan 06, 2017 610 ``````Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope. `````` Jacques-Henri Jourdan committed Oct 05, 2016 611 `````` `````` Ralf Jung committed Nov 22, 2016 612 613 ``````Instance ofe_funCF_contractive (T : Type) (F : cFunctor) : cFunctorContractive F → cFunctorContractive (ofe_funCF T F). `````` Jacques-Henri Jourdan committed Oct 05, 2016 614 615 ``````Proof. intros ?? A1 A2 B1 B2 n ???; `````` Ralf Jung committed Nov 22, 2016 616 `````` by apply ofe_funC_map_ne; apply cFunctor_contractive. `````` Jacques-Henri Jourdan committed Oct 05, 2016 617 618 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 619 ``````Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {| `````` Robbert Krebbers committed Jul 25, 2016 620 `````` cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B; `````` Ralf Jung committed Mar 02, 2016 621 `````` cFunctor_map A1 A2 B1 B2 fg := `````` Ralf Jung committed Nov 22, 2016 622 `````` ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg) `````` Ralf Jung committed Mar 02, 2016 623 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 624 625 ``````Next Obligation. intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. `````` Ralf Jung committed Nov 22, 2016 626 `````` apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg. `````` Robbert Krebbers committed Mar 07, 2016 627 ``````Qed. `````` Ralf Jung committed Mar 02, 2016 628 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 629 630 `````` intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id. apply (ne_proper f). apply cFunctor_id. `````` Ralf Jung committed Mar 02, 2016 631 632 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 633 634 `````` 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. `````` Ralf Jung committed Mar 02, 2016 635 ``````Qed. `````` Ralf Jung committed Jan 06, 2017 636 ``````Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope. `````` Ralf Jung committed Mar 02, 2016 637 `````` `````` Ralf Jung committed Nov 22, 2016 638 ``````Instance ofe_morCF_contractive F1 F2 : `````` Ralf Jung committed Mar 07, 2016 639 `````` cFunctorContractive F1 → cFunctorContractive F2 → `````` Ralf Jung committed Nov 22, 2016 640 `````` cFunctorContractive (ofe_morCF F1 F2). `````` Ralf Jung committed Mar 07, 2016 641 642 ``````Proof. intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. `````` Robbert Krebbers committed Dec 05, 2016 643 `````` apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split. `````` Ralf Jung committed Mar 07, 2016 644 645 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 646 647 ``````(** Sum *) Section sum. `````` Ralf Jung committed Nov 22, 2016 648 `````` Context {A B : ofeT}. `````` Robbert Krebbers committed May 27, 2016 649 650 651 652 653 654 655 `````` Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n). Global Instance inl_ne : Proper (dist n ==> dist n) (@inl A B) := _. Global Instance inr_ne : Proper (dist n ==> dist n) (@inr A B) := _. Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _. Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _. `````` Ralf Jung committed Nov 22, 2016 656 657 658 659 660 661 662 663 664 665 666 667 `````` Definition sum_ofe_mixin : OfeMixin (A + B). Proof. split. - intros x y; split=> Hx. + destruct Hx=> n; constructor; by apply equiv_dist. + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _). - apply _. - destruct 1; constructor; by apply dist_S. Qed. Canonical Structure sumC : ofeT := OfeT (A + B) sum_ofe_mixin. Program Definition inl_chain (c : chain sumC) (a : A) : chain A := `````` Robbert Krebbers committed May 27, 2016 668 669 `````` {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}. Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed. `````` Ralf Jung committed Nov 22, 2016 670 `````` Program Definition inr_chain (c : chain sumC) (b : B) : chain B := `````` Robbert Krebbers committed May 27, 2016 671 672 673 `````` {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}. Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed. `````` Ralf Jung committed Nov 22, 2016 674 `````` Definition sum_compl `{Cofe A, Cofe B} : Compl sumC := λ c, `````` Robbert Krebbers committed May 27, 2016 675 676 677 678 `````` match c 0 with | inl a => inl (compl (inl_chain c a)) | inr b => inr (compl (inr_chain c b)) end. `````` Ralf Jung committed Nov 22, 2016 679 680 681 682 683 684 685 `````` Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumC := { compl := sum_compl }. Next Obligation. intros ?? n c; rewrite /compl /sum_compl. feed inversion (chain_cauchy c 0 n); first by auto with lia; constructor. - rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver. - rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver. `````` Robbert Krebbers committed May 27, 2016 686 687 688 689 690 691 692 693 694 695 696 697 698 `````` Qed. Global Instance inl_timeless (x : A) : Timeless x → Timeless (inl x). Proof. inversion_clear 2; constructor; by apply (timeless _). Qed. Global Instance inr_timeless (y : B) : Timeless y → Timeless (inr y). Proof. inversion_clear 2; constructor; by apply (timeless _). Qed. Global Instance sum_discrete_cofe : Discrete A → Discrete B → Discrete sumC. Proof. intros ?? [?|?]; apply _. Qed. End sum. Arguments sumC : clear implicits. Typeclasses Opaque sum_dist. `````` Ralf Jung committed Nov 22, 2016 699 ``````Instance sum_map_ne {A A' B B' : ofeT} n : `````` Robbert Krebbers committed May 27, 2016 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 `````` Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n) (@sum_map A A' B B'). Proof. intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg]. Qed. Definition sumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') : sumC A B -n> sumC A' B' := CofeMor (sum_map f g). Instance sumC_map_ne {A A' B B'} n : Proper (dist n ==> dist n ==> dist n) (@sumC_map A A' B B'). Proof. intros 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 := 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. 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; by rewrite !cFunctor_compose. Qed. `````` Ralf Jung committed Jan 06, 2017 724 ``````Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope. `````` Robbert Krebbers committed May 27, 2016 725 726 727 728 729 730 731 732 733 `````` Instance sumCF_contractive F1 F2 : cFunctorContractive F1 → cFunctorContractive F2 → cFunctorContractive (sumCF F1 F2). Proof. intros ?? A1 A2 B1 B2 n ???; by apply sumC_map_ne; apply cFunctor_contractive. Qed. `````` Robbert Krebbers committed Nov 16, 2015 734 735 736 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Dec 05, 2016 737 `````` `````` Robbert Krebbers committed Feb 10, 2016 738 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Ralf Jung committed Nov 22, 2016 739 `````` Definition discrete_ofe_mixin : OfeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 740 741 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 742 743 744 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Ralf Jung committed Nov 22, 2016 745 `````` Qed. `````` Robbert Krebbers committed Dec 05, 2016 746 `````` `````` Ralf Jung committed Nov 22, 2016 747 748 749 750 751 `````` Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) := { compl c := c 0 }. Next Obligation. intros n c. rewrite /compl /=; symmetry; apply (chain_cauchy c 0 n). omega. `````` Robbert Krebbers committed Nov 16, 2015 752 753 754 `````` Qed. End discrete_cofe. `````` Ralf Jung committed Nov 22, 2016 755 756 ``````Notation discreteC A := (OfeT A discrete_ofe_mixin). Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)). `````` Robbert Krebbers committed May 25, 2016 757 758 759 760 761 762 `````` Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} : Discrete (discreteC A). Proof. by intros x y. Qed. Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A). Proof. by intros x y. Qed. `````` Robbert Krebbers committed Jan 16, 2016 763 `````` `````` Robbert Krebbers committed Dec 11, 2015 764 ``````Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Dec 09, 2016 765 766 767 768 ``````Canonical Structure natC := leibnizC nat. Canonical Structure positiveC := leibnizC positive. Canonical Structure NC := leibnizC N. Canonical Structure ZC := leibnizC Z. `````` Robbert Krebbers committed Nov 19, 2015 769 `````` `````` Robbert Krebbers committed May 25, 2016 770 771 ``````(* Option *) Section option. `````` Ralf Jung committed Nov 22, 2016 772 `````` Context {A : ofeT}. `````` Robbert Krebbers committed May 25, 2016 773 `````` `````` Robbert Krebbers committed May 27, 2016 774 `````` Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n). `````` Robbert Krebbers committed May 25, 2016 775 `````` Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my. `````` Robbert Krebbers committed May 27, 2016 776 `````` Proof. done. Qed. `````` Robbert Krebbers committed May 25, 2016 777 `````` `````` Ralf Jung committed Nov 22, 2016 778 `````` Definition option_ofe_mixin : OfeMixin (option A). `````` Robbert Krebbers committed May 25, 2016 779 780 781 782 783 `````` Proof. split. - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|]. intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist. by intros n; feed inversion (Hxy n). `````` Robbert Krebbers committed May 27, 2016 784 `````` - apply _. `````` Robbert Krebbers committed May 25, 2016 785 786 `````` - destruct 1; constructor; by apply dist_S. Qed. `````` Ralf Jung committed Nov 22, 2016 787 788 789 790 791