ofe.v 50 KB
Newer Older
1
From iris.algebra Require Export base.
2
Set Default Proof Using "Type".
3
Set Primitive Projections.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5
(** This files defines (a shallow embedding of) the category of OFEs:
6 7 8 9
    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.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
10
    This makes writing such functions much easier. It turns out that it many
11 12 13
    cases, we do not even need non-expansiveness.
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
14 15
(** Unbundeled version *)
Class Dist A := dist : nat  relation A.
16
Instance: Params (@dist) 3 := {}.
17 18
Notation "x ≡{ n }≡ y" := (dist n x y)
  (at level 70, n at next level, format "x  ≡{ n }≡  y").
19 20 21
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
  (at level 70, n at next level, only parsing).

Tej Chajed's avatar
Tej Chajed committed
22 23
Hint Extern 0 (_ {_} _) => reflexivity : core.
Hint Extern 0 (_ {_} _) => symmetry; assumption : core.
24 25
Notation NonExpansive f := ( n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := ( n, Proper (dist n ==> dist n ==> dist n) f).
26

27
Tactic Notation "ofe_subst" ident(x) :=
28
  repeat match goal with
29
  | _ => progress simplify_eq/=
30 31 32
  | 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.
33
Tactic Notation "ofe_subst" :=
34
  repeat match goal with
35
  | _ => progress simplify_eq/=
36 37
  | 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
38
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
39

40 41 42 43 44
Record OfeMixin A `{Equiv A, Dist A} := {
  mixin_equiv_dist x y : x  y   n, x {n} y;
  mixin_dist_equivalence n : Equivalence (dist n);
  mixin_dist_S n x y : x {S n} y  x {n} y
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46

(** Bundeled version *)
47
Structure ofeT := OfeT {
48 49 50
  ofe_car :> Type;
  ofe_equiv : Equiv ofe_car;
  ofe_dist : Dist ofe_car;
51
  ofe_mixin : OfeMixin ofe_car
Robbert Krebbers's avatar
Robbert Krebbers committed
52
}.
53
Arguments OfeT _ {_ _} _.
54 55 56 57 58 59 60
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.
61

62 63 64
(** When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
we need Coq to *infer* the canonical OFE instance of a given type and take the
mixin out of it. This makes sure we do not use two different OFE instances in
65
different places (see for example the constructors [CmraT] and [UcmraT] in the
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
file [cmra.v].)

In order to infer the OFE instance, we use the definition [ofe_mixin_of'] which
is inspired by the [clone] trick in ssreflect. It works as follows, when type
checking [@ofe_mixin_of' A ?Ac id] Coq faces a unification problem:

  ofe_car ?Ac  ~  A

which will resolve [?Ac] to the canonical OFE instance corresponding to [A]. The
definition [@ofe_mixin_of' A ?Ac id] will then provide the corresponding mixin.
Note that type checking of [ofe_mixin_of' A id] will fail when [A] does not have
a canonical OFE instance.

The notation [ofe_mixin_of A] that we define on top of [ofe_mixin_of' A id]
hides the [id] and normalizes the mixin to head normal form. The latter is to
ensure that we do not end up with redundant canonical projections to the mixin,
i.e. them all being of the shape [ofe_mixin_of' A id]. *)
Definition ofe_mixin_of' A {Ac : ofeT} (f : Ac  A) : OfeMixin Ac := ofe_mixin Ac.
Notation ofe_mixin_of A :=
  ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).

87
(** Lifting properties from the mixin *)
88 89
Section ofe_mixin.
  Context {A : ofeT}.
90
  Implicit Types x y : A.
91
  Lemma equiv_dist x y : x  y   n, x {n} y.
92
  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
93
  Global Instance dist_equivalence n : Equivalence (@dist A _ n).
94
  Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
95
  Lemma dist_S n x y : x {S n} y  x {n} y.
96 97
  Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
End ofe_mixin.
98

Tej Chajed's avatar
Tej Chajed committed
99
Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
100

101 102 103 104
(** Discrete OFEs and discrete OFE elements *)
Class Discrete {A : ofeT} (x : A) := discrete y : x {0} y  x  y.
Arguments discrete {_} _ {_} _ _.
Hint Mode Discrete + ! : typeclass_instances.
105
Instance: Params (@Discrete) 1 := {}.
106

107
Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
108 109 110 111 112 113 114 115 116

(** 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 {_} _ _ _ _.

117
Program Definition chain_map {A B : ofeT} (f : A  B)
118
    `{!NonExpansive f} (c : chain A) : chain B :=
119 120 121
  {| chain_car n := f (c n) |}.
Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.

122 123 124 125 126 127
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.
128

129
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A  B) c `(NonExpansive f) :
130 131 132
  compl (chain_map f c)  f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.

133 134 135 136 137 138 139 140
Program Definition chain_const {A : ofeT} (a : A) : chain A :=
  {| chain_car n := a |}.
Next Obligation. by intros A a n i _. Qed.

Lemma compl_chain_const {A : ofeT} `{!Cofe A} (a : A) :
  compl (chain_const a)  a.
Proof. apply equiv_dist=>n. by rewrite conv_compl. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
141
(** General properties *)
142
Section ofe.
143
  Context {A : ofeT}.
144
  Implicit Types x y : A.
145
  Global Instance ofe_equivalence : Equivalence (() : relation A).
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147
  Proof.
    split.
148 149
    - by intros x; rewrite equiv_dist.
    - by intros x y; rewrite !equiv_dist.
150
    - by intros x y z; rewrite !equiv_dist; intros; trans y.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  Qed.
152
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
155 156
    - by trans x1; [|trans y1].
    - by trans x2; [|trans y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  Qed.
158
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163
  Qed.
  Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.
164 165
  Global Instance Discrete_proper : Proper (() ==> iff) (@Discrete A).
  Proof. intros x y Hxy. rewrite /Discrete. by setoid_rewrite Hxy. Qed.
166

Robbert Krebbers's avatar
Robbert Krebbers committed
167
  Lemma dist_le n n' x y : x {n} y  n'  n  x {n'} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  Proof. induction 2; eauto using dist_S. Qed.
169 170
  Lemma dist_le' n n' x y : n'  n  x {n} y  x {n'} y.
  Proof. intros; eauto using dist_le. Qed.
171 172
  Instance ne_proper {B : ofeT} (f : A  B) `{!NonExpansive f} :
    Proper (() ==> ()) f | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
174
  Instance ne_proper_2 {B C : ofeT} (f : A  B  C) `{!NonExpansive2 f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176 177
    Proper (() ==> () ==> ()) f | 100.
  Proof.
     unfold Proper, respectful; setoid_rewrite equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  Qed.
180

181
  Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c {n} c (S n).
182 183
  Proof.
    transitivity (c n); first by apply conv_compl. symmetry.
Ralf Jung's avatar
Ralf Jung committed
184
    apply chain_cauchy. lia.
185
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186

187
  Lemma discrete_iff n (x : A) `{!Discrete x} y : x  y  x {n} y.
188
  Proof.
189
    split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
190
  Qed.
191
  Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x {0} y  x {n} y.
192
  Proof. by rewrite -!discrete_iff. Qed.
193
End ofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
194

195
(** Contractive functions *)
196
Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
197
  match n with 0 => True | S n => x {n} y end.
198
Arguments dist_later _ _ !_ _ _ /.
199

200
Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
201 202
Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.

203 204 205
Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y  dist_later n x y.
Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.

206 207 208 209 210 211 212 213 214 215 216
Lemma dist_later_dist {A : ofeT} n (x y : A) : dist_later (S n) x y  dist n x y.
Proof. done. Qed.

(* We don't actually need this lemma (as our tactics deal with this through
   other means), but technically speaking, this is the reason why
   pre-composing a non-expansive function to a contractive function
   preserves contractivity. *)
Lemma ne_dist_later {A B : ofeT} (f : A  B) :
  NonExpansive f   n, Proper (dist_later n ==> dist_later n) f.
Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.

217
Notation Contractive f := ( n, Proper (dist_later n ==> dist n) f).
218

219
Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
220 221
Proof. by intros n y1 y2. Qed.

222
Section contractive.
223
  Local Set Default Proof Using "Type*".
224 225 226 227
  Context {A B : ofeT} (f : A  B) `{!Contractive f}.
  Implicit Types x y : A.

  Lemma contractive_0 x y : f x {0} f y.
228
  Proof. by apply (_ : Contractive f). Qed.
229
  Lemma contractive_S n x y : x {n} y  f x {S n} f y.
230
  Proof. intros. by apply (_ : Contractive f). Qed.
231

232 233
  Global Instance contractive_ne : NonExpansive f | 100.
  Proof. by intros n x y ?; apply dist_S, contractive_S. Qed.
234 235 236 237
  Global Instance contractive_proper : Proper (() ==> ()) f | 100.
  Proof. apply (ne_proper _). Qed.
End contractive.

238 239
Ltac f_contractive :=
  match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242
  | |- ?f _ {_} ?f _ => simple apply (_ : Proper (dist_later _ ==> _) f)
  | |- ?f _ _ {_} ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> _) f)
  | |- ?f _ _ {_} ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> _) f)
