base.v 43.5 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
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
132
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
133 134 135 136 137 138
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
Definition equivL {A} : Equiv A := (=).

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
238
Class Intersection A := intersection: A  A  A.
239
Instance: Params (@intersection) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242 243 244 245
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.
246
Instance: Params (@difference) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
247 248 249 250
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.
251 252 253 254 255 256
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
257

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

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

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

320 321
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y  ¬R Y X.
Instance: Params (@strict) 2.
322 323 324 325
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.
326 327 328 329
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
330

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

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

383 384 385 386 387 388
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.
389

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

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

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

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

443 444 445 446 447
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").

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

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

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

476 477 478
(** 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. *)
479
Class Delete (K M : Type) := delete: K  M  M.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
Instance: Params (@delete) 4.
481
Arguments delete _ _ _ !_ !_ / : simpl nomatch.
482 483

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

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

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

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

511 512 513 514 515
(** 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.
516
Instance: Params (@union_with) 3.
517
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
518

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

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

530 531 532 533
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 _ _ _ _ _ !_ /.

534 535 536 537 538 539 540 541
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
Instance: Params (@insertE) 6.
543 544 545 546
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.

547 548 549 550
(** ** 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]. *)
551 552 553 554 555
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.
556 557 558 559
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.
560
Class Idempotent {A} (R : relation A) (f : A  A  A) : Prop :=
561
  idempotent:  x, R (f x x) x.
562
Class Commutative {A B} (R : relation A) (f : B  B  A) : Prop :=
563
  commutative:  x y, R (f x y) (f y x).
564
Class LeftId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
565
  left_id:  x, R (f i x) x.
566
Class RightId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
567
  right_id:  x, R (f x i) x.
568
Class Associative {A} (R : relation A) (f : A  A  A) : Prop :=
569
  associative:  x y z, R (f x (f y z)) (f (f x y) z).
570
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
571
  left_absorb:  x, R (f i x) i.
572
Class RightAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
573
  right_absorb:  x, R (f x i) i.
574 575 576 577
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)).
578 579
Class AntiSymmetric {A} (R S : relation A) : Prop :=
  anti_symmetric:  x y, S x y  S y x  R x y.
580 581
Class Total {A} (R : relation A) := total x y : R x y  R y x.
Class Trichotomy {A} (R : relation A) :=
582
  trichotomy :  x y, R x y  x = y  R y x.
583
Class TrichotomyT {A} (R : relation A) :=
584
  trichotomyT :  x y, {R x y} + {x = y} + {R y x}.
Robbert Krebbers's avatar
Robbert Krebbers committed
585

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

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

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

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

648 649 650 651 652 653
(** 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 ();
654 655 656
  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
657
}.
658 659
Class MeetSemiLattice A `{SubsetEq A, Intersection A} : Prop := {
  meet_semi_lattice_pre :>> PreOrder ();
660 661 662
  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
663
}.
664 665 666 667
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)
668
}.
669

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

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

(** 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. *)
712 713 714
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
715
  fin_collection :>> Collection A C;
716 717
  elem_of_elements X x : x  elements X  x  X;
  NoDup_elements X : NoDup (elements X)
718 719
}.
Class Size C := size: C  nat.
720
Arguments size {_ _} !_ / : simpl nomatch.
721
Instance: Params (@size) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
722

723 724 725 726 727 728 729 730
(** 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]. *)
731 732 733
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 := {
734 735 736
  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;
737
  elem_of_ret {A} (x y : A) : x  mret y  x = y;
738 739
  elem_of_fmap {A B} (f : A  B) (X : M A) (x : B) :
    x  f <$> X   y, x = f y  y  X;
740
  elem_of_join {A} (X : M (M A)) (x : A) : x  mjoin X   Y, x  Y  Y  X
741 742
}.

743 744 745
(** 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
746
Class Fresh A C := fresh: C  A.
747
Instance: Params (@fresh) 3.
748 749
Class FreshSpec A C `{ElemOf A C,
    Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
750
  fresh_collection_simple :>> SimpleCollection A C;
751
  fresh_proper_alt X Y : ( x, x  X  x  Y)  fresh X = fresh Y;
Robbert Krebbers's avatar
Robbert Krebbers committed
752 753 754
  is_fresh (X : C) : fresh X  X
}.

755 756 757
(** * Booleans *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
758
Hint Unfold Is_true.
759
Hint Immediate Is_true_eq_left.
760
Hint Resolve orb_prop_intro andb_prop_intro.
761 762 763 764 765 766 767 768 769 770 771
Notation "(&&)" := andb (only parsing).
Notation "(||)" := orb (only parsing).
Infix "&&*" := (zip_with (&&)) (at level 40).
Infix "||*" := (zip_with (||)) (at level 50).

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.

772 773 774 775 776 777 778 779 780
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.

781
(** * Miscellaneous *)
782
Class Half A := half: A  A.
783 784
Notation "½" := half : C_scope.
Notation "½*" := (fmap (M:=list) half) : C_scope.
785

786 787
Lemma proj1_sig_inj {A} (P : A  Prop) x (Px : P x) y (Py : P y) :
  xPx = yPy  x = y.
788
Proof. injection 1; trivial. Qed.
789
Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y  ¬R y x.
790
Proof. intuition. Qed.
791
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y  R y x.
792 793
Proof. intuition. Qed.

794 795 796
(** ** Pointwise relations *)
(** These instances are in Coq trunk since revision 15455, but are not in Coq
8.4 yet. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
797 798 799 800 801 802 803 804 805 806
Instance pointwise_reflexive {A} `{R : relation B} :
  Reflexive R  Reflexive (pointwise_relation A R) | 9.
Proof. firstorder. Qed.
Instance pointwise_symmetric {A} `{R : relation B} :
  Symmetric R  Symmetric (pointwise_relation A R) | 9.
Proof. firstorder. Qed.
Instance pointwise_transitive {A} `{R : relation B} :
  Transitive R  Transitive (pointwise_relation A R) | 9.
Proof. firstorder. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
807 808 809 810 811
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.

812
(** ** Products *)
813 814 815 816 817 818 819
Instance prod_map_injective {A A' B B'} (f : A  A') (g : B  B') :
  Injective (=) (=) f  Injective (=) (=) g 
  <