ofe.v 69.2 KB
Newer Older
1
From iris.prelude Require Export prelude.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.prelude Require Import options.
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.
*)

Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
14
(** Unbundled version *)
Robbert Krebbers's avatar
Robbert Krebbers committed
15
Class Dist A := dist : nat  relation A.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
16
Global Hint Mode Dist ! : typeclass_instances.
17
Global Instance: Params (@dist) 3 := {}.
18
19
Notation "x ≡{ n }≡ y" := (dist n x y)
  (at level 70, n at next level, format "x  ≡{ n }≡  y").
20
21
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
  (at level 70, n at next level, only parsing).
22
23
24
25
Notation "(≡{ n }≡)" := (dist n) (only parsing).
Notation "(≡{ n }@{ A }≡)" := (dist (A:=A) n) (only parsing).
Notation "( x ≡{ n }≡.)" := (dist n x) (only parsing).
Notation "(.≡{ n }≡ y )" := (λ x, x {n} y) (only parsing).
26

27
28
Global Hint Extern 0 (_ {_} _) => reflexivity : core.
Global Hint Extern 0 (_ {_} _) => symmetry; assumption : core.
29
30
Notation NonExpansive f := ( n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := ( n, Proper (dist n ==> dist n ==> dist n) f).
Ralf Jung's avatar
Ralf Jung committed
31
32
33
34
Notation NonExpansive3 f :=
  ( n, Proper (dist n ==> dist n ==> dist n ==> dist n) f).
Notation NonExpansive4 f :=
  ( n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f).
35

36
Tactic Notation "ofe_subst" ident(x) :=
37
  repeat match goal with
38
  | _ => progress simplify_eq/=
39
40
41
  | 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.
42
Tactic Notation "ofe_subst" :=
43
  repeat match goal with
44
  | _ => progress simplify_eq/=
45
46
  | 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
47
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

49
Record OfeMixin A `{Equiv A, Dist A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
52
  mixin_equiv_dist (x y : A) : x  y   n, x {n} y;
  mixin_dist_equivalence n : Equivalence (@dist A _ n);
  mixin_dist_S n (x y : A) : x {S n} y  x {n} y
53
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
54

Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
55
(** Bundled version *)
56
Structure ofe := Ofe {
57
58
59
  ofe_car :> Type;
  ofe_equiv : Equiv ofe_car;
  ofe_dist : Dist ofe_car;
60
  ofe_mixin : OfeMixin ofe_car
Robbert Krebbers's avatar
Robbert Krebbers committed
61
}.
62
63
Global Arguments Ofe _ {_ _} _.
Add Printing Constructor ofe.
64
65
66
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.
Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
Ralf Jung's avatar
Ralf Jung committed
67
68
69
70
Global Arguments ofe_car : simpl never.
Global Arguments ofe_equiv : simpl never.
Global Arguments ofe_dist : simpl never.
Global Arguments ofe_mixin : simpl never.
71

72
73
74
(** 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
75
different places (see for example the constructors [Cmra] and [Ucmra] in the
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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]. *)
93
Definition ofe_mixin_of' A {Ac : ofe} (f : Ac  A) : OfeMixin Ac := ofe_mixin Ac.
94
95
96
Notation ofe_mixin_of A :=
  ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).

97
(** Lifting properties from the mixin *)
98
Section ofe_mixin.
99
  Context {A : ofe}.
100
  Implicit Types x y : A.
101
  Lemma equiv_dist x y : x  y   n, x {n} y.
102
  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
103
  Global Instance dist_equivalence n : Equivalence (@dist A _ n).
104
  Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
105
  Lemma dist_S n x y : x {S n} y  x {n} y.
106
107
  Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
End ofe_mixin.
108

109
Global Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
110

111
(** Discrete OFEs and discrete OFE elements *)
112
Class Discrete {A : ofe} (x : A) := discrete y : x {0} y  x  y.
Ralf Jung's avatar
Ralf Jung committed
113
Global Arguments discrete {_} _ {_} _ _.
114
Global Hint Mode Discrete + ! : typeclass_instances.
115
Global Instance: Params (@Discrete) 1 := {}.
116

117
Class OfeDiscrete (A : ofe) := ofe_discrete_discrete (x : A) :> Discrete x.
118
Global Hint Mode OfeDiscrete ! : typeclass_instances.
119
120

(** OFEs with a completion *)
121
Record chain (A : ofe) := {
122
123
124
  chain_car :> nat  A;
  chain_cauchy n i : n  i  chain_car i {n} chain_car n
}.
Ralf Jung's avatar
Ralf Jung committed
125
126
Global Arguments chain_car {_} _ _.
Global Arguments chain_cauchy {_} _ _ _ _.
127

128
Program Definition chain_map {A B : ofe} (f : A  B)
129
    `{!NonExpansive f} (c : chain A) : chain B :=
130
131
132
  {| chain_car n := f (c n) |}.
Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.

133
Notation Compl A := (chain A%type  A).
134
Class Cofe (A : ofe) := {
135
136
137
  compl : Compl A;
  conv_compl n c : compl c {n} c n;
}.
Ralf Jung's avatar
Ralf Jung committed
138
Global Arguments compl : simpl never.
139
Global Hint Mode Cofe ! : typeclass_instances.
140

141
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A  B) c `(NonExpansive f) :
142
143
144
  compl (chain_map f c)  f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.

145
Program Definition chain_const {A : ofe} (a : A) : chain A :=
146
147
148
  {| chain_car n := a |}.
Next Obligation. by intros A a n i _. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
153
(** General properties *)
154
Section ofe.
155
  Context {A : ofe}.
156
  Implicit Types x y : A.
157
  Global Instance ofe_equivalence : Equivalence (() : relation A).
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
  Proof.
    split.
160
161
    - by intros x; rewrite equiv_dist.
    - by intros x y; rewrite !equiv_dist.
162
    - by intros x y z; rewrite !equiv_dist; intros; trans y.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  Qed.
164
  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
  Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
167
168
    - by trans x1; [|trans y1].
    - by trans x2; [|trans y2].
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  Qed.
170
  Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
173
174
175
  Qed.
  Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.
176
177
  Global Instance Discrete_proper : Proper (() ==> iff) (@Discrete A).
  Proof. intros x y Hxy. rewrite /Discrete. by setoid_rewrite Hxy. Qed.
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179
  Lemma dist_le n n' x y : x {n} y  n'  n  x {n'} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  Proof. induction 2; eauto using dist_S. Qed.
181
182
  Lemma dist_le' n n' x y : n'  n  x {n} y  x {n'} y.
  Proof. intros; eauto using dist_le. Qed.
183
184
  (** [ne_proper] and [ne_proper_2] are not instances to improve efficiency of
  type class search during setoid rewriting.
185
  Local Instances of [NonExpansive{,2}] are hence accompanied by instances of
186
  [Proper] built using these lemmas. *)
187
  Lemma ne_proper {B : ofe} (f : A  B) `{!NonExpansive f} :
