base.v 49.9 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
(** * Typeclass opaque definitions *)
50 51 52 53 54 55
(* 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 {_} _ /.

56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
(* 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. *)
72
Inductive TCOr (P1 P2 : Prop) : Prop :=
73 74 75 76 77
  | 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
78

79
Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1  P2  TCAnd P1 P2.
80 81
Existing Class TCAnd.
Existing Instance TCAnd_intro.
82

83 84 85
Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
Existing Class TCTrue.
Existing Instance TCTrue_intro.
86

87 88 89 90 91 92 93
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.

94
(** Throughout this development we use [stdpp_scope] for all general purpose
95
notations that do not belong to a more specific scope. *)
96 97
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.
98

99
(** Change [True] and [False] into notations in order to enable overloading.
100 101
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
102 103
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105


106
(** * Equality *)
107
(** Introduce some Haskell style like notations. *)
108 109 110 111 112 113
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
114

115
Hint Extern 0 (_ = _) => reflexivity.
116
Hint Extern 100 (_  _) => discriminate.
Robbert Krebbers's avatar
Robbert Krebbers committed
117

118 119 120 121
Instance: @PreOrder A (=).
Proof. split; repeat intro; congruence. Qed.

(** ** Setoid equality *)
Ralf Jung's avatar
Ralf Jung committed
122 123 124
(** 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). *)
125
Class Equiv A := equiv: relation A.
126 127 128
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)

129 130 131 132 133 134 135 136
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.
137 138 139 140 141 142

(** 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.
143 144
Hint Mode LeibnizEquiv ! - : typeclass_instances.

145 146 147
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
  x  y  x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
148

149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
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
182
propositions. *)
183
Class Decision (P : Prop) := decide : {P} + {¬P}.
184
Hint Mode Decision ! : typeclass_instances.
185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
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)).
206 207 208 209

(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
210
Hint Mode Inhabited ! : typeclass_instances.
211
Arguments populate {_} _ : assert.
212 213 214 215 216 217

(** ** 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.
218
Hint Mode ProofIrrel ! : typeclass_instances.
219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254

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

255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
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.
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334

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 *)
335 336 337
Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope.
Notation "(∧ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
338

339 340 341
Notation "(∨)" := or (only parsing) : stdpp_scope.
Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope.
Notation "(∨ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
342

343 344 345
Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
346 347 348 349 350 351 352 353 354 355 356 357 358 359

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.
360 361 362 363 364 365
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.
366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408

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 *)
409 410 411
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.
412

413
Notation "t $ r" := (t r)
414 415 416
  (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.
417

418 419 420 421
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.
422

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

426 427
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
428 429 430 431
Arguments id _ _ / : assert.
Arguments compose _ _ _ _ _ _ / : assert.
Arguments flip _ _ _ _ _ _ / : assert.
Arguments const _ _ _ _ / : assert.
432 433 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 475 476 477 478 479 480 481 482 483 484 485 486 487 488
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.
489

490 491 492 493 494
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.
495

496 497 498 499 500 501 502 503
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.
504

505 506 507 508
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.
509 510
Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
511
Instance unit_inhabited: Inhabited unit := populate ().
512

513
(** ** Products *)
514 515
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
516

517 518
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").
519

520
Instance: Params (@pair) 2.
521 522
Instance: Params (@fst) 2.
Instance: Params (@snd) 2.
523

524 525 526 527 528 529 530
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
531 532 533 534 535
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).

536 537
Definition prod_map {A A' B B'} (f: A  A') (g: B  B') (p : A * B) : A' * B' :=
  (f (p.1), g (p.2)).
538
Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
539

540 541
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)).
542
Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
543

544 545 546
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.
547

548 549 550 551 552 553 554 555
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.
556

557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572
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.
573

574 575
  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
  Proof. firstorder eauto. Qed.
576 577
  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
  Proof. inversion_clear 1; eauto. Qed.
578 579 580 581 582
  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
583