243 244
  end;
  try match goal with
245
  | |- @dist_later ?A _ ?n ?x ?y =>
246
         destruct n as [|n]; [exact I|change (@dist A _ n x y)]
247
  end;
Robbert Krebbers's avatar
Robbert Krebbers committed
248
  try simple apply reflexivity.
249

Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
Ltac solve_contractive :=
  solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
Robbert Krebbers's avatar
Robbert Krebbers committed
252

Robbert Krebbers's avatar
Robbert Krebbers committed
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
(** Limit preserving predicates *)
Class LimitPreserving `{!Cofe A} (P : A  Prop) : Prop :=
  limit_preserving (c : chain A) : ( n, P (c n))  P (compl c).
Hint Mode LimitPreserving + + ! : typeclass_instances.

Section limit_preserving.
  Context `{Cofe A}.
  (* These are not instances as they will never fire automatically...
     but they can still be helpful in proving things to be limit preserving. *)

  Lemma limit_preserving_ext (P Q : A  Prop) :
    ( x, P x  Q x)  LimitPreserving P  LimitPreserving Q.
  Proof. intros HP Hlimit c ?. apply HP, Hlimit=> n; by apply HP. Qed.

  Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P).
  Proof. intros c HP. apply (HP 0). Qed.

270
  Lemma limit_preserving_discrete (P : A  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
    Proper (dist 0 ==> impl) P  LimitPreserving P.
  Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.

  Lemma limit_preserving_and (P1 P2 : A  Prop) :
    LimitPreserving P1  LimitPreserving P2 
    LimitPreserving (λ x, P1 x  P2 x).
  Proof. intros Hlim1 Hlim2 c Hc. split. apply Hlim1, Hc. apply Hlim2, Hc. Qed.

  Lemma limit_preserving_impl (P1 P2 : A  Prop) :
    Proper (dist 0 ==> impl) P1  LimitPreserving P2 
    LimitPreserving (λ x, P1 x  P2 x).
  Proof.
    intros Hlim1 Hlim2 c Hc HP1. apply Hlim2=> n; apply Hc.
    eapply Hlim1, HP1. apply dist_le with n; last lia. apply (conv_compl n).
  Qed.

  Lemma limit_preserving_forall {B} (P : B  A  Prop) :
    ( y, LimitPreserving (P y)) 
    LimitPreserving (λ x,  y, P y x).
  Proof. intros Hlim c Hc y. by apply Hlim. Qed.
End limit_preserving.

Robbert Krebbers's avatar
Robbert Krebbers committed
293
(** Fixpoint *)
294
Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A  A)
295
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Next Obligation.
297
  intros A ? f ? n.
