base.v 43.1 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
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
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
(** * General *)
13 14 15 16 17
(** Zipping lists. *)
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).
18

19 20
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
21
Arguments id _ _ /.
22
Arguments compose _ _ _ _ _ _ /.
23
Arguments flip _ _ _ _ _ _ /.
24 25
Arguments const _ _ _ _ /.
Typeclasses Transparent id compose flip const.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Instance: Params (@pair) 2.
27

28 29 30 31
(** Change [True] and [False] into notations in order to enable overloading.
We will use this in the file [assertions] to give [True] and [False] a
different interpretation in [assert_scope] used for assertions of our axiomatic
semantics. *)
32 33
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
34

35 36
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
37 38 39 40
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.
41

42 43
(** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46
Delimit Scope C_scope with C.
Global Open Scope C_scope.

47
(** Introduce some Haskell style like notations. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51 52 53 54 55
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.

Hint Extern 0 (?x = ?x) => reflexivity.
56
Hint Extern 100 (_  _) => discriminate.
Robbert Krebbers's avatar
Robbert Krebbers committed
57

58 59 60 61
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.

62
Notation "t $ r" := (t r)
63
  (at level 65, right associativity, only parsing) : C_scope.
64 65 66
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
67 68 69 70
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.
71

72 73 74 75 76 77 78 79 80 81 82 83
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.

84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
Hint Extern 0 (_  _) => reflexivity.
Hint Extern 0 (_  _) => symmetry; assumption.

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").

Definition prod_map {A A' B B'} (f : A  A') (g : B  B')
  (p : A * B) : A' * B' := (f (p.1), g (p.2)).
Arguments prod_map {_ _ _ _} _ _ !_ /.
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 {_ _ _ _ _ _} _ _ !_ !_ /.

100 101
(** Set convenient implicit arguments for [existT] and introduce notations. *)
Arguments existT {_ _} _ _.
102
Arguments proj1_sig {_ _} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
104
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
105

106 107 108 109
(** * Type classes *)
(** ** Provable propositions *)
(** This type class collects provable propositions. It is useful to constraint
type classes by arbitrary propositions. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111
Class PropHolds (P : Prop) := prop_holds: P.

112 113
Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
Instance: Proper (iff ==> iff) PropHolds.
114
Proof. repeat intro; trivial. Qed.
115 116 117

Ltac solve_propholds :=
  match goal with
118 119
  | |- PropHolds (?P) => apply _
  | |- ?P => change (PropHolds P); apply _
120 121 122 123 124 125 126
  end.

(** ** 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)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129
Class Decision (P : Prop) := decide : {P} + {¬P}.
Arguments decide _ {_}.

130 131 132 133 134 135 136 137 138
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Prop := populate { _ : A }.
Arguments populate {_} _.

Instance unit_inhabited: Inhabited unit := populate ().
Instance list_inhabited {A} : Inhabited (list A) := populate [].
Instance prod_inhabited {A B} (iA : Inhabited A)
    (iB : Inhabited B) : Inhabited (A * B) :=
139
  match iA, iB with populate x, populate y => populate (x,y) end.
140
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
141
  match iA with populate x => populate (inl x) end.
142
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
143
  match iB with populate y => populate (inl y) end.
144 145
Instance option_inhabited {A} : Inhabited (option A) := populate None.

146 147 148 149 150 151
(** ** 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.

152 153 154
(** ** Setoid equality *)
(** We define an operational type class for setoid equality. This is based on
(Spitters/van der Weegen, 2011). *)
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : C_scope.
Notation "(≡)" := equiv (only parsing) : C_scope.
158 159 160 161 162 163
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
164

165 166 167 168 169
Class EquivE E A := equivE: E  relation A.
Instance: Params (@equivE) 4.
Notation "X ≡{ Γ } Y" := (equivE Γ X Y)
  (at level 70, format "X  ≡{ Γ }  Y") : C_scope.
Notation "(≡{ Γ } )" := (equivE Γ) (only parsing, Γ at level 1) : C_scope.
170 171 172 173 174
Notation "X ≡{ Γ1 , Γ2 , .. , Γ3 } Y" :=
  (equivE (pair .. (Γ1, Γ2) .. Γ3) X Y)
  (at level 70, format "'[' X  ≡{ Γ1 , Γ2 , .. , Γ3 }  '/' Y ']'") : C_scope.
Notation "(≡{ Γ1 , Γ2 , .. , Γ3 } )" := (equivE (pair .. (Γ1, Γ2) .. Γ3))
  (only parsing, Γ1 at level 1) : C_scope.
175

176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
(** 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.

Ltac fold_leibniz := repeat
  match goal with
  | H : context [ @equiv ?A _ _ _ ] |- _ =>
    setoid_rewrite (leibniz_equiv (A:=A)) in H
  | |- context [ @equiv ?A _ _ _ ] =>
    setoid_rewrite (leibniz_equiv (A:=A))
  end.
Ltac unfold_leibniz := repeat
  match goal with
  | H : context [ @eq ?A _ _ ] |- _ =>
    setoid_rewrite <-(leibniz_equiv (A:=A)) in H
  | |- context [ @eq ?A _ _ ] =>
    setoid_rewrite <-(leibniz_equiv (A:=A))
  end.

197 198 199 200 201 202 203 204
(** 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
206 207
Hint Extern 0 (_  _) => reflexivity.
Hint Extern 0 (_  _) => symmetry; assumption.
208 209
Hint Extern 0 (_ {_} _) => reflexivity.
Hint Extern 0 (_ {_} _) => symmetry; assumption.
Robbert Krebbers's avatar
Robbert Krebbers committed
210

211
(** ** Operations on collections *)
212
(** We define operational type classes for the traditional operations and
213
relations on collections: the empty collection [∅], the union [(∪)],
214 215
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218 219
Class Empty A := empty: A.
Notation "∅" := empty : C_scope.

Class Union A := union: A  A  A.
220
Instance: Params (@union) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
221 222 223 224
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.
225 226 227 228 229 230
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
231

232
Definition union_list `{Empty A} `{Union A} : list A  A := fold_right () .
233 234 235
Arguments union_list _ _ _ !_ /.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
236
Class Intersection A := intersection: A  A  A.
237
Instance: Params (@intersection) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
238 239 240 241 242 243
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.
244
Instance: Params (@difference) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247 248
Infix "∖" := difference (at level 40) : C_scope.
Notation "(∖)" := difference (only parsing) : C_scope.
Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
249 250 251 252 253 254
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
255

256 257
Class Singleton A B := singleton: A  B.
Instance: Params (@singleton) 3.
258
Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope.
259
Notation "{[ x ; y ; .. ; z ]}" :=
260 261 262 263 264 265
  (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.
266

267
Class SubsetEq A := subseteq: relation A.
268
Instance: Params (@subseteq) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
269 270 271
Infix "⊆" := subseteq (at level 70) : C_scope.
Notation "(⊆)" := subseteq (only parsing) : C_scope.
Notation "( X ⊆ )" := (subseteq X) (only parsing) : C_scope.
272
Notation "( ⊆ X )" := (λ Y, Y  X) (only parsing) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
273 274 275 276
Notation "X ⊈ Y" := (¬X  Y) (at level 70) : 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.
277 278 279 280 281 282 283
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
284

285
Hint Extern 0 (_  _) => reflexivity.
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
Hint Extern 0 (_ * _) => reflexivity.
Hint Extern 0 (_ ** _) => reflexivity.

Class SubsetEqE E A := subseteqE: E  relation A.
Instance: Params (@subseteqE) 4.
Notation "X ⊆{ Γ } Y" := (subseteqE Γ X Y)
  (at level 70, format "X  ⊆{ Γ }  Y") : C_scope.
Notation "(⊆{ Γ } )" := (subseteqE Γ) (only parsing, Γ at level 1) : C_scope.
Notation "X ⊈{ Γ } Y" := (¬X {Γ} Y)
  (at level 70, format "X  ⊈{ Γ }  Y") : C_scope.
Notation "(⊈{ Γ } )" := (λ X Y, X {Γ} Y)
  (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" :=
  (subseteqE (pair .. (Γ1, Γ2) .. Γ3) X Y)
  (at level 70, format "'[' X  ⊆{ Γ1 , Γ2 , .. , Γ3 }  '/' Y ']'") : C_scope.
Notation "(⊆{ Γ1 , Γ2 , .. , Γ3 } )" := (subseteqE (pair .. (Γ1, Γ2) .. Γ3))
  (only parsing, Γ1 at level 1) : C_scope.
Notation "X ⊈{ Γ1 , Γ2 , .. , Γ3 } Y" := (¬X {pair .. (Γ1, Γ2) .. Γ3} Y)
  (at level 70, format "X  ⊈{ Γ1 , Γ2 , .. , Γ3 }  Y") : C_scope.
Notation "(⊈{ Γ1 , Γ2 , .. , Γ3 } )" := (λ X Y, X {pair .. (Γ1, Γ2) .. Γ3} Y)
  (only parsing) : C_scope.
Notation "Xs ⊆{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
  (Forall2 ({pair .. (Γ1, Γ2) .. Γ3}) Xs Ys)
  (at level 70, format "Xs  ⊆{ Γ1 , Γ2 , .. , Γ3 }*  Ys") : C_scope.
Notation "(⊆{ Γ1 , Γ2 , .. , Γ3 }* )" := (Forall2 ({pair .. (Γ1, Γ2) .. Γ3}))
  (only parsing, Γ1 at level 1) : C_scope.
Hint Extern 0 (_ {_} _) => reflexivity.
317

318 319
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y  ¬R Y X.
Instance: Params (@strict) 2.
320 321 322 323
Infix "⊂" := (strict ()) (at level 70) : C_scope.
Notation "(⊂)" := (strict ()) (only parsing) : C_scope.
Notation "( X ⊂ )" := (strict () X) (only parsing) : C_scope.
Notation "( ⊂ X )" := (λ Y, Y  X) (only parsing) : C_scope.
324 325 326 327
Notation "X ⊄  Y" := (¬X  Y) (at level 70) : 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
328

329 330 331 332 333
(** 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
334
Class ElemOf A B := elem_of: A  B  Prop.
335
Instance: Params (@elem_of) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
336 337 338 339 340 341 342 343 344
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
345 346 347 348
Class Disjoint A := disjoint : A  A  Prop.
Instance: Params (@disjoint) 2.
Infix "⊥" := disjoint (at level 70) : C_scope.
Notation "(⊥)" := disjoint (only parsing) : C_scope.
349
Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
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
Notation "(.⊥ X )" := (λ Y, Y   X) (only parsing) : C_scope.
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.
376 377 378

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

381 382 383 384 385 386
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.
387

388
  Lemma disjoint_list_nil  :  @nil A  True.
389 390 391
  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.
392
End disjoint_list.
393 394

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

(** ** Monadic operations *)
(** We define operational type classes for the monadic operations bind, join 
398 399 400
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). *)
401 402 403
Class MRet (M : Type  Type) := mret:  {A}, A  M A.
Instance: Params (@mret) 3.
Arguments mret {_ _ _} _.
404 405
Class MBind (M : Type  Type) := mbind :  {A B}, (A  M B)  M A  M B.
Arguments mbind {_ _ _ _} _ !_ /.
406 407 408
Instance: Params (@mbind) 5.
Class MJoin (M : Type  Type) := mjoin:  {A}, M (M A)  M A.
Instance: Params (@mjoin) 3.
409
Arguments mjoin {_ _ _} !_ /.
410
Class FMap (M : Type  Type) := fmap :  {A B}, (A  B)  M A  M B.
411
Instance: Params (@fmap) 6.
412 413
Arguments fmap {_ _ _ _} _ !_ /.
Class OMap (M : Type  Type) := omap:  {A B}, (A  option B)  M A  M B.
414
Instance: Params (@omap) 6.
415
Arguments omap {_ _ _ _} _ !_ /.
416

417 418 419 420 421 422
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
423
  (at level 65, only parsing, right associativity) : C_scope.
424
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
425
Notation "' ( x1 , x2 ) ← y ; z" :=
426
  (y = (λ x : _, let ' (x1, x2) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  (at level 65, only parsing, right associativity) : C_scope.
428
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
429
  (y = (λ x : _, let ' (x1,x2,x3) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
430
  (at level 65, only parsing, right associativity) : C_scope.
431
Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
432
  (y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
433
  (at level 65, only parsing, right associativity) : C_scope.
434 435
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
436
  (at level 65, only parsing, right associativity) : C_scope.
437 438
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
439
  (at level 65, only parsing, right associativity) : C_scope.
440

441 442 443 444 445
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").

446
Class MGuard (M : Type  Type) :=
447 448 449
  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
450
  (at level 65, only parsing, right associativity) : C_scope.
451
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
Robbert Krebbers's avatar
Robbert Krebbers committed
452
  (at level 65, only parsing, right associativity) : C_scope.
453

454
(** ** Operations on maps *)
455 456
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
457
The function look up [m !! k] should yield the element at key [k] in [m]. *)
458
Class Lookup (K A M : Type) := lookup: K  M  option A.
459 460 461
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope.
462
Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
463
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
464
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
465 466 467

(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
468
Class Insert (K A M : Type) := insert: K  A  M  M.
469 470 471
Instance: Params (@insert) 4.
Notation "<[ k := a ]>" := (insert k a)
  (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
472
Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
473

474 475 476
(** 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. *)
477
Class Delete (K M : Type) := delete: K  M  M.
478 479
Instance: Params (@delete) 3.
Arguments delete _ _ _ !_ !_ / : simpl nomatch.
480 481

(** The function [alter f k m] should update the value at key [k] using the
482
function [f], which is called with the original value. *)
483
Class Alter (K A M : Type) := alter: (A  A)  K  M  M.
484
Instance: Params (@alter) 5.
485
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
486 487

(** The function [alter f k m] should update the value at key [k] using the
488 489 490
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]. *)
491 492
Class PartialAlter (K A M : Type) :=
  partial_alter: (option A  option A)  K  M  M.
493
Instance: Params (@partial_alter) 4.
494
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
495 496 497

(** 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]. *)
498 499 500
Class Dom (M C : Type) := dom: M  C.
Instance: Params (@dom) 3.
Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
501 502

(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
503 504 505 506 507
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.
508

509 510 511 512 513
(** 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]. *)
Class UnionWith (A M : Type) :=
  union_with: (A  A  option A)  M  M  M.
514
Instance: Params (@union_with) 3.
515
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
516

517 518 519
(** Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type) :=
  intersection_with: (A  A  option A)  M  M  M.
520
Instance: Params (@intersection_with) 3.
521 522
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.

523 524
Class DifferenceWith (A M : Type) :=
  difference_with: (A  A  option A)  M  M  M.
525
Instance: Params (@difference_with) 3.
526
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
527

528 529 530 531
Definition intersection_with_list `{IntersectionWith A M}
  (f : A  A  option A) : M  list M  M := fold_right (intersection_with f).
Arguments intersection_with_list _ _ _ _ _ !_ /.

532 533 534 535 536 537 538 539 540 541 542 543 544
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 (@insert) 6.
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.

545 546 547 548
(** ** 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 [injective (k ++)] instead of [app_inv_head k]. *)
549 550 551 552 553
Class Injective {A B} (R : relation A) (S : relation B) (f : A  B) : Prop :=
  injective:  x y, S (f x) (f y)  R x y.
Class Injective2 {A B C} (R1 : relation A) (R2 : relation B)
    (S : relation C) (f : A  B  C) : Prop :=
  injective2:  x1 x2  y1 y2, S (f x1 x2) (f y1 y2)  R1 x1 y1  R2 x2 y2.
554 555 556 557
Class Cancel {A B} (S : relation B) (f : A  B) (g : B  A) : Prop :=
  cancel:  x, S (f (g x)) x.
Class Surjective {A B} (R : relation B) (f : A  B) :=
  surjective :  y,  x, R (f x) y.
558
Class Idempotent {A} (R : relation A) (f : A  A  A) : Prop :=
559
  idempotent:  x, R (f x x) x.
560
Class Commutative {A B} (R : relation A) (f : B  B  A) : Prop :=
561
  commutative:  x y, R (f x y) (f y x).
562
Class LeftId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
563
  left_id:  x, R (f i x) x.
564
Class RightId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
565
  right_id:  x, R (f x i) x.
566
Class Associative {A} (R : relation A) (f : A  A  A) : Prop :=
567
  associative:  x y z, R (f x (f y z)) (f (f x y) z).
568
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
569
  left_absorb:  x, R (f i x) i.
570
Class RightAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
571
  right_absorb:  x, R (f x i) i.
572 573 574 575
Class LeftDistr {A} (R : relation A) (f g : A  A  A) : Prop :=
  left_distr:  x y z, R (f x (g y z)) (g (f x y) (f x z)).
Class RightDistr {A} (R : relation A) (f g : A  A  A) : Prop :=
  right_distr:  y z x, R (f (g y z) x) (g (f y x) (f z x)).
576 577
Class AntiSymmetric {A} (R S : relation A) : Prop :=
  anti_symmetric:  x y, S x y  S y x  R x y.
578 579
Class Total {A} (R : relation A) := total x y : R x y  R y x.
Class Trichotomy {A} (R : relation A) :=
580
  trichotomy :  x y, R x y  x = y  R y x.
581
Class TrichotomyT {A} (R : relation A) :=
582
  trichotomyT :  x y, {R x y} + {x = y} + {R y x}.
Robbert Krebbers's avatar
Robbert Krebbers committed
583

584
Arguments irreflexivity {_} _ {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
Arguments injective {_ _ _ _} _ {_} _ _ _.
586
Arguments injective2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
587 588
Arguments cancel {_ _ _} _ _ {_} _.
Arguments surjective {_ _ _} _ {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
589 590 591 592 593
Arguments idempotent {_ _} _ {_} _.
Arguments commutative {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
Arguments right_id {_ _} _ _ {_} _.
Arguments associative {_ _} _ {_} _ _ _.
594 595
Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
596 597
Arguments left_distr {_ _} _ _ {_} _ _ _.
Arguments right_distr {_ _} _ _ {_} _ _ _.
598
Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
599 600 601
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.
602

603 604 605
Instance id_injective {A} : Injective (=) (=) (@id A).
Proof. intros ??; auto. Qed.

606 607 608 609
(** 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 idempotent_L {A} (f : A  A  A) `{!Idempotent (=) f} x : f x x = x.
610
Proof. auto. Qed.
611
Lemma commutative_L {A B} (f : B  B  A) `{!Commutative (=) f} x y :
612
  f x y = f y x.
613
Proof. auto. Qed.
614
Lemma left_id_L {A} (i : A) (f : A  A  A) `{!LeftId (=) i f} x : f i x = x.
615
Proof. auto. Qed.
616
Lemma right_id_L {A} (i : A) (f : A  A  A) `{!RightId (=) i f} x : f x i = x.
617
Proof. auto. Qed.
618
Lemma associative_L {A} (f : A  A  A) `{!Associative (=) f} x y z :
619
  f x (f y z) = f (f x y) z.
620
Proof. auto. Qed.
621
Lemma left_absorb_L {A} (i : A) (f : A  A  A) `{!LeftAbsorb (=) i f} x :
622 623
  f i x = i.
Proof. auto. Qed.
624
Lemma right_absorb_L {A} (i : A) (f : A  A  A) `{!RightAbsorb (=) i f} x :
625 626
  f x i = i.
Proof. auto. Qed.
627
Lemma left_distr_L {A} (f g : A  A  A) `{!LeftDistr (=) f g} x y z :
628 629
  f x (g y z) = g (f x y) (f x z).
Proof. auto. Qed.
630
Lemma right_distr_L {A} (f g : A  A  A) `{!RightDistr (=) f g} y z x :
631 632
  f (g y z) x = g (f y x) (f z x).
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
633

634
(** ** Axiomatization of ordered structures *)
635 636
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
relation [R] instead of [⊆] to support multiple orders on the same type. *)
637
Class PartialOrder {A} (R : relation A) : Prop := {
638 639
  partial_order_pre :> PreOrder R;
  partial_order_anti_symmetric :> AntiSymmetric (=) R
640 641
}.
Class TotalOrder {A} (R : relation A) : Prop := {
642 643
  total_order_partial :> PartialOrder R;
  total_order_trichotomy :> Trichotomy (strict R)
644 645
}.

646 647 648 649 650 651
(** We do not use a setoid equality in the following interfaces to avoid the
need for proofs that the relations and operations are proper. Instead, we
define setoid equality generically [λ X Y, X ⊆ Y ∧ Y ⊆ X]. *)
Class EmptySpec A `{Empty A, SubsetEq A} : Prop := subseteq_empty X :   X.
Class JoinSemiLattice A `{SubsetEq A, Union A} : Prop := {
  join_semi_lattice_pre :>> PreOrder ();
652 653 654
  union_subseteq_l X Y : X  X  Y;
  union_subseteq_r X Y : Y  X  Y;
  union_least X Y Z : X  Z  Y  Z  X  Y  Z
Robbert Krebbers's avatar
Robbert Krebbers committed
655
}.
656 657
Class MeetSemiLattice A `{SubsetEq A, Intersection A} : Prop := {
  meet_semi_lattice_pre :>> PreOrder ();
658 659 660
  intersection_subseteq_l X Y : X  Y  X;
  intersection_subseteq_r X Y : X  Y  Y;
  intersection_greatest X Y Z : Z  X  Z  Y  Z  X  Y
Robbert Krebbers's avatar
Robbert Krebbers committed
661
}.
662 663 664 665
Class Lattice A `{SubsetEq A, Union A, Intersection A} : Prop := {
  lattice_join :>> JoinSemiLattice A;
  lattice_meet :>> MeetSemiLattice A;
  lattice_distr X Y Z : (X  Y)  (X  Z)  X  (Y  Z)
666
}.
667

668
(** ** Axiomatization of collections *)
669 670
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *)
671
Instance: Params (@map) 3.
672 673
Class SimpleCollection A C `{ElemOf A C,
    Empty C, Singleton A C, Union C} : Prop := {
674
  not_elem_of_empty (x : A) : x  ;
675
  elem_of_singleton (x y : A) : x  {[ y ]}  x = y;
676 677
  elem_of_union X Y (x : A) : x  X  Y  x  X  x  Y
}.
678 679
Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
    Union C, Intersection C, Difference C} : Prop := {
680
  collection_simple :>> SimpleCollection A C;
Robbert Krebbers's avatar
Robbert Krebbers committed
681
  elem_of_intersection X Y (x : A) : x  X  Y  x  X  x  Y;
682 683
  elem_of_difference X Y (x : A) : x  X  Y  x  X  x  Y
}.
684 685
Class CollectionOps A C `{ElemOf A C, Empty C, Singleton A C, Union C,
    Intersection C, Difference C, IntersectionWith A C, Filter A C} : Prop := {
686
  collection_ops :>> Collection A C;
687
  elem_of_intersection_with (f : A  A  option A) X Y (x : A) :
688
    x  intersection_with f X Y   x1 x2, x1  X  x2  Y  f x1 x2 = Some x;
689
  elem_of_filter X P `{ x, Decision (P x)} x : x  filter P X  P x  x  X
Robbert Krebbers's avatar
Robbert Krebbers committed
690 691
}.

692 693 694
(** 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
695
Class Elements A C := elements: C  list A.
696
Instance: Params (@elements) 3.
697 698 699 700 701 702 703 704 705 706 707 708 709

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

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

(** Decidability of equality of the carrier set is admissible, but we add it
anyway so as to avoid cycles in type class search. *)
710 711 712
Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C,
    Union C, Intersection C, Difference C,
    Elements A C,  x y : A, Decision (x = y)} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
713
  fin_collection :>> Collection A C;
714 715
  elem_of_elements X x : x  elements X  x  X;
  NoDup_elements X : NoDup (elements X)
716 717
}.
Class Size C := size: C  nat.
718
Arguments size {_ _} !_ / : simpl nomatch.
719
Instance: Params (@size) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
720

721 722 723 724 725 726 727 728
(** The class [Collection M] axiomatizes a type constructor [M] that can be
used to construct a collection [M A] with elements of type [A]. The advantage
of this class, compared to [Collection], is that it also axiomatizes the
the monadic operations. The disadvantage, is that not many inhabits are
possible (we will only provide an inhabitant using unordered lists without
duplicates removed). More interesting implementations typically need
decidability of equality, or a total order on the elements, which do not fit
in a type constructor of type [Type → Type]. *)
729 730 731
Class CollectionMonad M `{ A, ElemOf A (M A),
     A, Empty (M A),  A, Singleton A (M A),  A, Union (M A),
    !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
732 733 734
  collection_monad_simple A :> SimpleCollection A (M A);
  elem_of_bind {A B} (f : A  M B) (X : M A) (x : B) :
    x  X = f   y, x  f y  y  X;
735
  elem_of_ret {A} (x y : A) : x  mret y  x = y;
736 737
  elem_of_fmap {A B} (f : A  B) (X : M A) (x : B) :
    x  f <$> X   y, x = f y  y  X;
738
  elem_of_join {A} (X : M (M A)) (x : A) : x  mjoin X   Y, x  Y  Y  X
739 740
}.

741 742 743
(** The function [fresh X] yields an element that is not contained in [X]. We
will later prove that [fresh] is [Proper] with respect to the induced setoid
equality on collections. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
744
Class Fresh A C := fresh: C  A.
745
Instance: Params (@fresh) 3.