base.v 13.1 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
Global Generalizable All Variables.
Global Set Automatic Coercions Import.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.

Arguments existT {_ _} _ _.
Arguments existT2 {_ _ _} _ _ _.

Definition proj1_T2 {A} {P Q : A  Type} (x : sigT2 P Q) : A :=
  match x with existT2 a _ _ => a end.
Definition proj2_T2 {A} {P Q : A  Type} (x : sigT2 P Q) : P (proj1_T2 x) :=
  match x with existT2 _ p _ => p end.
Definition proj3_T2 {A} {P Q : A  Type} (x : sigT2 P Q) : Q (proj1_T2 x) :=
  match x with existT2 _ _ q => q end.

(*  Common notations *)
Delimit Scope C_scope with C.
Global Open Scope C_scope.

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.

Notation "(→)" := (λ x y, x  y) : C_scope.
Notation "( T →)" := (λ y, T  y) : C_scope.
Notation "(→ T )" := (λ y, y  T) : C_scope.
Notation "t $ r" := (t r) (at level 65, right associativity, only parsing) : C_scope.
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.
Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
Notation "` x" := (proj1_sig x) : C_scope.

(* Provable propositions *)
Class PropHolds (P : Prop) := prop_holds: P.

(* Decidable propositions *)
Class Decision (P : Prop) := decide : {P} + {¬P}.
Arguments decide _ {_}.

(* Common relations & operations *)
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.

Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
Hint Extern 0 (?x  ?x) => reflexivity.

Class Empty A := empty: A.
Notation "∅" := empty : C_scope.

Class Union A := union: A  A  A.
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.

Class Intersection A := intersection: A  A  A.
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.
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.

Class SubsetEq A := subseteq: A  A  Prop.
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.

Hint Extern 0 (?x  ?x) => reflexivity.

