base.v 40.2 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
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
11
Obligation Tactic := idtac.
Robbert Krebbers's avatar
Robbert Krebbers committed
12

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

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

29 30 31 32
(** 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. *)
33 34
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
35

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

43 44
(** 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
45 46 47
Delimit Scope C_scope with C.
Global Open Scope C_scope.

48
(** Introduce some Haskell style like notations. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

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

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

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

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

85 86 87 88 89 90 91 92 93
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").

94 95
Definition fun_map {A A' B B'} (f : A' -> A) (g : B -> B')
  (h : A -> B) : A' -> B' := g  h  f.
96 97 98 99 100 101 102
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 {_ _ _ _ _ _} _ _ !_ !_ /.

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

109 110 111 112
(** * 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
113 114
Class PropHolds (P : Prop) := prop_holds: P.

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

Ltac solve_propholds :=
  match goal with
121 122
  | |- PropHolds (?P) => apply _
  | |- ?P => change (PropHolds P); apply _
123 124 125 126 127 128 129
  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
130 131 132
Class Decision (P : Prop) := decide : {P} + {¬P}.
Arguments decide _ {_}.

133 134
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
135
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
136 137 138 139 140 141
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) :=
142
  match iA, iB with populate x, populate y => populate (x,y) end.
143
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
144
  match iA with populate x => populate (inl x) end.
145
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
146
  match iB with populate y => populate (inl y) end.
147 148
Instance option_inhabited {A} : Inhabited (option A) := populate None.

149 150 151 152 153 154
(** ** 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.

155 156 157
(** ** 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
158 159 160
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : C_scope.
Notation "(≡)" := equiv (only parsing) : C_scope.
161 162 163 164 165 166
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
167

168 169 170 171
(** 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. *)
172 173 174 175 176
Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x  y  x = y.
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
  x  y  x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
 
177 178 179
Ltac fold_leibniz := repeat
  match goal with
  | H : context [ @equiv ?A _ _ _ ] |- _ =>
180
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
181
  | |- context [ @equiv ?A _ _ _ ] =>
182
    setoid_rewrite (leibniz_equiv_iff (A:=A))
183 184 185 186
  end.
Ltac unfold_leibniz := repeat
  match goal with
  | H : context [ @eq ?A _ _ ] |- _ =>
187
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
188
  | |- context [ @eq ?A _ _ ] =>
189
    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
190 191
  end.

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

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

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

214 215 216
Class Top A := top : A.
Notation "⊤" := top : C_scope.

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

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

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

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

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

283
Hint Extern 0 (_  _) => reflexivity.
284 285 286
Hint Extern 0 (_ * _) => reflexivity.
Hint Extern 0 (_ ** _) => reflexivity.

287 288
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y  ¬R Y X.
Instance: Params (@strict) 2.
289 290 291 292
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.
293 294 295 296
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
297

298 299 300 301 302
(** 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
303
Class ElemOf A B := elem_of: A  B  Prop.
304
Instance: Params (@elem_of) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
305 306 307 308 309 310 311 312 313
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
314 315 316 317
Class Disjoint A := disjoint : A  A  Prop.
Instance: Params (@disjoint) 2.
Infix "⊥" := disjoint (at level 70) : C_scope.
Notation "(⊥)" := disjoint (only parsing) : C_scope.
318
Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
319
Notation "(.⊥ X )" := (λ Y, Y  X) (only parsing) : C_scope.
320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
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.
345 346 347

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

350 351 352 353 354 355
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.
356

357
  Lemma disjoint_list_nil  :  @nil A  True.
358 359 360
  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.
361
End disjoint_list.
362 363

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

(** ** Monadic operations *)
(** We define operational type classes for the monadic operations bind, join 
367 368 369
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). *)
370 371
Class MRet (M : Type  Type) := mret:  {A}, A  M A.
Arguments mret {_ _ _} _.
372
Instance: Params (@mret) 3.
373 374
Class MBind (M : Type  Type) := mbind :  {A B}, (A  M B)  M A  M B.
Arguments mbind {_ _ _ _} _ !_ /.
375
Instance: Params (@mbind) 4.
376
Class MJoin (M : Type  Type) := mjoin:  {A}, M (M A)  M A.
377
Arguments mjoin {_ _ _} !_ /.
378
Instance: Params (@mjoin) 3.
379 380
Class FMap (M : Type  Type) := fmap :  {A B}, (A  B)  M A  M B.
Arguments fmap {_ _ _ _} _ !_ /.
381
Instance: Params (@fmap) 4.
382 383
Class OMap (M : Type  Type) := omap:  {A B}, (A  option B)  M A  M B.
Arguments omap {_ _ _ _} _ !_ /.
384
Instance: Params (@omap) 4.
385

386 387 388 389 390 391
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
392
  (at level 65, only parsing, right associativity) : C_scope.
393
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
394
Notation "' ( x1 , x2 ) ← y ; z" :=
395
  (y = (λ x : _, let ' (x1, x2) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
396
  (at level 65, only parsing, right associativity) : C_scope.
397
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
398
  (y = (λ x : _, let ' (x1,x2,x3) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
399
  (at level 65, only parsing, right associativity) : C_scope.
400
Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
401
  (y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  (at level 65, only parsing, right associativity) : C_scope.
403 404
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
405
  (at level 65, only parsing, right associativity) : C_scope.
406 407
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
408
  (at level 65, only parsing, right associativity) : C_scope.
409

410 411 412 413 414
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").

415
Class MGuard (M : Type  Type) :=
416 417 418
  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
419
  (at level 65, only parsing, right associativity) : C_scope.
420
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
Robbert Krebbers's avatar
Robbert Krebbers committed
421
  (at level 65, only parsing, right associativity) : C_scope.
422

423
(** ** Operations on maps *)
424 425
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
426
The function look up [m !! k] should yield the element at key [k] in [m]. *)
427
Class Lookup (K A M : Type) := lookup: K  M  option A.
428 429 430
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope.
431
Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
432
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
433
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
434

435 436 437
(** The singleton map *)
Class SingletonM K A M := singletonM: K  A  M.
Instance: Params (@singletonM) 5.
438
Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
439

440 441
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
442
Class Insert (K A M : Type) := insert: K  A  M  M.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Instance: Params (@insert) 5.
444 445
Notation "<[ k := a ]>" := (insert k a)
  (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
446
Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
447

448 449 450
(** 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. *)
451
Class Delete (K M : Type) := delete: K  M  M.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
Instance: Params (@delete) 4.
453
Arguments delete _ _ _ !_ !_ / : simpl nomatch.
454 455

(** The function [alter f k m] should update the value at key [k] using the
456
function [f], which is called with the original value. *)
457
Class Alter (K A M : Type) := alter: (A  A)  K  M  M.
458
Instance: Params (@alter) 5.
459
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
460 461

(** The function [alter f k m] should update the value at key [k] using the
462 463 464
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]. *)
465 466
Class PartialAlter (K A M : Type) :=
  partial_alter: (option A  option A)  K  M  M.
467
Instance: Params (@partial_alter) 4.
468
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
469 470 471

(** 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]. *)
472 473 474
Class Dom (M C : Type) := dom: M  C.
Instance: Params (@dom) 3.
Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
475 476

(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
477 478 479 480 481
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.
482

483 484 485 486 487
(** 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.
488
Instance: Params (@union_with) 3.
489
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
490

491 492 493
(** Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type) :=
  intersection_with: (A  A  option A)  M  M  M.
494
Instance: Params (@intersection_with) 3.
495 496
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.

497 498
Class DifferenceWith (A M : Type) :=
  difference_with: (A  A  option A)  M  M  M.
499
Instance: Params (@difference_with) 3.
500
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
501

502 503 504 505
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 _ _ _ _ _ !_ /.

506 507 508 509 510 511 512 513
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
514
Instance: Params (@insertE) 6.
515 516 517 518
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.

519 520 521
(** ** 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
522 523 524 525
allows us to write [inj (k ++)] instead of [app_inv_head k]. *)
Class Inj {A B} (R : relation A) (S : relation B) (f : A  B) : Prop :=
  inj x y : S (f x) (f y)  R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
526
    (S : relation C) (f : A  B  C) : Prop :=
527
  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2)  R1 x1 y1  R2 x2 y2.
528
Class Cancel {A B} (S : relation B) (f : A  B) (g : B  A) : Prop :=
529 530 531 532 533 534 535
  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).
536
Class LeftId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
537
  left_id x : R (f i x) x.
538
Class RightId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
539 540 541
  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).
542
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
543
  left_absorb x : R (f i x) i.
544
Class RightAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
545 546 547
  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.
548 549
Class Total {A} (R : relation A) := total x y : R x y  R y x.
Class Trichotomy {A} (R : relation A) :=
550
  trichotomy x y : R x y  x = y  R y x.
551
Class TrichotomyT {A} (R : relation A) :=
552
  trichotomyT x y : {R x y} + {x = y} + {R y x}.
Robbert Krebbers's avatar
Robbert Krebbers committed
553

554
Arguments irreflexivity {_} _ {_} _ _.
555 556
Arguments inj {_ _ _ _} _ {_} _ _ _.
Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
557
Arguments cancel {_ _ _} _ _ {_} _.
558 559 560
Arguments surj {_ _ _} _ {_} _.
Arguments idemp {_ _} _ {_} _.
Arguments comm {_ _ _} _ {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
561 562
Arguments left_id {_ _} _ _ {_} _.
Arguments right_id {_ _} _ _ {_} _.
563
Arguments assoc {_ _} _ {_} _ _ _.
564 565
Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
566
Arguments anti_symm {_ _} _ {_} _ _ _ _.
567 568 569
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.
570

571
Instance id_inj {A} : Inj (=) (=) (@id A).
572 573
Proof. intros ??; auto. Qed.

574 575 576
(** 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. *)
577
Lemma idemp_L {A} (f : A  A  A) `{!IdemP (=) f} x : f x x = x.
578
Proof. auto. Qed.
579
Lemma comm_L {A B} (f : B  B  A) `{!Comm (=) f} x y :
580
  f x y = f y x.
581
Proof. auto. Qed.
582
Lemma left_id_L {A} (i : A) (f : A  A  A) `{!LeftId (=) i f} x : f i x = x.
583
Proof. auto. Qed.
584
Lemma right_id_L {A} (i : A) (f : A  A  A) `{!RightId (=) i f} x : f x i = x.
585
Proof. auto. Qed.
586
Lemma assoc_L {A} (f : A  A  A) `{!Assoc (=) f} x y z :
587
  f x (f y z) = f (f x y) z.
588
Proof. auto. Qed.
589
Lemma left_absorb_L {A} (i : A) (f : A  A  A) `{!LeftAbsorb (=) i f} x :
590 591
  f i x = i.
Proof. auto. Qed.
592
Lemma right_absorb_L {A} (i : A) (f : A  A  A) `{!RightAbsorb (=) i f} x :
593 594
  f x i = i.
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
595

596
(** ** Axiomatization of ordered structures *)
597 598
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
relation [R] instead of [⊆] to support multiple orders on the same type. *)
599
Class PartialOrder {A} (R : relation A) : Prop := {
600
  partial_order_pre :> PreOrder R;
601
  partial_order_anti_symm :> AntiSymm (=) R
602 603
}.
Class TotalOrder {A} (R : relation A) : Prop := {
604 605
  total_order_partial :> PartialOrder R;
  total_order_trichotomy :> Trichotomy (strict R)
606 607
}.

608 609 610 611 612 613
(** 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 ();
614 615 616
  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
617
}.
618 619
Class MeetSemiLattice A `{SubsetEq A, Intersection A} : Prop := {
  meet_semi_lattice_pre :>> PreOrder ();
620 621 622
  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
623
}.
624 625 626 627
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)
628
}.
629

630
(** ** Axiomatization of collections *)
631 632
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *)
633 634
Class SimpleCollection A C `{ElemOf A C,
    Empty C, Singleton A C, Union C} : Prop := {
635
  not_elem_of_empty (x : A) : x  ;
636
  elem_of_singleton (x y : A) : x  {[ y ]}  x = y;
637 638
  elem_of_union X Y (x : A) : x  X  Y  x  X  x  Y
}.
639 640
Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
    Union C, Intersection C, Difference C} : Prop := {
641
  collection_simple :>> SimpleCollection A C;
Robbert Krebbers's avatar
Robbert Krebbers committed
642
  elem_of_intersection X Y (x : A) : x  X  Y  x  X  x  Y;
643 644
  elem_of_difference X Y (x : A) : x  X  Y  x  X  x  Y
}.
645 646
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 := {
647
  collection_ops :>> Collection A C;
648
  elem_of_intersection_with (f : A  A  option A) X Y (x : A) :
649
    x  intersection_with f X Y   x1 x2, x1  X  x2  Y  f x1 x2 = Some x;
650
  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
651 652
}.

653 654 655
(** 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
656
Class Elements A C := elements: C  list A.
657
Instance: Params (@elements) 3.
658 659 660 661 662 663 664 665 666 667 668 669 670

(** 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. *)
671 672 673
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
674
  fin_collection :>> Collection A C;
675 676
  elem_of_elements X x : x  elements X  x  X;
  NoDup_elements X : NoDup (elements X)
677 678
}.
Class Size C := size: C  nat.
679
Arguments size {_ _} !_ / : simpl nomatch.
680
Instance: Params (@size) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
681

682 683 684 685 686 687 688 689
(** 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]. *)
690 691 692
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 := {
693 694 695
  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;
696
  elem_of_ret {A} (x y : A) : x  mret y  x = y;
697 698
  elem_of_fmap {A B} (f : A  B) (X : M A) (x : B) :
    x  f <$> X   y, x = f y  y  X;
699
  elem_of_join {A} (X : M (M A)) (x : A) : x  mjoin X   Y, x  Y  Y  X
700 701
}.

702 703 704
(** 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
705
Class Fresh A C := fresh: C  A.
706
Instance: Params (@fresh) 3.
707 708
Class FreshSpec A C `{ElemOf A C,
    Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
709
  fresh_collection_simple :>> SimpleCollection A C;
710
  fresh_proper_alt X Y : ( x, x  X  x  Y)  fresh X = fresh Y;
Robbert Krebbers's avatar
Robbert Krebbers committed
711 712 713
  is_fresh (X : C) : fresh X  X
}.

714 715 716
(** * Booleans *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
717
Hint Unfold Is_true.
718
Hint Immediate Is_true_eq_left.
719
Hint Resolve orb_prop_intro andb_prop_intro.
720 721 722 723 724 725 726 727 728 729 730
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.

731 732 733 734 735 736 737 738 739
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.

740
(** * Miscellaneous *)
741
Class Half A := half: A  A.
742 743
Notation "½" := half : C_scope.
Notation "½*" := (fmap (M:=list) half) : C_scope.
744

745 746
Lemma proj1_sig_inj {A} (P : A  Prop) x (Px : P x) y (Py : P y) :
  xPx = yPy  x = y.
747
Proof. injection 1; trivial. Qed.
748
Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y  ¬R y x.
749
Proof. intuition. Qed.
750
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y  R y x.
751 752
Proof. intuition. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
753 754 755 756 757
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.

758
(** ** Products *)
759 760
Instance prod_map_inj {A A' B B'} (f : A  A') (g : B  B') :
  Inj (=) (=) f  Inj (=) (=) g  Inj (=) (=) (prod_map f g).
761 762
Proof.
  intros ?? [??] [??] ?; simpl in *; f_equal;
763
    [apply (inj f)|apply (inj g)]; congruence.
764
Qed.
765

766
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
767
  relation (A * B) := λ x y, R1 (x.1) (y.1)  R2 (x.2) (y.2).
Robbert Krebbers's avatar
Robbert Krebbers committed
768
Section prod_relation.
769
  Context `{R1 : relation A, R2 : relation B}.
770 771
  Global Instance:
    Reflexive R1  Reflexive R2  Reflexive (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
772
  Proof. firstorder eauto. Qed.
773 774
  Global Instance:
    Symmetric R1  Symmetric R2  Symmetric (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
775
  Proof. firstorder eauto. Qed.
776 777
  Global Instance:
    Transitive R1  Transitive R2  Transitive (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
778
  Proof. firstorder eauto. Qed.
Robbert Krebbers's avatar