188
    Proper (() ==> ()) f.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
190
  Lemma ne_proper_2 {B C : ofe} (f : A  B  C) `{!NonExpansive2 f} :
191
    Proper (() ==> () ==> ()) f.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
  Proof.
     unfold Proper, respectful; setoid_rewrite equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Robbert Krebbers's avatar
Robbert Krebbers committed
195
  Qed.
196

197
  Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c {n} c (S n).
198
199
  Proof.
    transitivity (c n); first by apply conv_compl. symmetry.
Ralf Jung's avatar
Ralf Jung committed
200
    apply chain_cauchy. lia.
201
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
202

203
  Lemma discrete_iff n (x : A) `{!Discrete x} y : x  y  x {n} y.
204
  Proof.
205
    split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
206
  Qed.
207
  Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x {0} y  x {n} y.
208
  Proof. by rewrite -!discrete_iff. Qed.
209
End ofe.
Robbert Krebbers's avatar
Robbert Krebbers committed
210

211
(** Contractive functions *)
212
Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
213
  match n with 0 => True | S n => x {n} y end.
Ralf Jung's avatar
Ralf Jung committed
214
Global Arguments dist_later _ _ !_ _ _ /.
215

216
Global Instance dist_later_equivalence (A : ofe) n : Equivalence (@dist_later A _ n).
217
Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
218