584 585
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Instance pair_proper `{Equiv A, Equiv B} :
586 587
  Proper (() ==> () ==> ()) (@pair A B) := _.
Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B) := _.
588 589 590
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.
591

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

595
(** ** Sums *)
596 597
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.
598
Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
599

600
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
601
  match iA with populate x => populate (inl x) end.
602
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
603
  match iB with populate y => populate (inl y) end.
604

605 606 607 608
Instance inl_inj : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
Instance inr_inj : Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
609

610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636
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.
637 638 639 640
  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.
641 642 643 644 645
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) := _.
646 647
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inl A B) := _.
Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inr A B) := _.
648 649
Typeclasses Opaque sum_equiv.

650 651
(** ** Option *)
Instance option_inhabited {A} : Inhabited (option A) := populate None.
Robbert Krebbers's avatar
Robbert Krebbers committed
652

653
(** ** Sigma types *)
654 655 656
Arguments existT {_ _} _ _ : assert.
Arguments projT1 {_ _} _ : assert.
Arguments projT2 {_ _} _ : assert.
657

658 659 660
Arguments exist {_} _ _ _ : assert.
Arguments proj1_sig {_ _} _ : assert.
Arguments proj2_sig {_ _} _ : assert.
661 662
Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope.
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
663

664 665 666
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.
667

668 669 670 671 672 673 674 675 676 677
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.
678
Arguments sig_map _ _ _ _ _ _ !_ / : assert.
679

Robbert Krebbers's avatar
Robbert Krebbers committed
680

681
(** * Operations on collections *)
682
(** We define operational type classes for the traditional operations and
683
relations on collections: the empty collection [∅], the union [(∪)],
684
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
685
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
686
Class Empty A := empty: A.
687
Hint Mode Empty ! : typeclass_instances.
688
Notation "∅" := empty : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
689

690 691
Instance empty_inhabited `(Empty A) : Inhabited A := populate .

Robbert Krebbers's avatar
Robbert Krebbers committed
692
Class Union A := union: A  A  A.
693
Hint Mode Union ! : typeclass_instances.
694
Instance: Params (@union) 2.
695 696 697 698 699 700
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.
701
Infix "∪**" := (zip_with (zip_with ()))
702
  (at level 50, left associativity) : stdpp_scope.
