Definition funcomp {X Y Z} (g : Y Z) (f : X Y) :=
   x g (f x).

Lemma funcomp_assoc {W X Y Z} (g: Y Z) (f: X Y) (h: W X) :
  funcomp g (funcomp f h) = (funcomp (funcomp g f) h).
Proof.
  reflexivity.
Qed.

Definition ap {X Y} (f : X Y) {x y : X} (p : x = y) : f x = f y :=
  match p with eq_refl eq_refl end.

Definition apc {X Y} {f g : X Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
  match q with eq_refl match p with eq_refl eq_refl end end.

Functor Instances

Exemplary functor instances needed to make Autosubst's generation possible for functors. Two things are important: 1. The names are fixed. 2. For Coq to check termination, also the proofs have to be closed with Defined.

List Instance

Require Import List.

Notation "'list_map'" := map.

Definition list_ext {A B} {f g : A B} :
  ( x, f x = g x) xs, list_map f xs = list_map g xs.
  intros H. induction xs. reflexivity.
  cbn. f_equal. apply H. apply IHxs.
Defined.

Definition list_id {A} { f : A A} :
  ( x, f x = x) xs, list_map f xs = xs.
Proof.
  intros H. induction xs. reflexivity.
  cbn. rewrite H. rewrite IHxs; eauto.
Defined.

Definition list_comp {A B C} {f: A B} {g: B C} {h} :
  ( x, (funcomp g f) x = h x) xs, map g (map f xs) = map h xs.
Proof.
  induction xs. reflexivity.
  cbn. rewrite H. f_equal. apply IHxs.
Defined.

Prod Instance


Definition prod_map {A B C D} (f : A C) (g : B D) (p : A * B) :
  C * D.
Proof.
  destruct p as [a b]. split.
  exact (f a). exact (g b).
Defined.

Definition prod_id {A B} {f : A A} {g : B B} :
  ( x, f x = x) ( x, g x = x) p, prod_map f g p = p.
Proof.
  intros . destruct p. cbn. f_equal; [ apply | apply ].
Defined.

Definition prod_ext {A B C D} {f f' : A C} {g g': B D} :
  ( x, f x = f' x) ( x, g x = g' x) p, prod_map f g p = prod_map f' g' p.
Proof.
  intros . destruct p as [a b]. cbn. f_equal; [ apply | apply ].
Defined.

Definition prod_comp {A B C D E F} {f1 : A C} {g1 : C E} {h1 : A E} {f2: B D} {g2: D F} {h2 : B F}:
  ( x, (funcomp ) x = x) ( x, (funcomp ) x = x) p, prod_map (prod_map p) = prod_map p.
Proof.
  intros . destruct p as [a b]. cbn. f_equal; [ apply | apply ].
Defined.

Option Instance


Definition option_map {A B} (f : A B) (p : option A) :
  option B :=
match p with
  | Some a Some (f a)
  | None None
end.

Definition option_id {A} {f : A A} :
  ( x, f x = x) p, option_map f p = p.
Proof.
  intros H. destruct p ; cbn.
  - f_equal. apply H.
  - reflexivity.
Defined.

Definition option_ext {A B} {f f' : A B} :
  ( x, f x = f' x) p, option_map f p = option_map f' p.
Proof.
  intros H. destruct p as [a|] ; cbn.
  - f_equal. apply H.
  - reflexivity.
Defined.

Definition option_comp {A B C} {f : A B} {g : B C} {h : A C}:
  ( x, (funcomp g f) x = h x)
   p, option_map g (option_map f p) = option_map h p.
Proof.
  intros H. destruct p as [a|]; cbn.
  - f_equal. apply H.
  - reflexivity.
Defined.

Hint Rewrite in_map_iff : FunctorInstances.

Declare Scope fscope.
Declare Scope subst_scope.

Ltac eta_reduce :=
  repeat match goal with
         | [|- context[ x ?f x]] change ( x f x) with f
         end.

Ltac minimize :=
  repeat match goal with
         | [|- context[ x ?f x]] change ( x f x) with f
         | [|- context[ x ?g (?f x)]] change ( x g (f x)) with (funcomp g f)
         end.

Ltac setoid_rewrite_left t := setoid_rewrite t.

Ltac check_no_evars :=
  match goal with
  | [|- ?x] assert_fails (has_evar x)
  end.

Require Import Setoid Morphisms.

Lemma pointwise_forall {X Y:Type} (f g: X Y) :
  (pointwise_relation _ eq f g) x, f x = g x.
Proof.
  trivial.
Qed.

Instance funcomp_morphism {X Y Z} :
  Proper (@pointwise_relation Y Z eq @pointwise_relation X Y eq @pointwise_relation X Z eq) funcomp.
Proof.
  cbv - [funcomp].
  intros Hg Hf x.
  unfold funcomp. rewrite Hf, Hg.
  reflexivity.
Qed.

Instance funcomp_morphism2 {X Y Z} :
  Proper (@pointwise_relation Y Z eq @pointwise_relation X Y eq eq eq) funcomp.
Proof.
  intros Hg Hf ? x .
  unfold funcomp. rewrite Hf, Hg.
  reflexivity.
Qed.

Ltac unfold_funcomp := match goal with
                           | |- context[(funcomp ?f ?g) ?s] change ((funcomp f g) s) with (f (g s))
                           end.