219
Lemma dist_dist_later {A : ofe} n (x y : A) : dist n x y  dist_later n x y.
220
221
Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.

222
Lemma dist_later_dist {A : ofe} n (x y : A) : dist_later (S n) x y  dist n x y.
223
224
225
226
227
228
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. *)
229
Lemma ne_dist_later {A B : ofe} (f : A  B) :
230
231
232
  NonExpansive f   n, Proper (dist_later n ==> dist_later n) f.
Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.

233
Notation Contractive f := ( n, Proper (dist_later n ==> dist n) f).
234

235
Global Instance const_contractive {A B : ofe} (x : A) : Contractive (@const A B x).
236
237
Proof. by intros n y1 y2. Qed.

238
Section contractive.
239
  Local Set Default Proof Using "Type*".
240
  Context {A B : ofe} (f : A  B) `{!Contractive f}.
241
242
243
  Implicit Types x y : A.

  Lemma contractive_0 x y : f x {0} f y.
244
  Proof. by apply (_ : Contractive f). Qed.
245
  Lemma contractive_S n x y : x {n} y  f x {S n} f y.
246
  Proof. intros. by apply (_ : Contractive f). Qed.
247

248
249
  Global Instance contractive_ne : NonExpansive f | 100.
  Proof. by intros n x y ?; apply dist_S, contractive_S. Qed.
250
251
252
253
  Global Instance contractive_proper : Proper (() ==> ()) f | 100.
  Proof. apply (ne_proper _). Qed.
End contractive.

254
255
Ltac f_contractive :=
  match goal with
256
257
258
  | |- ?f _ {_} ?f _ => simple apply (_ : Proper (dist_later _ ==> dist _) f)
  | |- ?f _ _ {_} ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> dist _) f)
  | |- ?f _ _ {_} ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> dist _) f)
259
260
  end;
  try match goal with
261
  | |- @dist_later ?A _ ?n ?x ?y =>
262
         destruct n as [|n]; [exact I|change (@dist A _ n x y)]
263
  end;
264
265
266
  (* Only try reflexivity if the terms are syntactically equal. This avoids
     very expensive failing unification. *)
  try match goal with  |- _ ?x ?x => simple apply reflexivity end.
267

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

Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
273
(** Limit preserving predicates *)
Class LimitPreserving `{!Cofe A} (P : A  Prop) : Prop :=
  limit_preserving (c : chain A) : ( n, P (c n))  P (compl c).
274
Global Hint Mode LimitPreserving + + ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
276
277
278
279
280
281
282
283
284

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.

Robbert Krebbers's avatar
Robbert Krebbers committed
285
  Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _ : A, P).
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
  Proof. intros c HP. apply (HP 0). Qed.

288
  Lemma limit_preserving_discrete (P : A  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
289
290
291
292
293
294
    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).
295
296
  Proof.
    intros Hlim1 Hlim2 c Hc.
Tej Chajed's avatar
Tej Chajed committed
297
298
299
    split.
    - apply Hlim1, Hc.
    - apply Hlim2, Hc.
300
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
303
304
305
306
307
308
309
310
311
312
313

  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.
314
315
316
317
318
319
320

  Lemma limit_preserving_equiv `{!Cofe B} (f g : A  B) :
    NonExpansive f  NonExpansive g  LimitPreserving (λ x, f x  g x).
  Proof.
    intros Hf Hg c Hc. apply equiv_dist=> n.
    by rewrite -!compl_chain_map !conv_compl /= Hc.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
End limit_preserving.

Robbert Krebbers's avatar
Robbert Krebbers committed
323
(** Fixpoint *)
324
Program Definition fixpoint_chain {A : ofe} `{Inhabited A} (f : A  A)
325
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Next Obligation.
327
  intros A ? f ? n.