703
Infix "∪*∪**" := (zip_with (prod_zip () (*)))
704
  (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
705

706
Definition union_list `{Empty A} `{Union A} : list A  A := fold_right () .
707
Arguments union_list _ _ _ !_ / : assert.
708
Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
709

Robbert Krebbers's avatar
Robbert Krebbers committed
710
Class Intersection A := intersection: A  A  A.
711
Hint Mode Intersection ! : typeclass_instances.
712
Instance: Params (@intersection) 2.
713 714 715 716
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
717 718

Class Difference A := difference: A  A  A.
719
Hint Mode Difference ! : typeclass_instances.
720
Instance: Params (@difference) 2.
721 722 723 724 725 726
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.
727
Infix "∖**" := (zip_with (zip_with ()))
728
  (at level 40, left associativity) : stdpp_scope.
729
Infix "∖*∖**" := (zip_with (prod_zip () (*)))
730
  (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
731

732
Class Singleton A B := singleton: A  B.
733
Hint Mode Singleton - ! : typeclass_instances.
734
Instance: Params (@singleton) 3.
735
Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
736
Notation "{[ x ; y ; .. ; z ]}" :=
737
  (union .. (union (singleton x) (singleton y)) .. (singleton z))
738
  (at level 1) : stdpp_scope.
739
Notation "{[ x , y ]}" := (singleton (x,y))
740
  (at level 1, y at next level) : stdpp_scope.
741
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
742
  (at level 1, y at next level, z at next level) : stdpp_scope.
743

744
Class SubsetEq A := subseteq: relation A.
745
Hint Mode SubsetEq ! : typeclass_instances.
746
Instance: Params (@subseteq) 2.
747 748 749 750 751 752 753 754 755 756 757 758 759 760 761
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
762

763
Hint Extern 0 (_  _) => reflexivity.
764 765 766
Hint Extern 0 (_ * _) => reflexivity.
Hint Extern 0 (_ ** _) => reflexivity.

767 768 769 770 771 772 773 774
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
775

776 777 778 779
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.
780

781 782 783 784
(** 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.
785
Hint Mode Lexico ! : typeclass_instances.
786

Robbert Krebbers's avatar
Robbert Krebbers committed
787
Class ElemOf A B := elem_of: A  B  Prop.
788
Hint Mode ElemOf - ! : typeclass_instances.
789
Instance: Params (@elem_of) 3.
790 791 792 793 794 795 796 797
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
798

Robbert Krebbers's avatar
Robbert Krebbers committed
799
Class Disjoint A := disjoint : A  A  Prop.
800
 Hint Mode Disjoint ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
801
Instance: Params (@disjoint) 2.
802 803 804 805 806 807 808 809 810 811 812
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.
813 814
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Hint Extern 0 (_ ##* _) => symmetry; eassumption.
815 816

Class DisjointE E A := disjointE : E  A  A  Prop.
817
Hint Mode DisjointE - ! : typeclass_instances.
818
Instance: Params (@disjointE) 4.
819
Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
820 821
  (at level 70, format "X  ##{ Γ }  Y") : stdpp_scope.
Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : stdpp_scope.
822
Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
823
  (at level 70, format "Xs  ##{ Γ }*  Ys") : stdpp_scope.
824
Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
825
  (only parsing, Γ at level 1) : stdpp_scope.
826
Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
827
  (at level 70, format "X  ##{ Γ1 , Γ2 , .. , Γ3 }  Y") : stdpp_scope.
828
Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
829
  (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
830
  (at level 70, format "Xs  ##{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : stdpp_scope.
831
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
832 833

Class DisjointList A := disjoint_list : list A  Prop.
834
Hint Mode DisjointList ! : typeclass_instances.
835
Instance: Params (@disjoint_list) 2.
836
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "##  Xs") : stdpp_scope.
837

838 839
Section disjoint_list.
  Context `{Disjoint A, Union A, Empty A}.
840 841
  Implicit Types X : A.

842
  Inductive disjoint_list_default : DisjointList A :=
843 844
    | disjoint_nil_2 : ## (@nil A)
    | disjoint_cons_2 (X : A) (Xs : list A) : X ##  Xs  ## Xs  ## (X :: Xs).
845
  Global Existing Instance disjoint_list_default.
846

847
  Lemma disjoint_list_nil  : ## @nil A  True.
848
  Proof. split; constructor. Qed.
849
  Lemma disjoint_list_cons X Xs : ## (X :: Xs)  X ##  Xs  ## Xs.
850
  Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
851
End disjoint_list.
852 853

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

856
Class UpClose A B := up_close : A  B.
857
Hint Mode UpClose - ! : typeclass_instances.
858
Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
859 860

(** * Monadic operations *)
861
(** We define operational type classes for the monadic operations bind, join 
862 863 864
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). *)
865
Class MRet (M : Type  Type) := mret:  {A}, A  M A.
866
Arguments mret {_ _ _} _ : assert.
867
Instance: Params (@mret) 3.
868
Class MBind (M : Type  Type) := mbind :  {A B}, (A  M B)  M A  M B.
869
Arguments mbind {_ _ _ _} _ !_ / : assert.
870
Instance: Params (@mbind) 4.
871
Class MJoin (M : Type  Type) := mjoin:  {A}, M (M A)  M A.
872
Arguments mjoin {_ _ _} !_ / : assert.
873
Instance: Params (@mjoin) 3.
874
Class FMap (M : Type  Type) := fmap :  {A B}, (A  B)  M A  M B.
875
Arguments fmap {_ _ _ _} _ !_ / : assert.
876
Instance: Params (@fmap) 4.
877
Class OMap (M : Type  Type) := omap:  {A B}, (A  option B)  M A  M B.
878
Arguments omap {_ _ _ _} _ !_ / : assert.
879
Instance: Params (@omap) 4.
880

881 882 883 884
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
885 886

Notation "x ← y ; z" := (y = (λ x : _, z))
887 888 889 890 891
  (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.

Notation "' x1 .. xn ← y ; z" := (y = (λ x1, .. (λ xn, z) .. ))
  (at level 20, x1 binder, xn binder, y at level 100, z at level 200,
   only parsing, right associativity) : stdpp_scope.
892

893 894
Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.

895
Notation "x ;; z" := (x = λ _, z)
896
  (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.
897

898
Notation "ps .*1" := (fmap (M:=list) fst ps)
899
  (at level 2, left associativity, format "ps .*1").
900
Notation "ps .*2" := (fmap (M:=list) snd ps)
901
  (at level 2, left associativity, format "ps .*2").
902

903
Class MGuard (M : Type  Type) :=
904
  mguard:  P {dec : Decision P} {A}, (P  M A)  M A.
905
Arguments mguard _ _ _ !_ _ _ / : assert.
906
Notation "'guard' P ; z" := (mguard P (λ _, z))
907
  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
908
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
909
  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
910 911

(** * Operations on maps *)
912 913
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
914
The function look up [m !! k] should yield the element at key [k] in [m]. *)
915
Class Lookup (K A M : Type) := lookup: K  M  option A.