base.v 53.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

Ralf Jung's avatar
Ralf Jung committed
13 14
(** * Enable implicit generalization. *)
(** This option enables implicit generalization in arguments of the form
15 16 17 18 19 20
   `{...} (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 66 67 68
(* A conditional at the type class level. Note that [TCIf P Q R] is not the same
as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
establish [R], i.e. does not have the behavior of a conditional. Furthermore,
note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
Robbert Krebbers's avatar
Robbert Krebbers committed
69
would not be able to prove the negation of [P]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Inductive TCIf (P Q R : Prop) : Prop :=
71 72 73 74 75 76 77 78
  | TCIf_true : P  Q  TCIf P Q R
  | TCIf_false : R  TCIf P Q R.
Existing Class TCIf.

Hint Extern 0 (TCIf _ _ _) =>
  first [apply TCIf_true; [apply _|]
        |apply TCIf_false] : typeclass_instances.

79
(** * Typeclass opaque definitions *)
Ralf Jung's avatar
Ralf Jung committed
80
(** The constant [tc_opaque] is used to make definitions opaque for just type
81 82 83 84 85
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 {_} _ /.

Ralf Jung's avatar
Ralf Jung committed
86
(** Below we define type class versions of the common logical operators. It is
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
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. *)
102
Inductive TCOr (P1 P2 : Prop) : Prop :=
103 104 105 106 107
  | 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
108

109
Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1  P2  TCAnd P1 P2.
110 111
Existing Class TCAnd.
Existing Instance TCAnd_intro.
112

113 114 115
Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
Existing Class TCTrue.
Existing Instance TCTrue_intro.
116

117 118 119 120 121 122 123
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
124 125 126 127 128 129 130 131
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.

132 133 134 135 136 137 138
Inductive TCElemOf {A} (x : A) : list A  Prop :=
  | TCElemOf_here xs : TCElemOf x (x :: xs)
  | TCElemOf_further y xs : TCElemOf x xs  TCElemOf x (y :: xs).
Existing Class TCElemOf.
Existing Instance TCElemOf_here.
Existing Instance TCElemOf_further.

139 140 141 142
Inductive TCEq {A} (x : A) : A  Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
Existing Instance TCEq_refl.

Robbert Krebbers's avatar
Robbert Krebbers committed
143 144 145 146 147
Inductive TCDiag {A} (C : A  Prop) : A  A  Prop :=
  | TCDiag_diag x : C x  TCDiag C x x.
Existing Class TCDiag.
Existing Instance TCDiag_diag.

148
(** Throughout this development we use [stdpp_scope] for all general purpose
149
notations that do not belong to a more specific scope. *)
150 151
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.
152

153
(** Change [True] and [False] into notations in order to enable overloading.
154 155
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
156 157
Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False (format "False") : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
158 159


160
(** * Equality *)
161
(** Introduce some Haskell style like notations. *)
162 163 164 165 166 167
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
168

169 170 171 172
Infix "=@{ A }" := (@eq A)
  (at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
173 174
Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.
175

176 177
Hint Extern 0 (_ = _) => reflexivity : core.
Hint Extern 100 (_  _) => discriminate : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
178

179
Instance:  A, PreOrder (=@{A}).
180 181 182
Proof. split; repeat intro; congruence. Qed.

(** ** Setoid equality *)
Ralf Jung's avatar
Ralf Jung committed
183 184 185
(** 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). *)
186
Class Equiv A := equiv: relation A.
187 188 189
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)

190
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
191 192 193
Infix "≡@{ A }" := (@equiv A _)
  (at level 70, only parsing, no associativity) : stdpp_scope.

194 195 196 197 198 199 200
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.
201

202 203
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope.
204 205
Notation "X ≢@{ A } Y":= (¬X @{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.
206

207 208 209 210 211
(** 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.
212 213
Hint Mode LeibnizEquiv ! - : typeclass_instances.

214
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@{A})} (x y : A) :
215 216
  x  y  x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
217

218 219
Ltac fold_leibniz := repeat
  match goal with
220
  | H : context [ _ @{?A} _ ] |- _ =>
221
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
222
  | |- context [ _ @{?A} _ ] =>
223 224 225 226
    setoid_rewrite (leibniz_equiv_iff (A:=A))
  end.
Ltac unfold_leibniz := repeat
  match goal with
227
  | H : context [ _ =@{?A} _ ] |- _ =>
228
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
229
  | |- context [ _ =@{?A} _ ] =>
230 231 232 233 234 235 236 237 238 239 240 241 242 243
    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.
244 245
Hint Extern 0 (_  _) => reflexivity : core.
Hint Extern 0 (_  _) => symmetry; assumption : core.
246 247 248 249 250


(** * Type classes *)
(** ** Decidable propositions *)
(** This type class by (Spitters/van der Weegen, 2011) collects decidable
251
propositions. *)
252
Class Decision (P : Prop) := decide : {P} + {¬P}.
253
Hint Mode Decision ! : typeclass_instances.
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
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.
274
Notation EqDecision A := (RelDecision (=@{A})).
275 276 277 278

(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
279
Hint Mode Inhabited ! : typeclass_instances.
280
Arguments populate {_} _ : assert.
281 282 283 284 285 286

(** ** 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.
287
Hint Mode ProofIrrel ! : typeclass_instances.
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

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

324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339
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.
340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 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

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 *)
404 405 406
Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope.
Notation "(∧ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
407

408 409 410
Notation "(∨)" := or (only parsing) : stdpp_scope.
Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope.
Notation "(∨ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
411

412 413 414
Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
415

416 417
Hint Extern 0 (_  _) => reflexivity : core.
Hint Extern 0 (_  _) => symmetry; assumption : core.
418 419 420 421 422 423 424 425 426 427 428

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.
429 430 431 432 433 434
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.
435

436
Instance: Comm () (=@{A}).
437
Proof. red; intuition. Qed.
438
Instance: Comm () (λ x y, y =@{A} x).
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
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 *)
478 479 480
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.
481

482
Notation "t $ r" := (t r)
483 484 485
  (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.
486

487 488 489 490
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.
491

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

495 496
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
497 498 499 500
Arguments id _ _ / : assert.
Arguments compose _ _ _ _ _ _ / : assert.
Arguments flip _ _ _ _ _ _ / : assert.
Arguments const _ _ _ _ / : assert.
501 502 503 504 505 506 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 538 539 540 541 542 543 544 545 546 547 548
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.
549 550 551
Hint Unfold Is_true : core.
Hint Immediate Is_true_eq_left : core.
Hint Resolve orb_prop_intro andb_prop_intro : core.
552 553 554 555 556 557
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.
558

559 560 561 562 563
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.
564

565 566 567 568 569 570 571 572
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.
573

574 575
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
576
Instance unit_equivalence : Equivalence (@{unit}).
577
Proof. repeat split. Qed.
578 579
Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
580
Instance unit_inhabited: Inhabited unit := populate ().
581

582
(** ** Products *)
583 584
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
585

586 587
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").
588

589
Instance: Params (@pair) 2.
590 591
Instance: Params (@fst) 2.
Instance: Params (@snd) 2.
592

593 594 595 596 597 598 599
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.

600 601 602 603 604
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).

605 606
Definition prod_map {A A' B B'} (f: A  A') (g: B  B') (p : A * B) : A' * B' :=
  (f (p.1), g (p.2)).
607
Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
608

609 610
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)).
611
Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
612

613 614 615
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.
616

617 618 619 620 621 622 623 624
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.
625

626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641
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.
642

643 644
  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
  Proof. firstorder eauto. Qed.
645 646
  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
  Proof. inversion_clear 1; eauto. Qed.
647 648 649 650 651
  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
652

653 654
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Instance pair_proper `{Equiv A, Equiv B} :
655 656
  Proper (() ==> () ==> ()) (@pair A B) := _.
Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B) := _.
657 658 659
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.
660

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

