base.v 66.6 KB
Newer Older
1
2
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
3
abstract interfaces for ordered structures, sets, and various other data
4
structures. *)
5

Olivier Laurent's avatar
Olivier Laurent committed
6
7
8
(* We want to ensure that [le] and [lt] refer to operations on [nat].
These two functions being defined both in [Coq.Bool] and in [Coq.Peano],
we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
9
10
11
(* We also want to ensure that notations from [Coq.Utf8] take precedence
over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
12
From Coq Require Import Permutation.
13
14
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
15
From stdpp Require Import options.
16

Michael Sammler's avatar
Michael Sammler committed
17
18
19
20
21
(** This notation is necessary to prevent [length] from being printed
as [strings.length] if strings.v is imported and later base.v. See
also strings.v and
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129. *)
22
23
Notation length := Datatypes.length.

Ralf Jung's avatar
Ralf Jung committed
24
25
(** * Enable implicit generalization. *)
(** This option enables implicit generalization in arguments of the form
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
   [`{...}] (i.e., anonymous arguments).  Unfortunately, it also enables
   implicit generalization in [Instance].  We think that the fact that both
28
29
30
31
   behaviors are coupled together is a [bug in
   Coq](https://github.com/coq/coq/issues/6030). *)
Global Generalizable All Variables.

32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
(** * Tweak program *)
(** 1. Since we only use Program to solve logical side-conditions, they should
always be made Opaque, otherwise we end up with performance problems due to
Coq blindly unfolding them.

Note that in most cases we use [Next Obligation. (* ... *) Qed.], for which
this option does not matter. However, sometimes we write things like
[Solve Obligations with naive_solver (* ... *)], and then the obligations
should surely be opaque. *)
Global Unset Transparent Obligations.

(** 2. Do not let Program automatically simplify obligations. The default
obligation tactic is [Tactics.program_simpl], which, among other things,
introduces all variables and gives them fresh names. As such, it becomes
impossible to refer to hypotheses in a robust way. *)
47
Obligation Tactic := idtac.
48
49

(** 3. Hide obligations from the results of the [Search] commands. *)
50
Add Search Blacklist "_obligation_".
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
(** * Sealing off definitions *)
Ralf Jung's avatar
Ralf Jung committed
53
54
55
56
Section seal.
  Local Set Primitive Projections.
  Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
End seal.
57
58
Global Arguments unseal {_ _} _ : assert.
Global Arguments seal_eq {_ _} _ : assert.
59

60
(** * Non-backtracking type classes *)
61
(** The type class [TCNoBackTrack P] can be used to establish [P] without ever
62
63
64
65
66
67
68
69
70
71
72
backtracking on the instance of [P] that has been found. Backtracking may
normally happen when [P] contains evars that could be instanciated in different
ways depending on which instance is picked, and type class search somewhere else
depends on this evar.

The proper way of handling this would be by setting Coq's option
`Typeclasses Unique Instances`. However, this option seems to be broken, see Coq
issue #6714.

See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
of this type class. *)
73
Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
74
Global Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
75

76
77
(* A conditional at the type class level. Note that [TCIf P Q R] is not the same
as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
78
establish [Q], i.e. does not have the behavior of a conditional. Furthermore,
79
note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
Robbert Krebbers's avatar
Robbert Krebbers committed
80
would not be able to prove the negation of [P]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Inductive TCIf (P Q R : Prop) : Prop :=
82
83
84
85
  | TCIf_true : P  Q  TCIf P Q R
  | TCIf_false : R  TCIf P Q R.
Existing Class TCIf.

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

90
(** * Typeclass opaque definitions *)
Ralf Jung's avatar
Ralf Jung committed
91
(** The constant [tc_opaque] is used to make definitions opaque for just type
92
93
94
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque tc_opaque.
95
Global Arguments tc_opaque {_} _ /.
96

Ralf Jung's avatar
Ralf Jung committed
97
(** Below we define type class versions of the common logical operators. It is
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
important to note that we duplicate the definitions, and do not declare the
existing logical operators as type classes. That is, we do not say:

  Existing Class or.
  Existing Class and.

If we could define the existing logical operators as classes, there is no way
of disambiguating whether a premise of a lemma should be solved by type class
resolution or not.

These classes are useful for two purposes: writing complicated type class
premises in a more concise way, and for efficiency. For example, using the [Or]
class, instead of defining two instances [P → Q1 → R] and [P → Q2 → R] we could
have one instance [P → Or Q1 Q2 → R]. When we declare the instance that way, we
avoid the need to derive [P] twice. *)
113
Inductive TCOr (P1 P2 : Prop) : Prop :=
114
115
116
  | TCOr_l : P1  TCOr P1 P2
  | TCOr_r : P2  TCOr P1 P2.
Existing Class TCOr.
117
118
Global Existing Instance TCOr_l | 9.
Global Existing Instance TCOr_r | 10.
119
Global Hint Mode TCOr ! ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
120

121
Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1  P2  TCAnd P1 P2.
122
Existing Class TCAnd.
123
Global Existing Instance TCAnd_intro.
124
Global Hint Mode TCAnd ! ! : typeclass_instances.
125

126
127
Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
Existing Class TCTrue.
128
Global Existing Instance TCTrue_intro.
129

Michael Sammler's avatar
Michael Sammler committed
130
131
132
133
134
135
136
137
138
139
140
141
142
(** The class [TCFalse] is not stricly necessary as one could also use
[False]. However, users might expect that TCFalse exists and if it
does not, it can cause hard to diagnose bugs due to automatic
generalization. *)
Inductive TCFalse : Prop :=.
Existing Class TCFalse.

(** The class [TCUnless] can be used to check that search for [P]
fails. This is useful as a guard for certain instances together with
classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
(e.g. when saturating the context). *)
Notation TCUnless P := (TCIf P TCFalse TCTrue).

143
144
145
146
Inductive TCForall {A} (P : A  Prop) : list A  Prop :=
  | TCForall_nil : TCForall P []
  | TCForall_cons x xs : P x  TCForall P xs  TCForall P (x :: xs).
Existing Class TCForall.
147
148
Global Existing Instance TCForall_nil.
Global Existing Instance TCForall_cons.
149
Global Hint Mode TCForall ! ! ! : typeclass_instances.
150

151
152
153
(** The class [TCForall2 P l k] is commonly used to transform an input list [l]
into an output list [k], or the converse. Therefore there are two modes, either
[l] input and [k] output, or [k] input and [l] input. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156
157
158
Inductive TCForall2 {A B} (P : A  B  Prop) : list A  list B  Prop :=
  | TCForall2_nil : TCForall2 P [] []
  | TCForall2_cons x y xs ys :
     P x y  TCForall2 P xs ys  TCForall2 P (x :: xs) (y :: ys).
Existing Class TCForall2.
159
160
Global Existing Instance TCForall2_nil.
Global Existing Instance TCForall2_cons.
161
162
Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
163

Michael Sammler's avatar
Michael Sammler committed
164
165
166
167
Inductive TCExists {A} (P : A  Prop) : list A  Prop :=
  | TCExists_cons_hd x l : P x  TCExists P (x :: l)
  | TCExists_cons_tl x l: TCExists P l  TCExists P (x :: l).
Existing Class TCExists.
168
169
Global Existing Instance TCExists_cons_hd | 10.
Global Existing Instance TCExists_cons_tl | 20.
Michael Sammler's avatar
Michael Sammler committed
170
171
Global Hint Mode TCExists ! ! ! : typeclass_instances.

172
173
174
175
Inductive TCElemOf {A} (x : A) : list A  Prop :=
  | TCElemOf_here xs : TCElemOf x (x :: xs)
  | TCElemOf_further y xs : TCElemOf x xs  TCElemOf x (y :: xs).
Existing Class TCElemOf.
176
177
Global Existing Instance TCElemOf_here.
Global Existing Instance TCElemOf_further.
178
Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
179

Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
182
183
(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
[TCEq] can also be used to unify evars. This is harmless: since the only
instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
184
185
Inductive TCEq {A} (x : A) : A  Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
186
Global Existing Instance TCEq_refl.
187
Global Hint Mode TCEq ! - - : typeclass_instances.
188

Michael Sammler's avatar
Michael Sammler committed
189
190
191
Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2  x1 = x2.
Proof. split; destruct 1; reflexivity. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
Inductive TCDiag {A} (C : A  Prop) : A  A  Prop :=
  | TCDiag_diag x : C x  TCDiag C x x.
Existing Class TCDiag.
195
Global Existing Instance TCDiag_diag.
196
197
Global Hint Mode TCDiag ! ! ! - : typeclass_instances.
Global Hint Mode TCDiag ! ! - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
198

199
200
201
202
203
204
(** Given a proposition [P] that is a type class, [tc_to_bool P] will return
[true] iff there is an instance of [P]. It is often useful in Ltac programming,
where one can do [lazymatch tc_to_bool P with true => .. | false => .. end]. *)
Definition tc_to_bool (P : Prop)
  {p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : bool := p.

205
(** Throughout this development we use [stdpp_scope] for all general purpose
206
notations that do not belong to a more specific scope. *)
Ralf Jung's avatar
Ralf Jung committed
207
Declare Scope stdpp_scope.
208
209
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.
210

211
(** Change [True] and [False] into notations in order to enable overloading.
212
213
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
214
215
Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False (format "False") : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

Gregory Malecha's avatar
Gregory Malecha committed
217
(** Change [forall] into a notation in order to enable overloading. *)
218
Notation "'forall' x .. y , P" := (forall x, .. (forall y, P) ..)
Gregory Malecha's avatar
Gregory Malecha committed
219
220
221
  (at level 200, x binder, y binder, right associativity,
   only parsing) : type_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
222

223
(** * Equality *)
224
(** Introduce some Haskell style like notations. *)
225
Notation "(=)" := eq (only parsing) : stdpp_scope.
226
227
Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope.
Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
228
Notation "(≠)" := (λ x y, x  y) (only parsing) : stdpp_scope.
229
230
Notation "( x ≠.)" := (λ y, x  y) (only parsing) : stdpp_scope.
Notation "(.≠ x )" := (λ y, y  x) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
231

232
233
234
235
Infix "=@{ A }" := (@eq A)
  (at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
236
237
Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.
238

239
240
Global Hint Extern 0 (_ = _) => reflexivity : core.
Global Hint Extern 100 (_  _) => discriminate : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
241

242
Global Instance:  A, PreOrder (=@{A}).
243
244
245
Proof. split; repeat intro; congruence. Qed.

(** ** Setoid equality *)
Ralf Jung's avatar
Ralf Jung committed
246
247
248
(** We define an operational type class for setoid equality, i.e., the
"canonical" equivalence for a type. The typeclass is tied to the \equiv
symbol. This is based on (Spitters/van der Weegen, 2011). *)
249
Class Equiv A := equiv: relation A.
250
251
(* No Hint Mode set because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12.
252
Global Hint Mode Equiv ! : typeclass_instances. *)
253

254
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
255
256
257
Infix "≡@{ A }" := (@equiv A _)
  (at level 70, only parsing, no associativity) : stdpp_scope.

258
Notation "(≡)" := equiv (only parsing) : stdpp_scope.
259
260
Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope.
Notation "(.≡ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
261
262
Notation "(≢)" := (λ X Y, ¬X  Y) (only parsing) : stdpp_scope.
Notation "X ≢ Y":= (¬X  Y) (at level 70, no associativity) : stdpp_scope.
263
264
Notation "( X ≢.)" := (λ Y, X  Y) (only parsing) : stdpp_scope.
Notation "(.≢ X )" := (λ Y, Y  X) (only parsing) : stdpp_scope.
265

266
267
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope.
268
269
Notation "X ≢@{ A } Y":= (¬X @{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.
270

271
272
273
274
275
(** 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.
276
Global Hint Mode LeibnizEquiv ! - : typeclass_instances.
277

278
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@{A})} (x y : A) :
279
  x  y  x = y.
280
Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
281

282
283
Ltac fold_leibniz := repeat
  match goal with
284
  | H : context [ _ @{?A} _ ] |- _ =>
285
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
286
  | |- context [ _ @{?A} _ ] =>
287
288
289
290
    setoid_rewrite (leibniz_equiv_iff (A:=A))
  end.
Ltac unfold_leibniz := repeat
  match goal with
291
  | H : context [ _ =@{?A} _ ] |- _ =>
292
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
293
  | |- context [ _ =@{?A} _ ] =>
294
295
296
297
298
299
300
301
    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
  end.

Definition equivL {A} : Equiv A := (=).

(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
302
Global Instance: Params (@equiv) 2 := {}.
303
304
305
306

(** The following instance forces [setoid_replace] to use setoid equality
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
307
Global Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3 := {}.
308
309
Global Hint Extern 0 (_  _) => reflexivity : core.
Global Hint Extern 0 (_  _) => symmetry; assumption : core.
310
311
312
313
314


(** * Type classes *)
(** ** Decidable propositions *)
(** This type class by (Spitters/van der Weegen, 2011) collects decidable
315
propositions. *)
316
Class Decision (P : Prop) := decide : {P} + {¬P}.
317
Global Hint Mode Decision ! : typeclass_instances.
318
Global Arguments decide _ {_} : simpl never, assert.
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335

(** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
an explicit class instead of a notation for two reasons:

- It allows us to control [Hint Mode] more precisely. In particular, if it were
  defined as a notation, the above [Hint Mode] for [Decision] would not prevent
  diverging instance search when looking for [RelDecision (@eq ?A)], which would
  result in it looking for [Decision (@eq ?A x y)], i.e. an instance where the
  head position of [Decision] is not en evar.
- We use it to avoid inefficient computation due to eager evaluation of
  propositions by [vm_compute]. This inefficiency arises for example if
  [(x = y) := (f x = f y)]. Since [decide (x = y)] evaluates to
  [decide (f x = f y)], this would then lead to evaluation of [f x] and [f y].
  Using the [RelDecision], the [f] is hidden under a lambda, which prevents
  unnecessary evaluation. *)
Class RelDecision {A B} (R : A  B  Prop) :=
  decide_rel x y :> Decision (R x y).
336
Global Hint Mode RelDecision ! ! ! : typeclass_instances.
337
Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
338
Notation EqDecision A := (RelDecision (=@{A})).
339
340
341
342

(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
343
Global Hint Mode Inhabited ! : typeclass_instances.
344
Global Arguments populate {_} _ : assert.
345
346
347
348
349
350

(** ** 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.
351
Global Hint Mode ProofIrrel ! : typeclass_instances.
352
353
354

(** ** Common properties *)
(** These operational type classes allow us to refer to common mathematical
355
356
properties in a generic way. For example, for injectivity of [(k ++.)] it
allows us to write [inj (k ++.)] instead of [app_inv_head k]. *)
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
Class Inj {A B} (R : relation A) (S : relation B) (f : A  B) : Prop :=
  inj x y : S (f x) (f y)  R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
    (S : relation C) (f : A  B  C) : Prop :=
  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2)  R1 x1 y1  R2 x2 y2.
Class Cancel {A B} (S : relation B) (f : A  B) (g : B  A) : Prop :=
  cancel :  x, S (f (g x)) x.
Class Surj {A B} (R : relation B) (f : A  B) :=
  surj y :  x, R (f x) y.
Class IdemP {A} (R : relation A) (f : A  A  A) : Prop :=
  idemp x : R (f x x) x.
Class Comm {A B} (R : relation A) (f : B  B  A) : Prop :=
  comm x y : R (f x y) (f y x).
Class LeftId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  left_id x : R (f i x) x.
Class RightId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  right_id x : R (f x i) x.
Class Assoc {A} (R : relation A) (f : A  A  A) : Prop :=
  assoc x y z : R (f x (f y z)) (f (f x y) z).
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  left_absorb x : R (f i x) i.
Class RightAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
  right_absorb x : R (f x i) i.
Class AntiSymm {A} (R S : relation A) : Prop :=
  anti_symm x y : S x y  S y x  R x y.
Class Total {A} (R : relation A) := total x y : R x y  R y x.
Class Trichotomy {A} (R : relation A) :=
  trichotomy x y : R x y  x = y  R y x.
Class TrichotomyT {A} (R : relation A) :=
  trichotomyT x y : {R x y} + {x = y} + {R y x}.
387
388
389
390
391

Notation Involutive R f := (Cancel R f f).
Lemma involutive {A} {R : relation A} (f : A  A) `{Involutive R f} x :
  R (f (f x)) x.
Proof. auto. Qed.
392

393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
Global Arguments irreflexivity {_} _ {_} _ _ : assert.
Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
Global Arguments cancel {_ _ _} _ _ {_} _ : assert.
Global Arguments surj {_ _ _} _ {_} _ : assert.
Global Arguments idemp {_ _} _ {_} _ : assert.
Global Arguments comm {_ _ _} _ {_} _ _ : assert.
Global Arguments left_id {_ _} _ _ {_} _ : assert.
Global Arguments right_id {_ _} _ _ {_} _ : assert.
Global Arguments assoc {_ _} _ {_} _ _ _ : assert.
Global Arguments left_absorb {_ _} _ _ {_} _ : assert.
Global Arguments right_absorb {_ _} _ _ {_} _ : assert.
Global Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
Global Arguments total {_} _ {_} _ _ : assert.
Global Arguments trichotomy {_} _ {_} _ _ : assert.
Global Arguments trichotomyT {_} _ {_} _ _ : assert.
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426

Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y  ¬R y x.
Proof. intuition. Qed.
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y  R y x.
Proof. intuition. Qed.

Lemma not_inj `{Inj A B R R' f} x y : ¬R x y  ¬R' (f x) (f y).
Proof. intuition. Qed.
Lemma not_inj2_1 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
  ¬R x1 x2  ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
Lemma not_inj2_2 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
  ¬R' y1 y2  ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.

Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A  B)
  `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y)  R x y.
Proof. firstorder. Qed.
427
Global Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
428
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
429
Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.

Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} :
  Inj R1 R2 g.
Proof.
  intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity.
Qed.
Lemma cancel_surj `{Cancel A B R1 f g} : Surj R1 f.
Proof. intros y. exists (g y). auto. Qed.

(** The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
use the setoid rewriting mechanism. *)
Lemma idemp_L {A} f `{!@IdemP A (=) f} x : f x x = x.
Proof. auto. Qed.
Lemma comm_L {A B} f `{!@Comm A B (=) f} x y : f x y = f y x.
Proof. auto. Qed.
Lemma left_id_L {A} i f `{!@LeftId A (=) i f} x : f i x = x.
Proof. auto. Qed.
Lemma right_id_L {A} i f `{!@RightId A (=) i f} x : f x i = x.
Proof. auto. Qed.
Lemma assoc_L {A} f `{!@Assoc A (=) f} x y z : f x (f y z) = f (f x y) z.
Proof. auto. Qed.
Lemma left_absorb_L {A} i f `{!@LeftAbsorb A (=) i f} x : f i x = i.
Proof. auto. Qed.
Lemma right_absorb_L {A} i f `{!@RightAbsorb A (=) i f} x : f x i = i.
Proof. auto. Qed.

(** ** Generic orders *)
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y  ¬R Y X.
462
Global Instance: Params (@strict) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
463

464
465
466
467
Class PartialOrder {A} (R : relation A) : Prop := {
  partial_order_pre :> PreOrder R;
  partial_order_anti_symm :> AntiSymm (=) R
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Global Hint Mode PartialOrder ! ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
469

470
471
472
473
Class TotalOrder {A} (R : relation A) : Prop := {
  total_order_partial :> PartialOrder R;
  total_order_trichotomy :> Trichotomy (strict R)
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
474
Global Hint Mode TotalOrder ! ! : typeclass_instances.
475
476

(** * Logic *)
477
Global Instance prop_inhabited : Inhabited Prop := populate True.
Robbert Krebbers's avatar
Robbert Krebbers committed
478

479
Notation "(∧)" := and (only parsing) : stdpp_scope.
480
481
Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
Notation "(.∧ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
482

483
Notation "(∨)" := or (only parsing) : stdpp_scope.
484
485
Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope.
Notation "(.∨ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
486

487
Notation "(↔)" := iff (only parsing) : stdpp_scope.
488
489
Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
Notation "(.↔ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
490

491
492
Global Hint Extern 0 (_  _) => reflexivity : core.
Global Hint Extern 0 (_  _) => symmetry; assumption : core.
493
494
495
496
497
498
499
500
501
502
503

Lemma or_l P Q : ¬Q  P  Q  P.
Proof. tauto. Qed.
Lemma or_r P Q : ¬P  P  Q  Q.
Proof. tauto. Qed.
Lemma and_wlog_l (P Q : Prop) : (Q  P)  Q  (P  Q).
Proof. tauto. Qed.
Lemma and_wlog_r (P Q : Prop) : P  (P  Q)  (P  Q).
Proof. tauto. Qed.
Lemma impl_transitive (P Q R : Prop) : (P  Q)  (Q  R)  (P  R).
Proof. tauto. Qed.
504
505
506
507
508
509
Lemma forall_proper {A} (P Q : A  Prop) :
  ( x, P x  Q x)  ( x, P x)  ( x, Q x).
Proof. firstorder. Qed.
Lemma exist_proper {A} (P Q : A  Prop) :
  ( x, P x  Q x)  ( x, P x)  ( x, Q x).
Proof. firstorder. Qed.
510

511
Global Instance eq_comm {A} : Comm () (=@{A}).
512
Proof. red; intuition. Qed.
513
Global Instance flip_eq_comm {A} : Comm () (λ x y, y =@{A} x).
514
Proof. red; intuition. Qed.
515
Global Instance iff_comm : Comm () ().
516
Proof. red; intuition. Qed.
517
Global Instance and_comm : Comm () ().
518
Proof. red; intuition. Qed.
519
Global Instance and_assoc : Assoc () ().
520
Proof. red; intuition. Qed.
521
Global Instance and_idemp : IdemP () ().
522
Proof. red; intuition. Qed.
523
Global Instance or_comm : Comm () ().
524
Proof. red; intuition. Qed.
525
Global Instance or_assoc : Assoc () ().
526
Proof. red; intuition. Qed.
527
Global Instance or_idemp : IdemP () ().
528
Proof. red; intuition. Qed.
529
Global Instance True_and : LeftId () True ().
530
Proof. red; intuition. Qed.
531
Global Instance and_True : RightId () True ().
532
Proof. red; intuition. Qed.
533
Global Instance False_and : LeftAbsorb () False ().
534
Proof. red; intuition. Qed.
535
Global Instance and_False : RightAbsorb () False ().
536
Proof. red; intuition. Qed.
537
Global Instance False_or : LeftId () False ().
538
Proof. red; intuition. Qed.
539
Global Instance or_False : RightId () False ().
540
Proof. red; intuition. Qed.
541
Global Instance True_or : LeftAbsorb () True ().
542
Proof. red; intuition. Qed.
543
Global Instance or_True : RightAbsorb () True ().
544
Proof. red; intuition. Qed.
545
Global Instance True_impl : LeftId () True impl.
546
Proof. unfold impl. red; intuition. Qed.
547
Global Instance impl_True : RightAbsorb () True impl.
548
549
550
551
552
Proof. unfold impl. red; intuition. Qed.


(** * Common data types *)
(** ** Functions *)
553
Notation "(→)" := (λ A B, A  B) (only parsing) : stdpp_scope.
554
555
Notation "( A →.)" := (λ B, A  B) (only parsing) : stdpp_scope.
Notation "(.→ B )" := (λ A, A  B) (only parsing) : stdpp_scope.
556

557
Notation "t $ r" := (t r)
558
559
  (at level 65, right associativity, only parsing) : stdpp_scope.
Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope.
560
Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope.
561

562
563
Infix "∘" := compose : stdpp_scope.
Notation "(∘)" := compose (only parsing) : stdpp_scope.
564
565
Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
566

567
Global Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A  B) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
568
569
  populate (λ _, inhabitant).

570
571
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
572
573
574
575
Global Arguments id _ _ / : assert.
Global Arguments compose _ _ _ _ _ _ / : assert.
Global Arguments flip _ _ _ _ _ _ / : assert.
Global Arguments const _ _ _ _ / : assert.
576
Typeclasses Transparent id compose flip const.
577
578
579
580

Definition fun_map {A A' B B'} (f: A'  A) (g: B  B') (h : A  B) : A'  B' :=
  g  h  f.

581
Global Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
582
583
584
  Reflexive R2  Proper (R1 ==> R2) (λ _, x).
Proof. intros ? y1 y2; reflexivity. Qed.

585
Global Instance id_inj {A} : Inj (=) (=) (@id A).
586
Proof. intros ??; auto. Qed.
587
Global Instance compose_inj {A B C} R1 R2 R3 (f : A  B) (g : B  C) :
588
589
590
  Inj R1 R2 f  Inj R2 R3 g  Inj R1 R3 (g  f).
Proof. red; intuition. Qed.

591
Global Instance id_surj {A} : Surj (=) (@id A).
592
Proof. intros y; exists y; reflexivity. Qed.
593
Global Instance compose_surj {A B C} R (f : A  B) (g : B  C) :
594
595
596
597
598
599
  Surj (=) f  Surj R g  Surj R (g  f).
Proof.
  intros ?? x. unfold compose. destruct (surj g x) as [y ?].
  destruct (surj f y) as [z ?]. exists z. congruence.
Qed.

600
Global Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
601
Proof. intros ?; reflexivity. Qed.
602
Global Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
603
Proof. intros ???; reflexivity. Qed.
604
Global Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x).
605
Proof. intros ???; reflexivity. Qed.
606
Global Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x).
607
Proof. intros ???; reflexivity. Qed.
608
Global Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x).
609
Proof. intros ?; reflexivity. Qed.
610
Global Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x).
611
612
613
Proof. intros ?; reflexivity. Qed.

