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.