664
(** ** Sums *)
665 666
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.
667
Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
668

669
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
670
  match iA with populate x => populate (inl x) end.
671
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
672
  match iB with populate y => populate (inl y) end.
673

674 675 676 677
Instance inl_inj : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
Instance inr_inj : Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
678

679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
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.
706 707 708 709
  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.
710 711 712 713 714
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) := _.
715 716
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inl A B) := _.
Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inr A B) := _.
717 718
Typeclasses Opaque sum_equiv.

719 720
(** ** Option *)
Instance option_inhabited {A} : Inhabited (option A) := populate None.
Robbert Krebbers's avatar
Robbert Krebbers committed
721

722
(** ** Sigma types *)
723 724 725
Arguments existT {_ _} _ _ : assert.
Arguments projT1 {_ _} _ : assert.
Arguments projT2 {_ _} _ : assert.
726

727 728 729
Arguments exist {_} _ _ _ : assert.
Arguments proj1_sig {_ _} _ : assert.
Arguments proj2_sig {_ _} _ : assert.
730 731
Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope.
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
732

733 734 735
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.
736

737 738 739 740 741 742 743 744 745 746
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.
747
Arguments sig_map _ _ _ _ _ _ !_ / : assert.
748

Robbert Krebbers's avatar
Robbert Krebbers committed
749

