ofe.v 39.3 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.algebra Require Export base. `````` Ralf Jung committed Jan 03, 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 162 163 164 165 ``````Section contractive. 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 166 `````` Proof. by apply (_ : Contractive f). Qed. `````` Robbert Krebbers committed Dec 02, 2016 167 `````` Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y. `````` Robbert Krebbers committed Dec 05, 2016 168 `````` Proof. intros. by apply (_ : Contractive f). Qed. `````` Robbert Krebbers committed Dec 02, 2016 169 170 171 172 173 174 175 `````` 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 176 177 178 179 180 181 182 ``````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 183 184 `````` | |- @dist_later ?A ?n ?x ?y => destruct n as [|n]; [done|change (@dist A _ n x y)] `````` Robbert Krebbers committed Dec 05, 2016 185 186 187 188 189 190 `````` end; try reflexivity. Ltac solve_contractive := preprocess_solve_proper; solve [repeat (first [f_contractive|f_equiv]; try eassumption)]. `````` Robbert Krebbers committed Nov 22, 2015 191 `````` `````` Robbert Krebbers committed Nov 11, 2015 192 ``````(** Fixpoint *) `````` Ralf Jung committed Nov 22, 2016 193 ``````Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A) `````` Robbert Krebbers committed Feb 10, 2016 194 `````` `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. `````` Robbert Krebbers committed Nov 11, 2015 195 ``````Next Obligation. `````` Robbert Krebbers committed Mar 06, 2016 196 `````` intros A ? f ? n. `````` Robbert Krebbers committed Dec 05, 2016 197 `````` induction n as [|n IH]=> -[|i] //= ?; try omega. `````` Robbert Krebbers committed Feb 17, 2016 198 199 `````` - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. `````` Robbert Krebbers committed Nov 11, 2015 200 ``````Qed. `````` Robbert Krebbers committed Mar 18, 2016 201 `````` `````` Ralf Jung committed Nov 22, 2016 202 ``````Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A) `````` Robbert Krebbers committed Nov 17, 2015 203 `````` `{!Contractive f} : A := compl (fixpoint_chain f). `````` Robbert Krebbers committed Mar 18, 2016 204 ``````Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed. `````` Ralf Jung committed Nov 22, 2016 205 ``````Definition fixpoint {A AC AiH} f {Hf} := proj1_sig fixpoint_aux A AC AiH f Hf. `````` Robbert Krebbers committed Mar 18, 2016 206 ``````Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux. `````` Robbert Krebbers committed Nov 11, 2015 207 208 `````` Section fixpoint. `````` Ralf Jung committed Nov 22, 2016 209 `````` Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}. `````` Robbert Krebbers committed Aug 21, 2016 210 `````` `````` Robbert Krebbers committed Nov 17, 2015 211 `````` Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). `````` Robbert Krebbers committed Nov 11, 2015 212 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 213 214 `````` apply equiv_dist=>n. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //. `````` Robbert Krebbers committed Feb 12, 2016 215 `````` induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. `````` Robbert Krebbers committed Nov 11, 2015 216 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2016 217 218 219 `````` Lemma fixpoint_unique (x : A) : x ≡ f x → x ≡ fixpoint f. Proof. `````` Robbert Krebbers committed Aug 22, 2016 220 221 222 `````` 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 223 224 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 225 `````` Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : `````` Ralf Jung committed Feb 10, 2016 226 `````` (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 227 `````` Proof. `````` Robbert Krebbers committed Mar 18, 2016 228 `````` intros Hfg. rewrite fixpoint_eq /fixpoint_def `````` Robbert Krebbers committed Feb 18, 2016 229 `````` (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=. `````` Robbert Krebbers committed Feb 10, 2016 230 231 `````` 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 232 `````` Qed. `````` Robbert Krebbers committed Nov 17, 2015 233 234 `````` Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. `````` Robbert Krebbers committed Nov 11, 2015 235 `````` Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. `````` Jacques-Henri Jourdan committed Dec 23, 2016 236 237 `````` Lemma fixpoint_ind (P : A → Prop) : `````` Jacques-Henri Jourdan committed Dec 23, 2016 238 `````` Proper ((≡) ==> impl) P → `````` Jacques-Henri Jourdan committed Dec 23, 2016 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 `````` (∃ 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 254 255 ``````End fixpoint. `````` Robbert Krebbers committed Dec 05, 2016 256 257 ``````(** Mutual fixpoints *) Section fixpoint2. `````` 258 259 `````` Local Unset Default Proof Using. `````` Robbert Krebbers committed Dec 05, 2016 260 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 `````` 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 337 ``````(** Function space *) `````` Ralf Jung committed Nov 22, 2016 338 ``````(* We make [ofe_fun] a definition so that we can register it as a canonical `````` Robbert Krebbers committed Aug 05, 2016 339 ``````structure. *) `````` Ralf Jung committed Nov 22, 2016 340 ``````Definition ofe_fun (A : Type) (B : ofeT) := A → B. `````` Robbert Krebbers committed Jul 25, 2016 341 `````` `````` Ralf Jung committed Nov 22, 2016 342 343 344 345 346 ``````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 347 348 349 350 351 352 353 354 355 356 `````` 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 357 `````` Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin. `````` Robbert Krebbers committed Jul 25, 2016 358 `````` `````` Ralf Jung committed Nov 22, 2016 359 360 361 362 363 364 365 366 367 `````` 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 368 ``````Notation "A -c> B" := `````` Ralf Jung committed Nov 22, 2016 369 370 `````` (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 371 372 `````` Inhabited (A -c> B) := populate (λ _, inhabitant). `````` Robbert Krebbers committed Jul 25, 2016 373 ``````(** Non-expansive function space *) `````` Ralf Jung committed Nov 22, 2016 374 375 376 ``````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 377 378 ``````}. Arguments CofeMor {_ _} _ {_}. `````` Ralf Jung committed Nov 22, 2016 379 380 ``````Add Printing Constructor ofe_mor. Existing Instance ofe_mor_ne. `````` Robbert Krebbers committed Nov 11, 2015 381 `````` `````` Robbert Krebbers committed Jun 17, 2016 382 383 384 385 ``````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 386 387 388 389 390 391 392 ``````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 393 394 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 395 `````` - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. `````` Robbert Krebbers committed Feb 18, 2016 396 `````` intros Hfg k; apply equiv_dist=> n; apply Hfg. `````` Robbert Krebbers committed Feb 17, 2016 397 `````` - intros n; split. `````` Robbert Krebbers committed Jan 14, 2016 398 399 `````` + by intros f x. + by intros f g ? x. `````` Ralf Jung committed Feb 20, 2016 400 `````` + by intros f g h ?? x; trans (g x). `````` Robbert Krebbers committed Feb 17, 2016 401 `````` - by intros n f g ? x; apply dist_S. `````` Robbert Krebbers committed Jan 14, 2016 402 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 `````` 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 420 `````` `````` Ralf Jung committed Nov 22, 2016 421 422 `````` 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 423 `````` Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed. `````` Ralf Jung committed Nov 22, 2016 424 425 426 `````` 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 427 `````` Proof. done. Qed. `````` Ralf Jung committed Nov 22, 2016 428 ``````End ofe_mor. `````` Robbert Krebbers committed Jan 14, 2016 429 `````` `````` Ralf Jung committed Nov 22, 2016 430 ``````Arguments ofe_morC : clear implicits. `````` Robbert Krebbers committed Jul 25, 2016 431 ``````Notation "A -n> B" := `````` Ralf Jung committed Nov 22, 2016 432 433 `````` (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 434 `````` Inhabited (A -n> B) := populate (λne _, inhabitant). `````` Robbert Krebbers committed Nov 11, 2015 435 `````` `````` Ralf Jung committed Mar 17, 2016 436 ``````(** Identity and composition and constant function *) `````` Robbert Krebbers committed Nov 11, 2015 437 438 ``````Definition cid {A} : A -n> A := CofeMor id. Instance: Params (@cid) 1. `````` Ralf Jung committed Nov 22, 2016 439 ``````Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x). `````` Ralf Jung committed Mar 17, 2016 440 ``````Instance: Params (@cconst) 2. `````` Robbert Krebbers committed Mar 02, 2016 441 `````` `````` Robbert Krebbers committed Nov 11, 2015 442 443 444 445 446 ``````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 447 `````` f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. `````` Robbert Krebbers committed Jan 13, 2016 448 ``````Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. `````` Robbert Krebbers committed Nov 11, 2015 449 `````` `````` Ralf Jung committed Mar 02, 2016 450 ``````(* Function space maps *) `````` Ralf Jung committed Nov 22, 2016 451 ``````Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') `````` Ralf Jung committed Mar 02, 2016 452 `````` (h : A -n> B) : A' -n> B' := g ◎ h ◎ f. `````` Ralf Jung committed Nov 22, 2016 453 454 ``````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 455 ``````Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed. `````` Ralf Jung committed Mar 02, 2016 456 `````` `````` Ralf Jung committed Nov 22, 2016 457 458 459 460 ``````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 461 ``````Proof. `````` Ralf Jung committed Nov 22, 2016 462 `````` intros f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map. `````` Robbert Krebbers committed Mar 02, 2016 463 `````` by repeat apply ccompose_ne. `````` Ralf Jung committed Mar 02, 2016 464 465 ``````Qed. `````` Robbert Krebbers committed Nov 11, 2015 466 ``````(** unit *) `````` Robbert Krebbers committed Jan 14, 2016 467 468 ``````Section unit. Instance unit_dist : Dist unit := λ _ _ _, True. `````` Ralf Jung committed Nov 22, 2016 469 `````` Definition unit_ofe_mixin : OfeMixin unit. `````` Robbert Krebbers committed Jan 14, 2016 470 `````` Proof. by repeat split; try exists 0. Qed. `````` Ralf Jung committed Nov 22, 2016 471 `````` Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin. `````` Robbert Krebbers committed Nov 28, 2016 472 `````` `````` Ralf Jung committed Nov 22, 2016 473 474 `````` Global Program Instance unit_cofe : Cofe unitC := { compl x := () }. Next Obligation. by repeat split; try exists 0. Qed. `````` Robbert Krebbers committed Nov 28, 2016 475 476 `````` Global Instance unit_discrete_cofe : Discrete unitC. `````` Robbert Krebbers committed Jan 31, 2016 477 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jan 14, 2016 478 ``````End unit. `````` Robbert Krebbers committed Nov 11, 2015 479 480 `````` (** Product *) `````` Robbert Krebbers committed Jan 14, 2016 481 ``````Section product. `````` Ralf Jung committed Nov 22, 2016 482 `````` Context {A B : ofeT}. `````` Robbert Krebbers committed Jan 14, 2016 483 484 485 486 487 488 `````` 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 489 `````` Definition prod_ofe_mixin : OfeMixin (A * B). `````` Robbert Krebbers committed Jan 14, 2016 490 491 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 492 `````` - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation. `````` Robbert Krebbers committed Jan 14, 2016 493 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 494 495 `````` - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. `````` Robbert Krebbers committed Jan 14, 2016 496 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 497 498 499 500 501 502 503 504 505 `````` 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 506 507 508 `````` 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 509 510 `````` Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC. Proof. intros ?? [??]; apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 511 512 513 514 515 ``````End product. Arguments prodC : clear implicits. Typeclasses Opaque prod_dist. `````` Ralf Jung committed Nov 22, 2016 516 ``````Instance prod_map_ne {A A' B B' : ofeT} n : `````` Robbert Krebbers committed Nov 11, 2015 517 518 519 520 521 522 523 524 525 `````` 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 526 527 ``````(** Functors *) Structure cFunctor := CFunctor { `````` Ralf Jung committed Nov 22, 2016 528 `````` cFunctor_car : ofeT → ofeT → ofeT; `````` Robbert Krebbers committed Mar 02, 2016 529 530 `````` 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 531 532 `````` cFunctor_ne {A1 A2 B1 B2} n : Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2); `````` Ralf Jung committed Nov 22, 2016 533 `````` cFunctor_id {A B : ofeT} (x : cFunctor_car A B) : `````` Robbert Krebbers committed Mar 02, 2016 534 535 536 537 538 `````` 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 539 ``````Existing Instance cFunctor_ne. `````` Robbert Krebbers committed Mar 02, 2016 540 541 ``````Instance: Params (@cFunctor_map) 5. `````` Ralf Jung committed Mar 07, 2016 542 543 544 ``````Delimit Scope cFunctor_scope with CF. Bind Scope cFunctor_scope with cFunctor. `````` Ralf Jung committed Mar 07, 2016 545 546 547 ``````Class cFunctorContractive (F : cFunctor) := cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). `````` Ralf Jung committed Nov 22, 2016 548 ``````Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A. `````` Robbert Krebbers committed Mar 02, 2016 549 550 ``````Coercion cFunctor_diag : cFunctor >-> Funclass. `````` Ralf Jung committed Nov 22, 2016 551 ``````Program Definition constCF (B : ofeT) : cFunctor := `````` Robbert Krebbers committed Mar 02, 2016 552 553 554 `````` {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}. Solve Obligations with done. `````` Ralf Jung committed Mar 07, 2016 555 ``````Instance constCF_contractive B : cFunctorContractive (constCF B). `````` Robbert Krebbers committed Mar 07, 2016 556 ``````Proof. rewrite /cFunctorContractive; apply _. Qed. `````` Ralf Jung committed Mar 07, 2016 557 558 559 560 561 `````` Program Definition idCF : cFunctor := {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}. Solve Obligations with done. `````` Robbert Krebbers committed Mar 02, 2016 562 563 564 565 566 ``````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 567 568 569 ``````Next Obligation. intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 570 571 572 573 574 575 ``````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 Mar 07, 2016 576 577 578 579 580 581 582 583 ``````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 584 ``````Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') n : `````` Jacques-Henri Jourdan committed Oct 05, 2016 585 586 587 `````` 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 588 ``````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 589 `````` @CofeMor (_ -c> _) (_ -c> _) (compose f) _. `````` Ralf Jung committed Nov 22, 2016 590 591 ``````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 592 593 ``````Proof. intros f f' Hf g x. apply Hf. Qed. `````` Ralf Jung committed Nov 22, 2016 594 595 596 ``````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 597 598 ``````|}. Next Obligation. `````` Ralf Jung committed Nov 22, 2016 599 `````` intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne. `````` Jacques-Henri Jourdan committed Oct 05, 2016 600 601 602 603 604 605 606 ``````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 Nov 22, 2016 607 608 ``````Instance ofe_funCF_contractive (T : Type) (F : cFunctor) : cFunctorContractive F → cFunctorContractive (ofe_funCF T F). `````` Jacques-Henri Jourdan committed Oct 05, 2016 609 610 ``````Proof. intros ?? A1 A2 B1 B2 n ???; `````` Ralf Jung committed Nov 22, 2016 611 `````` by apply ofe_funC_map_ne; apply cFunctor_contractive. `````` Jacques-Henri Jourdan committed Oct 05, 2016 612 613 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 614 ``````Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {| `````` Robbert Krebbers committed Jul 25, 2016 615 `````` cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B; `````` Ralf Jung committed Mar 02, 2016 616 `````` cFunctor_map A1 A2 B1 B2 fg := `````` Ralf Jung committed Nov 22, 2016 617 `````` ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg) `````` Ralf Jung committed Mar 02, 2016 618 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 619 620 ``````Next Obligation. intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. `````` Ralf Jung committed Nov 22, 2016 621 `````` apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg. `````` Robbert Krebbers committed Mar 07, 2016 622 ``````Qed. `````` Ralf Jung committed Mar 02, 2016 623 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 624 625 `````` intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id. apply (ne_proper f). apply cFunctor_id. `````` Ralf Jung committed Mar 02, 2016 626 627 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 628 629 `````` 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 630 631 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 632 ``````Instance ofe_morCF_contractive F1 F2 : `````` Ralf Jung committed Mar 07, 2016 633 `````` cFunctorContractive F1 → cFunctorContractive F2 → `````` Ralf Jung committed Nov 22, 2016 634 `````` cFunctorContractive (ofe_morCF F1 F2). `````` Ralf Jung committed Mar 07, 2016 635 636 ``````Proof. intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. `````` Robbert Krebbers committed Dec 05, 2016 637 `````` apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split. `````` Ralf Jung committed Mar 07, 2016 638 639 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 640 641 ``````(** Sum *) Section sum. `````` Ralf Jung committed Nov 22, 2016 642 `````` Context {A B : ofeT}. `````` Robbert Krebbers committed May 27, 2016 643 644 645 646 647 648 649 `````` 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 650 651 652 653 654 655 656 657 658 659 660 661 `````` 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 662 663 `````` {| 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 664 `````` Program Definition inr_chain (c : chain sumC) (b : B) : chain B := `````` Robbert Krebbers committed May 27, 2016 665 666 667 `````` {| 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 668 `````` Definition sum_compl `{Cofe A, Cofe B} : Compl sumC := λ c, `````` Robbert Krebbers committed May 27, 2016 669 670 671 672 `````` 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 673 674 675 676 677 678 679 `````` 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 680 681 682 683 684 685 686 687 688 689 690 691 692 `````` 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 693 ``````Instance sum_map_ne {A A' B B' : ofeT} n : `````` Robbert Krebbers committed May 27, 2016 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 `````` 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. 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 727 728 729 ``````(** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. `````` Robbert Krebbers committed Dec 05, 2016 730 `````` `````` Robbert Krebbers committed Feb 10, 2016 731 `````` Instance discrete_dist : Dist A := λ n x y, x ≡ y. `````` Ralf Jung committed Nov 22, 2016 732 `````` Definition discrete_ofe_mixin : OfeMixin A. `````` Robbert Krebbers committed Nov 16, 2015 733 734 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 735 736 737 `````` - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. `````` Ralf Jung committed Nov 22, 2016 738 `````` Qed. `````` Robbert Krebbers committed Dec 05, 2016 739 `````` `````` Ralf Jung committed Nov 22, 2016 740 741 742 743 744 `````` 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 745 746 747 `````` Qed. End discrete_cofe. `````` Ralf Jung committed Nov 22, 2016 748 749 ``````Notation discreteC A := (OfeT A discrete_ofe_mixin). Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)). `````` Robbert Krebbers committed May 25, 2016 750 751 752 753 754 755 `````` 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 756 `````` `````` Robbert Krebbers committed Dec 11, 2015 757 ``````Canonical Structure boolC := leibnizC bool. `````` Robbert Krebbers committed Dec 09, 2016 758 759 760 761 ``````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 762 `````` `````` Robbert Krebbers committed May 25, 2016 763 764 ``````(* Option *) Section option. `````` Ralf Jung committed Nov 22, 2016 765 `````` Context {A : ofeT}. `````` Robbert Krebbers committed May 25, 2016 766 `````` `````` Robbert Krebbers committed May 27, 2016 767 `````` Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n). `````` Robbert Krebbers committed May 25, 2016 768 `````` Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my. `````` Robbert Krebbers committed May 27, 2016 769 `````` Proof. done. Qed. `````` Robbert Krebbers committed May 25, 2016 770 `````` `````` Ralf Jung committed Nov 22, 2016 771 `````` Definition option_ofe_mixin : OfeMixin (option A). `````` Robbert Krebbers committed May 25, 2016 772 773 774 775 776 `````` 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 777 `````` - apply _. `````` Robbert Krebbers committed May 25, 2016 778 779 `````` - destruct 1; constructor; by apply dist_S. Qed. `````` Ralf Jung committed Nov 22, 2016 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 `````` Canonical Structure optionC := OfeT (option A) option_ofe_mixin. Program Definition option_chain (c : chain optionC) (x : A) : chain A := {| chain_car n := from_option id x (c n) |}. Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Definition option_compl `{Cofe A} : Compl optionC := λ c, match c 0 with Some x => Some (compl (option_chain c x)) | None => None end. Global Program Instance option_cofe `{Cofe A} : Cofe optionC := { compl := option_compl }. Next Obligation. intros ? n c; rewrite /compl /option_compl. feed inversion (chain_cauchy c 0 n); auto with lia; []. constructor. rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver. Qed. `````` Robbert Krebbers committed May 25, 2016 796 797 798 799 800 801 802 803 804 `````` Global Instance option_discrete : Discrete A → Discrete optionC. Proof. destruct 2; constructor; by apply (timeless _). Qed. Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A). Proof. by constructor. Qed. Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A). Proof. destruct 1; split; eauto. Qed. Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A). Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed May 28, 2016 805 806 807 `````` Global Instance from_option_ne {B} (R : relation B) (f : A → B) n : Proper (dist n ==> R) f → Proper (R ==> dist n ==> R) (from_option f). Proof. destruct 3; simpl; auto. Qed. `````` Robbert Krebbers committed May 25, 2016 808 809 810 811 812 `````` Global Instance None_timeless : Timeless (@None A). Proof. inversion_clear 1; constructor. Qed. Global Instance Some_timeless x : Timeless x → Timeless (Some x). Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed. `````` Robbert Krebbers committed May 27, 2016 813 814 815 816 817 818 819 820 821 822 823 824 825 `````` Lemma dist_None n mx : mx ≡{n}≡ None ↔ mx = None. Proof. split; [by inversion_clear 1|by intros ->]. Qed. Lemma dist_Some_inv_l n mx my x : mx ≡{n}≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡{n}≡ y. Proof. destruct 1; naive_solver. Qed. Lemma dist_Some_inv_r n mx my y : mx ≡{n}≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡{n}≡ y. Proof. destruct 1; naive_solver. Qed. Lemma dist_Some_inv_l' n my x : Some x ≡{n}≡ my → ∃ x', Some x' = my ∧ x ≡{n}≡ x'. Proof. intros ?%(dist_Some_inv_l _ _ _ x); naive_solver. Qed. Lemma dist_Some_inv_r' n mx y : mx ≡{n}≡ Some y → ∃ y', mx = Some y' ∧ y ≡{n}≡ y'. Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed. `````` Robbert Krebbers committed May 25, 2016 826 827 ``````End option. `````` Robbert Krebbers committed May 27, 2016 828 ``````Typeclasses Opaque option_dist. `````` Robbert Krebbers committed May 25, 2016 829 830 ``````Arguments optionC : clear implicits. `````` Ralf Jung committed Nov 22, 2016 831 ``````Instance option_fmap_ne {A B : ofeT} n: `````` Robbert Krebbers committed May 28, 2016 832 833 `````` Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B). Proof. intros f f' Hf ?? []; constructor; auto. Qed. `````` Robbert Krebbers committed May 25, 2016 834 835 836 837 838 839 840 841 842 843 844 845 846 847 ``````Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B := CofeMor (fmap f : optionC A → optionC B). Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B). Proof. by intros f f' Hf []; constructor; apply Hf. Qed. Program Definition optionCF (F : cFunctor) : cFunctor := {| cFunctor_car A B := optionC (cFunctor_car F A B); cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg) |}. Next Obligation. by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne. Qed. Next Obligation. intros F A B x. rewrite /= -{2}(option_fmap_id x). `````` 848 `````` apply option_fmap_equiv_ext=>y; apply cFunctor_id. `````` Robbert Krebbers committed May 25, 2016 849 850 851 ``````Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose. `````` 852 `````` apply option_fmap_equiv_ext=>y; apply cFunctor_compose. `````` Robbert Krebbers committed May 25, 2016 853 854 855 856 857 858 859 860 ``````Qed. Instance optionCF_contractive F : cFunctorContractive F → cFunctorContractive (optionCF F). Proof. by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive. Qed. `````` Robbert Krebbers committed Nov 16, 2015 861 ``````(** Later *) `````` Robbert Krebbers committed Feb 10, 2016 862 ``````Inductive later (A : Type) : Type := Next { later_car : A }. `````` Robbert Krebbers committed Dec 21, 2015 863 ``````Add Printing Constructor later. `````` Robbert Krebbers committed Feb 10, 2016 864 ``````Arguments Next {_} _. `````` Robbert Krebbers committed Nov 16, 2015 865 ``````Arguments later_car {_} _. `````` Robbert Krebbers committed Dec 21, 2015 866 `````` `````` Robbert Krebbers committed Nov 16, 2015 867 ``````Section later. `````` Ralf Jung committed Nov 22, 2016 868 `````` Context {A : ofeT}. `````` Robbert Krebbers committed Jan 14, 2016 869 870 `````` Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y. Instance later_dist : Dist (later A) := λ n x y, `````` Robbert Krebbers committed Dec 05, 2016 871 `````` dist_later n (later_car x) (later_car y). `````` Ralf Jung committed Nov 22, 2016 872 `````` Definition later_ofe_mixin : OfeMixin (later A). `````` Robbert Krebbers committed Nov 16, 2015 873 874 `````` Proof. split. `````` Ralf Jung committed Apr 24, 2016 875 876 `````` - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). `````` Robbert Krebbers committed Dec 05, 2016 877 `````` - split; rewrite /dist /later_dist. `````` Robbert Krebbers committed Nov 16, 2015 878 879 `````` + by intros [x]. + by intros [x] [y]. `````` Ralf Jung committed Feb 20, 2016 880 `````` + by intros [x] [y] [z] ??; trans y. `````` Robbert Krebbers committed Dec 05, 2016 881 `````` - intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S. `````` Robbert Krebbers committed Nov 16, 2015 882 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 883 884 885 886 887 `````` Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin. Program Definition later_chain (c : chain laterC) : chain A := {| chain_car n := later_car (c (S n)) |}. Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. ``````