Very long code that generates an error on `split` with HoTT/Coq

hott-bug-01.v

Require Import JMeq ProofIrrelevance.

Set Implicit Arguments.
Set Asymmetric Patterns.

Local Infix "==" := JMeq (at level 70).

(* The standard library does not provide projections of [sigT2] or [sig2].
   I define coercions to [sigT] and [sig], so that [projT1], [projT2],
   [proj1_sig], and [proj2_sig] do the right thing, and I define [projT3],
   [proj3_sig]. *)
Section sig.
  Polymorphic Definition sigT_of_sigT2 A P Q (x : @sigT2 A P Q) := let (a, h, _) := x in existT _ a h.
  Global Coercion sigT_of_sigT2 : sigT2 >-> sigT.
  Polymorphic Definition projT3 A P Q (x : @sigT2 A P Q) :=
    let (x0, _, h) as x0 return (Q (projT1 x0)) := x in h.

  Polymorphic Definition sig_of_sig2 A P Q (x : @sig2 A P Q) := let (a, h, _) := x in exist _ a h.
  Global Coercion sig_of_sig2 : sig2 >-> sig.
  Polymorphic Definition proj3_sig A P Q (x : @sig2 A P Q) :=
    let (x0, _, h) as x0 return (Q (proj1_sig x0)) := x in h.
End sig.

(* fail if [tac] succeeds, do nothing otherwise *)
Tactic Notation "not_tac" tactic(tac) := (tac; fail 1) || idtac.