Ralf Jung's avatar
Ralf Jung committed
328
  induction n as [|n IH]=> -[|i] //= ?; try lia.
329
  - apply (contractive_0 f).
Ralf Jung's avatar
Ralf Jung committed
330
  - apply (contractive_S f), IH; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Qed.
332

333
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A  A)
334
  `{!Contractive f} : A := compl (fixpoint_chain f).
335
Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Ralf Jung's avatar
Ralf Jung committed
336
Definition fixpoint := fixpoint_aux.(unseal).
Ralf Jung's avatar
Ralf Jung committed
337
Global Arguments fixpoint {A _ _} f {_}.
338
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
339
340

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

343
  Lemma fixpoint_unfold : fixpoint f  f (fixpoint f).
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  Proof.
345
346
    apply equiv_dist=>n.
    rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
347
    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
  Qed.
349
350
351

  Lemma fixpoint_unique (x : A) : x  f x  x  fixpoint f.
  Proof.
352
353
354
    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.
355
356
  Qed.

357
  Lemma fixpoint_ne (g : A  A) `{!Contractive g} n :
358
    ( z, f z {n} g z)  fixpoint f {n} fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
359
  Proof.
360
    intros Hfg. rewrite fixpoint_eq /fixpoint_def
Robbert Krebbers's avatar
Robbert Krebbers committed
361
      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
362
363
    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
364
  Qed.
365
366
  Lemma fixpoint_proper (g : A  A) `{!Contractive g} :
    ( x, f x  g x)  fixpoint f  fixpoint g.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
368
369

  Lemma fixpoint_ind (P : A  Prop) :
370
    Proper (() ==> impl) P 
371
    ( x, P x)  ( x, P x  P (f x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
372
    LimitPreserving P 
373
374
375
376
    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
377
    { intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
Ralf Jung's avatar
Ralf Jung committed
378
        eauto using contractive_0, contractive_S with lia. }
379
    set (fp2 := compl {| chain_cauchy := Hcauch |}).
Robbert Krebbers's avatar
Robbert Krebbers committed
380
381
382
383
    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
384
    apply Hlim=> n /=. by apply Nat_iter_ind.
385
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
387
End fixpoint.

Robbert Krebbers's avatar
Robbert Krebbers committed
388

389
390
391
(** 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).
392

393
Section fixpointK.
394
  Local Set Default Proof Using "Type*".
395
  Context `{Cofe A, Inhabited A} (f : A  A) (k : nat).
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
  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.
   *)
419
420

  Let f_proper : Proper (() ==> ()) f := ne_proper f.
421
  Local Existing Instance f_proper.
422

423
  Lemma fixpointK_unfold : fixpointK k f  f (fixpointK k f).
424
  Proof.
425
426
    symmetry. rewrite /fixpointK. apply fixpoint_unique.
    by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold.
427
428
  Qed.

429
  Lemma fixpointK_unique (x : A) : x  f x  x  fixpointK k f.
430
  Proof.
