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

11 12 13 14
(** * General *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.

15 16
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
17
Arguments id _ _ /.
18
Arguments compose _ _ _ _ _ _ /.
19
Arguments flip _ _ _ _ _ _ /.
20
Typeclasses Transparent id compose flip.
21

22 23 24 25
(** 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. *)
26 27
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
28

29 30 31
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.

32 33
(** 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
34 35 36
Delimit Scope C_scope with C.
Global Open Scope C_scope.

37
(** Introduce some Haskell style like notations. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40 41 42 43 44 45 46
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.

47 48 49 50
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.

51
Notation "t $ r" := (t r)
52
  (at level 65, right associativity, only parsing) : C_scope.
53 54 55
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
56 57 58 59
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.
60

61 62 63 64 65 66 67 68 69 70 71 72
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.

73 74
(** Set convenient implicit arguments for [existT] and introduce notations. *)
Arguments existT {_ _} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76 77
Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
Notation "` x" := (proj1_sig x) : C_scope.

78 79 80 81
(** * 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
82 83
Class PropHolds (P : Prop) := prop_holds: P.

84 85
Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
Instance: Proper (iff ==> iff) PropHolds.
86
Proof. repeat intro; trivial. Qed.
87 88 89

Ltac solve_propholds :=
  match goal with
90 91
  | |- PropHolds (?P) => apply _
  | |- ?P => change (PropHolds P); apply _
92 93 94 95 96 97 98
  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
99 100 101
Class Decision (P : Prop) := decide : {P} + {¬P}.
Arguments decide _ {_}.

102 103 104 105 106 107 108 109 110
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Prop := populate { _ : A }.
Arguments populate {_} _.

Instance unit_inhabited: Inhabited unit := populate ().
Instance list_inhabited {A} : Inhabited (list A) := populate [].
Instance prod_inhabited {A B} (iA : Inhabited A)
    (iB : Inhabited B) : Inhabited (A * B) :=
111
  match iA, iB with populate x, populate y => populate (x,y) end.
112
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
113
  match iA with populate x => populate (inl x) end.
114
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
115
  match iB with populate y => populate (inl y) end.
116 117
Instance option_inhabited {A} : Inhabited (option A) := populate None.

118 119 120 121 122 123
(** ** 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.

124 125 126
(** ** 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
127 128 129 130 131 132 133 134 135 136
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : C_scope.
Notation "(≡)" := equiv (only parsing) : C_scope.
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.

137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
(** 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.

158 159 160 161 162 163 164 165
(** 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
166
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
167 168
Hint Extern 0 (_  _) => reflexivity.
Hint Extern 0 (_  _) => symmetry; assumption.
Robbert Krebbers's avatar
Robbert Krebbers committed
169

170
(** ** Operations on collections *)
171
(** We define operational type classes for the traditional operations and
172
relations on collections: the empty collection [∅], the union [(∪)],
173 174
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176 177 178
Class Empty A := empty: A.
Notation "∅" := empty : C_scope.

Class Union A := union: A  A  A.
179
Instance: Params (@union) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182 183 184
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.

185
Definition union_list `{Empty A} `{Union A} : list A  A := fold_right () .
186 187 188
Arguments union_list _ _ _ !_ /.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
189
Class Intersection A := intersection: A  A  A.
190
Instance: Params (@intersection) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193 194 195 196
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.
197
Instance: Params (@difference) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199 200 201 202
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.

203 204
Class Singleton A B := singleton: A  B.
Instance: Params (@singleton) 3.
205
Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope.
206
Notation "{[ x ; y ; .. ; z ]}" :=
207 208 209 210 211 212
  (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.
213

214
Class SubsetEq A := subseteq: relation A.
215
Instance: Params (@subseteq) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218 219 220 221 222 223
Infix "⊆" := subseteq (at level 70) : C_scope.
Notation "(⊆)" := subseteq (only parsing) : C_scope.
Notation "( X ⊆ )" := (subseteq X) (only parsing) : C_scope.
Notation "( ⊆ X )" := (λ Y, subseteq Y X) (only parsing) : C_scope.
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.
224 225
Infix "⊆*" := (Forall2 subseteq) (at level 70) : C_scope.
Notation "(⊆*)" := (Forall2 subseteq) (only parsing) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
226

227 228
Hint Extern 0 (_  _) => reflexivity.

229 230 231 232 233 234
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y  ¬R Y X.
Instance: Params (@strict) 2.
Infix "⊂" := (strict subseteq) (at level 70) : C_scope.
Notation "(⊂)" := (strict subseteq) (only parsing) : C_scope.
Notation "( X ⊂ )" := (strict subseteq X) (only parsing) : C_scope.
Notation "( ⊂ X )" := (λ Y, strict subseteq Y X) (only parsing) : C_scope.
235 236 237 238
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
239

240 241 242 243 244
(** 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
245
Class ElemOf A B := elem_of: A  B  Prop.
246
Instance: Params (@elem_of) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
247 248 249 250 251 252 253 254 255
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
256 257 258 259
Class Disjoint A := disjoint : A  A  Prop.
Instance: Params (@disjoint) 2.
Infix "⊥" := disjoint (at level 70) : C_scope.
Notation "(⊥)" := disjoint (only parsing) : C_scope.
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
Notation "(.⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope.

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

Section default_disjoint_list.
  Context `{Empty A} `{Union A} `{Disjoint A}.
  Inductive default_disjoint_list : DisjointList A :=
    | disjoint_nil_2 :  []
    | disjoint_cons_2 X Xs : X   Xs   Xs   (X :: Xs).
  Global Existing Instance default_disjoint_list.

  Lemma disjoint_list_nil :  @nil A  True.
  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.
End default_disjoint_list.

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

282 283 284 285 286
(** We define variants of the relations [(≡)] and [(⊆)] that are indexed by
an environment. *)
Class EquivEnv A B := equiv_env : A  relation B.
Notation "X ≡@{ E } Y" := (equiv_env E X Y)
  (at level 70, format "X  ≡@{ E }  Y") : C_scope.
287
Notation "(≡@{ E } )" := (equiv_env E) (E at level 1, only parsing) : C_scope.
288 289 290
Instance: Params (@equiv_env) 4.

Class SubsetEqEnv A B := subseteq_env : A  relation B.
291 292 293 294 295 296 297 298
Instance: Params (@subseteq_env) 4.
Notation "X ⊑@{ E } Y" := (subseteq_env E X Y)
  (at level 70, format "X  ⊑@{ E }  Y") : C_scope.
Notation "(⊑@{ E } )" := (subseteq_env E)
  (E at level 1, only parsing) : C_scope.
Notation "X ⊑@{ E }* Y" := (Forall2 (subseteq_env E) X Y)
  (at level 70, format "X  ⊑@{ E }*  Y") : C_scope.
Notation "(⊑@{ E }*)" := (Forall2 (subseteq_env E))
299 300 301
  (E at level 1, only parsing) : C_scope.
Instance: Params (@subseteq_env) 4.

302 303 304
Hint Extern 0 (_ @{_} _) => reflexivity.
Hint Extern 0 (_ @{_} _) => reflexivity.

305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320
(** ** Monadic operations *)
(** We define operational type classes for the monadic operations bind, join 
and fmap. These type classes are defined in a non-standard way by taking the
function as a parameter of the class. For example, we define
<<
  Class FMapD := fmap: ∀ {A B}, (A → B) → M A → M B.
>>
instead of
<<
  Class FMap {A B} (f : A → B) := fmap: M A → M B.
>>
This approach allows us to define [fmap] on lists such that [simpl] unfolds it
in the appropriate way, and so that it can be used for mutual recursion
(the mapped function [f] is not part of the fixpoint) as well. This is a hack,
and should be replaced by something more appropriate in future versions. *)

321
(** We use these type classes merely for convenient overloading of notations and
322 323 324 325 326 327 328 329 330
do not formalize any theory on monads (we do not even define a class with the
monad laws). *)
Class MRet (M : Type  Type) := mret:  {A}, A  M A.
Instance: Params (@mret) 3.
Arguments mret {_ _ _} _.

Class MBindD (M : Type  Type) {A B} (f : A  M B) := mbind: M A  M B.
Notation MBind M := ( {A B} (f : A  M B), MBindD M f)%type.
Instance: Params (@mbind) 5.
331
Arguments mbind {_ _ _} _ {_} !_ /.
332 333 334

Class MJoin (M : Type  Type) := mjoin:  {A}, M (M A)  M A.
Instance: Params (@mjoin) 3.
335
Arguments mjoin {_ _ _} !_ /.
336 337 338 339

Class FMapD (M : Type  Type) {A B} (f : A  B) := fmap: M A  M B.
Notation FMap M := ( {A B} (f : A  B), FMapD M f)%type.
Instance: Params (@fmap) 6.
340
Arguments fmap {_ _ _} _ {_} !_ /.
341 342 343 344 345 346 347

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))
348
  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
349
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
350 351

Class MGuard (M : Type  Type) :=
352 353 354 355 356 357
  mguard:  P {dec : Decision P} {A}, (P  M A)  M A.
Arguments mguard _ _ _ !_ _ _ /.
Notation "'guard' P ; o" := (mguard P (λ _, o))
  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
358

359
(** ** Operations on maps *)
360 361
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
362
The function look up [m !! k] should yield the element at key [k] in [m]. *)
363
Class Lookup (K A M : Type) := lookup: K  M  option A.
364 365 366 367 368 369
Instance: Params (@lookup) 4.

Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope.
Notation "( m !!)" := (λ i, lookup i m) (only parsing) : C_scope.
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
370
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
371 372 373

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

380 381 382
(** 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. *)
383
Class Delete (K M : Type) := delete: K  M  M.
384 385
Instance: Params (@delete) 3.
Arguments delete _ _ _ !_ !_ / : simpl nomatch.
386 387

(** The function [alter f k m] should update the value at key [k] using the
388
function [f], which is called with the original value. *)
389
Class AlterD (K A M : Type) (f : A  A) := alter: K  M  M.
390 391 392
Notation Alter K A M := ( (f : A  A), AlterD K A M f)%type.
Instance: Params (@alter) 5.
Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
393 394

(** The function [alter f k m] should update the value at key [k] using the
395 396 397
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]. *)
398 399
Class PartialAlter (K A M : Type) :=
  partial_alter: (option A  option A)  K  M  M.
400
Instance: Params (@partial_alter) 4.
401
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
402 403 404

(** 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]. *)
405 406 407
Class Dom (M C : Type) := dom: M  C.
Instance: Params (@dom) 3.
Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
408 409

(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
410 411 412 413 414
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.
415 416

(** We lift the insert and delete operation to lists of elements. *)
417
Definition insert_list `{Insert K A M} (l : list (K * A)) (m : M) : M :=
418 419
  fold_right (λ p, <[ fst p := snd p ]>) m l.
Instance: Params (@insert_list) 4.
420
Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
421
  fold_right delete m l.
422 423 424 425 426 427 428
Instance: Params (@delete_list) 3.

(** 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.
429
Instance: Params (@union_with) 3.
430
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
431

432 433 434
(** Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type) :=
  intersection_with: (A  A  option A)  M  M  M.
435
Instance: Params (@intersection_with) 3.
436 437
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.

438 439
Class DifferenceWith (A M : Type) :=
  difference_with: (A  A  option A)  M  M  M.
440
Instance: Params (@difference_with) 3.
441
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
442

443 444 445 446
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 _ _ _ _ _ !_ /.

447 448 449 450
(** ** 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]. *)
451 452 453 454 455
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.
456 457 458 459
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.
460
Class Idempotent {A} (R : relation A) (f : A  A  A) : Prop :=
461
  idempotent:  x, R (f x x) x.
462
Class Commutative {A B} (R : relation A) (f : B  B  A) : Prop :=
463
  commutative:  x y, R (f x y) (f y x).
464
Class LeftId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
465
  left_id:  x, R (f i x) x.
466
Class RightId {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
467
  right_id:  x, R (f x i) x.
468
Class Associative {A} (R : relation A) (f : A  A  A) : Prop :=
469
  associative:  x y z, R (f x (f y z)) (f (f x y) z).
470
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
471
  left_absorb:  x, R (f i x) i.
472
Class RightAbsorb {A} (R : relation A) (i : A) (f : A  A  A) : Prop :=
473
  right_absorb:  x, R (f x i) i.
474 475 476 477
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)).
478 479
Class AntiSymmetric {A} (R S : relation A) : Prop :=
  anti_symmetric:  x y, S x y  S y x  R x y.
480 481 482 483 484
Class Total {A} (R : relation A) := total x y : R x y  R y x.
Class Trichotomy {A} (R : relation A) :=
  trichotomy :  x y, strict R x y  x = y  strict R y x.
Class TrichotomyT {A} (R : relation A) :=
  trichotomyT :  x y, {strict R x y} + {x = y} + {strict R y x}.
Robbert Krebbers's avatar
Robbert Krebbers committed
485

486
Arguments irreflexivity {_} _ {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
487
Arguments injective {_ _ _ _} _ {_} _ _ _.
488
Arguments injective2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
489 490
Arguments cancel {_ _ _} _ _ {_} _.
Arguments surjective {_ _ _} _ {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
491 492 493 494 495
Arguments idempotent {_ _} _ {_} _.
Arguments commutative {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
Arguments right_id {_ _} _ _ {_} _.
Arguments associative {_ _} _ {_} _ _ _.
496 497
Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
498 499
Arguments left_distr {_ _} _ _ {_} _ _ _.
Arguments right_distr {_ _} _ _ {_} _ _ _.
500
Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
501 502 503
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.
504

505 506 507 508
(** 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.
509
Proof. auto. Qed.
510
Lemma commutative_L {A B} (f : B  B  A) `{!Commutative (=) f} x y :
511
  f x y = f y x.
512
Proof. auto. Qed.
513
Lemma left_id_L {A} (i : A) (f : A  A  A) `{!LeftId (=) i f} x : f i x = x.
514
Proof. auto. Qed.
515
Lemma right_id_L {A} (i : A) (f : A  A  A) `{!RightId (=) i f} x : f x i = x.
516
Proof. auto. Qed.
517
Lemma associative_L {A} (f : A  A  A) `{!Associative (=) f} x y z :
518
  f x (f y z) = f (f x y) z.
519
Proof. auto. Qed.
520
Lemma left_absorb_L {A} (i : A) (f : A  A  A) `{!LeftAbsorb (=) i f} x :
521 522
  f i x = i.
Proof. auto. Qed.
523
Lemma right_absorb_L {A} (i : A) (f : A  A  A) `{!RightAbsorb (=) i f} x :
524 525
  f x i = i.
Proof. auto. Qed.
526
Lemma left_distr_L {A} (f g : A  A  A) `{!LeftDistr (=) f g} x y z :
527 528
  f x (g y z) = g (f x y) (f x z).
Proof. auto. Qed.
529
Lemma right_distr_L {A} (f g : A  A  A) `{!RightDistr (=) f g} y z x :
530 531
  f (g y z) x = g (f y x) (f z x).
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
532

533
(** ** Axiomatization of ordered structures *)
534 535 536 537 538 539 540 541 542 543 544
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] do not use the
relation [⊆] because we often have multiple orders on the same structure. *)
Class PartialOrder {A} (R : relation A) : Prop := {
  po_preorder :> PreOrder R;
  po_anti_symmetric :> AntiSymmetric (=) R
}.
Class TotalOrder {A} (R : relation A) : Prop := {
  to_po :> PartialOrder R;
  to_trichotomy :> Trichotomy R
}.

545 546
(** A pre-order equipped with a smallest element. *)
Class BoundedPreOrder A `{Empty A} `{SubsetEq A} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548 549 550
  bounded_preorder :>> PreOrder ();
  subseteq_empty x :   x
}.

551
(** We do not include equality in the following interfaces so as to avoid the
552
need for proofs that the relations and operations respect setoid equality.
553 554
Instead, we will define setoid equality in a generic way as
[λ X Y, X ⊆ Y ∧ Y ⊆ X]. *)
555
Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} : Prop := {
556
  bjsl_preorder :>> BoundedPreOrder A;
557 558
  union_subseteq_l x y : x  x  y;
  union_subseteq_r x y : y  x  y;
Robbert Krebbers's avatar
Robbert Krebbers committed
559 560
  union_least x y z : x  z  y  z  x  y  z
}.
561
Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
562
  msl_preorder :>> BoundedPreOrder A;
563 564
  intersection_subseteq_l x y : x  y  x;
  intersection_subseteq_r x y : x  y  y;
Robbert Krebbers's avatar
Robbert Krebbers committed
565 566
  intersection_greatest x y z : z  x  z  y  z  x  y
}.
567 568 569 570

(** A join distributive lattice with distributivity stated in the order
theoretic way. We will prove that distributivity of join, and distributivity
as an equality can be derived. *)
571
Class LowerBoundedLattice A `{Empty A} `{SubsetEq A}
572
    `{Union A} `{Intersection A} : Prop := {
573
  lbl_bjsl :>> BoundedJoinSemiLattice A;
574 575
  lbl_msl :>> MeetSemiLattice A;
  lbl_distr x y z : (x  y)  (x  z)  x  (y  z)
576
}.
577

578
(** ** Axiomatization of collections *)
579 580
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *)
581
Instance: Params (@map) 3.
582
Class SimpleCollection A C `{ElemOf A C}
583
    `{Empty C} `{Singleton A C} `{Union C} : Prop := {
584
  not_elem_of_empty (x : A) : x  ;
585
  elem_of_singleton (x y : A) : x  {[ y ]}  x = y;
586 587 588
  elem_of_union X Y (x : A) : x  X  Y  x  X  x  Y
}.
Class Collection A C `{ElemOf A C} `{Empty C} `{Singleton A C}
589
    `{Union C} `{Intersection C} `{Difference C} : Prop := {
590
  collection_simple :>> SimpleCollection A C;
Robbert Krebbers's avatar
Robbert Krebbers committed
591
  elem_of_intersection X Y (x : A) : x  X  Y  x  X  x  Y;
592 593 594 595 596 597 598
  elem_of_difference X Y (x : A) : x  X  Y  x  X  x  Y
}.
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 := {
  collection_ops :>> Collection A C;
599
  elem_of_intersection_with (f : A  A  option A) X Y (x : A) :
600 601 602
    x  intersection_with f X Y   x1 x2, x1  X  x2  Y  f x1 x2 = Some x;
  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
603 604
}.

605 606 607
(** 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
608
Class Elements A C := elements: C  list A.
609
Instance: Params (@elements) 3.
610 611 612 613 614 615 616 617 618 619 620 621 622 623

(** 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. *)
Class FinCollection A C `{ElemOf A C} `{Empty C} `{Singleton A C}
624 625
    `{Union C} `{Intersection C} `{Difference C}
    `{Elements A C} `{ x y : A, Decision (x = y)} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
626
  fin_collection :>> Collection A C;
627
  elements_spec X x : x  X  x  elements X;
Robbert Krebbers's avatar
Robbert Krebbers committed
628
  elements_nodup X : NoDup (elements X)
629 630
}.
Class Size C := size: C  nat.
631
Arguments size {_ _} !_ / : simpl nomatch.
632
Instance: Params (@size) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
633

634 635 636 637 638 639 640 641 642 643
(** 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]. *)
Class CollectionMonad M `{ A, ElemOf A (M A)}
    `{ A, Empty (M A)} `{ A, Singleton A (M A)} `{ A, Union (M A)}
644
    `{!MBind M} `{!MRet M} `{!FMap M} `{!MJoin M} : Prop := {
645 646 647
  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;
648
  elem_of_ret {A} (x y : A) : x  mret y  x = y;
649 650
  elem_of_fmap {A B} (f : A  B) (X : M A) (x : B) :
    x  f <$> X   y, x = f y  y  X;
651
  elem_of_join {A} (X : M (M A)) (x : A) : x  mjoin X   Y, x  Y  Y  X
652 653
}.

654 655 656
(** 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
657
Class Fresh A C := fresh: C  A.
658
Instance: Params (@fresh) 3.
659
Class FreshSpec A C `{ElemOf A C}
660
    `{Empty C} `{Singleton A C} `{Union C} `{Fresh A C} : Prop := {
661
  fresh_collection_simple :>> SimpleCollection A C;
662
  fresh_proper_alt X Y : ( x, x  X  x  Y)  fresh X = fresh Y;
Robbert Krebbers's avatar
Robbert Krebbers committed
663 664 665
  is_fresh (X : C) : fresh X  X
}.

666
(** * Miscellaneous *)
667 668 669
Class Half A := half: A  A.
Notation "x .½" := (half x) (at level 20, format "x .½") : C_scope.

670 671
Lemma proj1_sig_inj {A} (P : A  Prop) x (Px : P x) y (Py : P y) :
  xPx = yPy  x = y.
672
Proof. injection 1; trivial. Qed.
673
Lemma not_symmetry `{R : relation A} `{!Symmetric R} x y : ¬R x y  ¬R y x.
674
Proof. intuition. Qed.
675
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y  R y x.
676 677
Proof. intuition. Qed.

678 679 680
(** ** Pointwise relations *)
(** These instances are in Coq trunk since revision 15455, but are not in Coq
8.4 yet. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
681 682 683 684 685 686 687 688 689 690
Instance pointwise_reflexive {A} `{R : relation B} :
  Reflexive R  Reflexive (pointwise_relation A R) | 9.
Proof. firstorder. Qed.
Instance pointwise_symmetric {A} `{R : relation B} :
  Symmetric R  Symmetric (pointwise_relation A R) | 9.
Proof. firstorder. Qed.
Instance pointwise_transitive {A} `{R : relation B} :
  Transitive R  Transitive (pointwise_relation A R) | 9.
Proof. firstorder. Qed.

691
(** ** Products *)
692 693 694 695
Definition fst_map {A A' B} (f : A  A') (p : A * B) : A' * B :=
  (f (fst p), snd p).
Definition snd_map {A B B'} (f : B  B') (p : A * B) : A * B' :=
  (fst p, f (snd p)).
696 697 698 699 700
Arguments fst_map {_ _ _} _ !_ /.
Arguments snd_map {_ _ _} _ !_ /.

Instance:  {A A' B} (f : A  A'),
  Injective (=) (=) f  Injective (=) (=) (@fst_map A A' B f).
701
Proof. intros ????? [??] [??]; injection 1; firstorder congruence. Qed.
702 703
Instance:  {A B B'} (f : B  B'),
  Injective (=) (=) f  Injective (=) (=) (@snd_map A B B' f).
704
Proof. intros ????? [??] [??]; injection 1; firstorder congruence. Qed.
705

706 707
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
  relation (A * B) := λ x y, R1 (fst x) (fst y)  R2 (snd x) (snd y).
Robbert Krebbers's avatar
Robbert Krebbers committed
708 709 710

Section prod_relation.
  Context `{R1 : relation A} `{R2 : relation B}.
711 712
  Global Instance:
    Reflexive R1  Reflexive R2  Reflexive (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
713
  Proof. firstorder eauto. Qed.
714 715
  Global Instance:
    Symmetric R1  Symmetric R2  Symmetric (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
716
  Proof. firstorder eauto. Qed.
717 718
  Global Instance:
    Transitive R1  Transitive R2  Transitive (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
719
  Proof. firstorder eauto. Qed.
720 721
  Global Instance:
    Equivalence R1  Equivalence R2  Equivalence (prod_relation R1 R2).
Robbert Krebbers's avatar
Robbert Krebbers committed
722 723 724 725 726 727 728 729 730
  Proof. split; apply _. Qed.
  Global Instance: Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
  Proof. firstorder eauto. Qed.
  Global Instance: Proper (prod_relation R1 R2 ==> R1) fst.
  Proof. firstorder eauto. Qed.
  Global Instance: Proper (prod_relation R1 R2 ==> R2) snd.
  Proof. firstorder eauto. Qed.
End prod_relation.

731
(** ** Other *)
732 733 734 735 736 737 738 739 740
Definition proj_eq {A B} (f : B  A) : relation B := λ x y, f x = f y.
Global Instance proj_eq_equivalence `(f : B  A) : Equivalence (proj_eq f).
Proof. unfold proj_eq. repeat split; red; intuition congruence. Qed.
Notation "x ~{ f } y" := (proj_eq f x y)
  (at level 70, format "x  ~{ f }  y") : C_scope.
Notation "(~{ f } )" := (proj_eq f) (f at level 10, only parsing) : C_scope.

Hint Extern 0 (_ ~{_} _) => reflexivity.
Hint Extern 0 (_ ~{_} _) => symmetry; assumption.
Robbert Krebbers's avatar
Robbert Krebbers committed
741 742

Instance:  A B (x : B), Commutative (=) (λ _ _ : A, x).
743
Proof. red. trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
744
Instance:  A (x : A), Associative (=) (λ _ _ : A, x).
745
Proof. red. trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
746
Instance:  A, Associative (=) (λ x _ : A, x).
747
Proof. red. trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
748
Instance:  A, Associative (=) (λ _ x : A, x).
749
Proof. red. trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
750
Instance:  A, Idempotent (=) (λ x _ : A, x).
751
Proof. red. trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
752
Instance:  A, Idempotent (=) (λ _ x : A, x).
753
Proof. red. trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
754

755 756
Instance left_id_propholds {A} (R : relation A) i f :
  LeftId R i f   x, PropHolds (R (f i x) x).
757
Proof. red. trivial. Qed.
758 759
Instance right_id_propholds {A} (R : relation A) i f :
  RightId R i f   x, PropHolds (R (f x i) x).
760
Proof. red. trivial. Qed.
761 762 763 764 765 766
Instance left_absorb_propholds {A} (R : relation A) i f :
  LeftAbsorb R i f   x, PropHolds (R (f i x) i).
Proof. red. trivial. Qed.
Instance right_absorb_propholds {A} (R : relation A) i f :
  RightAbsorb R i f   x, PropHolds (R (f x i) i).
Proof. red. trivial. Qed.
767 768
Instance idem_propholds {A} (R : relation A) f :
  Idempotent R f   x, PropHolds (R (f x x) x).
769
Proof. red. trivial. Qed.
770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795

Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A  B)
  `{!Injective R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y)  R x y.
Proof. firstorder. Qed.
Instance: Injective (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
Instance: Injective (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
Instance: Injective2 (=) (=) (=) (@pair A B).
Proof. injection 1; auto. Qed.
Instance:  `{Injective2 A B C R1 R2 R3 f} y, Injective R1 R3 (λ x, f x y).
Proof. repeat intro; edestruct (injective2 f); eauto. Qed.
Instance:  `{Injective2 A B C R1 R2 R3 f} x, Injective R2 R3 (f x).
Proof. repeat intro; edestruct (injective2 f); eauto. Qed.

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

Lemma impl_transitive (P Q R : Prop) : (P  Q)  (Q  R)  (P  R).
Proof. tauto. Qed.
Instance: Commutative () (@eq A).
796
Proof. red; intuition. Qed.
797
Instance: Commutative () (λ x y, @eq A y x).
798
Proof. red; intuition. Qed.
799
Instance: Commutative () ().
800
Proof. red; intuition. Qed.
801
Instance: Commutative () ().
802
Proof. red; intuition. Qed.
803
Instance: Associative () ().
804
Proof. red; intuition. Qed.
805
Instance: Idempotent () ().
806
Proof. red; intuition. Qed.
807
Instance: Commutative () ().
808
Proof. red; intuition. Qed.
809
Instance: Associative () ().
810
Proof. red; intuition. Qed.
811
Instance: Idempotent () ().
812
Proof. red; intuition. Qed.
813
Instance: LeftId () True ().
814
Proof. red; intuition. Qed.
815
Instance: RightId () True ().
816
Proof. red; intuition. Qed.
817
Instance: LeftAbsorb () False ().
818
Proof. red; intuition. Qed.
819
Instance: RightAbsorb () False ().
820
Proof. red; intuition. Qed.
821
Instance: LeftId () False ().
822
Proof. red; intuition. Qed.
823
Instance: RightId () False ().
824
Proof. red; intuition. Qed.
825
Instance: LeftAbsorb () True ().
826
Proof. red; intuition. Qed.
827
Instance: RightAbsorb () True ().
828
Proof. red; intuition. Qed.
829
Instance: LeftId () True impl.
830
Proof. unfold impl. red; intuition. Qed.
831
Instance: RightAbsorb () True impl.
832
Proof. unfold impl. red; intuition. Qed.
833
Instance: LeftDistr () () ().
834
Proof. red; intuition. Qed.
835
Instance: RightDistr () () ().
836
Proof. red; intuition. Qed.
837
Instance: LeftDistr () () ().
838
Proof. red; intuition. Qed<