(* fail if [tac] fails, but don't actually execute [tac] *)
Tactic Notation "test_tac" tactic(tac) := not_tac (not_tac tac).

(* fail if [x] is a function application, a dependent product ([fun _ => _]),
   or a sigma type ([forall _, _]) *)
Ltac atomic x :=
  match x with
    | ?f _ => fail 1 x "is not atomic"
    | (fun _ => _) => fail 1 x "is not atomic"
    | forall _, _ => fail 1 x "is not atomic"
    | _ => idtac
  end.

(* [pose proof defn], but only if no hypothesis of the same type exists.
   most useful for proofs of a proposition *)
Ltac unique_pose defn :=
  let T := type of defn in
    match goal with
      | [ H : T |- _ ] => fail 1
      | _ => pose proof defn
    end.

(* [pose defn], but only if that hypothesis doesn't exist *)
Ltac unique_pose_with_body defn :=
  match goal with
    | [ H := defn |- _ ] => fail 1
    | _ => pose defn
  end.

(* check's if the given hypothesis has a body, i.e., if [clearbody]
   could ever succeed.  We can't just do [test_tac (clearbody H)],
   because maybe the correctness of the proof depends on the body
   of H *)
Tactic Notation "has_no_body" hyp(H) :=
  not_tac (let H' := fresh in pose H as H'; unfold H in H').

Tactic Notation "has_body" hyp(H) :=
  not_tac (has_no_body H).

(* find the head of the given expression *)
Ltac head expr :=
  match expr with
    | ?f _ => head f
    | _ => expr
  end.

Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.

(* call [tac H], but first [simpl]ify [H].
   This tactic leaves behind the simplified hypothesis. *)
Ltac simpl_do tac H :=
  let H' := fresh in pose H as H'; simpl; simpl in H'; tac H'.

(* clear the left-over hypothesis after [simpl_do]ing it *)
Ltac simpl_do_clear tac H := simpl_do ltac:(fun H => tac H; try clear H) H.

Ltac do_with_hyp tac :=
  match goal with
    | [ H : _ |- _ ] => tac H
  end.

Ltac rewrite_hyp' := do_with_hyp ltac:(fun H => rewrite H).
Ltac rewrite_hyp := repeat rewrite_hyp'.
Ltac rewrite_rev_hyp' := do_with_hyp ltac:(fun H => rewrite <- H).
Ltac rewrite_rev_hyp := repeat rewrite_rev_hyp'.

Ltac apply_hyp' := do_with_hyp ltac:(fun H => apply H).
Ltac apply_hyp := repeat apply_hyp'.
Ltac eapply_hyp' := do_with_hyp ltac:(fun H => eapply H).
Ltac eapply_hyp := repeat eapply_hyp'.

(* some simple tactics to solve the goal by rewriting *)
Ltac t' := repeat progress (simpl in *; intros; try split; trivial).
Ltac t'_long := repeat progress (simpl in *; intuition).

Ltac t_con_with con tac := tac;
  repeat (match goal with
            | [ H : context[con] |- _ ] => rewrite H
            | _ => progress autorewrite with core in *
          end; tac).

Ltac t_con_rev_with con tac := tac;
  repeat (match goal with
            | [ H : context[con] |- _ ] => rewrite <- H
            | _ => progress autorewrite with core in *
          end; tac).

Ltac t_with tac := t_con_with @eq tac.

Ltac t_rev_with tac := t_con_rev_with @eq tac.

Ltac t_con con := t_con_with con t'; t_con_with con t'_long.
Ltac t_con_rev con := t_con_rev_with con t'; t_con_rev_with con t'_long.

Ltac t := t_with t'; t_with t'_long.
Ltac t_rev := t_rev_with t'; t_rev_with t'_long.

(* solve simple setiod goals that can be solved by [transitivity] *)
Ltac simpl_transitivity :=
  try solve [ match goal with
                | [ _ : ?Rel ?a ?b, _ : ?Rel ?b ?c |- ?Rel ?a ?c ] => transitivity b; assumption
              end ].

(* given a [matcher] that succeeds on some hypotheses and fails on
   others, destruct any matching hypotheses, and then execute [tac]
   after each [destruct].

   The [tac] part exists so that you can, e.g., [simpl in *], to
   speed things up. *)
Ltac destruct_all_matches_then matcher tac :=
  repeat match goal with
           | [ H : ?T |- _ ] => matcher T; destruct H; tac
         end.

Ltac destruct_all_matches matcher := destruct_all_matches_then matcher ltac:(simpl in *).
Ltac destruct_all_matches' matcher := destruct_all_matches_then matcher idtac.

(* matches anything whose type has a [T] in it *)
Ltac destruct_type_matcher T HT :=
  match HT with
    | context[T] => idtac
  end.
Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T).
Ltac destruct_type' T := destruct_all_matches' ltac:(destruct_type_matcher T).

Ltac destruct_head_matcher T HT :=
  match head HT with
    | T => idtac
  end.
Ltac destruct_head T := destruct_all_matches ltac:(destruct_head_matcher T).
Ltac destruct_head' T := destruct_all_matches' ltac:(destruct_head_matcher T).

Ltac destruct_head_hnf_matcher T HT :=
  match head_hnf HT with
    | T => idtac
  end.
Ltac destruct_head_hnf T := destruct_all_matches ltac:(destruct_head_hnf_matcher T).
Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(destruct_head_hnf_matcher T).

Ltac destruct_hypotheses_matcher HT :=
  let HT' := eval hnf in HT in
    match HT' with
      | ex _ => idtac
      | and _ _ => idtac
      | prod _ _ => idtac
    end.
Ltac destruct_hypotheses := destruct_all_matches destruct_hypotheses_matcher.
Ltac destruct_hypotheses' := destruct_all_matches' destruct_hypotheses_matcher.

Ltac destruct_sig_matcher HT :=
  let HT' := eval hnf in HT in
    match HT' with
      | @sig _ _ => idtac
      | @sigT _ _ => idtac
      | @sig2 _ _ _ => idtac
      | @sigT2 _ _ _ => idtac
    end.
Ltac destruct_sig := destruct_all_matches destruct_sig_matcher.
Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher.

Ltac destruct_all_hypotheses := destruct_all_matches ltac:(fun HT =>
  destruct_hypotheses_matcher HT || destruct_sig_matcher HT
).

(* if progress can be made by [exists _], but it doesn't matter what
   fills in the [_], assume that something exists, and leave the two
   goals of finding a member of the apropriate type, and proving that
   all members of the appropriate type prove the goal *)
Ltac destruct_exists' T := cut T; try (let H := fresh in intro H; exists H).
Ltac destruct_exists := destruct_head_hnf @ex;
  match goal with
    | [ |- @ex ?T _ ] => destruct_exists' T
    | [ |- @sig ?T _ ] => destruct_exists' T
    | [ |- @sigT ?T _ ] => destruct_exists' T
    | [ |- @sig2 ?T _ _ ] => destruct_exists' T
    | [ |- @sigT2 ?T _ _ ] => destruct_exists' T
  end.

(* if the goal can be solved by repeated specialization of some
   hypothesis with other [specialized] hypotheses, solve the goal
   by brute force *)
Ltac specialized_assumption tac := tac;
  match goal with
    | [ x : ?T, H : forall _ : ?T, _ |- _ ] => specialize (H x); specialized_assumption tac
    | _ => assumption
  end.

(* for each hypothesis of type [H : forall _ : ?T, _], if there is exactly
   one hypothesis of type [H' : T], do [specialize (H H')]. *)
Ltac specialize_uniquely :=
  repeat match goal with
           | [ x : ?T, y : ?T, H : _ |- _ ] => test_tac (specialize (H x)); fail 1
           | [ x : ?T, H : _ |- _ ] => specialize (H x)
         end.

(* specialize all hypotheses of type [forall _ : ?T, _] with
   appropriately typed hypotheses *)
Ltac specialize_all_ways_forall :=
  repeat match goal with
           | [ x : ?T, H : forall _ : ?T, _ |- _ ] => unique_pose (H x)
         end.

(* try to specialize all hypotheses with all other hypotheses.
   This includes [specialize (H x)] where [H x] requires a coercion
   from the type of [H] to Funclass. *)
Ltac specialize_all_ways :=
  repeat match goal with
           | [ x : ?T, H : _ |- _ ] => unique_pose (H x)
         end.

(* try to do [tac] after [repeat rewrite] on [rew_H], in both directions *)
Ltac try_rewrite rew_H tac :=
  (repeat rewrite rew_H; tac) ||
    (repeat rewrite <- rew_H; tac).

Ltac try_rewrite_by rew_H by_tac tac :=
  (repeat rewrite rew_H by by_tac; tac) ||
    (repeat rewrite <- rew_H by by_tac; tac).

Ltac try_rewrite_repeat rew_H tac :=
  (repeat (rewrite rew_H; tac)) ||
    (repeat (rewrite <- rew_H; tac)).

Ltac solve_repeat_rewrite rew_H tac :=
  solve [ repeat (rewrite rew_H; tac) ] ||
    solve [ repeat (rewrite <- rew_H; tac) ].

Lemma sig_eq A P (s s' : @sig A P) : proj1_sig s = proj1_sig s' -> s = s'.
  destruct s, s'; simpl; intro; subst; f_equal; apply proof_irrelevance.
Qed.

Lemma sig2_eq A P Q (s s' : @sig2 A P Q) : proj1_sig s = proj1_sig s' -> s = s'.
  destruct s, s'; simpl; intro; subst; f_equal; apply proof_irrelevance.
Qed.

Lemma sigT_eq A P (s s' : @sigT A P) : projT1 s = projT1 s' -> projT2 s == projT2 s' -> s = s'.
  destruct s, s'; simpl; intros; firstorder; repeat subst; reflexivity.
Qed.

Lemma sigT2_eq A P Q (s s' : @sigT2 A P Q) :
  projT1 s = projT1 s'
  -> projT2 s == projT2 s'
  -> projT3 s == projT3 s'
  -> s = s'.
  destruct s, s'; simpl; intros; firstorder; repeat subst; reflexivity.
Qed.

Lemma injective_projections_JMeq (A B A' B' : Type) (p1 : A * B) (p2 : A' * B') :
  fst p1 == fst p2 -> snd p1 == snd p2 -> p1 == p2.
Proof.
  destruct p1, p2; simpl; intros H0 H1; subst;
    rewrite H0; rewrite H1; reflexivity.
Qed.

Ltac clear_refl_eq :=
  repeat match goal with
           | [ H : ?x = ?x |- _ ] => clear H
         end.

(* reduce the proving of equality of sigma types to proving equality
   of their components *)
Ltac simpl_eq' :=
  apply sig_eq
        || apply sig2_eq
        || ((apply sigT_eq || apply sigT2_eq); intros; clear_refl_eq)
        || apply injective_projections
        || apply injective_projections_JMeq.

Ltac simpl_eq := intros; repeat (
  simpl_eq'; simpl in *
).

(* Coq's build in tactics don't work so well with things like [iff]
   so split them up into multiple hypotheses *)
Ltac split_in_context ident funl funr :=
  repeat match goal with
           | [ H : context p [ident] |- _ ] =>
             let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (apply H);
               let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (apply H);
                 clear H
         end.

Ltac split_iff := split_in_context iff (fun a b : Prop => a -> b) (fun a b : Prop => b -> a).

Ltac split_and' :=
  repeat match goal with
           | [ H : ?a /\ ?b |- _ ] => let H0 := fresh in let H1 := fresh in
             assert (H0 := proj1 H); assert (H1 := proj2 H); clear H
         end.
Ltac split_and := split_and'; split_in_context and (fun a b : Prop => a) (fun a b : Prop => b).

Ltac clear_hyp_of_type type :=
  repeat match goal with
           | [ H : type |- _ ] => clear H
         end.

(* If [conVar] is not mentioned in any hypothesis other than [hyp],
   nor in the goal, then clear any hypothesis of the same type as [hyp] *)
Ltac clear_hyp_unless_context hyp conVar :=
  let hypT := type of hyp in
    match goal with
      | [ H0 : hypT, H : context[conVar] |- _ ] => fail 1 (* there is a hypotheses distinct from [hyp] which mentions [conVar] *)
      | [ |- context[conVar] ] => fail 1
      | _ => clear_hyp_of_type hypT
    end.

Ltac recur_clear_context con :=
  repeat match goal with
           | [ H : appcontext[con] |- _ ] =>
             recur_clear_context H; try clear H
           | [ H := appcontext[con] |- _ ] =>
             recur_clear_context H; try clear H
         end.

(* equivalent to [idtac] if [subexpr] appears nowhere in [expr],
   equivalent to [fail] otherwise *)
Ltac FreeQ expr subexpr :=
  match expr with
    | appcontext[subexpr] => fail 1
    | _ => idtac
  end.

Ltac subst_mor x :=
  match goal with
    | [ H : ?Rel ?a x |- _ ] => FreeQ a x; rewrite <- H in *;
      try clear_hyp_unless_context H x
    | [ H : ?Rel x ?a |- _ ] => FreeQ a x; rewrite H in *;
      try clear_hyp_unless_context H x
  end.

Ltac repeat_subst_mor_of_type type :=
  repeat match goal with
           | [ m : context[type] |- _ ] => subst_mor m; try clear m
         end.

(* Using [rew] instead of [rew'] makes this fail... WTF? *)
Ltac subst_by_rewrite_hyp_rew a H rew' :=
  rew' H; clear H;
  match goal with
    | [ H : appcontext[a] |- _ ] => fail 1 "Rewrite failed to clear all instances of" a
    | [ |- appcontext[a] ] => fail 1 "Rewrite failed to clear all instances of" a
    | _ => idtac
  end.

Ltac subst_by_rewrite_hyp a H :=
  subst_by_rewrite_hyp_rew a H ltac:(fun H => try rewrite H in *; try setoid_rewrite H).

Ltac subst_by_rewrite_rev_hyp a H :=
  subst_by_rewrite_hyp_rew a H ltac:(fun H => try rewrite <- H in *; try setoid_rewrite <- H).

Ltac subst_by_rewrite a :=
  match goal with
    | [ H : ?Rel a ?b |- _ ] => subst_by_rewrite_hyp a H
    | [ H : ?Rel ?b a |- _ ] => subst_by_rewrite_rev_hyp a H
  end.

Ltac subst_atomic a := first [ atomic a | fail "Non-atomic variable" a ];
                      subst_by_rewrite a.

Ltac subst_rel rel :=
  match goal with
    | [ H : rel ?a ?b |- _ ] => (atomic a; subst_by_rewrite_hyp a H) || (atomic b; subst_by_rewrite_rev_hyp b H)
  end.

Ltac subst_body :=
  repeat match goal with
           | [ H := _ |- _ ] => subst H
         end.

(* So we know the difference betwen the [sigT]s we're using and the [sigT]s others use *)
Inductive Common_sigT (A : Type) (P : A -> Type) : Type :=
    Common_existT : forall x : A, P x -> Common_sigT P.
Polymorphic Definition Common_projT1 (A : Type) (P : A -> Type) (x : @Common_sigT A P) := let (a, _) := x in a.
Polymorphic Definition Common_projT2 (A : Type) (P : A -> Type) (x : @Common_sigT A P) := let (x0, h) as x0 return (P (Common_projT1 x0)) := x in h.

Ltac uncurryT H :=
  match eval simpl in H with
    | forall (x : ?T1) (y : @?T2 x), @?f x y => uncurryT (forall xy : @Common_sigT T1 T2, f (Common_projT1 xy) (Common_projT2 xy))
    | ?H' => H'
  end.

Ltac curryT H :=
  match eval simpl in H with
    | forall xy : @Common_sigT ?T1 ?T2, @?f xy => curryT (forall (x : T1) (y : T2 x), f (@Common_existT T1 T2 x y))
    | ?H' => H'
  end.

Ltac uncurry H := let HT := type of H in
  match eval simpl in HT with
    | forall (x : ?T1) (y : @?T2 x) (z : @?T3 x y), @?f x y z =>
      uncurry (fun xyz => H (Common_projT1 (Common_projT1 xyz)) (Common_projT2 (Common_projT1 xyz)) (Common_projT2 xyz))
    | forall (x : ?T1) (y : @?T2 x), @?f x y => uncurry (fun xy : @Common_sigT T1 T2 => H (Common_projT1 xy) (Common_projT2 xy))
    | ?H' => H
  end.

Ltac curry H := let HT := type of H in
  match eval simpl in HT with
    | forall xy : @Common_sigT ?T1 ?T2, @?f xy => curry (fun (x : T1) (y : T2 x) => H (@Common_existT T1 T2 x y))
    | ?H' => H
  end.

Lemma fg_equal A B (f g : A -> B) : f = g -> forall x, f x = g x.
  intros; repeat subst; reflexivity.
Qed.

Section telescope.
  Inductive telescope :=
  | Base : forall (A : Type) (B : A -> Type), (forall a, B a) -> (forall a, B a) -> telescope
  | Quant : forall A : Type, (A -> telescope) -> telescope.

  Fixpoint telescopeOut (t : telescope) :=
    match t with
      | @Base _ _ x y => x = y
      | @Quant _ f => forall x, telescopeOut (f x)
    end.

  Fixpoint telescopeOut' (t : telescope) :=
    match t with
      | @Base _ _ f g => forall x, f x = g x
      | @Quant _ f => forall x, telescopeOut' (f x)
    end.

  Theorem generalized_fg_equal : forall (t : telescope),
    telescopeOut t
    -> telescopeOut' t.
    induction t; simpl; intuition; subst; auto.
  Qed.
End telescope.

Ltac curry_in_Quant H :=
  match eval simpl in H with
    | @Quant (@Common_sigT ?T1 ?T2) (fun xy => @?f xy) => curry_in_Quant (@Quant T1 (fun x => @Quant (T2 x) (fun y => f (@Common_existT T1 T2 x y))))
    | ?H' => H'
  end.

Ltac reifyToTelescope' H := let HT := type of H in let H' := uncurryT HT in
  match H' with
    | @eq ?T ?f ?g => let T' := eval hnf in T in
      match T' with
        | forall x : ?a, @?b x => constr:(@Base a b f g)
      end
    | forall x, @eq (@?T x) (@?f x) (@?g x) => let T' := eval hnf in T in (* XXX does [hnf] even do anything on [(fun _ => _)]?  I want to do [hnf] inside the function, but I don't want to do [compute] *)
      match T' with
        | (fun x => forall y : @?a x, @?b x y) => constr:(Quant (fun x => @Base (a x) (b x) (f x) (g x)))
      end
  end.

Ltac reifyToTelescope H := let t' := reifyToTelescope' H in curry_in_Quant t'.
Ltac fg_equal_in H := let t := reifyToTelescope H in apply (generalized_fg_equal t) in H; simpl in H.

Ltac fg_equal :=
  repeat match goal with
           | [ H : _ |- _ ] => fg_equal_in H
         end.

Lemma f_equal_helper A0 (A B : A0 -> Type) (f : forall a0, A a0 -> B a0) (x y : forall a0, A a0) :
  (forall a0, x a0 = y a0) -> (forall a0, f a0 (x a0) = f a0 (y a0)).
  intros H a0; specialize (H a0); rewrite H; reflexivity.
Qed.

Ltac f_equal_in_r H k := let H' := uncurry H in let H'T := type of H' in
  let k' := (fun v => let v' := curry v in let H := fresh in assert (H := v'); simpl in H) in
    match eval simpl in H'T with
      | @eq ?A ?x ?y => k (fun B (f : A -> B) => @f_equal A B f x y H') k'
      | forall a0 : ?A0, @eq (@?A a0) (@?x a0) (@?y a0)
        => k (fun (B : A0 -> Type) (f : forall a0 : A0, A a0 -> B a0) => @f_equal_helper A0 A B f x y H') k'
    end; clear H.
Ltac f_equal_in f H := f_equal_in_r H ltac:(fun pf k => k (pf _ f)).

Ltac eta_red :=
  repeat match goal with
           | [ H : appcontext[fun x => ?f x] |- _ ] => change (fun x => f x) with f in H
           | [ |- appcontext[fun x => ?f x] ] => change (fun x => f x) with f
         end.

Lemma sigT_eta : forall A (P : A -> Type) (x : sigT P),
  x = existT _ (projT1 x) (projT2 x).
  destruct x; reflexivity.
Qed.

Lemma sigT2_eta : forall A (P Q : A -> Type) (x : sigT2 P Q),
  x = existT2 _ _ (projT1 x) (projT2 x) (projT3 x).
  destruct x; reflexivity.
Qed.

Lemma sig_eta : forall A (P : A -> Prop) (x : sig P),
  x = exist _ (proj1_sig x) (proj2_sig x).
  destruct x; reflexivity.
Qed.

Lemma sig2_eta : forall A (P Q : A -> Prop) (x : sig2 P Q),
  x = exist2 _ _ (proj1_sig x) (proj2_sig x) (proj3_sig x).
  destruct x; reflexivity.
Qed.

Lemma prod_eta : forall (A B : Type) (x : A * B),
  x = pair (fst x) (snd x).
  destruct x; reflexivity.
Qed.

Ltac rewrite_eta_in Hf :=
  repeat match type of Hf with
           | context[match ?E with existT2 _ _ _ => _ end] => rewrite (sigT2_eta E) in Hf; simpl in Hf
           | context[match ?E with exist2 _ _ _ => _ end] => rewrite (sig2_eta E) in Hf; simpl in Hf
           | context[match ?E with existT _ _ => _ end] => rewrite (sigT_eta E) in Hf; simpl in Hf
           | context[match ?E with exist _ _ => _ end] => rewrite (sig_eta E) in Hf; simpl in Hf
           | context[match ?E with pair _ _ => _ end] => rewrite (prod_eta E) in Hf; simpl in Hf
         end.

Ltac rewrite_eta :=
  repeat match goal with
           | [ |- context[match ?E with existT2 _ _ _ => _ end] ] => rewrite (sigT2_eta E); simpl
           | [ |- context[match ?E with exist2 _ _ _ => _ end] ] => rewrite (sig2_eta E); simpl
           | [ |- context[match ?E with existT _ _ => _ end] ] => rewrite (sigT_eta E); simpl
           | [ |- context[match ?E with exist _ _ => _ end] ] => rewrite (sig_eta E); simpl
           | [ |- context[match ?E with pair _ _ => _ end] ] => rewrite (prod_eta E); simpl
         end.

Ltac intro_proj2_sig_from_goal'_by tac :=
  repeat match goal with
           | [ |- appcontext[proj1_sig ?x] ] => tac (proj2_sig x)
           | [ |- appcontext[proj1_sig (sig_of_sig2 ?x)] ] => tac (proj3_sig x)
         end.

Ltac intro_proj2_sig_from_goal_by tac :=
  repeat match goal with
           | [ |- appcontext[proj1_sig ?x] ] => tac (proj2_sig x)
           | [ |- appcontext[proj1_sig (sig_of_sig2 ?x)] ] => tac (proj3_sig x)
         end; simpl in *.

Ltac intro_projT2_from_goal_by tac :=
  repeat match goal with
           | [ |- appcontext[projT1 ?x] ] => tac (projT2 x)
           | [ |- appcontext[projT1 (sigT_of_sigT2 ?x)] ] => tac (projT3 x)
         end; simpl in *.

Ltac intro_proj2_sig_by tac :=
  repeat match goal with
           | [ |- appcontext[proj1_sig ?x] ] => tac (proj2_sig x)
           | [ H : appcontext[proj1_sig ?x] |- _ ] => tac (proj2_sig x)
           | [ H := appcontext[proj1_sig ?x] |- _ ] => tac (proj2_sig x)
           | [ |- appcontext[proj1_sig (sig_of_sig2 ?x)] ] => tac (proj3_sig x)
           | [ H : appcontext[proj1_sig (sig_of_sig2 ?x)] |- _ ] => tac (proj3_sig x)
           | [ H := appcontext[proj1_sig (sig_of_sig2 ?x)] |- _ ] => tac (proj3_sig x)
         end; simpl in *.

Ltac intro_projT2_by tac :=
  repeat match goal with
           | [ |- appcontext[projT1 ?x] ] => tac (projT2 x)
           | [ H : appcontext[projT1 ?x] |- _ ] => tac (projT2 x)
           | [ H := appcontext[projT1 ?x] |- _ ] => tac (projT2 x)
           | [ |- appcontext[projT1 (sigT_of_sigT2 ?x)] ] => tac (projT3 x)
           | [ H : appcontext[projT1 (sigT_of_sigT2 ?x)] |- _ ] => tac (projT3 x)
           | [ H := appcontext[projT1 (sigT_of_sigT2 ?x)] |- _ ] => tac (projT3 x)
         end; simpl in *.


Ltac intro_proj2_sig_from_goal' := intro_proj2_sig_from_goal'_by unique_pose.
Ltac intro_proj2_sig_from_goal := intro_proj2_sig_from_goal_by unique_pose.
Ltac intro_projT2_from_goal := intro_projT2_from_goal_by unique_pose.
Ltac intro_projT2_from_goal_with_body := intro_projT2_from_goal_by unique_pose_with_body.
Ltac intro_proj2_sig := intro_proj2_sig_by unique_pose.
Ltac intro_projT2 := intro_projT2_by unique_pose.
Ltac intro_projT2_with_body := intro_projT2_by unique_pose_with_body.

Ltac recr_destruct_with tac H :=
  let H0 := fresh in let H1 := fresh in
    (tac H; try reflexivity; try clear H) ||
      (destruct H as [ H0 H1 ];
        simpl in H0, H1;
          recr_destruct_with tac H0 || recr_destruct_with tac H1;
            try clear H0; try clear H1).

Ltac do_rewrite H := rewrite H.
Ltac do_rewrite_rev H := rewrite <- H.
Ltac recr_destruct_rewrite H := recr_destruct_with do_rewrite H.
Ltac recr_destruct_rewrite_rev H := recr_destruct_with do_rewrite_rev H.


Ltac use_proj2_sig_with tac :=
  repeat match goal with
           | [ |- appcontext[proj1_sig ?x] ] =>
             match x with
               | context[proj1_sig] => fail 1
               | _ => simpl_do_clear tac (proj2_sig x)
             end
         end.

Ltac rewrite_proj2_sig := use_proj2_sig_with recr_destruct_rewrite.
Ltac rewrite_rev_proj2_sig := use_proj2_sig_with recr_destruct_rewrite_rev.

Polymorphic Definition is_unique (A : Type) (x : A) := forall x' : A, x' = x.
Implicit Arguments is_unique [A].

Ltac rewrite_unique :=
  match goal with
    | [ H : is_unique _ |- _ ] => unfold is_unique in H; rewrite H || rewrite <- H; reflexivity
  end.

Ltac generalize_is_unique_hyp H T :=
  assert (forall a b : T, a = b) by (intros; etransitivity; apply H || symmetry; apply H); clear H.

Ltac generalize_is_unique :=
  repeat match goal with
           | [ H : @is_unique ?T _ |- _ ] => generalize_is_unique_hyp H T
         end.

Ltac intro_fresh_unique :=
  repeat match goal with
           | [ H : @is_unique ?T ?x |- _ ] => let x' := fresh in assert (x' := x); rewrite <- (H x') in *; generalize_is_unique_hyp H T
         end.

Ltac specialize_with_evars_then_do E tac :=
  match type of E with
    | forall x : ?T, _ =>
      let y := fresh in evar (y : T);
        let y' := (eval unfold y in y) in clear y;
          specialize_with_evars_then_do (E y') tac
    | _ => tac E
  end.

Ltac specialize_hyp_with_evars E :=
  repeat match type of E with
           | forall x : ?T, _ =>
             let y := fresh in evar (y : T);
               let y' := (eval unfold y in y) in clear y;
                 specialize (E y')
         end.

(* tries to convert an existential to an evar *)
Ltac existential_to_evar x :=
  is_evar x;
  let x' := fresh in
  set (x' := x) in *.

(* converts existentials in the goal into evars *)
Ltac existentials_to_evars_in_goal :=
  repeat match goal with
           | [ |- context[?x] ] => existential_to_evar x
         end.

(* converts all the existentials in the hypotheses to evars *)
Ltac existentials_to_evars_in_hyps :=
  repeat match goal with
           | [ H : context[?x] |- _ ] => existential_to_evar x
         end.

(* converts all the existentials in the hypothesis [H] to evars *)
Ltac existentials_to_evars_in H :=
  repeat match type of H with
           | context[?x] => existential_to_evar x
         end.

Tactic Notation "existentials_to_evars" := existentials_to_evars_in_goal.
Tactic Notation "existentials_to_evars" "in" "|-" "*" := existentials_to_evars_in_goal.
Tactic Notation "existentials_to_evars" "in" "*" := existentials_to_evars_in_goal; existentials_to_evars_in_hyps.
Tactic Notation "existentials_to_evars" "in" "*" "|-" := existentials_to_evars_in_hyps.
Tactic Notation "existentials_to_evars" "in" hyp(H) "|-" "*" := existentials_to_evars_in H; existentials_to_evars_in_goal.
Tactic Notation "existentials_to_evars" "in" hyp(H) := existentials_to_evars_in H.
Tactic Notation "existentials_to_evars" "in" hyp(H) "|-" := existentials_to_evars_in H.

(* rewrite fails if hypotheses depend on one another.  simultaneous rewrite does not *)
Ltac simultaneous_rewrite' E :=
  match type of E with
    | ?X = _ => generalize E; generalize dependent X; intros until 1;
      let H := fresh in intro H at top;
        match type of H with
          ?X' = _ => subst X'
        end
  end.

Ltac simultaneous_rewrite_rev' E :=
  match type of E with
    | _ = ?X => generalize E; generalize dependent X; intros until 1;
      let H := fresh in intro H at top;
        match type of H with
          _ = ?X' => subst X'
        end
  end.

Ltac simultaneous_rewrite E := specialize_with_evars_then_do E ltac:(fun E =>
  match type of E with
    | ?T = _ => let H := fresh in
      match goal with
        | [ _ : context[?F] |- _ ] =>
          assert (H : T = F) by reflexivity; clear H
      end; simultaneous_rewrite' E
  end
).

Ltac simultaneous_rewrite_rev E := specialize_with_evars_then_do E ltac:(fun E =>
  match type of E with
    | _ = ?T => let H := fresh in
      match goal with
        | [ _ : context[?F] |- _ ] =>
          assert (H : T = F) by reflexivity; clear H
      end; simultaneous_rewrite_rev' E
  end
).

(* rewrite by convertiblity rather than syntactic equality *)
Ltac conv_rewrite_with rew_tac H := specialize_with_evars_then_do H ltac:(fun H =>
  match type of H with
    | ?a = _ => match goal with
                  | [ |- appcontext[?a'] ] => let H' := fresh in assert (H' : a = a') by reflexivity; clear H';
                    change a' with a; rew_tac H
                end
  end
).
Ltac conv_rewrite_rev_with rew_tac H := specialize_with_evars_then_do H ltac:(fun H =>
  match type of H with
    | _ = ?a => match goal with
                  | [ |- appcontext[?a'] ] => let H' := fresh in assert (H' : a = a') by reflexivity; clear H';
                    change a' with a; rew_tac H
                end
  end
).

Ltac conv_rewrite H := conv_rewrite_with ltac:(fun h => rewrite h) H.
Ltac conv_rewrite_rev H := conv_rewrite_rev_with ltac:(fun h => rewrite <- h) H.
Ltac conv_repeat_rewrite H := repeat conv_rewrite_with ltac:(fun h => repeat rewrite h) H.
Ltac conv_repeat_rewrite_rev H := repeat conv_rewrite_rev_with ltac:(fun h => repeat rewrite <- h) H.

Ltac rewrite_by_context ctx H :=
  match type of H with
    | ?x = ?y => let ctx' := context ctx[x] in let ctx'' := context ctx[y] in
      cut ctx'; [ let H' := fresh in intro H'; simpl in H' |- *; exact H' | ];
        cut ctx''; [ let H' := fresh in intro H'; etransitivity; try apply H'; rewrite H; reflexivity
          |
        ]
  end.

Ltac rewrite_rev_by_context ctx H :=
  match type of H with
    | ?x = ?y => let ctx' := context ctx[y] in let ctx'' := context ctx[x] in
      cut ctx'; [ let H' := fresh in intro H'; simpl in H' |- *; exact H' | ];
        cut ctx''; [ let H' := fresh in intro H'; etransitivity; try apply H'; rewrite <- H; reflexivity
          |
        ]
  end.

Ltac do_for_each_hyp' tac fail_if_seen :=
  match goal with
    | [ H : _ |- _ ] => fail_if_seen H; tac H; try do_for_each_hyp' tac ltac:(fun H' => fail_if_seen H'; match H' with | H => fail 1 | _ => idtac end)
  end.
Ltac do_for_each_hyp tac := do_for_each_hyp' tac ltac:(fun H => idtac).

(* [change a with b in *] fails if it would create a self-referential hypothesis.
   This version does not. *)
Tactic Notation "change_in_all" constr(from) "with" constr(to) :=
  change from with to; do_for_each_hyp ltac:(fun H => change from with to in H).

(* [expand] replaces both terms of an equality (either [eq] or [JMeq]
   in the goal with their head normal forms *)
Ltac expand :=
  match goal with
    | [ |- ?X = ?Y ] =>
      let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')
    | [ |- ?X == ?Y ] =>
      let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')
  end; simpl.

(* [hideProof' pf] generalizes [pf] only if it does not already exist
   as a hypothesis *)
Ltac hideProof' pf :=
  match goal with
    | [ x : _ |- _ ] => match x with
                          | pf => fail 2
                        end
    | _ => generalize pf; intro
  end.

(* TODO(jgross): Is there a better way to do this? *)
Tactic Notation "hideProofs" constr(pf)
  := hideProof' pf.
Tactic Notation "hideProofs" constr(pf0) constr(pf1)
  := progress (try hideProof' pf0; try hideProof' pf1).
Tactic Notation "hideProofs" constr(pf0) constr(pf1) constr(pf2)
  := progress (try hideProof' pf0; try hideProof' pf1; try hideProof' pf2).
Tactic Notation "hideProofs" constr(pf0) constr(pf1) constr(pf2) constr(pf3)
  := progress (try hideProof' pf0; try hideProof' pf1; try hideProof' pf2; try hideProof' pf3).
Tactic Notation "hideProofs" constr(pf0) constr(pf1) constr(pf2) constr(pf3) constr(pf4)
  := progress (try hideProof' pf0; try hideProof' pf1; try hideProof' pf2; try hideProof' pf3; try hideProof' pf4).
Tactic Notation "hideProofs" constr(pf0) constr(pf1) constr(pf2) constr(pf3) constr(pf4) constr(pf5)
  := progress (try hideProof' pf0; try hideProof' pf1; try hideProof' pf2; try hideProof' pf3; try hideProof' pf4; try hideProof' pf5).

Ltac destruct_to_empty_set :=
  match goal with
    | [ H : Empty_set |- _ ] => destruct H
    | [ H : ?T -> Empty_set, a : ?T |- _ ] => destruct (H a)
    | [ H : context[Empty_set] |- _ ] => solve [ destruct H; trivial; assumption ]
  end.

Ltac destruct_to_empty_set_in_match :=
  match goal with
    | [ |- appcontext[match ?x with end] ] => solve [ destruct x || let H := fresh in pose x as H; destruct H ]
    | [ _ : appcontext[match ?x with end] |- _ ] => solve [ destruct x || let H := fresh in pose x as H; destruct H ]
  end.

Section unit.
  Lemma unit_singleton (u : unit) : u = tt.
    case u; reflexivity.
  Qed.

  Lemma unit_eq (u u' : unit) : u = u'.
    case u; case u'; reflexivity.
  Defined.

  Lemma unit_eq_singleton (u u' : unit) (H : u = u') : H = unit_eq _ _.
    destruct u; destruct H; reflexivity.
  Defined.

  Lemma unit_eq_eq (u u' : unit) (H H' : u = u') : H = H'.
    transitivity (@unit_eq u u');
    destruct_head @eq; subst_body; destruct_head unit; reflexivity.
  Defined.

  Lemma unit_JMeq (u u' : unit) : u == u'.
    case u; case u'; reflexivity.
  Defined.

  Lemma Empty_set_eq (a b : Empty_set) : a = b.
    destruct a.
  Defined.

  Lemma Empty_set_JMeql (a : Empty_set) T (b : T) : a == b.
    destruct a.
  Defined.

  Lemma Empty_set_JMeqr T (a : T) (b : Empty_set) : a == b.
    destruct b.
  Defined.
End unit.

Polymorphic Hint Rewrite unit_singleton.
Polymorphic Hint Extern 0 (@eq unit _ _) => apply unit_eq.
Polymorphic Hint Extern 0 (@eq (eq unit _ _) _ _) => apply unit_eq_eq.
Polymorphic Hint Extern 0 (@JMeq unit _ unit _) => apply unit_JMeq.
Polymorphic Hint Extern 0 unit => constructor.
Polymorphic Hint Extern 0 (@eq Empty_set _ _) => apply Empty_set_eq.
Polymorphic Hint Extern 0 (@JMeq Empty_set _ _ _) => apply Empty_set_JMeql.
Polymorphic Hint Extern 0 (@JMeq _ _ Empty_set _) => apply Empty_set_JMeqr.
Reserved Notation "x == y" (at level 70, no associativity).
Reserved Notation "x == y == z" (at level 70, no associativity, y at next level).

Reserved Notation "x ~= y" (at level 70, no associativity).
Reserved Notation "x ~= y ~= z" (at level 70, no associativity, y at next level).

Reserved Notation "i ⁻¹" (at level 10).
Reserved Notation "C áµ’áµ–" (at level 10).

Reserved Notation "C ★^ M D" (at level 70, no associativity).
Reserved Notation "C ★^{ M } D" (at level 70, no associativity).

Reserved Notation "S ↓ T" (at level 70, no associativity).

Reserved Notation "S ⇑ T" (at level 70, no associativity).
Reserved Notation "S ⇓ T" (at level 70, no associativity).
Reserved Notation "'CAT' ⇑ D" (at level 70, no associativity).
Reserved Notation "'CAT' ⇓ D" (at level 70, no associativity).

Reserved Notation "x ⊗ y" (at level 40, left associativity).
Reserved Notation "x ⊗m y" (at level 40, left associativity).

Reserved Notation "f â—‹ g" (at level 70, right associativity).

Reserved Notation "x ~> y" (at level 99, right associativity, y at level 200).

Reserved Notation "x ∏ y" (at level 40, left associativity).
Reserved Notation "x ∐ y" (at level 50, left associativity).

Reserved Notation "∏_{ x } f" (at level 0, x at level 99).
Reserved Notation "∏_{ x : A } f" (at level 0, x at level 99).
Reserved Notation "∐_{ x } f" (at level 0, x at level 99).
Reserved Notation "∐_{ x : A } f" (at level 0, x at level 99).

(* I'm not terribly happy with this notation, but '('s don't work
   because they interfere with things like [prod]s and grouping,
   and '['s interfere with list notation in Program. *)
Reserved Notation "F ⟨ c , - ⟩" (at level 70, no associativity).
Reserved Notation "F ⟨ - , d ⟩" (at level 70, no associativity).

(* Forced by the notation in Program *)
Reserved Notation "[ x ]" (at level 0, x at level 200).

Reserved Notation "∫ F" (at level 0).

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.
Delimit Scope natural_transformation_scope with natural_transformation.

Delimit Scope graph_scope with graph.
Delimit Scope vertex_scope with vertex.
Delimit Scope edge_scope with edge.
Require Import FunctionalExtensionality JMeq.

Set Implicit Arguments.

Local Infix "==" := JMeq.

Section f_equal_dep.
  Theorem f_type_equal {A B A' B'} : A = A' -> B = B' -> (A -> B) = (A' -> B').
    intros; repeat subst; reflexivity.
  Qed.

  Theorem forall_extensionality_dep : forall {A}
    (f g : A -> Type),
    (forall x, f x = g x) -> (forall x, f x) = (forall x, g x).
    intros.
    replace f with g; auto.
    apply functional_extensionality_dep; auto.
  Qed.

  Theorem forall_extensionality_dep_JMeq : forall {A B}
    (f : A -> Type) (g : B -> Type),
    A = B -> (A = B -> forall x y, x == y -> f x == g y) -> (forall x, f x) = (forall x, g x).
    intros; firstorder; intuition; repeat subst.
    apply forall_extensionality_dep.
    intro.
    apply JMeq_eq.
    eauto.
  Qed.


  Lemma JMeq_eqT A B (x : A) (y : B) : x == y -> A = B.
    intro H; destruct H; reflexivity.
  Qed.

  Lemma fg_equal_JMeq A B B' (f : forall a : A, B a) (g : forall a : A, B' a) x :
    f == g -> (f == g -> B = B') -> f x == g x.
    intros.
    repeat (firstorder; repeat subst).
  Qed.

  Lemma f_equal_JMeq A A' B B' a b (f : forall a : A, A' a) (g : forall b : B, B' b) :
    f == g -> (f == g -> A' == B') -> (f == g -> a == b) -> f a == g b.
    intros.
    firstorder.
    repeat destruct_type @JMeq.
    repeat subst; reflexivity.
  Qed.

  Lemma f_equal1_JMeq A0 B a0 b0 (f : forall (a0 : A0), B a0) :
    a0 = b0
    -> f a0 == f b0.
    intros.
    repeat (firstorder; repeat subst).
  Qed.

  Lemma f_equal2_JMeq A0 A1 B a0 b0 a1 b1 (f : forall (a0 : A0) (a1 : A1 a0), B a0 a1) :
    a0 = b0
    -> (a0 = b0 -> a1 == b1)
    -> f a0 a1 == f b0 b1.
    intros.
    repeat (firstorder; repeat subst).
  Qed.

  Lemma f_equal3_JMeq A0 A1 A2 B a0 b0 a1 b1 a2 b2 (f : forall (a0 : A0) (a1 : A1 a0) (a2 : A2 a0 a1), B a0 a1 a2) :
    a0 = b0
    -> (a0 = b0 -> a1 == b1)
    -> (a0 = b0 -> a1 == b1 -> a2 == b2)
    -> f a0 a1 a2 == f b0 b1 b2.
    intros.
    repeat (firstorder; repeat subst).
  Qed.

  Lemma f_equal4_JMeq A0 A1 A2 A3 B a0 b0 a1 b1 a2 b2 a3 b3 (f : forall (a0 : A0) (a1 : A1 a0) (a2 : A2 a0 a1) (a3 : A3 a0 a1 a2), B a0 a1 a2 a3) :
    a0 = b0
    -> (a0 = b0 -> a1 == b1)
    -> (a0 = b0 -> a1 == b1 -> a2 == b2)
    -> (a0 = b0 -> a1 == b1 -> a2 == b2 -> a3 == b3)
    -> f a0 a1 a2 a3 == f b0 b1 b2 b3.
    intros.
    repeat (firstorder; repeat subst).
  Qed.

  Lemma f_equal5_JMeq A0 A1 A2 A3 A4 B a0 b0 a1 b1 a2 b2 a3 b3 a4 b4 (f : forall (a0 : A0) (a1 : A1 a0) (a2 : A2 a0 a1) (a3 : A3 a0 a1 a2) (a4 : A4 a0 a1 a2 a3), B a0 a1 a2 a3 a4) :
    a0 = b0
    -> (a0 = b0 -> a1 == b1)
    -> (a0 = b0 -> a1 == b1 -> a2 == b2)
    -> (a0 = b0 -> a1 == b1 -> a2 == b2 -> a3 == b3)
    -> (a0 = b0 -> a1 == b1 -> a2 == b2 -> a3 == b3 -> a4 == b4)
    -> f a0 a1 a2 a3 a4 == f b0 b1 b2 b3 b4.
    intros.
    repeat (firstorder; repeat subst).
  Qed.

  Lemma eq_JMeq T (A B : T) : A = B -> A == B.
    intro; subst; reflexivity.
  Qed.

  Theorem functional_extensionality_dep_JMeq : forall {A} {B1 B2 : A -> Type},
    forall (f : forall x : A, B1 x) (g : forall x : A, B2 x),
      (forall x, B1 x = B2 x)
      -> (forall x, f x == g x) -> f == g.
    intros.
    assert (B1 = B2) by (extensionality x; auto); subst.
    assert (f = g) by (extensionality x; apply JMeq_eq; auto).
    subst; reflexivity.
  Qed.

  Theorem functional_extensionality_dep_JMeq' : forall {A1 A2} {B1 : A1 -> Type} {B2 : A2 -> Type},
    forall (f : forall x : A1, B1 x) (g : forall x : A2, B2 x),
      A1 = A2
      -> (A1 = A2 -> forall x y, x == y -> B1 x = B2 y)
      -> (A1 = A2 -> forall x y, x == y -> f x == g y) -> f == g.
    intros.
    intuition; repeat subst.
    apply functional_extensionality_dep_JMeq; intros;
      intuition.
  Qed.
End f_equal_dep.

Ltac JMeq_eq :=
  repeat match goal with
           | [ |- _ == _ ] => apply eq_JMeq
           | [ H : _ == _ |- _ ] => apply JMeq_eq in H
         end.

Ltac f_equal_dep_cleanup := JMeq_eq; eta_red.

Ltac f_equal_dep' := intros; f_equal; simpl in *;
  match goal with
    | [ |- ?f ?a == ?g ?b ] => apply (@f_equal_JMeq _ _ _ _ a b f g); intros; try reflexivity; repeat subst; intros;
      match goal with
        | [ |- f == g ] => f_equal_dep'
        | [ |- ?x == ?y ] => f_equal_dep_cleanup; try reflexivity
        | _ => idtac
      end
  end; f_equal_dep_cleanup.

Ltac f_equal_dep := intros; f_equal; simpl in *;
  repeat match goal with
           | [ |- ?f ?a = ?g ?b ] => apply JMeq_eq; f_equal_dep'
           | [ |- ?f ?a == ?g ?b ] => f_equal_dep'
           | _ => try reflexivity
         end; f_equal_dep_cleanup.

Section misc.
  Lemma sig_JMeq A0 A1 B0 B1 (a : @sig A0 A1) (b : @sig B0 B1) : A1 == B1 -> proj1_sig a == proj1_sig b -> a == b.
    intros.
    destruct_sig.
    repeat destruct_type @JMeq.
    JMeq_eq; subst.
    JMeq_eq.
    simpl_eq.
    trivial.
  Qed.
End misc.
Require Import FunctionalExtensionality ProofIrrelevance JMeq.

Set Implicit Arguments.

Local Infix "==" := JMeq.

Ltac structures_eq_simpl_step_with tac := intros; simpl in *;
  match goal with
    | _ => reflexivity
    | [ |- (fun _ : ?A => _) = _ ] => apply functional_extensionality_dep; intro
    | [ |- (fun _ : ?A => _) == _ ] => apply (@functional_extensionality_dep_JMeq A); intro
    | [ |- (forall _ : ?A, _) = _ ] => apply (@forall_extensionality_dep A); intro
    | _ => tac
  end; simpl; JMeq_eq.

Ltac structures_eq_step_with_tac structures_equal_tac tac := intros; simpl in *;
  match goal with
    | _ => reflexivity
    | [ |- _ = _ ] => structures_equal_tac
    | [ |- _ == _ ] => structures_equal_tac
    | _ => structures_eq_simpl_step_with tac
  end.

Ltac structures_eq_step_with structures_equal_lemma tac := structures_eq_step_with_tac ltac:(apply structures_equal_lemma) tac.
Require Import JMeq ProofIrrelevance.

Set Implicit Arguments.

Generalizable All Variables.

Local Infix "==" := JMeq.

Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
  Object :> _ := obj;
  Morphism' : obj -> obj -> Type;

  Identity' : forall o, Morphism' o o;
  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d';

  Associativity' : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
    Compose' (Compose' m3 m2) m1 = Compose' m3 (Compose' m2 m1);
  (* ask for [eq_sym (Associativity' ...)], so that C^{op}^{op} is convertible with C *)
  Associativity'_sym : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
    Compose' m3 (Compose' m2 m1) = Compose' (Compose' m3 m2) m1;
  LeftIdentity' : forall a b (f : Morphism' a b), Compose' (Identity' b) f = f;
  RightIdentity' : forall a b (f : Morphism' a b), Compose' f (Identity' a) = f
}.

Bind Scope category_scope with SpecializedCategory.
Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism'.

Arguments Object {obj%type} C%category : rename.
Arguments Identity' {obj%type} C%category o%object : rename.
Arguments Compose' {obj%type} C%category s%object d%object d'%object m1%morphism m2%morphism : rename.

(* create a hint db for all category theory things *)
Create HintDb category discriminated.
(* create a hint db for morphisms in categories *)
Create HintDb morphism discriminated.

Section SpecializedCategoryInterface.
  Polymorphic Definition Build_SpecializedCategory (obj : Type)
    (Morphism' : obj -> obj -> Type)
    (Identity' : forall o : obj, Morphism' o o)
    (Compose' : forall s d d' : obj, Morphism' d d' -> Morphism' s d -> Morphism' s d')
    (Associativity' : forall (o1 o2 o3 o4 : obj) (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
      Compose' o1 o2 o4 (Compose' o2 o3 o4 m3 m2) m1 = Compose' o1 o3 o4 m3 (Compose' o1 o2 o3 m2 m1))
    (LeftIdentity' : forall (a b : obj) (f : Morphism' a b), Compose' a b b (Identity' b) f = f)
    (RightIdentity' : forall (a b : obj) (f : Morphism' a b), Compose' a a b f (Identity' a) = f) :
    @SpecializedCategory obj
    := @Build_SpecializedCategory' obj
    Morphism'
    Identity' Compose'
    Associativity'
    (fun _ _ _ _ _ _ _ => eq_sym (Associativity' _ _ _ _ _ _ _))
    LeftIdentity'
    RightIdentity'.

  Context `(C : @SpecializedCategory obj).

  Polymorphic Definition Morphism : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').

  Bind Scope morphism_scope with Morphism.

  Polymorphic Definition Identity : forall o : C, Morphism o o := Eval cbv beta delta [Identity'] in C.(Identity').
  Polymorphic Definition Compose : forall {s d d' : C} (m : Morphism d d') (m0 : Morphism s d), Morphism s d' := Eval cbv beta delta [Compose'] in C.(Compose').
  Polymorphic Definition Associativity : forall (o1 o2 o3 o4 : C) (m1 : Morphism o1 o2) (m2 : Morphism o2 o3) (m3 : Morphism o3 o4),
    Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1)
    := C.(Associativity').
  Polymorphic Definition LeftIdentity : forall (a b : C) (f : Morphism a b),
    Compose (Identity b) f = f
    := C.(LeftIdentity').
  Polymorphic Definition RightIdentity : forall (a b : C) (f : Morphism a b),
    Compose f (Identity a) = f
    := C.(RightIdentity').
End SpecializedCategoryInterface.

Bind Scope morphism_scope with Morphism.

Arguments Object {obj} C : rename, simpl never.
Arguments Morphism {obj} C s d : rename, simpl nomatch.
Arguments Compose {obj} [C s d d'] m m0 : simpl nomatch.
Arguments Identity {obj} [C] o : simpl nomatch.

Global Opaque Associativity LeftIdentity RightIdentity.

Ltac sanitize_spcategory :=
  repeat match goal with
           | [ _ : appcontext[fun x => ?f x] |- _ ] => progress change (fun x => f x) with f in *
           | [ |- appcontext[fun x => ?f x] ] => progress change (fun x => f x) with f in *
           | [ _ : appcontext [?f (@Object ?obj ?C) ?C] |- _ ] => progress change (f (@Object obj C) C) with (f obj C) in *
           | [ |- appcontext [?f (@Object ?obj ?C) ?C] ] => progress change (f (@Object obj C) C) with (f obj C) in *
         end.

Ltac present_obj from to :=
  repeat match goal with
           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj) with (to obj) in *
           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj) with (to obj) in *
         end.

Ltac present_spcategory := present_obj @Morphism' @Morphism; present_obj @Identity' @Identity; present_obj @Compose' @Compose.

Ltac present_spcategory_all := present_spcategory;
  repeat match goal with
           | [ C : @SpecializedCategory ?obj |- _ ] => progress (change_in_all obj with (@Object obj C); sanitize_spcategory)
         end;
  sanitize_spcategory.

Ltac spcategory_hideProofs :=
  repeat match goal with
             | [ |- context[{|
                               Morphism' := _;
                               Identity' := _;
                               Compose' := _;
                               Associativity' := ?pf0;
                               Associativity'_sym := ?pf1;
                               LeftIdentity' := ?pf2;
                               RightIdentity' := ?pf3
                             |}] ] =>
               hideProofs pf0 pf1 pf2 pf3
         end.


(* TODO(jgross): Remove these when [Polymorphic Hint Rewrite] is fixed *)
Global Arguments LeftIdentity [_] _ _ _ _.
Global Arguments RightIdentity [_] _ _ _ _.
Global Arguments Associativity [_] _ _ _ _ _ _ _ _.

Polymorphic Hint Resolve LeftIdentity RightIdentity Associativity : category.
Polymorphic Hint Rewrite LeftIdentity RightIdentity : category.
Polymorphic Hint Resolve LeftIdentity RightIdentity Associativity : morphism.
Polymorphic Hint Rewrite LeftIdentity RightIdentity : morphism.

(* eh, I'm not terribly happy.  meh. *)
Polymorphic Definition LocallySmallSpecializedCategory (obj : Type) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
Polymorphic Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
Identity Coercion LocallySmallSpecializedCategory_SpecializedCategory_Id : LocallySmallSpecializedCategory >-> SpecializedCategory.
Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.

Section Categories_Equal.
  Lemma SpecializedCategory_eq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC) :
    @Morphism' _ C = @Morphism' _ D
    -> @Identity' _ C == @Identity' _ D
    -> @Compose' _ C == @Compose' _ D
    -> C = D.
    intros; intuition; destruct C, D; simpl in *; repeat subst;
      f_equal; apply proof_irrelevance.
  Qed.

  Lemma SpecializedCategory_JMeq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :
    objC = objD
    -> @Morphism' _ C == @Morphism' _ D
    -> @Identity' _ C == @Identity' _ D
    -> @Compose' _ C == @Compose' _ D
    -> C == D.
    intros; intuition; destruct C, D; simpl in *; repeat subst; JMeq_eq;
      f_equal; apply proof_irrelevance.
  Qed.
End Categories_Equal.

Ltac spcat_eq_step_with tac :=
  structures_eq_step_with_tac ltac:(apply SpecializedCategory_eq || apply SpecializedCategory_JMeq) tac.

Ltac spcat_eq_with tac := present_spcategory; repeat spcat_eq_step_with tac.

Ltac spcat_eq_step := spcat_eq_step_with idtac.
Ltac spcat_eq := spcategory_hideProofs; spcat_eq_with idtac.

Ltac solve_for_identity :=
  match goal with
    | [ |- @Compose _ ?C ?s ?s ?d ?a ?b = ?b ]
      => cut (a = @Identity _ C s);
        [ try solve [ let H := fresh in intro H; rewrite H; apply LeftIdentity ] | ]
    | [ |- @Compose _ ?C ?s ?d ?d ?a ?b = ?a ]
      => cut (b = @Identity _ C d );
        [ try solve [ let H := fresh in intro H; rewrite H; apply RightIdentity ] | ]
  end.

(** * Version of [Associativity] that avoids going off into the weeds in the presence of unification variables *)

Polymorphic Definition NoEvar T (_ : T) := True.

Lemma AssociativityNoEvar `(C : @SpecializedCategory obj) : forall (o1 o2 o3 o4 : C) (m1 : C.(Morphism) o1 o2)
  (m2 : C.(Morphism) o2 o3) (m3 : C.(Morphism) o3 o4),
  NoEvar (m1, m2) \/ NoEvar (m2, m3) \/ NoEvar (m1, m3)
  -> Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1).
  intros; apply Associativity.
Qed.

Ltac noEvar := match goal with
                 | [ |- context[NoEvar ?X] ] => (has_evar X; fail 1) ||
                   cut (NoEvar X); [ intro; tauto | constructor ]
               end.

(* TODO(jgross): Remove these when [Polymorphic Hint Rewrite] is fixed *)
Global Arguments AssociativityNoEvar [obj] _ _ _ _ _ [m1 m2 m3] _.

Polymorphic Hint Rewrite AssociativityNoEvar using noEvar : category.
Polymorphic Hint Rewrite AssociativityNoEvar using noEvar : morphism.

Ltac try_associativity_quick tac := try_rewrite Associativity tac.
Ltac try_associativity tac := try_rewrite_by AssociativityNoEvar ltac:(idtac; noEvar) tac.

Ltac find_composition_to_identity :=
  match goal with
    | [ H : @Compose _ _ _ _ _ ?a ?b = @Identity _ _ _ |- context[@Compose ?A ?B ?C ?D ?E ?c ?d] ]
      => let H' := fresh in
        assert (H' : b = d /\ a = c) by (split; reflexivity); clear H';
          assert (H' : @Compose A B C D E c d = @Identity _ _ _) by (
            exact H ||
              (unfold Object; simpl in H |- *; exact H || (rewrite H; reflexivity))
          );
          first [
            rewrite H'
            | simpl in H' |- *; rewrite H'
            | let H'T := type of H' in fail 2 "error in rewriting a found identity" H "[" H'T "]"
          ]; clear H'
  end.

(** * Back to the main content.... *)

Section Category.
  Context `(C : @SpecializedCategory obj).

  (* Quoting Wikipedia,
    In category theory, an epimorphism (also called an epic
    morphism or, colloquially, an epi) is a morphism [f : X → Y]
    which is right-cancellative in the sense that, for all
    morphisms [g, g' : Y → Z],
    [g â—‹ f = g' â—‹ f -> g = g']

    Epimorphisms are analogues of surjective functions, but they
    are not exactly the same. The dual of an epimorphism is a
    monomorphism (i.e. an epimorphism in a category [C] is a
    monomorphism in the dual category [OppositeCategory C]).
    *)
  Polymorphic Definition IsEpimorphism' x y (m : C.(Morphism') x y) : Prop :=
    forall z (m1 m2 : C.(Morphism) y z), Compose m1 m = Compose m2 m ->
      m1 = m2.
  Polymorphic Definition IsMonomorphism' x y (m : C.(Morphism') x y) : Prop :=
    forall z (m1 m2 : C.(Morphism) z x), Compose m m1 = Compose m m2 ->
      m1 = m2.
  Polymorphic Definition IsEpimorphism x y (m : C.(Morphism) x y) : Prop :=
    forall z (m1 m2 : C.(Morphism) y z), Compose m1 m = Compose m2 m ->
      m1 = m2.
  Polymorphic Definition IsMonomorphism x y (m : C.(Morphism) x y) : Prop :=
    forall z (m1 m2 : C.(Morphism) z x), Compose m m1 = Compose m m2 ->
      m1 = m2.
End Category.

Arguments IsEpimorphism' {obj} [C x y] m.
Arguments IsEpimorphism {obj} [C x y] m.
Arguments IsMonomorphism' {obj} [C x y] m.
Arguments IsMonomorphism {obj} [C x y] m.

Section AssociativityComposition.
  Context `(C : @SpecializedCategory obj).
  Variables o0 o1 o2 o3 o4 : C.

  Lemma compose4associativity_helper
    (a : Morphism _ o3 o4) (b : Morphism _ o2 o3)
    (c : Morphism _ o1 o2) (d : Morphism _ o0 o1) :
    Compose (Compose a b) (Compose c d) = (Compose a (Compose (Compose b c) d)).
    repeat rewrite Associativity; reflexivity.
  Qed.
End AssociativityComposition.

Ltac compose4associativity' a b c d := transitivity (Compose a (Compose (Compose b c) d)); try solve [ apply compose4associativity_helper ].
Ltac compose4associativity :=
  match goal with
    | [ |- Compose (Compose ?a ?b) (Compose ?c ?d) = _ ] => compose4associativity' a b c d
    | [ |- _ = Compose (Compose ?a ?b) (Compose ?c ?d) ] => compose4associativity' a b c d
  end.

Set Implicit Arguments.

Generalizable All Variables.

Polymorphic Record Category := {
  CObject : Type;

  UnderlyingCategory :> @SpecializedCategory CObject
}.

Polymorphic Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
  refine {| CObject := C.(Object) |}; auto.
Defined.

Coercion GeneralizeCategory : SpecializedCategory >-> Category.

Polymorphic Record SmallCategory := {
  SObject : Set;

  SUnderlyingCategory :> @SmallSpecializedCategory SObject
}.

Polymorphic Definition GeneralizeSmallCategory `(C : @SmallSpecializedCategory obj) : SmallCategory.
  refine {| SObject := obj |}; auto.
Defined.

Coercion GeneralizeSmallCategory : SmallSpecializedCategory >-> SmallCategory.

Polymorphic Record LocallySmallCategory := {
  LSObject : Type;

  LSUnderlyingCategory :> @LocallySmallSpecializedCategory LSObject
}.

Polymorphic Definition GeneralizeLocallySmallCategory `(C : @LocallySmallSpecializedCategory obj) : LocallySmallCategory.
  refine {| LSObject := obj |}; auto.
Defined.

Coercion GeneralizeLocallySmallCategory : LocallySmallSpecializedCategory >-> LocallySmallCategory.

Bind Scope category_scope with Category.
Bind Scope category_scope with SmallCategory.
Bind Scope category_scope with LocallySmallCategory.



(** * The saturation prover: up to some bound on number of steps, consider all ways to extend equivalences with pre- or post-composition. *)

(** The main tactic, which tries a single round of making deductions from hypotheses that exist at the start of the round.
    Only variables in the goal are chosen to compose. *)

Ltac saturate := repeat match goal with
                          | [ H : @eq (Morphism _ _ _) ?M ?N |- _ ] =>
                            let tryIt G :=
                              match goal with
                                | [ _ : G |- _ ] => fail 1
                                | [ |- context[G] ] => fail 1
                                | _ => let H' := fresh "H" in assert (H' : G) by eauto; generalize dependent H'
                              end in
                              repeat match goal with
                                       | [ m : Morphism _ _ _ |- _ ] =>
                                         tryIt (Compose M m = Compose N m)
                                       | [ m : Morphism _ _ _ |- _ ] =>
                                         tryIt (Compose m M = Compose m N)
                                     end; generalize dependent H
                        end; intros; autorewrite with core in *.

(** To be sure that all relevant terms are represented as variables, we use this tactic to create variables for
    all non-[Compose] subterms of a morphism expression. *)

Ltac extractMorphisms G :=
  match G with
    | Compose ?G1 ?G2 =>
      extractMorphisms G1;
      extractMorphisms G2
    | _ =>
      match goal with
        | [ x := G |- _ ] => idtac
        | [ x : _ |- _ ] =>
          match x with
            | G => idtac
          end
        | _ => pose G
      end
  end.

(** This tactic calls the above on two morphisms being compared for equivalence in the goal. *)

Ltac createVariables :=
  match goal with
    | [ |- @eq (Morphism _ _ _) ?X ?Y ] =>
      extractMorphisms X;
      extractMorphisms Y
  end.

(** After we are done with our variable-related hijinks, we can clean up by removing the new variables,
    replacing them by their definitions. *)

Ltac removeVariables :=
  repeat match goal with
           | [ x := _ |- _ ] => subst x
         end.

(** This notation ties it all together, taking as argument the number of [saturate] rounds to run. *)

Tactic Notation "morphisms" integer(numSaturations) :=
  t; createVariables; do numSaturations saturate; removeVariables; eauto 3.
Require Import JMeq ProofIrrelevance FunctionalExtensionality.

Set Implicit Arguments.

Generalizable All Variables.

Local Infix "==" := JMeq.

Section SpecializedFunctor.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  (**
     Quoting from the lecture notes for 18.705, Commutative Algebra:

     A map of categories is known as a functor. Namely, given
     categories [C] and [C'], a (covariant) functor [F : C -> C'] is a rule that assigns to
     each object [A] of [C] an object [F A] of [C'] and to each map [m : A -> B] of [C] a map
     [F m : F A -> F B] of [C'] preserving composition and identity; that is,
     (1) [F (m' â—‹ m) = (F m') â—‹ (F m)] for maps [m : A -> B] and [m' : B -> C] of [C], and
     (2) [F (id A) = id (F A)] for any object [A] of [C], where [id A] is the identity morphism of [A].
     **)
  Polymorphic Record SpecializedFunctor := {
    ObjectOf' : objC -> objD;
    MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d);
    FCompositionOf' : forall s d d' (m1 : C.(Morphism') s d) (m2: C.(Morphism') d d'),
      MorphismOf' _ _ (C.(Compose') _ _ _ m2 m1) = D.(Compose') _ _ _ (MorphismOf' _ _ m2) (MorphismOf' _ _ m1);
    FIdentityOf' : forall o, MorphismOf' _ _ (C.(Identity') o) = D.(Identity') (ObjectOf' o)
  }.
End SpecializedFunctor.

Bind Scope functor_scope with SpecializedFunctor.

Create HintDb functor discriminated.

Section FunctorInterface.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Variable F : SpecializedFunctor C D.

  Polymorphic Definition ObjectOf : C -> D := Eval cbv beta delta [ObjectOf'] in F.(ObjectOf'). (* [forall], so we can name it in [Arguments] *)
  Polymorphic Definition MorphismOf : forall {s d : C} (m : C.(Morphism) s d), D.(Morphism) (ObjectOf s) (ObjectOf d)
    := Eval cbv beta delta [MorphismOf'] in F.(MorphismOf').
  Polymorphic Definition FCompositionOf : forall (s d d' : C) (m1 : C.(Morphism) s d) (m2 : C.(Morphism) d d'),
    MorphismOf (Compose m2 m1) = Compose (MorphismOf m2) (MorphismOf m1)
    := F.(FCompositionOf').
  Polymorphic Definition FIdentityOf : forall (o : C), MorphismOf (Identity o) = Identity (ObjectOf o)
    := F.(FIdentityOf').
End FunctorInterface.

Global Coercion ObjectOf : SpecializedFunctor >-> Funclass.

Section Functor.
  Variable C D : Category.

  Polymorphic Definition Functor := SpecializedFunctor C D.
End Functor.

Bind Scope functor_scope with Functor.

Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
Polymorphic Definition GeneralizeFunctor objC C objD D (F : @SpecializedFunctor objC C objD D) : Functor C D := F.
Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.

(* try to always unfold [GeneralizeFunctor]; it's in there
   only for coercions *)
Arguments GeneralizeFunctor [objC C objD D] F /.
Polymorphic Hint Extern 0 => unfold GeneralizeFunctor : category.
Polymorphic Hint Extern 0 => unfold GeneralizeFunctor : functor.

Arguments SpecializedFunctor {objC} C {objD} D.
Arguments Functor C D.
Arguments ObjectOf {objC C objD D} F c : simpl nomatch.
Arguments MorphismOf {objC} [C] {objD} [D] F [s d] m : simpl nomatch.

Arguments FCompositionOf [objC C objD D] F _ _ _ _ _.
Arguments FIdentityOf [objC C objD D] F _.

(* TODO(jgross): Remove these when [Polymorphic Hint Rewrite] is fixed *)
Global Arguments FIdentityOf' [_ _ _ _] _ _.

Polymorphic Hint Resolve FCompositionOf FIdentityOf FCompositionOf' FIdentityOf' : category.
Polymorphic Hint Resolve FCompositionOf FIdentityOf FCompositionOf' FIdentityOf' : functor.
Polymorphic Hint Rewrite FIdentityOf FIdentityOf' : category.
Polymorphic Hint Rewrite FIdentityOf FIdentityOf' : functor.

Ltac present_obj_obj from to :=
  repeat match goal with
           | [ _ : appcontext[from ?obj ?C ?obj'] |- _ ] => change (from obj C obj') with (to obj C obj') in *
           | [ |- appcontext[from ?obj ?C ?obj'] ] => change (from obj C obj') with (to obj C obj') in *
         end.

Ltac present_spfunctor := present_spcategory;
  present_obj_obj @ObjectOf' @ObjectOf; present_obj_obj @MorphismOf' @MorphismOf.

Ltac functor_hideProofs :=
  repeat match goal with
             | [ |- context[{|
                               ObjectOf' := _;
                               MorphismOf' := _;
                               FCompositionOf' := ?pf0;
                               FIdentityOf' := ?pf1
                             |}] ] =>
               hideProofs pf0 pf1
         end.

Section Functors_Equal.
  Lemma Functor_eq' objC C objD D : forall (F G : @SpecializedFunctor objC C objD D),
    ObjectOf F = ObjectOf G
    -> MorphismOf F == MorphismOf G
    -> F = G.
    destruct F, G; simpl; intros; specialize_all_ways; repeat subst;
      f_equal; apply proof_irrelevance.
  Qed.

  Lemma Functor_eq objC C objD D :
    forall (F G : @SpecializedFunctor objC C objD D),
      (forall x, ObjectOf F x = ObjectOf G x)
      -> (forall s d m, MorphismOf F (s := s) (d := d) m == MorphismOf G (s := s) (d := d) m)
      -> F = G.
    intros; cut (ObjectOf F = ObjectOf G); intros; try apply Functor_eq'; destruct F, G; simpl in *; repeat subst;
    try apply eq_JMeq;
    repeat (apply functional_extensionality_dep; intro); trivial;
    try apply JMeq_eq; trivial.
  Qed.

  Lemma Functor_JMeq objC C objD D objC' C' objD' D' :
    forall (F : @SpecializedFunctor objC C objD D) (G : @SpecializedFunctor objC' C' objD' D'),
      objC = objC'
      -> objD = objD'
      -> C == C'
      -> D == D'
      -> ObjectOf F == ObjectOf G
      -> MorphismOf F == MorphismOf G
      -> F == G.
    simpl; intros; intuition; repeat subst; destruct F, G; simpl in *;
      repeat subst; JMeq_eq.
    f_equal; apply proof_irrelevance.
  Qed.
End Functors_Equal.

Ltac functor_eq_step_with tac :=
  structures_eq_step_with_tac ltac:(apply Functor_eq || apply Functor_JMeq) tac.

Ltac functor_eq_with tac := repeat functor_eq_step_with tac.

Ltac functor_eq_step := functor_eq_step_with idtac.
Ltac functor_eq := functor_hideProofs; functor_eq_with idtac.

Section FunctorComposition.
  Context `(B : @SpecializedCategory objB).
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).

  Polymorphic Hint Rewrite FCompositionOf : functor.

  Polymorphic Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E.
    refine {| ObjectOf' := (fun c => G (F c));
      MorphismOf' := (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m))
    |};
    abstract (
        intros; autorewrite with functor; reflexivity
      ).
  Defined.
End FunctorComposition.

Section IdentityFunctor.
  Context `(C : @SpecializedCategory objC).

  (* There is an identity functor.  It does the obvious thing. *)
  Polymorphic Definition IdentityFunctor : SpecializedFunctor C C.
    refine {| ObjectOf' := (fun x => x);
      MorphismOf' := (fun _ _ x => x)
    |};
    abstract t.
  Defined.
End IdentityFunctor.

Section IdentityFunctorLemmas.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Lemma LeftIdentityFunctor (F : SpecializedFunctor D C) : ComposeFunctors (IdentityFunctor _) F = F.
    functor_eq.
  Qed.

  Lemma RightIdentityFunctor (F : SpecializedFunctor C D) : ComposeFunctors F (IdentityFunctor _) = F.
    functor_eq.
  Qed.
End IdentityFunctorLemmas.

(* TODO(jgross): Remove these when [Polymorphic Hint Rewrite] is fixed *)
Global Arguments LeftIdentityFunctor [_ _ _ _] _.
Global Arguments RightIdentityFunctor [_ _ _ _] _.

Polymorphic Hint Rewrite LeftIdentityFunctor RightIdentityFunctor : category.
Polymorphic Hint Immediate LeftIdentityFunctor RightIdentityFunctor : category.
Polymorphic Hint Rewrite LeftIdentityFunctor RightIdentityFunctor : functor.
Polymorphic Hint Immediate LeftIdentityFunctor RightIdentityFunctor : functor.

Section FunctorCompositionLemmas.
  Context `(B : @SpecializedCategory objB).
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).

  Lemma ComposeFunctorsAssociativity (F : SpecializedFunctor B C) (G : SpecializedFunctor C D) (H : SpecializedFunctor D E) :
    ComposeFunctors (ComposeFunctors H G) F = ComposeFunctors H (ComposeFunctors G F).
    functor_eq.
  Qed.
End FunctorCompositionLemmas.

Polymorphic Hint Resolve ComposeFunctorsAssociativity : category.
Polymorphic Hint Resolve ComposeFunctorsAssociativity : functor.

Set Implicit Arguments.

Section DCategory.
  Variable O : Type.

  Local Ltac simpl_eq := subst_body; hnf in *; simpl in *; intros; destruct_type @inhabited; simpl in *;
    repeat constructor;
      repeat subst;
        auto;
          simpl_transitivity.

  Let DiscreteCategory_Morphism (s d : O) := s = d.

  Polymorphic Definition DiscreteCategory_Compose (s d d' : O) (m : DiscreteCategory_Morphism d d') (m' : DiscreteCategory_Morphism s d) :
    DiscreteCategory_Morphism s d'.
    simpl_eq.
  Defined.

  Polymorphic Definition DiscreteCategory_Identity o : DiscreteCategory_Morphism o o.
    simpl_eq.
  Defined.

  Global Arguments DiscreteCategory_Compose [s d d'] m m' /.
  Global Arguments DiscreteCategory_Identity o /.

  Polymorphic Definition DiscreteCategory : @SpecializedCategory O.
    refine {|
      Morphism' := DiscreteCategory_Morphism;
      Compose' := DiscreteCategory_Compose;
      Identity' := DiscreteCategory_Identity
    |};
    abstract (
      unfold DiscreteCategory_Compose, DiscreteCategory_Identity;
        simpl_eq
    ).
  Defined.
End DCategory.

Fixpoint CardinalityRepresentative (n : nat) : Set :=
  match n with
    | O => Empty_set
    | 1 => unit
    | S n' => (CardinalityRepresentative n' + unit)%type
  end.

Coercion CardinalityRepresentative : nat >-> Sortclass.

Polymorphic Definition NatCategory (n : nat) := Eval unfold DiscreteCategory, DiscreteCategory_Identity in DiscreteCategory n.

Coercion NatCategory : nat >-> SpecializedCategory.

Set Implicit Arguments.

Generalizable All Variables.

Section ProductCategory.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Polymorphic Definition ProductCategory : @SpecializedCategory (objC * objD)%type.
    refine {|
      Morphism' := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type);
      Identity' := (fun o => (Identity (fst o), Identity (snd o)));
(*      Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))) (* gives Uncaught exception: Not_found *) *)
      Compose' := (fun (s d d' : (C * D)%type) m2 m1 => (C.(Compose') _ _ _ (fst m2) (fst m1), D.(Compose') _ _ _ (snd m2) (snd m1)))
    |};
    abstract (intros; simpl_eq; auto with morphism).
  Defined.
End ProductCategory.

Infix "*" := ProductCategory : category_scope.

Section ProductCategoryFunctors.
  Context `{C : @SpecializedCategory objC}.
  Context `{D : @SpecializedCategory objD}.

  Polymorphic Definition fst_Functor : SpecializedFunctor (C * D) C.
    refine (Build_SpecializedFunctor (C * D) C
      (@fst _ _)
      (fun _ _ => @fst _ _)
      _
      _
    );
    abstract eauto.
  Defined.

  Polymorphic Definition snd_Functor : SpecializedFunctor (C * D) D.
    refine (Build_SpecializedFunctor (C * D) D
      (@snd _ _)
      (fun _ _ => @snd _ _)
      _
      _
    );
    abstract eauto.
  Defined.
End ProductCategoryFunctors.

Set Implicit Arguments.

Generalizable All Variables.

Local Open Scope category_scope.

Section swap.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Polymorphic Definition SwapFunctor : SpecializedFunctor (C * D) (D * C).
    refine (Build_SpecializedFunctor (C * D) (D * C)
                                     (fun cd => (snd cd, fst cd))
                                     (fun _ _ m => (snd m, fst m))
                                     _
                                     _);
    abstract (
        intros; simpl; present_spcategory; simpl_eq; reflexivity
      ).
  Defined.
End swap.

Section Law0.
  Context `(C : @SpecializedCategory objC).

  Polymorphic Definition ProductLaw0Functor : SpecializedFunctor (C * 0) 0.
    refine (Build_SpecializedFunctor (C * 0) 0
                                     (@snd _ _)
                                     (fun _ _ => @snd _ _)
                                     _
                                     _);
    abstract (
        intros;
        destruct_head_hnf @prod;
        destruct_head Empty_set
      ).
  Defined.

  Polymorphic Definition ProductLaw0Functor_Inverse : SpecializedFunctor 0 (C * 0).
    repeat esplit;
    intros; destruct_head_hnf Empty_set.
    Grab Existential Variables.
    intros; destruct_head_hnf Empty_set.
    intros; destruct_head_hnf Empty_set.
  Defined.

  Lemma ProductLaw0 : ComposeFunctors ProductLaw0Functor ProductLaw0Functor_Inverse = IdentityFunctor _ /\
    ComposeFunctors ProductLaw0Functor_Inverse ProductLaw0Functor = IdentityFunctor _.
  Proof.
    split.

If you add the line

Set Universe Polymorphism.

At the beginning of your file, the bug does not appear anymore. This maybe because one of the definition that you make in the long file is not declare Polymorphic, while it should. The directive makes all definitions universe polymorphic.