base.v

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.