750
(** * Operations on collections *)
751
(** We define operational type classes for the traditional operations and
752
relations on collections: the empty collection [∅], the union [(∪)],
753
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
754
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
755
Class Empty A := empty: A.
756
Hint Mode Empty ! : typeclass_instances.
757
Notation "∅" := empty (format "∅") : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
758

759 760
Instance empty_inhabited `(Empty A) : Inhabited A := populate .

Robbert Krebbers's avatar
Robbert Krebbers committed
761
Class Union A := union: A  A  A.
762
Hint Mode Union ! : typeclass_instances.
763
Instance: Params (@union) 2.
764 765 766 767 768 769
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.
770
Infix "∪**" := (zip_with (zip_with ()))
771
  (at level 50, left associativity) : stdpp_scope.
772
Infix "∪*∪**" := (zip_with (prod_zip () (*)))
773
  (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
774

775
Definition union_list `{Empty A} `{Union A} : list A  A := fold_right () .
776
Arguments union_list _ _ _ !_ / : assert.
777
Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
778

Robbert Krebbers's avatar
Robbert Krebbers committed
779
Class Intersection A := intersection: A  A  A.
780
Hint Mode Intersection ! : typeclass_instances.
781
Instance: Params (@intersection) 2.
782 783 784 785
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
786 787

Class Difference A := difference: A  A  A.
788
Hint Mode Difference ! : typeclass_instances.
789
Instance: Params (@difference) 2.
790 791 792 793 794 795
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.
796
Infix "∖**" := (zip_with (zip_with ()))
797
  (at level 40, left associativity) : stdpp_scope.
798
Infix "∖*∖**" := (zip_with (prod_zip () (*)))
799
  (at level 50, left associativity) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
800

801
Class Singleton A B := singleton: A  B.
802
Hint Mode Singleton - ! : typeclass_instances.
803
Instance: Params (@singleton) 3.
804
Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
805
Notation "{[ x ; y ; .. ; z ]}" :=
806
  (union .. (union (singleton x) (singleton y)) .. (singleton z))
807
  (at level 1) : stdpp_scope.
808
Notation "{[ x , y ]}" := (singleton (x,y))
809
  (at level 1, y at next level) : stdpp_scope.
810
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
811
  (at level 1, y at next level, z at next level) : stdpp_scope.
812

813
Class SubsetEq A := subseteq: relation A.
814
Hint Mode SubsetEq ! : typeclass_instances.
815
Instance: Params (@subseteq) 2.
816 817 818 819 820 821 822 823
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.
824 825 826 827

Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.

828 829 830 831 832 833 834
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
835

836 837 838
Hint Extern 0 (_  _) => reflexivity : core.
Hint Extern 0 (_ * _) => reflexivity : core.
Hint Extern 0 (_ ** _) => reflexivity : core.
839

840 841 842 843 844 845 846 847
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
848

849 850 851
Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope.
Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope.

852 853 854 855
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.
856

857 858 859 860
(** 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.
861
Hint Mode Lexico ! : typeclass_instances.
862

Robbert Krebbers's avatar
Robbert Krebbers committed
863
Class ElemOf A B := elem_of: A  B  Prop.
864
Hint Mode ElemOf - ! : typeclass_instances.
865
Instance: Params (@elem_of) 3.
866 867 868 869 870 871 872 873
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
874

Robbert Krebbers's avatar
Robbert Krebbers committed
875 876 877
Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
878
Class Disjoint A := disjoint : A  A  Prop.
879
 Hint Mode Disjoint ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
880
Instance: Params (@disjoint) 2.
881 882 883 884
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
885 886 887 888

Infix "##@{ A }" := (@disjoint A _) (at level 70, only parsing) : stdpp_scope.
Notation "(##@{ A } )" := (@disjoint A _) (only parsing) : stdpp_scope.

889 890 891 892 893 894 895
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.
896 897
Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
898 899

Class DisjointE E A := disjointE : E  A  A  Prop.
900
Hint Mode DisjointE - ! : typeclass_instances.
901
Instance: Params (@disjointE) 4.
902
Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
903 904
  (at level 70, format "X  ##{ Γ }  Y") : stdpp_scope.
Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : stdpp_scope.
905
Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
906
  (at level 70, format "Xs  ##{ Γ }*  Ys") : stdpp_scope.
907
Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
908
  (only parsing, Γ at level 1) : stdpp_scope.
909
Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
910
  (at level 70, format "X  ##{ Γ1 , Γ2 , .. , Γ3 }  Y") : stdpp_scope.
911
Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
912
  (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
913
  (at level 70, format "Xs  ##{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : stdpp_scope.
914
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
915 916

Class DisjointList A := disjoint_list : list A  Prop.
917
Hint Mode DisjointList ! : typeclass_instances.
918
Instance: Params (@disjoint_list) 2.
919
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "##  Xs") : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
920 921
Notation "##@{ A } Xs" :=
  (@disjoint_list A _ Xs) (at level 20, only parsing) : stdpp_scope.
922

923 924
Section disjoint_list.
  Context `{Disjoint A, Union A, Empty A}.
925 926
  Implicit Types X : A.

927
  Inductive disjoint_list_default : DisjointList A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
928
    | disjoint_nil_2 : ##@{A} []
929
    | disjoint_cons_2 (X : A) (Xs : list A) : X ##  Xs  ## Xs  ## (X :: Xs).
930
  Global Existing Instance disjoint_list_default.
931

Robbert Krebbers's avatar
Robbert Krebbers committed
932
  Lemma disjoint_list_nil  : ##@{A} []  True.
933
  Proof. split; constructor. Qed.
934
  Lemma disjoint_list_cons X Xs : ## (X :: Xs)  X ##  Xs  ## Xs.
935
  Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.