431
432
    intros Hf. apply fixpoint_unique. clear f_contractive.
    induction k as [|k' IH]=> //=. by rewrite -IH.
433
434
  Qed.

435
  Section fixpointK_ne.
436
    Context (g : A  A) `{g_contractive : !Contractive (Nat.iter k g)}.
437
    Context {g_ne : NonExpansive g}.
438

439
    Lemma fixpointK_ne n : ( z, f z {n} g z)  fixpointK k f {n} fixpointK k g.
440
    Proof.
441
442
443
      rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z.
      clear f_contractive g_contractive.
      induction k as [|k' IH]=> //=. by rewrite IH Hfg.
444
445
    Qed.

446
447
448
    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
449
450
451
452

  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
453
    LimitPreserving P 
Ralf Jung's avatar
Ralf Jung committed
454
455
    P (fixpointK k f).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
    intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
    intros; apply Nat_iter_ind; auto.
Ralf Jung's avatar
Ralf Jung committed
458
  Qed.
459
End fixpointK.
460

Robbert Krebbers's avatar
Robbert Krebbers committed
461
(** Mutual fixpoints *)
Ralf Jung's avatar
Ralf Jung committed
462
Section fixpointAB.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
  Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
  Context (fA : A  B  A).
  Context (fB : A  B  B).
Ralf Jung's avatar
Ralf Jung committed
466
467
  Context {fA_contractive :  n, Proper (dist_later n ==> dist n ==> dist n) fA}.
  Context {fB_contractive :  n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
Robbert Krebbers's avatar
Robbert Krebbers committed
468
469
470
471
472
473
474
475
476
477

  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.
Ralf Jung's avatar
Ralf Jung committed
478
  Proof using fA_contractive. solve_contractive. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
480
481
482
483
484
485
486
487

  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.

488
  Local Instance: Proper (() ==> () ==> ()) fA.
Ralf Jung's avatar
Ralf Jung committed
489
  Proof using fA_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
490
491
    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
  Qed.
492
  Local Instance: Proper (() ==> () ==> ()) fB.
Ralf Jung's avatar
Ralf Jung committed
493
  Proof using fB_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
494
495
496
497
498
499
500
501
502
503
    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
504
End fixpointAB.
Robbert Krebbers's avatar
Robbert Krebbers committed
505

Ralf Jung's avatar
Ralf Jung committed
506
Section fixpointAB_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
  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
538
End fixpointAB_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
539

540
(** Non-expansive function space *)
541
Record ofe_mor (A B : ofe) : Type := OfeMor {
542
  ofe_mor_car :> A  B;
543
  ofe_mor_ne : NonExpansive ofe_mor_car
Robbert Krebbers's avatar
Robbert Krebbers committed
544
}.
Ralf Jung's avatar
Ralf Jung committed
545
Global Arguments OfeMor {_ _} _ {_}.
546
Add Printing Constructor ofe_mor.
Ralf Jung's avatar
Ralf Jung committed
547
Global Existing Instance ofe_mor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
548

549
Notation "'λne' x .. y , t" :=
550
  (@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t) _) ..) _)
551
552
  (at level 200, x binder, y binder, right associativity).

553
Section ofe_mor.
554
  Context {A B : ofe}.
555
556
  Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper (() ==> ()) f.
  Proof. apply ne_proper, ofe_mor_ne. Qed.
557
558
  Local Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g,  x, f x  g x.
  Local Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g,  x, f x {n} g x.
559
  Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
560
561
  Proof.
    split.
562
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
Robbert Krebbers's avatar
Robbert Krebbers committed
563
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
564
    - intros n; split.
565
566
      + by intros f x.
      + by intros f g ? x.
567
      + by intros f g h ?? x; trans (g x).
568
    - by intros n f g ? x; apply dist_S.
569
  Qed.
570
  Canonical Structure ofe_morO := Ofe (ofe_mor A B) ofe_mor_ofe_mixin.
571

572
  Program Definition ofe_mor_chain (c : chain ofe_morO)
573
574
    (x : A) : chain B := {| chain_car n := c n x |}.
  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
575
  Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morO := λ c,
576
577
578
579
580
    {| 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.
581
  Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morO :=
582
583
584
585
586
    {| compl := ofe_mor_compl |}.
  Next Obligation.
    intros ? n c x; simpl.
    by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
  Qed.
587

588
589
590
  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.
591
592
593
  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.
594
  Proof. done. Qed.
595
End ofe_mor.
596

Ralf Jung's avatar
Ralf Jung committed
597
Global Arguments ofe_morO : clear implicits.
598
Notation "A -n> B" :=
599
  (ofe_morO A B) (at level 99, B at level 200, right associativity).
600
Global Instance ofe_mor_inhabited {A B : ofe} `{Inhabited B} :
601
  Inhabited (A -n> B) := populate (λne _, inhabitant).
Robbert Krebbers's avatar
Robbert Krebbers committed
602

603
(** Identity and composition and constant function *)
604
Definition cid {A} : A -n> A := OfeMor id.
605
Global Instance: Params (@cid) 1 := {}.
606
Definition cconst {A B : ofe} (x : B) : A -n> B := OfeMor (const x).
607
Global Instance: Params (@cconst) 2 := {}.
608

Robbert Krebbers's avatar
Robbert Krebbers committed
609
Definition ccompose {A B C}
610
  (f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f  g).
611
Global Instance: Params (@ccompose) 3 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
Infix "◎" := ccompose (at level 40, left associativity).
613
614
615
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.
616
617
618
Global Instance ccompose_proper {A B C} :
  Proper (() ==> () ==> ()) (@ccompose A B C).
Proof. apply ne_proper_2; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
619

Ralf Jung's avatar
Ralf Jung committed
620
(* Function space maps *)
621
Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
Ralf Jung's avatar
Ralf Jung committed
622
  (h : A -n> B) : A' -n> B' := g  h  f.
Ralf Jung's avatar
Ralf Jung committed
623
624
625
Global Instance ofe_mor_map_ne {A A' B B'} :
  NonExpansive3 (@ofe_mor_map A A' B B').
Proof. intros n ??? ??? ???. by repeat apply ccompose_ne. Qed.
Ralf Jung's avatar
Ralf Jung committed
626

627
628
Definition ofe_morO_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
  (A -n> B) -n> (A' -n>  B') := OfeMor (ofe_mor_map f g).
629
Global Instance ofe_morO_map_ne {A A' B B'} :
630
  NonExpansive2 (@ofe_morO_map A A' B B').
Ralf Jung's avatar
Ralf Jung committed
631
Proof.
632
  intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
633
  by repeat apply ccompose_ne.
Ralf Jung's avatar
Ralf Jung committed
634
635
Qed.

636
(** * Unit type *)
637
Section unit.
638
  Local Instance unit_dist : Dist unit := λ _ _ _, True.
639
  Definition unit_ofe_mixin : OfeMixin unit.
640
  Proof. by repeat split; try exists 0. Qed.
641
  Canonical Structure unitO : ofe := Ofe unit unit_ofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
642

643
  Global Program Instance unit_cofe : Cofe unitO := { compl x := () }.
644
  Next Obligation. by repeat split; try exists 0. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
645

646
  Global Instance unit_ofe_discrete : OfeDiscrete unitO.
Robbert Krebbers's avatar
Robbert Krebbers committed
647
  Proof. done. Qed.
648
End unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
649

650
(** * Empty type *)
651
Section empty.
652
  Local Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
653
654
  Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
  Proof. by repeat split; try exists 0. Qed.
655
  Canonical Structure Empty_setO : ofe := Ofe Empty_set Empty_set_ofe_mixin.
656
657
658
659
660
661
662
663

  Global Program Instance Empty_set_cofe : Cofe Empty_setO := { compl x := x 0 }.
  Next Obligation. by repeat split; try exists 0. Qed.

  Global Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
  Proof. done. Qed.
End empty.

664
(** * Product type *)
665
Section product.
666
  Context {A B : ofe}.
667

668
  Local Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
669

670
  Definition prod_ofe_mixin : OfeMixin (A * B).
671
672
  Proof.
    split.
673
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
674
      rewrite !equiv_dist; naive_solver.
675
676
    - apply _.
    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
677
  Qed.
678
  Canonical Structure prodO : ofe := Ofe (A * B) prod_ofe_mixin.
679

680
  Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
681
682
    { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
  Next Obligation.
683
684
685
    intros ?? n c; split.
    - apply (conv_compl n (chain_map fst