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