base.v 42.8 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8
Global Generalizable All Variables.
Global Set Automatic Coercions Import.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Global Set Asymmetric Patterns.
10
Global Unset Transparent Obligations.
11
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
12
Set Default Proof Using "Type".
13 14
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
15 16 17

(* Tweak program: don't let it automatically simplify obligations and hide
them from the results of the [Search] commands. *)
18
Obligation Tactic := idtac.
19
Add Search Blacklist "_obligation_".
Robbert Krebbers's avatar
Robbert Krebbers committed
20

21 22 23 24 25 26 27
(** Sealing off definitions *)
Set Primitive Projections.
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
Arguments unseal {_ _} _.
Arguments seal_eq {_ _} _.
Unset Primitive Projections.

Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30 31 32 33 34 35 36 37
(* The [Or] class is useful for efficiency: instead of having two instances
[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
which avoids the need to derive [P] twice. *)
Inductive Or (P1 P2 : Type) :=
  | Or_l : P1  Or P1 P2
  | Or_r : P2  Or P1 P2.
Existing Class Or.
Existing Instance Or_l | 9.
Existing Instance Or_r | 10.

38 39 40 41
(** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Delimit Scope C_scope with C.
Global Open Scope C_scope.
42

43
(** Change [True] and [False] into notations in order to enable overloading.
44 45
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
46 47
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49


50
(** * Equality *)
51
(** Introduce some Haskell style like notations. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54 55 56 57 58
Notation "(=)" := eq (only parsing) : C_scope.
Notation "( x =)" := (eq x) (only parsing) : C_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : C_scope.
Notation "(≠)" := (λ x y, x  y) (only parsing) : C_scope.
Notation "( x ≠)" := (λ y, x  y) (only parsing) : C_scope.
Notation "(≠ x )" := (λ y, y  x) (only parsing) : C_scope.

59
Hint Extern 0 (_ = _) => reflexivity.
60
Hint Extern 100 (_  _) => discriminate.
Robbert Krebbers's avatar
Robbert Krebbers committed
61

62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
Instance: @PreOrder A (=).
Proof. split; repeat intro; congruence. Qed.

(** ** Setoid equality *)
(** We define an operational type class for setoid equality. This is based on
(Spitters/van der Weegen, 2011). *)
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : C_scope.
Notation "(≡)" := equiv (only parsing) : C_scope.
Notation "( X ≡)" := (equiv X) (only parsing) : C_scope.
Notation "(≡ X )" := (λ Y, Y  X) (only parsing) : C_scope.
Notation "(≢)" := (λ X Y, ¬X  Y) (only parsing) : C_scope.
Notation "X ≢ Y":= (¬X  Y) (at level 70, no associativity) : C_scope.
Notation "( X ≢)" := (λ Y, X  Y) (only parsing) : C_scope.
Notation "(≢ X )" := (λ Y, Y  X) (only parsing) : C_scope.

(** 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.
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
  x  y  x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
 
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
propositions. For example to declare a parameter expressing decidable equality
on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing
[decide (x = y)]. *)
Class Decision (P : Prop) := decide : {P} + {¬P}.
Arguments decide _ {_}.
125
Notation EqDecision A := ( x y : A, Decision (x = y)).
126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 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 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 210 211 212 213 214 215 216 217 218 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 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277

(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Arguments populate {_} _.

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

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

Arguments irreflexivity {_} _ {_} _ _.
Arguments inj {_ _ _ _} _ {_} _ _ _.
Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
Arguments cancel {_ _ _} _ _ {_} _.
Arguments surj {_ _ _} _ {_} _.
Arguments idemp {_ _} _ {_} _.
Arguments comm {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
Arguments right_id {_ _} _ _ {_} _.
Arguments assoc {_ _} _ {_} _ _ _.
Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
Arguments anti_symm {_ _} _ {_} _ _ _ _.
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.

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

Notation "(∨)" := or (only parsing) : C_scope.
Notation "( A ∨)" := (or A) (only parsing) : C_scope.
Notation "(∨ B )" := (λ A, A  B) (only parsing) : C_scope.

Notation "(↔)" := iff (only parsing) : C_scope.
Notation "( A ↔)" := (iff A) (only parsing) : C_scope.
Notation "(↔ B )" := (λ A, A  B) (only parsing) : C_scope.

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.
278 279 280 281 282 283
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.
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

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 *)
327 328 329 330
Notation "(→)" := (λ A B, A  B) (only parsing) : C_scope.
Notation "( A →)" := (λ B, A  B) (only parsing) : C_scope.
Notation "(→ B )" := (λ A, A  B) (only parsing) : C_scope.

331
Notation "t $ r" := (t r)
332
  (at level 65, right associativity, only parsing) : C_scope.
333 334 335
Notation "($)" := (λ f x, f x) (only parsing) : C_scope.
Notation "($ x )" := (λ f, f x) (only parsing) : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
336 337 338 339
Infix "∘" := compose : C_scope.
Notation "(∘)" := compose (only parsing) : C_scope.
Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
Notation "(∘ f )" := (λ g, compose g f) (only parsing) : C_scope.
340

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

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 404 405 406
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
Arguments id _ _ /.
Arguments compose _ _ _ _ _ _ /.
Arguments flip _ _ _ _ _ _ /.
Arguments const _ _ _ _ /.
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.
407

408 409 410 411 412
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.
413

414 415 416 417 418 419 420 421
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.
422

423 424 425 426
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.
427 428
Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
429
Instance unit_inhabited: Inhabited unit := populate ().
430

431
(** ** Products *)
432 433 434 435 436 437
Notation "( x ,)" := (pair x) (only parsing) : C_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.

Notation "p .1" := (fst p) (at level 10, format "p .1").
Notation "p .2" := (snd p) (at level 10, format "p .2").

438
Instance: Params (@pair) 2.
439 440
Instance: Params (@fst) 2.
Instance: Params (@snd) 2.
441

442 443 444 445 446 447 448 449 450
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.

Definition prod_map {A A' B B'} (f: A  A') (g: B  B') (p : A * B) : A' * B' :=
  (f (p.1), g (p.2)).
451
Arguments prod_map {_ _ _ _} _ _ !_ /.
452

453 454 455 456
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)).
Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ /.

457 458 459
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.
460

461 462 463 464 465 466 467 468
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.
469

470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485
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.
486

487 488
  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
  Proof. firstorder eauto. Qed.
489 490
  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
  Proof. inversion_clear 1; eauto. Qed.
491 492 493 494 495
  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
496

497 498
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Instance pair_proper `{Equiv A, Equiv B} :
499 500
  Proper (() ==> () ==> ()) (@pair A B) := _.
Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B) := _.
501 502 503
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.
504

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

508
(** ** Sums *)
509 510 511 512
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.
Arguments sum_map {_ _ _ _} _ _ !_ /.

513
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
514
  match iA with populate x => populate (inl x) end.
515
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
516
  match iB with populate y => populate (inl y) end.
517

518 519 520 521
Instance inl_inj : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
Instance inr_inj : Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
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 549
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.
550 551 552 553
  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.
554 555 556 557 558
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) := _.
559 560
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inl A B) := _.
Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inr A B) := _.
561 562
Typeclasses Opaque sum_equiv.

563 564
(** ** Option *)
Instance option_inhabited {A} : Inhabited (option A) := populate None.
Robbert Krebbers's avatar
Robbert Krebbers committed
565

566 567
(** ** Sigma types *)
Arguments existT {_ _} _ _.
568 569 570 571
Arguments projT1 {_ _} _.
Arguments projT2 {_ _} _.

Arguments exist {_} _ _ _.
572
Arguments proj1_sig {_ _} _.
573
Arguments proj2_sig {_ _} _.
574 575
Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : C_scope.
576

577 578 579
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.
580

581 582 583 584 585 586 587 588 589 590 591
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.
Arguments sig_map _ _ _ _ _ _ !_ /.
592

Robbert Krebbers's avatar
Robbert Krebbers committed
593

594
(** * Operations on collections *)
595
(** We define operational type classes for the traditional operations and
596
relations on collections: the empty collection [∅], the union [(∪)],
597 598
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
599 600 601
Class Empty A := empty: A.
Notation "∅" := empty : C_scope.

602 603
Instance empty_inhabited `(Empty A) : Inhabited A := populate .

604 605 606
Class Top A := top : A.
Notation "⊤" := top : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
607
Class Union A := union: A  A  A.
608
Instance: Params (@union) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
609 610 611 612
Infix "∪" := union (at level 50, left associativity) : C_scope.
Notation "(∪)" := union (only parsing) : C_scope.
Notation "( x ∪)" := (union x) (only parsing) : C_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : C_scope.
613 614 615 616 617 618
Infix "∪*" := (zip_with ()) (at level 50, left associativity) : C_scope.
Notation "(∪*)" := (zip_with ()) (only parsing) : C_scope.
Infix "∪**" := (zip_with (zip_with ()))
  (at level 50, left associativity) : C_scope.
Infix "∪*∪**" := (zip_with (prod_zip () (*)))
  (at level 50, left associativity) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
619

620
Definition union_list `{Empty A} `{Union A} : list A  A := fold_right () .
621 622 623
Arguments union_list _ _ _ !_ /.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
624
Class Intersection A := intersection: A  A  A.
625
Instance: Params (@intersection) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
626 627 628 629 630 631
Infix "∩" := intersection (at level 40) : C_scope.
Notation "(∩)" := intersection (only parsing) : C_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : C_scope.
Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.

Class Difference A := difference: A  A  A.
632
Instance: Params (@difference) 2.
633
Infix "∖" := difference (at level 40, left associativity) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
634 635 636
Notation "(∖)" := difference (only parsing) : C_scope.
Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
637 638 639 640 641 642
Infix "∖*" := (zip_with ()) (at level 40, left associativity) : C_scope.
Notation "(∖*)" := (zip_with ()) (only parsing) : C_scope.
Infix "∖**" := (zip_with (zip_with ()))
  (at level 40, left associativity) : C_scope.
Infix "∖*∖**" := (zip_with (prod_zip () (*)))
  (at level 50, left associativity) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
643

644 645
Class Singleton A B := singleton: A  B.
Instance: Params (@singleton) 3.
646
Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope.
647
Notation "{[ x ; y ; .. ; z ]}" :=
648 649 650 651 652 653
  (union .. (union (singleton x) (singleton y)) .. (singleton z))
  (at level 1) : C_scope.
Notation "{[ x , y ]}" := (singleton (x,y))
  (at level 1, y at next level) : C_scope.
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
  (at level 1, y at next level, z at next level) : C_scope.
654

655
Class SubsetEq A := subseteq: relation A.
656
Instance: Params (@subseteq) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
657 658
Infix "⊆" := subseteq (at level 70) : C_scope.
Notation "(⊆)" := subseteq (only parsing) : C_scope.
659 660
Notation "( X ⊆)" := (subseteq X) (only parsing) : C_scope.
Notation "(⊆ X )" := (λ Y, Y  X) (only parsing) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
661 662
Notation "X ⊈ Y" := (¬X  Y) (at level 70) : C_scope.
Notation "(⊈)" := (λ X Y, X  Y) (only parsing) : C_scope.
663 664
Notation "( X ⊈)" := (λ Y, X  Y) (only parsing) : C_scope.
Notation "(⊈ X )" := (λ Y, Y  X) (only parsing) : C_scope.
665 666 667 668 669 670 671
Infix "⊆*" := (Forall2 ()) (at level 70) : C_scope.
Notation "(⊆*)" := (Forall2 ()) (only parsing) : C_scope.
Infix "⊆**" := (Forall2 (*)) (at level 70) : C_scope.
Infix "⊆1*" := (Forall2 (λ p q, p.1  q.1)) (at level 70) : C_scope.
Infix "⊆2*" := (Forall2 (λ p q, p.2  q.2)) (at level 70) : C_scope.
Infix "⊆1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : C_scope.
Infix "⊆2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
672

673
Hint Extern 0 (_  _) => reflexivity.
674 675 676 677 678
Hint Extern 0 (_ * _) => reflexivity.
Hint Extern 0 (_ ** _) => reflexivity.

Infix "⊂" := (strict ()) (at level 70) : C_scope.
Notation "(⊂)" := (strict ()) (only parsing) : C_scope.
679 680 681
Notation "( X ⊂)" := (strict () X) (only parsing) : C_scope.
Notation "(⊂ X )" := (λ Y, Y  X) (only parsing) : C_scope.
Notation "X ⊄ Y" := (¬X  Y) (at level 70) : C_scope.
682
Notation "(⊄)" := (λ X Y, X  Y) (only parsing) : C_scope.
683 684
Notation "( X ⊄)" := (λ Y, X  Y) (only parsing) : C_scope.
Notation "(⊄ X )" := (λ Y, Y  X) (only parsing) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
685

686 687 688 689 690
Notation "X ⊆ Y ⊆ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊆ Y ⊂ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊂ Y ⊆ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊂ Y ⊂ Z" := (X  Y  Y  Z) (at level 70, Y at next level) : C_scope.

691 692 693 694 695
(** 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
696
Class ElemOf A B := elem_of: A  B  Prop.
697
Instance: Params (@elem_of) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
698 699 700 701 702 703 704 705 706
Infix "∈" := elem_of (at level 70) : C_scope.
Notation "(∈)" := elem_of (only parsing) : C_scope.
Notation "( x ∈)" := (elem_of x) (only parsing) : C_scope.
Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : C_scope.
Notation "x ∉ X" := (¬x  X) (at level 80) : C_scope.
Notation "(∉)" := (λ x X, x  X) (only parsing) : C_scope.
Notation "( x ∉)" := (λ X, x  X) (only parsing) : C_scope.
Notation "(∉ X )" := (λ x, x  X) (only parsing) : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
707 708 709 710
Class Disjoint A := disjoint : A  A  Prop.
Instance: Params (@disjoint) 2.
Infix "⊥" := disjoint (at level 70) : C_scope.
Notation "(⊥)" := disjoint (only parsing) : C_scope.
711
Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
712
Notation "(.⊥ X )" := (λ Y, Y  X) (only parsing) : C_scope.
713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737
Infix "⊥*" := (Forall2 ()) (at level 70) : C_scope.
Notation "(⊥*)" := (Forall2 ()) (only parsing) : C_scope.
Infix "⊥**" := (Forall2 (*)) (at level 70) : C_scope.
Infix "⊥1*" := (Forall2 (λ p q, p.1  q.1)) (at level 70) : C_scope.
Infix "⊥2*" := (Forall2 (λ p q, p.2  q.2)) (at level 70) : C_scope.
Infix "⊥1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : C_scope.
Infix "⊥2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : C_scope.
Hint Extern 0 (_  _) => symmetry; eassumption.
Hint Extern 0 (_ * _) => symmetry; eassumption.

Class DisjointE E A := disjointE : E  A  A  Prop.
Instance: Params (@disjointE) 4.
Notation "X ⊥{ Γ } Y" := (disjointE Γ X Y)
  (at level 70, format "X  ⊥{ Γ }  Y") : C_scope.
Notation "(⊥{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : C_scope.
Notation "Xs ⊥{ Γ }* Ys" := (Forall2 ({Γ}) Xs Ys)
  (at level 70, format "Xs  ⊥{ Γ }*  Ys") : C_scope.
Notation "(⊥{ Γ }* )" := (Forall2 ({Γ}))
  (only parsing, Γ at level 1) : C_scope.
Notation "X ⊥{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
  (at level 70, format "X  ⊥{ Γ1 , Γ2 , .. , Γ3 }  Y") : C_scope.
Notation "Xs ⊥{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
  (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
  (at level 70, format "Xs  ⊥{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : C_scope.
Hint Extern 0 (_ {_} _) => symmetry; eassumption.
738 739 740

Class DisjointList A := disjoint_list : list A  Prop.
Instance: Params (@disjoint_list) 2.
741
Notation "⊥ Xs" := (disjoint_list Xs) (at level 20, format "⊥  Xs") : C_scope.
742

743 744 745 746 747 748
Section disjoint_list.
  Context `{Disjoint A, Union A, Empty A}.
  Inductive disjoint_list_default : DisjointList A :=
    | disjoint_nil_2 :  (@nil A)
    | disjoint_cons_2 (X : A) (Xs : list A) : X   Xs   Xs   (X :: Xs).
  Global Existing Instance disjoint_list_default.
749

750
  Lemma disjoint_list_nil  :  @nil A  True.
751 752 753
  Proof. split; constructor. Qed.
  Lemma disjoint_list_cons X Xs :  (X :: Xs)  X   Xs   Xs.
  Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
754
End disjoint_list.
755 756

Class Filter A B := filter:  (P : A  Prop) `{ x, Decision (P x)}, B  B.
757

758 759
Class UpClose A B := up_close : A  B.
Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
760 761

(** * Monadic operations *)
762
(** We define operational type classes for the monadic operations bind, join 
763 764 765
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). *)
766 767
Class MRet (M : Type  Type) := mret:  {A}, A  M A.
Arguments mret {_ _ _} _.
768
Instance: Params (@mret) 3.
769 770
Class MBind (M : Type  Type) := mbind :  {A B}, (A  M B)  M A  M B.
Arguments mbind {_ _ _ _} _ !_ /.
771
Instance: Params (@mbind) 4.
772
Class MJoin (M : Type  Type) := mjoin:  {A}, M (M A)  M A.
773
Arguments mjoin {_ _ _} !_ /.
774
Instance: Params (@mjoin) 3.
775 776
Class FMap (M : Type  Type) := fmap :  {A B}, (A  B)  M A  M B.
Arguments fmap {_ _ _ _} _ !_ /.
777
Instance: Params (@fmap) 4.
778 779
Class OMap (M : Type  Type) := omap:  {A B}, (A  option B)  M A  M B.
Arguments omap {_ _ _ _} _ !_ /.
780
Instance: Params (@omap) 4.
781

782 783 784 785 786 787
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.

Notation "x ← y ; z" := (y = (λ x : _, z))
Robbert Krebbers's avatar
Robbert Krebbers committed
788
  (at level 65, only parsing, right associativity) : C_scope.
789
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
790
Notation "' ( x1 , x2 ) ← y ; z" :=
791
  (y = (λ x : _, let ' (x1, x2) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
792
  (at level 65, only parsing, right associativity) : C_scope.
793
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
794
  (y = (λ x : _, let ' (x1,x2,x3) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
795
  (at level 65, only parsing, right associativity) : C_scope.
796
Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
797
  (y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
798
  (at level 65, only parsing, right associativity) : C_scope.
799 800
Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
  (y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
801
  (at level 65, only parsing, right associativity) : C_scope.
802 803
Notation "' ( x1 , x2 , x3  , x4 , x5 , x6 ) ← y ; z" :=
  (y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
804
  (at level 65, only parsing, right associativity) : C_scope.
805

806 807 808 809 810
Notation "ps .*1" := (fmap (M:=list) fst ps)
  (at level 10, format "ps .*1").
Notation "ps .*2" := (fmap (M:=list) snd ps)
  (at level 10, format "ps .*2").

811
Class MGuard (M : Type  Type) :=
812 813 814
  mguard:  P {dec : Decision P} {A}, (P  M A)  M A.
Arguments mguard _ _ _ !_ _ _ /.
Notation "'guard' P ; o" := (mguard P (λ _, o))
Robbert Krebbers's avatar
Robbert Krebbers committed
815
  (at level 65, only parsing, right associativity) : C_scope.
816
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
Robbert Krebbers's avatar
Robbert Krebbers committed
817
  (at level 65, only parsing, right associativity) : C_scope.
818

819 820

(** * Operations on maps *)
821 822
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
823
The function look up [m !! k] should yield the element at key [k] in [m]. *)
824
Class Lookup (K A M : Type) := lookup: K  M  option A.
825 826 827
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope.
828
Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
829
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
830
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
831

832
(** The singleton map *)
833
Class SingletonM K A M := singletonM: K  A  M.
834
Instance: Params (@singletonM) 5.
835
Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
836

837 838
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
839
Class Insert (K A M : Type) := insert: K  A  M  M.
Robbert Krebbers's avatar
Robbert Krebbers committed
840
Instance: Params (@insert) 5.
841 842
Notation "<[ k := a ]>" := (insert k a)
  (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
843
Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
844

845 846 847
(** The function delete [delete k m] should delete the value at key [k] in
[m]. If the key [k] is not a member of [m], the original map should be
returned. *)
848 849 850
Class Delete (K M : Type) := delete: K  M  M.
Instance: Params (@delete) 4.
Arguments delete _ _ _ !_ !_ / : simpl nomatch.
851 852

(** The function [alter f k m] should update the value at key [k] using the
853
function [f], which is called with the original value. *)
854
Class Alter (K A M : Type) := alter: (A  A)  K  M  M.
855
Instance: Params (@alter) 5.
856
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
857 858

(** The function [alter f k m] should update the value at key [k] using the
859 860 861
function [f], which is called with the original value at key [k] or [None]
if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
yields [None]. *)
862 863
Class PartialAlter (K A M : Type) :=
  partial_alter: (option A  option A)  K  M  M.
864
Instance: Params (@partial_alter) 4.
865
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
866 867 868

(** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *)
869 870
Class Dom (M C : Type) := dom: M  C.
Instance: Params (@dom) 3.
Ralf Jung's avatar
Ralf Jung committed
871 872
Arguments dom _ _ _ _ : clear implicits.
Arguments dom {_} _ {_} !_ / : simpl nomatch.
873 874

(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
875 876 877 878 879
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
Class Merge (M : Type  Type) :=
  merge:  {A B C}, (option A  option B  option C)  M A  M B  M C.
Instance: Params (@merge) 4.
Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
880

881 882 883
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
and [m2] using the function [f] to combine values of members that are in
both [m1] and [m2]. *)
884 885
Class UnionWith (A M : Type) :=
  union_with: (A  A  option A)  M  M  M.
886 887
Instance: Params (@union_with) 3.
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
888

889
(** Similarly for intersection and difference. *)
890 891
Class IntersectionWith (A M : Type) :=
  intersection_with: (A  A  option A)  M  M  M.
892 893
Instance: Params (@intersection_with) 3.
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.
894

895 896
Class DifferenceWith (A M : Type) :=
  difference_with: (A  A  option A)  M  M  M.
897 898
Instance: Params (@difference_with) 3.
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
899

900 901
Definition intersection_with_list `{IntersectionWith A M}
  (f : A  A  option A) : M  list M  M := fold_right (intersection_with f).
902 903
Arguments intersection_with_list _ _ _ _ _ !_ /.

904 905 906 907 908 909 910 911 912 913 914 915 916
Class LookupE (E K A M : Type) := lookupE: E  K  M  option A.
Instance: Params (@lookupE) 6.
Notation "m !!{ Γ } i" := (lookupE Γ i m)
  (at level 20, format "m  !!{ Γ }  i") : C_scope.
Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch.

Class InsertE (E K A M : Type) := insertE: E  K  A  M  M.
Instance: Params (@insertE) 6.
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.

917

918
(** * Axiomatization of collections *)
919 920
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *)
921 922
Class SimpleCollection A C `{ElemOf A C,
    Empty C, Singleton A C, Union C} : Prop := {
923
  not_elem_of_empty (x : A) : x  ;
924
  elem_of_singleton (x y : A) : x  {[ y ]}  x = y;
925 926
  elem_of_union X Y (x : A) : x  X  Y  x  X  x  Y
}.
927 928
Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
    Union C, Intersection C, Difference C} : Prop := {
929
  collection_simple :>> SimpleCollection A C;
Robbert Krebbers's avatar
Robbert Krebbers committed
930
  elem_of_intersection X Y (x : A) : x  X  Y  x  X  x  Y;
931 932
  elem_of_difference X Y (x : A) : x  X  Y  x  X  x  Y
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
933

934 935 936
(** We axiomative a finite collection as a collection whose elements can be
enumerated as a list. These elements, given by the [elements] function, may be
in any order and should not contain duplicates. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
937
Class Elements A C := elements: C  list A.
938
Instance: Params (@elements) 3.
939 940 941 942 943 944 945

(** We redefine the standard library's [In] and [NoDup] using type classes. *)
Inductive elem_of_list {A} : ElemOf A (list A) :=
  | elem_of_list_here (x : A) l : x  x :: l
  | elem_of_list_further (x y : A) l : x  l  x  y :: l.
Existing Instance elem_of_list.

Robbert Krebbers's avatar
Robbert Krebbers committed
946
Lemma elem_of_list_In {A} (l : list A) x : x  l  In x l.
947
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
948 949
  split.
  - induction 1; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
950
  - induction l; destruct 1; subst; constructor; auto.
951 952
Qed.

953 954 955 956
Inductive NoDup {A} : list A  Prop :=
  | NoDup_nil_2 : NoDup []
  | NoDup_cons_2 x l : x  l  NoDup l  NoDup (x :: l).

Robbert Krebbers's avatar
Robbert Krebbers committed
957
Lemma NoDup_ListNoDup {A} (l : list A) : NoDup l  List.NoDup l.
958
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
959 960 961
  split.
  - induction 1; constructor; rewrite <-?elem_of_list_In; auto.
  - induction 1; constructor; rewrite ?elem_of_list_In; auto.
962 963
Qed.

964 965
(** Decidability of equality of the carrier set is admissible, but we add it
anyway so as to avoid cycles in type class search. *)
966 967
Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
    Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
968
  fin_collection :>> Collection A C;
969 970
  elem_of_elements X x : x  elements X  x  X;
  NoDup_elements X : NoDup (elements X)
971 972
}.
Class Size C := size: C  nat.