Ralf Jung's avatar
Ralf Jung committed
298
  induction n as [|n IH]=> -[|i] //= ?; try lia.
299
  - apply (contractive_0 f).
Ralf Jung's avatar
Ralf Jung committed
300
  - apply (contractive_S f), IH; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Qed.
302

303
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A  A)
304
  `{!Contractive f} : A := compl (fixpoint_chain f).
305
Definition fixpoint_aux : seal (@fixpoint_def). by eexists. Qed.
306 307
Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
308 309

Section fixpoint.
310
  Context `{Cofe A, Inhabited A} (f : A  A) `{!Contractive f}.
311

312
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  Proof.
314 315
    apply equiv_dist=>n.
    rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
316
    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
  Qed.
318 319 320

  Lemma fixpoint_unique (x : A) : x  f x  x  fixpoint f.
  Proof.
321 322 323
    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.
324 325
  Qed.

326
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
327
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  Proof.
329
    intros Hfg. rewrite fixpoint_eq /fixpoint_def
Robbert Krebbers's avatar
Robbert Krebbers committed
330
      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
331 332
    induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
    rewrite Hfg; apply contractive_S, IH; auto using dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
  Qed.
334 335
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
337 338

  Lemma fixpoint_ind (P : A  Prop) :
339
    Proper (() ==> impl) P 
340
    ( x, P x)  ( x, P x  P (f x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
341
    LimitPreserving P 
342 343 344 345
    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).
Robbert Krebbers's avatar
Robbert Krebbers committed
346
    { intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
Ralf Jung's avatar
Ralf Jung committed
347
        eauto using contractive_0, contractive_S with lia. }
348
    set (fp2 := compl {| chain_cauchy := Hcauch |}).
Robbert Krebbers's avatar
Robbert Krebbers committed
349 350 351 352
    assert (f fp2  fp2).
    { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
      induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
    rewrite -(fixpoint_unique fp2) //.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
    apply Hlim=> n /=. by apply Nat_iter_ind.
354
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
355 356
End fixpoint.

Robbert Krebbers's avatar
Robbert Krebbers committed
357

358 359 360
(** Fixpoint of f when f^k is contractive. **)
Definition fixpointK `{Cofe A, Inhabited A} k (f : A  A)
  `{!Contractive (Nat.iter k f)} := fixpoint (Nat.iter k f).
361

362
Section fixpointK.
363
  Local Set Default Proof Using "Type*".
364
  Context `{Cofe A, Inhabited A} (f : A  A) (k : nat).
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387
  Context {f_contractive : Contractive (Nat.iter k f)} {f_ne : NonExpansive f}.
  (* Note than f_ne is crucial here:  there are functions f such that f^2 is contractive,
     but f is not non-expansive.
     Consider for example f: SPred → SPred (where SPred is "downclosed sets of natural numbers").
     Define f (using informative excluded middle) as follows:
     f(N) = N  (where N is the set of all natural numbers)
     f({0, ..., n}) = {0, ... n-1}  if n is even (so n-1 is at least -1, in which case we return the empty set)
     f({0, ..., n}) = {0, ..., n+2} if n is odd
     In other words, if we consider elements of SPred as ordinals, then we decreaste odd finite
     ordinals by 1 and increase even finite ordinals by 2.
     f is not non-expansive:  Consider f({0}) = ∅ and f({0,1}) = f({0,1,2,3}).
     The arguments are clearly 0-equal, but the results are not.

     Now consider g := f^2. We have
     g(N) = N
     g({0, ..., n}) = {0, ... n+1}  if n is even
     g({0, ..., n}) = {0, ..., n+4} if n is odd
     g is contractive.  All outputs contain 0, so they are all 0-equal.
     Now consider two n-equal inputs. We have to show that the outputs are n+1-equal.
     Either they both do not contain n in which case they have to be fully equal and
     hence so are the results.  Or else they both contain n, so the results will
     both contain n+1, so the results are n+1-equal.
   *)