(** ** Lists *)
614
Global Instance list_inhabited {A} : Inhabited (list A) := populate [].
615
616
617
618
619
620
621
622
623

Definition zip_with {A B C} (f : A  B  C) : list A  list B  list C :=
  fix go l1 l2 :=
  match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
Notation zip := (zip_with pair).

(** ** Booleans *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
624
625
626
Global Hint Unfold Is_true : core.
Global Hint Immediate Is_true_eq_left : core.
Global Hint Resolve orb_prop_intro andb_prop_intro : core.
627
628
629
630
631
Notation "(&&)" := andb (only parsing).
Notation "(||)" := orb (only parsing).
Infix "&&*" := (zip_with (&&)) (at level 40).
Infix "||*" := (zip_with (||)) (at level 50).

632
Global Instance bool_inhabated : Inhabited bool := populate true.
633

634
635
636
Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
Infix "=.>" := bool_le (at level 70).
Infix "=.>*" := (Forall2 bool_le) (at level 70).
637
Global Instance: PartialOrder bool_le.
638
Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
639

640
641
642
643
644
645
646
647
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.
648

649
(** ** Unit *)
650
651
Global Instance unit_equiv : Equiv unit := λ _ _, True.
Global Instance unit_equivalence : Equivalence (@{unit}).
652
Proof. repeat split. Qed.
653
Global Instance unit_leibniz : LeibnizEquiv unit.
654
Proof. intros [] []; reflexivity. Qed.
655
Global Instance unit_inhabited: Inhabited unit := populate ().
656

Ralf Jung's avatar
Ralf Jung committed
657
(** ** Empty *)
658
659
Global Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
Global Instance Empty_set_equivalence : Equivalence (@{Empty_set}).
Ralf Jung's avatar
Ralf Jung committed
660
Proof. repeat split. Qed.
661
Global Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
Ralf Jung's avatar
Ralf Jung committed
662
663
Proof. intros [] []; reflexivity. Qed.

664
(** ** Products *)
665
666
Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
667

668
669
Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
670

671
672
673
Global Instance: Params (@pair) 2 := {}.
Global Instance: Params (@fst) 2 := {}.
Global Instance: Params (@snd) 2 := {}.
674

675
676
677
678
679
680
681
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
Definition curry3 {A B C D} (f : A  B  C  D) (p : A * B * C) : D :=
  let '(a,b,c) := p in f a b c.
Definition curry4 {A B C D E} (f : A  B  C  D  E) (p : A * B * C * D) : E :=
  let '(a,b,c,d) := p in f a b c d.

Robbert Krebbers's avatar
Robbert Krebbers committed
682
683
684
685
686
Definition uncurry3 {A B C D} (f : A * B * C  D) (a : A) (b : B) (c : C) : D :=
  f (a, b, c).
Definition uncurry4 {A B C D E} (f : A * B * C * D  E)
  (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).

687
688
Definition prod_map {A A' B B'} (f: A  A') (g: B  B') (p : A * B) : A' * B' :=
  (f (p.1), g (p.2)).
689
Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
690

691
692
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)).
693
Global Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
694

