base.v 51.1 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
2
3
4
5
6
(* This file is distributed under the terms of the BSD license. *)
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, collections, and various other data
structures. *)
7

8
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
9
Set Default Proof Using "Type".
10
11
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
12

13
14
15
16
17
18
19
20
(** Enable implicit generalization. *)
(* This option enables implicit generalization in arguments of the form
   `{...} (i.e., anonymous arguments).  Unfortunately, it also enables
   implicit generalization in `Instance`.  We think that the fact taht both
   behaviors are coupled together is a [bug in
   Coq](https://github.com/coq/coq/issues/6030). *)
Global Generalizable All Variables.

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
(** * Tweak program *)
(** 1. Since we only use Program to solve logical side-conditions, they should
always be made Opaque, otherwise we end up with performance problems due to
Coq blindly unfolding them.

Note that in most cases we use [Next Obligation. (* ... *) Qed.], for which
this option does not matter. However, sometimes we write things like
[Solve Obligations with naive_solver (* ... *)], and then the obligations
should surely be opaque. *)
Global Unset Transparent Obligations.

(** 2. Do not let Program automatically simplify obligations. The default
obligation tactic is [Tactics.program_simpl], which, among other things,
introduces all variables and gives them fresh names. As such, it becomes
impossible to refer to hypotheses in a robust way. *)
36
Obligation Tactic := idtac.
37
38

(** 3. Hide obligations from the results of the [Search] commands. *)
39
Add Search Blacklist "_obligation_".
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
(** * Sealing off definitions *)
Ralf Jung's avatar
Ralf Jung committed
42
43
44
45
Section seal.
  Local Set Primitive Projections.
  Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
End seal.
Ralf Jung's avatar
Ralf Jung committed
46
47
Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
48

49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
(** * Non-backtracking type classes *)
(** The type class [NoBackTrack P] can be used to establish [P] without ever
backtracking on the instance of [P] that has been found. Backtracking may
normally happen when [P] contains evars that could be instanciated in different
ways depending on which instance is picked, and type class search somewhere else
depends on this evar.

The proper way of handling this would be by setting Coq's option
`Typeclasses Unique Instances`. However, this option seems to be broken, see Coq
issue #6714.

See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
of this type class. *)
Class NoBackTrack (P : Prop) := { no_backtrack : P }.
Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.

65
(** * Typeclass opaque definitions *)
66
67
68
69
70
71
(* The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque tc_opaque.
Arguments tc_opaque {_} _ /.

72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
(* Below we define type class versions of the common logical operators. It is
important to note that we duplicate the definitions, and do not declare the
existing logical operators as type classes. That is, we do not say:

  Existing Class or.
  Existing Class and.

If we could define the existing logical operators as classes, there is no way
of disambiguating whether a premise of a lemma should be solved by type class
resolution or not.

These classes are useful for two purposes: writing complicated type class
premises in a more concise way, and for efficiency. For example, using the [Or]
class, instead of defining two instances [P → Q1 → R] and [P → Q2 → R] we could
have one instance [P → Or Q1 Q2 → R]. When we declare the instance that way, we
avoid the need to derive [P] twice. *)
88
Inductive TCOr (P1 P2 : Prop) : Prop :=
89
90
91
92
93
  | TCOr_l : P1  TCOr P1 P2
  | TCOr_r : P2  TCOr P1 P2.
Existing Class TCOr.
Existing Instance TCOr_l | 9.
Existing Instance TCOr_r | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
94

95
Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1  P2  TCAnd P1 P2.
96
97
Existing Class TCAnd.
Existing Instance TCAnd_intro.
98

99
100
101
Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
Existing Class TCTrue.
Existing Instance TCTrue_intro.
102

103
104
105
106
107
108
109
Inductive TCForall {A} (P : A  Prop) : list A  Prop :=
  | TCForall_nil : TCForall P []
  | TCForall_cons x xs : P x  TCForall P xs  TCForall P (x :: xs).
Existing Class TCForall.
Existing Instance TCForall_nil.
Existing Instance TCForall_cons.

Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
113
114
115
116
117
Inductive TCForall2 {A B} (P : A  B  Prop) : list A  list B  Prop :=
  | TCForall2_nil : TCForall2 P [] []
  | TCForall2_cons x y xs ys :
     P x y  TCForall2 P xs ys  TCForall2 P (x :: xs) (y :: ys).
Existing Class TCForall2.
Existing Instance TCForall2_nil.
Existing Instance TCForall2_cons.

118
119
120
121
Inductive TCEq {A} (x : A) : A  Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
Existing Instance TCEq_refl.

122
(** Throughout this development we use [stdpp_scope] for all general purpose
123
notations that do not belong to a more specific scope. *)
124
125
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.
126

127
(** Change [True] and [False] into notations in order to enable overloading.
128
129
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
130
131
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133


134
(** * Equality *)
135
(** Introduce some Haskell style like notations. *)
136
137
138
139
140
141
Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "( x =)" := (eq x) (only parsing) : stdpp_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
Notation "(≠)" := (λ x y, x  y) (only parsing) : stdpp_scope.
Notation "( x ≠)" := (λ y, x  y) (only parsing) : stdpp_scope.
Notation "(≠ x )" := (λ y, y  x) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
142

143
Hint Extern 0 (_ = _) => reflexivity.
144
Hint Extern 100 (_  _) => discriminate.
Robbert Krebbers's avatar
Robbert Krebbers committed
145

146
147
148
149
Instance: @PreOrder A (=).
Proof. split; repeat intro; congruence. Qed.

(** ** Setoid equality *)
Ralf Jung's avatar
Ralf Jung committed
150
151
152
(** We define an operational type class for setoid equality, i.e., the
"canonical" equivalence for a type. The typeclass is tied to the \equiv
symbol. This is based on (Spitters/van der Weegen, 2011). *)
153
Class Equiv A := equiv: relation A.
154
155
156
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)

157
158
159
160
161
162
163
164
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope.
Notation "(≡ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
Notation "(≢)" := (λ X Y, ¬X  Y) (only parsing) : stdpp_scope.
Notation "X ≢ Y":= (¬X  Y) (at level 70, no associativity) : stdpp_scope.
Notation "( X ≢)" := (λ Y, X  Y) (only parsing) : stdpp_scope.
Notation "(≢ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
165
166
167
168
169
170

(** The type class [LeibnizEquiv] collects setoid equalities that coincide
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
reverse. *)
Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x  y  x = y.
171
172
Hint Mode LeibnizEquiv ! - : typeclass_instances.

173
174
175
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
  x  y  x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
176

177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
Ltac fold_leibniz := repeat
  match goal with
  | H : context [ @equiv ?A _ _ _ ] |- _ =>
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
  | |- context [ @equiv ?A _ _ _ ] =>
    setoid_rewrite (leibniz_equiv_iff (A:=A))
  end.
Ltac unfold_leibniz := repeat
  match goal with
  | H : context [ @eq ?A _ _ ] |- _ =>
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
  | |- context [ @eq ?A _ _ ] =>
    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
  end.

Definition equivL {A} : Equiv A := (=).

(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
Instance: Params (@equiv) 2.

(** The following instance forces [setoid_replace] to use setoid equality
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
Hint Extern 0 (_  _) => reflexivity.
Hint Extern 0 (_  _) => symmetry; assumption.


(** * Type classes *)
(** ** Decidable propositions *)
(** This type class by (Spitters/van der Weegen, 2011) collects decidable
210
propositions. *)
211
Class Decision (P : Prop) := decide : {P} + {¬P}.
212
Hint Mode Decision ! : typeclass_instances.
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
Arguments decide _ {_} : simpl never, assert.

(** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
an explicit class instead of a notation for two reasons:

- It allows us to control [Hint Mode] more precisely. In particular, if it were
  defined as a notation, the above [Hint Mode] for [Decision] would not prevent
  diverging instance search when looking for [RelDecision (@eq ?A)], which would
  result in it looking for [Decision (@eq ?A x y)], i.e. an instance where the
  head position of [Decision] is not en evar.
- We use it to avoid inefficient computation due to eager evaluation of
  propositions by [vm_compute]. This inefficiency arises for example if
  [(x = y) := (f x = f y)]. Since [decide (x = y)] evaluates to
  [decide (f x = f y)], this would then lead to evaluation of [f x] and [f y].
  Using the [RelDecision], the [f] is hidden under a lambda, which prevents
  unnecessary evaluation. *)
Class RelDecision {A B} (R : A  B  Prop) :=
  decide_rel x y :> Decision (R x y).
Hint Mode RelDecision ! ! ! : typeclass_instances.
Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
Notation EqDecision A := (RelDecision (@eq A)).
234
235
236
237

(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
238
Hint Mode Inhabited ! : typeclass_instances.
239
Arguments populate {_} _ : assert.
240
241
242
243
244
245

(** ** Proof irrelevant types *)
(** This type class collects types that are proof irrelevant. That means, all
elements of the type are equal. We use this notion only used for propositions,
but by universe polymorphism we can generalize it. *)
Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
246
Hint Mode ProofIrrel ! : typeclass_instances.
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282

(** ** Common properties *)
(** These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++)] it
allows us to write [inj (k ++)] instead of [app_inv_head k]. *)
Class Inj {A B} (R : relation A) (S : relation B) (f : A  B) : Prop :=
  inj x y : S (f x) (f y)  R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
    (S : relation C) (f : A  B  C) : Prop :=
  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2)  R1 x1 y1  R2 x2 y2.
Class Cancel {A B} (S : relation B) (f : A  B) (g : B  A) : Prop :=
  cancel :  x, S (f (g x)) x.
Class Surj {A B} (R : relation B) (f : A  B) :=
  surj y :  x, R (f x) y.
Class IdemP {A} (R : relation A) (f : A  A  A) : Prop :=
  idemp x : R (f x x) x.
Class Comm {A B} (R : relation A) (f : B  B  A) : Prop :=
  comm x y : R (f x y) (f y x).
Class LeftId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  left_id x : R (f i x) x.
Class RightId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  right_id x : R (f x i) x.
Class Assoc {A} (R : relation A) (f : A  A  A) : Prop :=
  assoc x y z : R (f x (f y z)) (f (f x y) z).
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  left_absorb x : R (f i x) i.
Class RightAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  right_absorb x : R (f x i) i.
Class AntiSymm {A} (R S : relation A) : Prop :=
  anti_symm x y : S x y  S y x  R x y.
Class Total {A} (R : relation A) := total x y : R x y  R y x.
Class Trichotomy {A} (R : relation A) :=
  trichotomy x y : R x y  x = y  R y x.
Class TrichotomyT {A} (R : relation A) :=
  trichotomyT x y : {R x y} + {x = y} + {R y x}.

283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
Arguments irreflexivity {_} _ {_} _ _ : assert.
Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
Arguments cancel {_ _ _} _ _ {_} _ : assert.
Arguments surj {_ _ _} _ {_} _ : assert.
Arguments idemp {_ _} _ {_} _ : assert.
Arguments comm {_ _ _} _ {_} _ _ : assert.
Arguments left_id {_ _} _ _ {_} _ : assert.
Arguments right_id {_ _} _ _ {_} _ : assert.
Arguments assoc {_ _} _ {_} _ _ _ : assert.
Arguments left_absorb {_ _} _ _ {_} _ : assert.
Arguments right_absorb {_ _} _ _ {_} _ : assert.
Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
Arguments total {_} _ {_} _ _ : assert.
Arguments trichotomy {_} _ {_} _ _ : assert.
Arguments trichotomyT {_} _ {_} _ _ : assert.
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362

Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y  ¬R y x.
Proof. intuition. Qed.
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y  R y x.
Proof. intuition. Qed.

Lemma not_inj `{Inj A B R R' f} x y : ¬R x y  ¬R' (f x) (f y).
Proof. intuition. Qed.
Lemma not_inj2_1 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
  ¬R x1 x2  ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
Lemma not_inj2_2 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
  ¬R' y1 y2  ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.

Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A  B)
  `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y)  R x y.
Proof. firstorder. Qed.
Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.

Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} :
  Inj R1 R2 g.
Proof.
  intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity.
Qed.
Lemma cancel_surj `{Cancel A B R1 f g} : Surj R1 f.
Proof. intros y. exists (g y). auto. Qed.

(** The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
use the setoid rewriting mechanism. *)
Lemma idemp_L {A} f `{!@IdemP A (=) f} x : f x x = x.
Proof. auto. Qed.
Lemma comm_L {A B} f `{!@Comm A B (=) f} x y : f x y = f y x.
Proof. auto. Qed.
Lemma left_id_L {A} i f `{!@LeftId A (=) i f} x : f i x = x.
Proof. auto. Qed.
Lemma right_id_L {A} i f `{!@RightId A (=) i f} x : f x i = x.
Proof. auto. Qed.
Lemma assoc_L {A} f `{!@Assoc A (=) f} x y z : f x (f y z) = f (f x y) z.
Proof. auto. Qed.
Lemma left_absorb_L {A} i f `{!@LeftAbsorb A (=) i f} x : f i x = i.
Proof. auto. Qed.
Lemma right_absorb_L {A} i f `{!@RightAbsorb A (=) i f} x : f x i = i.
Proof. auto. Qed.

(** ** Generic orders *)
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y  ¬R Y X.
Instance: Params (@strict) 2.
Class PartialOrder {A} (R : relation A) : Prop := {
  partial_order_pre :> PreOrder R;
  partial_order_anti_symm :> AntiSymm (=) R
}.
Class TotalOrder {A} (R : relation A) : Prop := {
  total_order_partial :> PartialOrder R;
  total_order_trichotomy :> Trichotomy (strict R)
}.

(** * Logic *)
363
364
365
Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope.
Notation "(∧ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
366

367
368
369
Notation "(∨)" := or (only parsing) : stdpp_scope.
Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope.
Notation "(∨ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
370

371
372
373
Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
374
375
376
377
378
379
380
381
382
383
384
385
386
387

Hint Extern 0 (_  _) => reflexivity.
Hint Extern 0 (_  _) => symmetry; assumption.

Lemma or_l P Q : ¬Q  P  Q  P.
Proof. tauto. Qed.
Lemma or_r P Q : ¬P  P  Q  Q.
Proof. tauto. Qed.
Lemma and_wlog_l (P Q : Prop) : (Q  P)  Q  (P  Q).
Proof. tauto. Qed.
Lemma and_wlog_r (P Q : Prop) : P  (P  Q)  (P  Q).
Proof. tauto. Qed.
Lemma impl_transitive (P Q R : Prop) : (P  Q)  (Q  R)  (P  R).
Proof. tauto. Qed.
388
389
390
391
392
393
Lemma forall_proper {A} (P Q : A  Prop) :
  ( x, P x  Q x)  ( x, P x)  ( x, Q x).
Proof. firstorder. Qed.
Lemma exist_proper {A} (P Q : A  Prop) :
  ( x, P x  Q x)  ( x, P x)  ( x, Q x).
Proof. firstorder. Qed.
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436

Instance: Comm () (@eq A).
Proof. red; intuition. Qed.
Instance: Comm () (λ x y, @eq A y x).
Proof. red; intuition. Qed.
Instance: Comm () ().
Proof. red; intuition. Qed.
Instance: Comm () ().
Proof. red; intuition. Qed.
Instance: Assoc () ().
Proof. red; intuition. Qed.
Instance: IdemP () ().
Proof. red; intuition. Qed.
Instance: Comm () ().
Proof. red; intuition. Qed.
Instance: Assoc () ().
Proof. red; intuition. Qed.
Instance: IdemP () ().
Proof. red; intuition. Qed.
Instance: LeftId () True ().
Proof. red; intuition. Qed.
Instance: RightId () True ().
Proof. red; intuition. Qed.
Instance: LeftAbsorb () False ().
Proof. red; intuition. Qed.
Instance: RightAbsorb () False ().
Proof. red; intuition. Qed.
Instance: LeftId () False ().
Proof. red; intuition. Qed.
Instance: RightId () False ().
Proof. red; intuition. Qed.
Instance: LeftAbsorb () True ().
Proof. red; intuition. Qed.
Instance: RightAbsorb () True ().
Proof. red; intuition. Qed.
Instance: LeftId () True impl.
Proof. unfold impl. red; intuition. Qed.
Instance: RightAbsorb () True impl.
Proof. unfold impl. red; intuition. Qed.


(** * Common data types *)
(** ** Functions *)
437
438
439
Notation "(→)" := (λ A B, A  B) (only parsing) : stdpp_scope.
Notation "( A →)" := (λ B, A  B) (only parsing) : stdpp_scope.
Notation "(→ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
440

441
Notation "t $ r" := (t r)
442
443
444
  (at level 65, right associativity, only parsing) : stdpp_scope.
Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope.
Notation "($ x )" := (λ f, f x) (only parsing) : stdpp_scope.
445

446
447
448
449
Infix "∘" := compose : stdpp_scope.
Notation "(∘)" := compose (only parsing) : stdpp_scope.
Notation "( f ∘)" := (compose f) (only parsing) : stdpp_scope.
Notation "(∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
450

Robbert Krebbers's avatar
Robbert Krebbers committed
451
452
453
Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A  B) :=
  populate (λ _, inhabitant).

454
455
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
456
457
458
459
Arguments id _ _ / : assert.
Arguments compose _ _ _ _ _ _ / : assert.
Arguments flip _ _ _ _ _ _ / : assert.
Arguments const _ _ _ _ / : assert.
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
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
509
510
511
512
513
514
515
516
Typeclasses Transparent id compose flip const.

Definition fun_map {A A' B B'} (f: A'  A) (g: B  B') (h : A  B) : A'  B' :=
  g  h  f.

Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
  Reflexive R2  Proper (R1 ==> R2) (λ _, x).
Proof. intros ? y1 y2; reflexivity. Qed.

Instance id_inj {A} : Inj (=) (=) (@id A).
Proof. intros ??; auto. Qed.
Instance compose_inj {A B C} R1 R2 R3 (f : A  B) (g : B  C) :
  Inj R1 R2 f  Inj R2 R3 g  Inj R1 R3 (g  f).
Proof. red; intuition. Qed.

Instance id_surj {A} : Surj (=) (@id A).
Proof. intros y; exists y; reflexivity. Qed.
Instance compose_surj {A B C} R (f : A  B) (g : B  C) :
  Surj (=) f  Surj R g  Surj R (g  f).
Proof.
  intros ?? x. unfold compose. destruct (surj g x) as [y ?].
  destruct (surj f y) as [z ?]. exists z. congruence.
Qed.

Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
Proof. intros ?; reflexivity. Qed.
Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
Proof. intros ???; reflexivity. Qed.
Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x).
Proof. intros ???; reflexivity. Qed.
Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x).
Proof. intros ???; reflexivity. Qed.
Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x).
Proof. intros ?; reflexivity. Qed.
Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x).
Proof. intros ?; reflexivity. Qed.

(** ** Lists *)
Instance list_inhabited {A} : Inhabited (list A) := populate [].

Definition zip_with {A B C} (f : A  B  C) : list A  list B  list C :=
  fix go l1 l2 :=
  match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
Notation zip := (zip_with pair).

(** ** Booleans *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
Hint Unfold Is_true.
Hint Immediate Is_true_eq_left.
Hint Resolve orb_prop_intro andb_prop_intro.
Notation "(&&)" := andb (only parsing).
Notation "(||)" := orb (only parsing).
Infix "&&*" := (zip_with (&&)) (at level 40).
Infix "||*" := (zip_with (||)) (at level 50).

Instance bool_inhabated : Inhabited bool := populate true.
517

518
519
520
521
522
Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
Infix "=.>" := bool_le (at level 70).
Infix "=.>*" := (Forall2 bool_le) (at level 70).
Instance: PartialOrder bool_le.
Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
523

524
525
526
527
528
529
530
531
Lemma andb_True b1 b2 : b1 && b2  b1  b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
Lemma orb_True b1 b2 : b1 || b2  b1  b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
Lemma negb_True b : negb b  ¬b.
Proof. destruct b; simpl; tauto. Qed.
Lemma Is_true_false (b : bool) : b = false  ¬b.
Proof. now intros -> ?. Qed.
532

533
534
535
536
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.
537
538
Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
539
Instance unit_inhabited: Inhabited unit := populate ().
540

541
(** ** Products *)
542
543
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
544

545
546
Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
547

548
Instance: Params (@pair) 2.
549
550
Instance: Params (@fst) 2.
Instance: Params (@snd) 2.
551

552
553
554
555
556
557
558
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
Definition curry3 {A B C D} (f : A  B  C  D) (p : A * B * C) : D :=
  let '(a,b,c) := p in f a b c.
Definition curry4 {A B C D E} (f : A  B  C  D  E) (p : A * B * C * D) : E :=
  let '(a,b,c,d) := p in f a b c d.

Robbert Krebbers's avatar
Robbert Krebbers committed
559
560
561
562
563
Definition uncurry3 {A B C D} (f : A * B * C  D) (a : A) (b : B) (c : C) : D :=
  f (a, b, c).
Definition uncurry4 {A B C D E} (f : A * B * C * D  E)
  (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).

564
565
Definition prod_map {A A' B B'} (f: A  A') (g: B  B') (p : A * B) : A' * B' :=
  (f (p.1), g (p.2)).
566
Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
567

568
569
Definition prod_zip {A A' A'' B B' B''} (f : A  A'  A'') (g : B  B'  B'')
    (p : A * B) (q : A' * B') : A'' * B'' := (f (p.1) (q.1), g (p.2) (q.2)).
570
Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
571

572
573
574
Instance prod_inhabited {A B} (iA : Inhabited A)
    (iB : Inhabited B) : Inhabited (A * B) :=
  match iA, iB with populate x, populate y => populate (x,y) end.
575

576
577
578
579
580
581
582
583
Instance pair_inj : Inj2 (=) (=) (=) (@pair A B).
Proof. injection 1; auto. Qed.
Instance prod_map_inj {A A' B B'} (f : A  A') (g : B  B') :
  Inj (=) (=) f  Inj (=) (=) g  Inj (=) (=) (prod_map f g).
Proof.
  intros ?? [??] [??] ?; simpl in *; f_equal;
    [apply (inj f)|apply (inj g)]; congruence.
Qed.
584

585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
  relation (A * B) := λ x y, R1 (x.1) (y.1)  R2 (x.2) (y.2).
Section prod_relation.
  Context `{R1 : relation A, R2 : relation B}.
  Global Instance prod_relation_refl :
    Reflexive R1  Reflexive R2  Reflexive (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance prod_relation_sym :
    Symmetric R1  Symmetric R2  Symmetric (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance prod_relation_trans :
    Transitive R1  Transitive R2  Transitive (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance prod_relation_equiv :
    Equivalence R1  Equivalence R2  Equivalence (prod_relation R1 R2).
  Proof. split; apply _. Qed.
601

602
603
  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
  Proof. firstorder eauto. Qed.
604
605
  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
  Proof. inversion_clear 1; eauto. Qed.
606
607
608
609
610
  Global Instance fst_proper' : Proper (prod_relation R1 R2 ==> R1) fst.
  Proof. firstorder eauto. Qed.
  Global Instance snd_proper' : Proper (prod_relation R1 R2 ==> R2) snd.
  Proof. firstorder eauto. Qed.
End prod_relation.
Robbert Krebbers's avatar
Robbert Krebbers committed
611

612
613
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Instance pair_proper `{Equiv A, Equiv B} :
614
615
  Proper (() ==> () ==> ()) (@pair A B) := _.
Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B) := _.
616
617
618
Instance fst_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@fst A B) := _.
Instance snd_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@snd A B) := _.
Typeclasses Opaque prod_equiv.
619

Robbert Krebbers's avatar
Robbert Krebbers committed
620
621
Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
622

623
(** ** Sums *)
624
625
Definition sum_map {A A' B B'} (f: A  A') (g: B  B') (xy : A + B) : A' + B' :=
  match xy with inl x => inl (f x) | inr y => inr (g y) end.
626
Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
627

628
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
629
  match iA with populate x => populate (inl x) end.
630
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
631
  match iB with populate y => populate (inl y) end.
632

633
634
635
636
Instance inl_inj : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
Instance inr_inj : Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
637

638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
Instance sum_map_inj {A A' B B'} (f : A  A') (g : B  B') :
  Inj (=) (=) f  Inj (=) (=) g  Inj (=) (=) (sum_map f g).
Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed.

Inductive sum_relation {A B}
     (R1 : relation A) (R2 : relation B) : relation (A + B) :=
  | inl_related x1 x2 : R1 x1 x2  sum_relation R1 R2 (inl x1) (inl x2)
  | inr_related y1 y2 : R2 y1 y2  sum_relation R1 R2 (inr y1) (inr y2).

Section sum_relation.
  Context `{R1 : relation A, R2 : relation B}.
  Global Instance sum_relation_refl :
    Reflexive R1  Reflexive R2  Reflexive (sum_relation R1 R2).
  Proof. intros ?? [?|?]; constructor; reflexivity. Qed.
  Global Instance sum_relation_sym :
    Symmetric R1  Symmetric R2  Symmetric (sum_relation R1 R2).
  Proof. destruct 3; constructor; eauto. Qed.
  Global Instance sum_relation_trans :
    Transitive R1  Transitive R2  Transitive (sum_relation R1 R2).
  Proof. destruct 3; inversion_clear 1; constructor; eauto. Qed.
  Global Instance sum_relation_equiv :
    Equivalence R1  Equivalence R2  Equivalence (sum_relation R1 R2).
  Proof. split; apply _. Qed.
  Global Instance inl_proper' : Proper (R1 ==> sum_relation R1 R2) inl.
  Proof. constructor; auto. Qed.
  Global Instance inr_proper' : Proper (R2 ==> sum_relation R1 R2) inr.
  Proof. constructor; auto. Qed.
665
666
667
668
  Global Instance inl_inj' : Inj R1 (sum_relation R1 R2) inl.
  Proof. inversion_clear 1; auto. Qed.
  Global Instance inr_inj' : Inj R2 (sum_relation R1 R2) inr.
  Proof. inversion_clear 1; auto. Qed.
669
670
671
672
673
End sum_relation.

Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation () ().
Instance inl_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@inl A B) := _.
Instance inr_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@inr A B) := _.
674
675
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inl A B) := _.
Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inr A B) := _.
676
677
Typeclasses Opaque sum_equiv.

