Global Generalizable All Variables.
Global Set Automatic Coercions Import.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
Arguments id _ _/.
Arguments compose _ _ _ _ _ _ /.
(* Change True and False into notations so we can overload them *)
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Arguments existT {_ _} _ _.
(* 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 IntersectionWith M :=
intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
Class DifferenceWith M :=
difference_with: ∀ {A}, (A → A → option 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 {_ _} _ {_} _ _ _.
(* 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.
(* 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 setoid
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, format "<[ k := a ]>") : C_scope.
Class Delete K M :=
delete: K → M → M.
Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
fold_right (λ p, <[ fst p := snd p ]>) m l.
Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
fold_right delete m l.
(* Misc *)
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
R x y ↔ R y x.
Proof. intuition. Qed.
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.
Ltac feed tac H :=
let H' := type of H in
match eval hnf in H' with
| ?T1 → ?T2 =>
let HT1 := fresh in assert T1 as HT1;
[| feed tac (H HT1); clear HT1 ]
| _ => tac H
end.
Tactic Notation "feed" tactic(tac) constr(H) := feed tac H.
Ltac efeed tac H :=
let H' := type of H in
match eval hnf in H' with
| ?T1 → ?T2 =>
let HT1 := fresh in assert T1 as HT1; [| efeed tac (H HT1); clear HT1 ]
| ?T1 → _ =>
let e := fresh in evar (e:T1);
let e' := eval unfold e in e in
clear e; efeed tac (H e')
| _ => tac H
end.
Tactic Notation "efeed" tactic(tac) constr(H) := efeed tac H.
Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
feed (fun H => pose proof H as H') H.
Tactic Notation "feed" "pose" "proof" constr(H) :=
feed (fun H => pose proof H) H.
Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
efeed (fun H => pose proof H as H') H.
Tactic Notation "efeed" "pose" "proof" constr(H) :=
efeed (fun H => pose proof H) H.
Tactic Notation "feed" "specialize" ident(H) :=
feed (fun H => specialize H) H.
Tactic Notation "efeed" "specialize" ident(H) :=
efeed (fun H => specialize H) H.
Tactic Notation "feed" "inversion" constr(H) :=
feed (fun H => let H':=fresh in pose proof H as H'; inversion H') H.
Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
feed (fun H => let H':=fresh in pose proof H as H'; inversion H' as IP) H.
Tactic Notation "feed" "destruct" constr(H) :=
feed (fun H => let H':=fresh in pose proof H as H'; destruct H') H.
Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
feed (fun H => let H':=fresh in pose proof H as H'; destruct H' as IP) H.