Class Singleton A B := singleton: A  B.
Notation "{{ x }}" := (singleton x) : C_scope.
Notation "{{ x ; y ; .. ; z }}" := (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.

Class ElemOf A B := elem_of: A  B  Prop.
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.

Class UnionWith M := union_with:  {A}, (A  A  A)  M A  M A  M A.
Class IntersectWith M := intersect_with:  {A}, (A  A  A)  M A  M A  M A.

(* Common properties *)
Class Injective {A B} R S (f : A  B) := injective:  x y : A, S (f x) (f y)  R x y.
Class Idempotent {A} R (f : A  A  A) := idempotent:  x, R (f x x) x.
Class Commutative {A B} R (f : B  B  A) := commutative:  x y, R (f x y) (f y x).
Class LeftId {A} R (i : A) (f : A  A  A) := left_id:  x, R (f i x) x.
Class RightId {A} R (i : A) (f : A  A  A) := right_id:  x, R (f x i) x.
Class Associative {A} R (f : A  A  A) := associative:  x y z, R (f x (f y z)) (f (f x y) z).

Arguments injective {_ _ _ _} _ {_} _ _ _.
Arguments idempotent {_ _} _ {_} _.
Arguments commutative {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
Arguments right_id {_ _} _ _ {_} _.
Arguments associative {_ _} _ {_} _ _ _.

125
126
127
128
129
130
131
132
133
134
135
136
(* Using idempotent_eq we can force Coq to not use the setoid mechanism *)
Lemma idempotent_eq {A} (f : A  A  A) `{!Idempotent (=) f} x : f x x = x.
Proof. auto. Qed.
Lemma commutative_eq {A B} (f : B  B  A) `{!Commutative (=) f} x y : f x y = f y x.
Proof. auto. Qed.
Lemma left_id_eq {A} (i : A) (f : A  A  A) `{!LeftId (=) i f} x : f i x = x.
Proof. auto. Qed.
Lemma right_id_eq {A} (i : A) (f : A  A  A) `{!RightId (=) i f} x : f x i = x.
Proof. auto. Qed.
Lemma associative_eq {A} (f : A  A  A) `{!Associative (=) f} x y z : f x (f y z) = f (f x y) z.
Proof. auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
(* Monadic operations *)
Section monad_ops.
  Context (M : Type  Type).

  Class MRet := mret:  {A}, A  M A.
  Class MBind := mbind:  {A B}, (A  M B)  M A  M B.
  Class MJoin := mjoin:  {A}, M (M A)  M A.
  Class FMap := fmap:  {A B}, (A  B)  M A  M B.
End monad_ops.

Arguments mret {M MRet A} _.
Arguments mbind {M MBind A B} _ _.
Arguments mjoin {M MJoin A} _.
Arguments fmap {M FMap A B} _ _.

Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
Notation "x ← y ; z" := (y = (λ x : _, z)) (at level 65, next at level 35, right associativity) : C_scope.
Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.

(* Ordered structures *)
Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
  bounded_preorder :>> PreOrder ();
  subseteq_empty x :   x
}.

(* Note: no equality to avoid the need for setoids. We define equality in a generic way. *)
Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} := {
  jsl_preorder :>> BoundedPreOrder A;
  subseteq_union_l x y : x  x  y;
  subseteq_union_r x y : y  x  y;
  union_least x y z : x  z  y  z  x  y  z
}.
Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} := {
  msl_preorder :>> BoundedPreOrder A;
  subseteq_intersection_l x y : x  y  x;
  subseteq_intersection_r x y : x  y  y;
  intersection_greatest x y z : z  x  z  y  z  x  y
}.

(* Containers *)
Class Size C := size: C  nat.
Class Map A C := map: (A  A)  (C  C).

Class Collection A C `{ElemOf A C} `{Empty C} `{Union C} 
    `{Intersection C} `{Difference C} `{Singleton A C} `{Map A C} := {
  elem_of_empty (x : A) : x  ;
  elem_of_singleton (x y : A) : x  {{ y }}  x = y;
  elem_of_union X Y (x : A) : x  X  Y  x  X  x  Y;
  elem_of_intersection X Y (x : A) : x  X  Y  x  X  x  Y;
  elem_of_difference X Y (x : A) : x  X  Y  x  X  x  Y;
  elem_of_map f X (x : A) : x  map f X   y, x = f y  y  X
}.

Class Elements A C := elements: C  list A.
Class FinCollection A C `{Empty C} `{Union C} `{Intersection C} `{Difference C} 
    `{Singleton A C} `{ElemOf A C} `{Map A C} `{Elements A C} := {
  fin_collection :>> Collection A C;
  elements_spec X x : x  X  In x (elements X);
  elements_nodup X : NoDup (elements X)
}. 

Class Fresh A C := fresh: C  A.
Class FreshSpec A C `{!Fresh A C} `{!ElemOf A C} := {
  fresh_proper X Y : ( x, x  X  x  Y)  fresh X = fresh Y;
  is_fresh (X : C) : fresh X  X
}.

(* Maps *)
Class Lookup K M := lookup:  {A}, K  M A  option A.
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.

Class PartialAlter K M := partial_alter:  {A}, (option A  option A)  K  M A  M A.
Class Alter K M := alter:  {A}, (A  A)  K  M A  M A.
Class Dom K M := dom:  C `{Empty C} `{Union C} `{Singleton K C}, M  C.
Class Merge M := merge:  {A}, (option A  option A  option A)  M A  M A  M A.
Class Insert K M := insert:  {A}, K  A  M A  M A.
Notation "<[ k := a ]>" := (insert k a) (at level 5, right associativity) : C_scope.
Class Delete K M := delete: K  M  M.

(* Misc *)
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.

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)).
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).

Section prod_relation.
  Context `{R1 : relation A} `{R2 : relation B}.
  Global Instance: Reflexive R1  Reflexive R2  Reflexive (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance: Symmetric R1  Symmetric R2  Symmetric (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance: Transitive R1  Transitive R2  Transitive (prod_relation R1 R2).
  Proof. firstorder eauto. Qed.
  Global Instance: Equivalence R1  Equivalence R2  Equivalence (prod_relation R1 R2).
  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.

Definition lift_relation {A B} (R : relation A) (f : B  A) : relation B := λ x y, R (f x) (f y).
Definition lift_relation_equivalence {A B} (R : relation A) (f : B  A) :
  Equivalence R  Equivalence (lift_relation R f).
Proof. unfold lift_relation. firstorder. Qed.
Hint Extern 0 (Equivalence (lift_relation _ _)) => eapply @lift_relation_equivalence : typeclass_instances.

Instance:  A B (x : B), Commutative (=) (λ _ _ : A, x).
Proof. easy. Qed.
Instance:  A (x : A), Associative (=) (λ _ _ : A, x).
Proof. easy. Qed.
Instance:  A, Associative (=) (λ x _ : A, x).
Proof. easy. Qed.
Instance:  A, Associative (=) (λ _ x : A, x).
Proof. easy. Qed.
Instance:  A, Idempotent (=) (λ x _ : A, x).
Proof. easy. Qed.
Instance:  A, Idempotent (=) (λ _ x : A, x).
Proof. easy. Qed.

Instance left_id_propholds {A} (R : relation A) i f : LeftId R i f   x, PropHolds (R (f i x) x).
Proof. easy. Qed.
Instance right_id_propholds {A} (R : relation A) i f : RightId R i f   x, PropHolds (R (f x i) x).
Proof. easy. Qed.
Instance idem_propholds {A} (R : relation A) f : Idempotent R f   x, PropHolds (R (f x x) x).
Proof. easy. Qed.

Ltac simplify_eqs := repeat
  match goal with
  | |- _ => progress subst
  | |- _ = _ => reflexivity
  | H : _  _ |- _ => now destruct H
  | H : _ = _  False |- _ => now destruct H
  | H : _ = _ |- _ => discriminate H
  | H : _ = _ |-  ?G => change (id G); injection H; clear H; intros; unfold id at 1
  | H : ?f _ = ?f _ |- _ => apply (injective f) in H
  | H : ?f _ ?x = ?f _ ?x |- _ => apply (injective (λ y, f y x)) in H
  end.

Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
Instance: Proper (iff ==> iff) PropHolds.
Proof. now repeat intro. Qed.

Ltac solve_propholds :=
  match goal with
  | [ |- PropHolds (?P) ] => apply _
  | [ |- ?P ] => change (PropHolds P); apply _
  end.

Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
  remember t as x;
  match goal with
  | E' : x = _ |- _ => rename E' into E
  end.