678
679
(** ** Option *)
Instance option_inhabited {A} : Inhabited (option A) := populate None.
Robbert Krebbers's avatar
Robbert Krebbers committed
680

681
(** ** Sigma types *)
682
683
684
Arguments existT {_ _} _ _ : assert.
Arguments projT1 {_ _} _ : assert.
Arguments projT2 {_ _} _ : assert.
685

686
687
688
Arguments exist {_} _ _ _ : assert.
Arguments proj1_sig {_ _} _ : assert.
Arguments proj2_sig {_ _} _ : assert.
689
690
Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope.
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
691

692
693
694
Lemma proj1_sig_inj {A} (P : A  Prop) x (Px : P x) y (Py : P y) :
  xPx = yPy  x = y.
Proof. injection 1; trivial. Qed.
695

696
697
698
699
700
701
702
703
704
705
Section sig_map.
  Context `{P : A  Prop} `{Q : B  Prop} (f : A  B) (Hf :  x, P x  Q (f x)).
  Definition sig_map (x : sig P) : sig Q := f (`x)  Hf _ (proj2_sig x).
  Global Instance sig_map_inj:
    ( x, ProofIrrel (P x))  Inj (=) (=) f  Inj (=) (=) sig_map.
  Proof.
    intros ?? [x Hx] [y Hy]. injection 1. intros Hxy.
    apply (inj f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
  Qed.
End sig_map.
706
Arguments sig_map _ _ _ _ _ _ !_ / : assert.
707

Robbert Krebbers's avatar
Robbert Krebbers committed
708

709
(** * Operations on collections *)
710
(** We define operational type classes for the traditional operations and
711
relations on collections: the empty collection [∅], the union [(∪)],
712
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
713
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
714
Class Empty A := empty: A.
715
Hint Mode Empty ! : typeclass_instances.
716
Notation "∅" := empty : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
717

718
719
Instance empty_inhabited `(Empty A) : Inhabited A := populate .

Robbert Krebbers's avatar
Robbert Krebbers committed
720
Class Union A := union: A  A  A.
721
Hint Mode Union ! : typeclass_instances.
722
Instance: Params (@union) 2.
723
724
725
726
727
728
Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
Notation "(∪)" := union (only parsing) : stdpp_scope.
Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
Infix "∪*" := (zip_with ()) (at level 50, left associativity) : stdpp_scope.
Notation "(∪*)" := (zip_with ()) (only parsing) : stdpp_scope.
729
Infix "∪**" := (zip_with (zip_with ()))
730
  (at level 50, left associativity) : stdpp_scope.
731
Infix "∪*∪**" := (zip_with (prod_zip () (*)))
732
  (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
733

734
Definition union_list `{Empty A} `{Union A} : list A  A := fold_right () .
735
Arguments union_list _ _ _ !_ / : assert.
736
Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
737

Robbert Krebbers's avatar
Robbert Krebbers committed
738
Class Intersection A := intersection: A  A  A.
739
Hint Mode Intersection ! : typeclass_instances.
740
Instance: Params (@intersection) 2.
741
742
743
744
Infix "∩" := intersection (at level 40) : stdpp_scope.
Notation "(∩)" := intersection (only parsing) : stdpp_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope.
Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
745
746

Class Difference A := difference: A  A  A.
747
Hint Mode Difference ! : typeclass_instances.
748
Instance: Params (@difference) 2.
749
750
751
752
753
754
Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
Notation "(∖)" := difference (only parsing) : stdpp_scope.
Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
Infix "∖*" := (zip_with ()) (at level 40, left associativity) : stdpp_scope.
Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope.
755
Infix "∖**" := (zip_with (zip_with ()))
756
  (at level 40, left associativity) : stdpp_scope.
757
Infix "∖*∖**" := (zip_with (prod_zip () (*)))
758
  (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
759

760
Class Singleton A B := singleton: A  B.
761
Hint Mode Singleton - ! : typeclass_instances.
762
Instance: Params (@singleton) 3.
763
Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
764
Notation "{[ x ; y ; .. ; z ]}" :=
765
  (union .. (union (singleton x) (singleton y)) .. (singleton z))
766
  (at level 1) : stdpp_scope.
767
Notation "{[ x , y ]}" := (singleton (x,y))
768
  (at level 1, y at next level) : stdpp_scope.
769
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
770
  (at level 1, y at next level, z at next level) : stdpp_scope.
771

772
Class SubsetEq A := subseteq: relation A.
773
Hint Mode SubsetEq ! : typeclass_instances.
774
Instance: Params (@subseteq) 2.
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
Infix "⊆" := subseteq (at level 70) : stdpp_scope.
Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope.
Notation "(⊆ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
Notation "X ⊈ Y" := (¬X  Y) (at level 70) : stdpp_scope.
Notation "(⊈)" := (λ X Y, X  Y) (only parsing) : stdpp_scope.
Notation "( X ⊈)" := (λ Y, X  Y) (only parsing) : stdpp_scope.
Notation "(⊈ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
Infix "⊆*" := (Forall2 ()) (at level 70) : stdpp_scope.
Notation "(⊆*)" := (Forall2 ()) (only parsing) : stdpp_scope.
Infix "⊆**" := (Forall2 (*)) (at level 70) : stdpp_scope.
Infix "⊆1*" := (Forall2 (λ p q, p.1  q.1)) (at level 70) : stdpp_scope.
Infix "⊆2*" := (Forall2 (λ p q, p.2  q.2)) (at level 70) : stdpp_scope.
Infix "⊆1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : stdpp_scope.
Infix "⊆2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
790

791
Hint Extern 0 (_  _) => reflexivity.
792
793
794
Hint Extern 0 (_ * _) => reflexivity.
Hint Extern 0 (_ ** _) => reflexivity.

795
796
797
798
799
800
801
802
Infix "⊂" := (strict ()) (at level 70) : stdpp_scope.
Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope.
Notation "( X ⊂)" := (strict () X) (only parsing) : stdpp_scope.
Notation "(⊂ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
Notation "X ⊄ Y" := (¬X  Y) (at level 70) : stdpp_scope.
Notation "(⊄)" := (λ X Y, X  Y) (only parsing) : stdpp_scope.
Notation "( X ⊄)" := (λ Y, X  Y) (only parsing) : stdpp_scope.
Notation "(⊄ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
803

804
805
806
807
Notation "X ⊆ Y ⊆ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊆ Y ⊂ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊂ Y ⊆ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊂ Y ⊂ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : stdpp_scope.
808

809
810
811
812
(** The class [Lexico A] is used for the lexicographic order on [A]. This order
is used to create finite maps, finite sets, etc, and is typically different from
the order [(⊆)]. *)
Class Lexico A := lexico: relation A.
813
Hint Mode Lexico ! : typeclass_instances.
814

Robbert Krebbers's avatar
Robbert Krebbers committed
815
Class ElemOf A B := elem_of: A  B  Prop.
816
Hint Mode ElemOf - ! : typeclass_instances.
817
Instance: Params (@elem_of) 3.
818
819
820
821
822
823
824
825
Infix "∈" := elem_of (at level 70) : stdpp_scope.
Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
Notation "( x ∈)" := (elem_of x) (only parsing) : stdpp_scope.
Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope.
Notation "x ∉ X" := (¬x  X) (at level 80) : stdpp_scope.
Notation "(∉)" := (λ x X, x  X) (only parsing) : stdpp_scope.
Notation "( x ∉)" := (λ X, x  X) (only parsing) : stdpp_scope.
Notation "(∉ X )" := (λ x, x  X) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
826

Robbert Krebbers's avatar
Robbert Krebbers committed
827
Class Disjoint A := disjoint : A  A  Prop.
828
 Hint Mode Disjoint ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
829
Instance: Params (@disjoint) 2.
830
831
832
833
834
835
836
837
838
839
840
Infix "##" := disjoint (at level 70) : stdpp_scope.
Notation "(##)" := disjoint (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope.
Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope.
Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : stdpp_scope.
Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : stdpp_scope.
Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : stdpp_scope.
Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : stdpp_scope.
841
842
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Hint Extern 0 (_ ##* _) => symmetry; eassumption.
843
844

Class DisjointE E A := disjointE : E  A  A  Prop.
845
Hint Mode DisjointE - ! : typeclass_instances.
846
Instance: Params (@disjointE) 4.
847
Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
848
849
  (at level 70, format "X  ##{ Γ }  Y") : stdpp_scope.
Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : stdpp_scope.
850
Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
851
  (at level 70, format "Xs  ##{ Γ }*  Ys") : stdpp_scope.
852
Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
853
  (only parsing, Γ at level 1) : stdpp_scope.
854
Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
855
  (at level 70, format "X  ##{ Γ1 , Γ2 , .. , Γ3 }  Y") : stdpp_scope.
856
Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
857
  (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
858
  (at level 70, format "Xs  ##{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : stdpp_scope.
859
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
860
861

Class DisjointList A := disjoint_list : list A  Prop.
862
Hint Mode DisjointList ! : typeclass_instances.
863
Instance: Params (@disjoint_list) 2.
864
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "##  Xs") : stdpp_scope.
865

866
867
Section disjoint_list.
  Context `{Disjoint A, Union A, Empty A}.
868
869
  Implicit Types X : A.

870
  Inductive disjoint_list_default : DisjointList A :=
871
872
    | disjoint_nil_2 : ## (@nil A)
    | disjoint_cons_2 (X : A) (Xs : list A) : X ##  Xs  ## Xs  ## (X :: Xs).
873
  Global Existing Instance disjoint_list_default.
874

875
  Lemma disjoint_list_nil  : ## @nil A  True.
876
  Proof. split; constructor. Qed.
877
  Lemma disjoint_list_cons X Xs : ## (X :: Xs)  X ##  Xs  ## Xs.
878
  Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
879
End disjoint_list.
880
881

Class Filter A B := filter:  (P : A  Prop) `{ x, Decision (P x)}, B  B.
882
Hint Mode Filter - ! : typeclass_instances.
883

884
Class UpClose A B := up_close : A  B.
885
Hint Mode UpClose - ! : typeclass_instances.
886
Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
887
888

(** * Monadic operations *)
889
(** We define operational type classes for the monadic operations bind, join 
890
891
892
and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
893
Class MRet (M : Type  Type) := mret:  {A}, A  M A.
894
Arguments mret {_ _ _} _ : assert.
895
Instance: Params (@mret) 3.
896
Class MBind (M : Type  Type) := mbind :  {A B}, (A  M B)  M A  M B.
897
Arguments mbind {_ _ _ _} _ !_ / : assert.
898
Instance: Params (@mbind) 4.
899
Class MJoin (M : Type  Type) := mjoin:  {A}, M (M A)  M A.
900
Arguments mjoin {_ _ _} !_ / : assert.
901
Instance: Params (@mjoin) 3.
902
Class FMap (M : Type  Type) := fmap :  {A B}, (A  B)  M A  M B.
903
Arguments fmap {_ _ _ _} _ !_ / : assert.
904
Instance: Params (@fmap) 4.
905
Class OMap (M : Type  Type) := omap:  {A B}, (A  option B)  M A  M B.
906
Arguments omap {_ _ _ _} _ !_ / : assert.
907
Instance: Params (@omap) 4.