388 389

  Let f_proper : Proper (() ==> ()) f := ne_proper f.
390
  Local Existing Instance f_proper.
391

392
  Lemma fixpointK_unfold : fixpointK k f  f (fixpointK k f).
393
  Proof.
394 395
    symmetry. rewrite /fixpointK. apply fixpoint_unique.
    by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold.
396 397
  Qed.

398
  Lemma fixpointK_unique (x : A) : x  f x  x  fixpointK k f.
399
  Proof.
400 401
    intros Hf. apply fixpoint_unique. clear f_contractive.
    induction k as [|k' IH]=> //=. by rewrite -IH.
402 403
  Qed.

404
  Section fixpointK_ne.
405
    Context (g : A  A) `{g_contractive : !Contractive (Nat.iter k g)}.
406
    Context {g_ne : NonExpansive g}.
407

408
    Lemma fixpointK_ne n : ( z, f z {n} g z)  fixpointK k f {n} fixpointK k g.
409
    Proof.
410 411 412
      rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z.
      clear f_contractive g_contractive.
      induction k as [|k' IH]=> //=. by rewrite IH Hfg.
413 414
    Qed.

415 416 417
    Lemma fixpointK_proper : ( z, f z  g z)  fixpointK k f  fixpointK k g.
    Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpointK_ne. Qed.
  End fixpointK_ne.
Ralf Jung's avatar
Ralf Jung committed
418 419 420 421

  Lemma fixpointK_ind (P : A  Prop) :
    Proper (() ==> impl) P 
    ( x, P x)  ( x, P x  P (f x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
422
    LimitPreserving P 
Ralf Jung's avatar
Ralf Jung committed
423 424
    P (fixpointK k f).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
    intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
    intros; apply Nat_iter_ind; auto.
Ralf Jung's avatar
Ralf Jung committed
427
  Qed.
428
End fixpointK.
429

Robbert Krebbers's avatar
Robbert Krebbers committed
430
(** Mutual fixpoints *)
Ralf Jung's avatar
Ralf Jung committed
431
Section fixpointAB.
432 433
  Local Unset Default Proof Using.

Robbert Krebbers's avatar
Robbert Krebbers committed
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474
  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.
Ralf Jung's avatar
Ralf Jung committed
475
End fixpointAB.
Robbert Krebbers's avatar
Robbert Krebbers committed
476

Ralf Jung's avatar
Ralf Jung committed
477
Section fixpointAB_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508
  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.
Ralf Jung's avatar
Ralf Jung committed
509
End fixpointAB_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
510

511
(** Non-expansive function space *)
512 513
Record ofe_mor (A B : ofeT) : Type := CofeMor {
  ofe_mor_car :> A  B;
514
  ofe_mor_ne : NonExpansive ofe_mor_car
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516
}.
Arguments CofeMor {_ _} _ {_}.
517 518
Add Printing Constructor ofe_mor.
Existing Instance ofe_mor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
519

520 521 522 523
Notation "'λne' x .. y , t" :=
  (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
  (at level 200, x binder, y binder, right associativity).

524 525 526 527 528 529 530
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).
531 532
  Proof.
    split.
533
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
Robbert Krebbers's avatar
Robbert Krebbers committed
534
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
535
    - intros n; split.
536 537
      + by intros f x.
      + by intros f g ? x.
538
      + by intros f g h ?? x; trans (g x).
539
    - by intros n f g ? x; apply dist_S.
540
  Qed.
541 542 543 544 545 546 547 548 549 550 551
  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.
Jacques-Henri Jourdan's avatar
Typo  
Jacques-Henri Jourdan committed
552
  Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morC :=
553 554 555 556 557
    {| compl := ofe_mor_compl |}.
  Next Obligation.
    intros ? n c x; simpl.
    by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
  Qed.
558

559 560 561
  Global Instance ofe_mor_car_ne :
    NonExpansive2 (@ofe_mor_car A B).
  Proof. intros n f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
562 563 564
  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.
565
  Proof. done. Qed.
566
End ofe_mor.
567

568
Arguments ofe_morC : clear implicits.
569
Notation "A -n> B" :=
570 571
  (ofe_morC A B) (at level 99, B at level 200, right associativity).
Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
572
  Inhabited (A -n> B) := populate (λne _, inhabitant).
Robbert Krebbers's avatar
Robbert Krebbers committed
573

574
(** Identity and composition and constant function *)
Robbert Krebbers's avatar
Robbert Krebbers committed
575
Definition cid {A} : A -n> A := CofeMor id.
576
Instance: Params (@cid) 1 := {}.
577
Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x).
578
Instance: Params (@cconst) 2 := {}.
579

Robbert Krebbers's avatar
Robbert Krebbers committed
580 581
Definition ccompose {A B C}
  (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f  g).
582
Instance: Params (@ccompose) 3 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Infix "◎" := ccompose (at level 40, left associativity).
584 585 586
Global Instance ccompose_ne {A B C} :
  NonExpansive2 (@ccompose A B C).
Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
587

Ralf Jung's avatar
Ralf Jung committed
588
(* Function space maps *)
589
Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
Ralf Jung's avatar
Ralf Jung committed
590
  (h : A -n> B) : A' -n> B' := g  h  f.
591 592
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').
593
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Ralf Jung's avatar
Ralf Jung committed
594

595 596
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).
597 598
Instance ofe_morC_map_ne {A A' B B'} :
  NonExpansive2 (@ofe_morC_map A A' B B').
Ralf Jung's avatar
Ralf Jung committed
599
Proof.
600
  intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
601
  by repeat apply ccompose_ne.
Ralf Jung's avatar
Ralf Jung committed
602 603
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
604
(** unit *)
605 606
Section unit.
  Instance unit_dist : Dist unit := λ _ _ _, True.
607
  Definition unit_ofe_mixin : OfeMixin unit.
608
  Proof. by repeat split; try exists 0. Qed.
609
  Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
610

611 612
  Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
  Next Obligation. by repeat split; try exists 0. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
613

614
  Global Instance unit_ofe_discrete : OfeDiscrete unitC.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
  Proof. done. Qed.
616
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
617 618

(** Product *)
619
Section product.
620
  Context {A B : ofeT}.
621 622 623

  Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
  Global Instance pair_ne :
624 625 626
    NonExpansive2 (@pair A B) := _.
  Global Instance fst_ne : NonExpansive (@fst A B) := _.
  Global Instance snd_ne : NonExpansive (@snd A B) := _.
627
  Definition prod_ofe_mixin : OfeMixin (A * B).
628 629
  Proof.
    split.
630
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
631
      rewrite !equiv_dist; naive_solver.
632 633
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
634
  Qed.
635 636 637 638 639 640 641 642 643
  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.

644 645 646
  Global Instance prod_discrete (x : A * B) :
    Discrete (x.1)  Discrete (x.2)  Discrete x.
  Proof. by intros ???[??]; split; apply (discrete _). Qed.
647 648
  Global Instance prod_ofe_discrete :
    OfeDiscrete A  OfeDiscrete B  OfeDiscrete prodC.
649
  Proof. intros ?? [??]; apply _. Qed.
650 651 652 653 654
End product.

Arguments prodC : clear implicits.
Typeclasses Opaque prod_dist.

655
Instance prod_map_ne {A A' B B' : ofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
656 657 658 659 660
  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).
661 662 663
Instance prodC_map_ne {A A' B B'} :
  NonExpansive2 (@prodC_map A A' B B').
Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
664

665 666
(** Functors *)
Structure cFunctor := CFunctor {
667
  cFunctor_car : ofeT  ofeT  ofeT;
668 669
  cFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
670 671
  cFunctor_ne {A1 A2 B1 B2} :
    NonExpansive (@cFunctor_map A1 A2 B1 B2);
672
  cFunctor_id {A B : ofeT} (x : cFunctor_car A B) :
673 674 675 676 677
    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 (fg, g'f') x  cFunctor_map (g,g') (cFunctor_map (f,f') x)
}.
678
Existing Instance cFunctor_ne.
679
Instance: Params (@cFunctor_map) 5 := {}.
680

681 682 683
Delimit Scope cFunctor_scope with CF.
Bind Scope cFunctor_scope with cFunctor.

684 685 686
Class cFunctorContractive (F : cFunctor) :=
  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).

687
Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
688 689
Coercion cFunctor_diag : cFunctor >-> Funclass.

690
Program Definition constCF (B : ofeT) : cFunctor :=
691 692
  {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
693
Coercion constCF : ofeT >-> cFunctor.
694

695
Instance constCF_contractive B : cFunctorContractive (constCF B).
696
Proof. rewrite /cFunctorContractive; apply _. Qed.
697 698 699 700

Program Definition idCF : cFunctor :=
  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
Solve Obligations with done.
701
Notation "∙" := idCF : cFunctor_scope.
702

703 704 705 706 707
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)
|}.
708 709 710
Next Obligation.
  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
Qed.
711 712 713 714 715
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.
716
Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
717

718 719 720 721 722 723 724 725
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.

726
Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
727
  cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
Ralf Jung's avatar
Ralf Jung committed
728
  cFunctor_map A1 A2 B1 B2 fg :=
729
    ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
Ralf Jung's avatar
Ralf Jung committed
730
|}.
731 732
Next Obligation.
  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
733
  apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
734
Qed.
Ralf Jung's avatar
Ralf Jung committed
735
Next Obligation.
736 737
  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
  apply (ne_proper f). apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
738 739
Qed.
Next Obligation.
740 741
  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's avatar
Ralf Jung committed
742
Qed.
743
Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
Ralf Jung's avatar
Ralf Jung committed
744

745
Instance ofe_morCF_contractive F1 F2 :
746
  cFunctorContractive F1  cFunctorContractive F2 
747
  cFunctorContractive (ofe_morCF F1 F2).
748 749