695
Global Instance prod_inhabited {A B} (iA : Inhabited A)
696
697
    (iB : Inhabited B) : Inhabited (A * B) :=
  match iA, iB with populate x, populate y => populate (x,y) end.
698

699
Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
700
Proof. injection 1; auto. Qed.
701
Global Instance prod_map_inj {A A' B B'} (f : A  A') (g : B  B') :
702
703
704
705
706
  Inj (=) (=) f  Inj (=) (=) g  Inj (=) (=) (prod_map f g).
Proof.
  intros ?? [??] [??] ?; simpl in *; f_equal;
    [apply (inj f)|apply (inj g)]; congruence.
Qed.
707

708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
  relation (A * B) := λ x y, R1 (x.1) (y.1)  R2 (x.2) (y.2).
Section prod_relation.
  Context `{R1 : relation A, R2 : relation B}.
  Global Instance prod_relation_refl :
    Reflexive R1  Reflexive R2  Reflexive (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance prod_relation_sym :
    Symmetric R1  Symmetric R2  Symmetric (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance prod_relation_trans :
    Transitive R1  Transitive R2  Transitive (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance prod_relation_equiv :
    Equivalence R1  Equivalence R2  Equivalence (prod_relation R1 R2).
  Proof. split; apply _. Qed.
724

725
726
  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
  Proof. firstorder eauto. Qed.
727
728
  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
  Proof. inversion_clear 1; eauto. Qed.
729
730
731
732
733
  Global Instance fst_proper' : Proper (prod_relation R1 R2 ==> R1) fst.
  Proof. firstorder eauto. Qed.
  Global Instance snd_proper' : Proper (prod_relation R1 R2 ==> R2) snd.
  Proof. firstorder eauto. Qed.
End prod_relation.
Robbert Krebbers's avatar
Robbert Krebbers committed
734

735
736
Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Global Instance pair_proper `{Equiv A, Equiv B} :
737
  Proper (() ==> () ==> ()) (@pair A B) := _.
738
739
740
Global Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B) := _.
Global Instance fst_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@fst A B) := _.
Global Instance snd_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@snd A B) := _.
741
Typeclasses Opaque prod_equiv.
742

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

746
(** ** Sums *)
747
748
Definition sum_map {A A' B B'} (f: A  A') (g: B  B') (xy : A + B) : A' + B' :=
  match xy with inl x => inl (f x) | inr y => inr (g y) end.
749
Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
750

751
Global Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
752
  match iA with populate x => populate (inl x) end.
753
Global Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
754
  match iB with populate y => populate (inl y) end.
755

756
Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
757
Proof. injection 1; auto. Qed.
758
Global Instance inr_inj {A B} : Inj (=) (=) (@inr A B).
759
Proof. injection 1; auto. Qed.
760

761
Global Instance sum_map_inj {A A' B B'} (f : A  A') (g : B  B') :
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
  Inj (=) (=) f  Inj (=) (=) g  Inj (=) (=) (sum_map f g).
Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _)