Library Common


Require Import JMeq ProofIrrelevance Eqdep_dec.
Require Export Notations.

Set Implicit Arguments.

Definition sumbool_to_bool A B : {A} + {B}bool
  := fun xif x then true else false.

Coercion sumbool_to_bool : sumbool >-> bool.

Section sig.
  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.
  Definition projT3 A P Q (x : @sigT2 A P Q) :=
    let (x0, _, h) as x0 return (Q (projT1 x0)) := x in h.

  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.
  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.

Tactic Notation "not_tac" tactic(tac) := (tac; fail 1) || idtac.

Tactic Notation "test_tac" tactic(tac) := not_tac (not_tac tac).

Ltac atomic x :=
  match x with
    | ?f _fail 1 x "is not atomic"
    | (fun __) ⇒ fail 1 x "is not atomic"
    | _, _fail 1 x "is not atomic"
    | _idtac
  end.

Ltac unique_pose defn :=
  let T := type of defn in
    match goal with
      | [ H : T |- _ ] ⇒ fail 1
      | _pose proof defn
    end.

Ltac unique_pose_with_body defn :=
  match goal with
    | [ H := defn |- _ ] ⇒ fail 1
    | _pose defn
  end.

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).

Ltac head expr :=
  match expr with
    | ?f _head f
    | _expr
  end.

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

Ltac simpl_do tac H :=
  let H' := fresh in pose H as H'; simpl; simpl in H'; tac H'.

Ltac simpl_do_clear tac H := simpl_do ltac:(fun Htac 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 Hrewrite H).
Ltac rewrite_hyp := repeat rewrite_hyp'.
Ltac rewrite_rev_hyp' := do_with_hyp ltac:(fun Hrewrite <- H).
Ltac rewrite_rev_hyp := repeat rewrite_rev_hyp'.

Ltac apply_hyp' := do_with_hyp ltac:(fun Happly H).
Ltac apply_hyp := repeat apply_hyp'.
Ltac eapply_hyp' := do_with_hyp ltac:(fun Heapply H).
Ltac eapply_hyp := repeat eapply_hyp'.

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.

Ltac simpl_transitivity :=
  try solve [ match goal with
                | [ _ : ?Rel ?a ?b, _ : ?Rel ?b ?c |- ?Rel ?a ?c ] ⇒ transitivity b; assumption
              end ].

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.

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
    | Tidtac
  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
    | Tidtac
  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
).

Ltac destruct_exists' T := cut T; try (let H := fresh in intro H; 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.

Ltac specialized_assumption tac := tac;
  match goal with
    | [ x : ?T, H : _ : ?T, _ |- _ ] ⇒ specialize (H x); specialized_assumption tac
    | _assumption
  end.

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.

Ltac specialize_all_ways_forall :=
  repeat match goal with
           | [ x : ?T, H : _ : ?T, _ |- _ ] ⇒ unique_pose (H x)
         end.

Ltac specialize_all_ways :=
  repeat match goal with
           | [ x : ?T, H : _ |- _ ] ⇒ unique_pose (H x)
         end.

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 ProofIrrelevance.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 ProofIrrelevance.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 p2snd p1 == snd p2p1 == 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.

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 ×
).

Ltac subst_eq_refl_dec :=
  repeat match goal with
           | [ H : ?a = ?a |- _ ] ⇒ clear H
           | [ H : ?a = ?a |- _ ] ⇒ assert (eq_refl = H)
                                    by abstract solve
                                                [ apply K_dec;
                                                  solve [ try decide equality; try congruence ]
                                                | assumption
                                                | easy ];
                                    subst H
         end.

Ltac subst_eq_refl :=
  repeat match goal with
           | _progress subst_eq_refl_dec
           | [ H : ?a = ?a |- _ ] ⇒ assert (eq_refl = H) by apply ProofIrrelevance.proof_irrelevance;
                                    subst H
         end.

Finds things of the form match E with _ _ end in the goal and tries to replace them with eq_refl

Ltac subst_eq_refl_dec_in_match :=
  repeat match goal with
           | [ |- appcontext[match ?E with __ end] ] ⇒
             let H := fresh in
             set (H := E) in *;
               clearbody H;
               hnf in H;
               simpl in H;
               match type of H with
                 | ?a = ?aidtac
                 | _ = _compute in H
               end;
               progress subst_eq_refl_dec; simpl in ×
         end.

Ltac subst_eq_refl_in_match :=
  repeat match goal with
           | [ |- appcontext[match ?E with __ end] ] ⇒
             let H := fresh in
             set (H := E) in *;
               clearbody H;
               hnf in H;
               simpl in H;
               match type of H with
                 | ?a = ?aidtac
                 | _ = _compute in H
               end;
               progress subst_eq_refl; simpl in ×
         end.

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 : Propab) (fun a b : Propba).

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 : Propa) (fun a b : Propb).

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

Ltac clear_hyp_unless_context hyp conVar :=
  let hypT := type of hyp in
    match goal with
      | [ H0 : hypT, H : context[conVar] |- _ ] ⇒ fail 1
      | [ |- 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.

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.

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 Htry rewrite H in *; try setoid_rewrite H).

Ltac subst_by_rewrite_rev_hyp a H :=
  subst_by_rewrite_hyp_rew a H ltac:(fun Htry 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.

Inductive Common_sigT (A : Type) (P : AType) : Type :=
    Common_existT : x : A, P xCommon_sigT P.
Definition Common_projT1 (A : Type) (P : AType) (x : @Common_sigT A P) := let (a, _) := x in a.
Definition Common_projT2 (A : Type) (P : AType) (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
    | (x : ?T1) (y : @?T2 x), @?f x yuncurryT ( xy : @Common_sigT T1 T2, f (Common_projT1 xy) (Common_projT2 xy))
    | ?H'H'
  end.

Ltac curryT H :=
  match eval simpl in H with
    | xy : @Common_sigT ?T1 ?T2, @?f xycurryT ( (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
    | (x : ?T1) (y : @?T2 x) (z : @?T3 x y), @?f x y z
      uncurry (fun xyzH (Common_projT1 (Common_projT1 xyz)) (Common_projT2 (Common_projT1 xyz)) (Common_projT2 xyz))
    | (x : ?T1) (y : @?T2 x), @?f x yuncurry (fun xy : @Common_sigT T1 T2H (Common_projT1 xy) (Common_projT2 xy))
    | ?H'H
  end.

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

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

Section telescope.
  Inductive telescope :=
  | Base : (A : Type) (B : AType), ( a, B a) → ( a, B a) → telescope
  | Quant : A : Type, (Atelescope) → telescope.

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

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

  Theorem generalized_fg_equal : (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 yf (@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 ?glet T' := eval hnf in T in
      match T' with
        | x : ?a, @?b xconstr:(@Base a b f g)
      end
    | x, @eq (@?T x) (@?f x) (@?g x) ⇒ let T' := eval hnf in T in
      match T' with
        | (fun x 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 : A0Type) (f : a0, A a0B a0) (x y : a0, A a0) :
  ( a0, x a0 = y a0) → ( 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 vlet 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 ?yk (fun B (f : AB) ⇒ @f_equal A B f x y H') k'
      | a0 : ?A0, @eq (@?A a0) (@?x a0) (@?y a0)
        ⇒ k (fun (B : A0Type) (f : a0 : A0, A a0B 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 kk (pf _ f)).

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

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

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

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

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

Lemma prod_eta : (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.

Definition is_unique (A : Type) (x : A) := 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 ( 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
    | 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
           | x : ?T, _
             let y := fresh in evar (y : T);
               let y' := (eval unfold y in y) in clear y;
                 specialize (E y')
         end.

Ltac existential_to_evar x :=
  is_evar x;
  let x' := fresh in
  set (x' := x) in ×.

Ltac existentials_to_evars_in_goal :=
  repeat match goal with
           | [ |- context[?x] ] ⇒ existential_to_evar x
         end.

Ltac existentials_to_evars_in_hyps :=
  repeat match goal with
           | [ H : context[?x] |- _ ] ⇒ existential_to_evar x
         end.

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.

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
    | _ = ?Xgeneralize 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
    | _ = ?Tlet H := fresh in
      match goal with
        | [ _ : context[?F] |- _ ] ⇒
          assert (H : T = F) by reflexivity; clear H
      end; simultaneous_rewrite_rev' E
  end
).

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
    | _ = ?amatch 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 hrewrite h) H.
Ltac conv_rewrite_rev H := conv_rewrite_rev_with ltac:(fun hrewrite <- h) H.
Ltac conv_repeat_rewrite H := repeat conv_rewrite_with ltac:(fun hrepeat rewrite h) H.
Ltac conv_repeat_rewrite_rev H := repeat conv_rewrite_rev_with ltac:(fun hrepeat rewrite <- h) H.

Ltac rewrite_by_context ctx H :=
  match type of H with
    | ?x = ?ylet 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 = ?ylet 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 | Hfail 1 | _idtac end)
  end.
Ltac do_for_each_hyp tac := do_for_each_hyp' tac ltac:(fun Hidtac).

Tactic Notation "change_in_all" constr(from) "with" constr(to) :=
  change from with to; do_for_each_hyp ltac:(fun Hchange from with to in H).

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.

Ltac hideProof' pf :=
  match goal with
    | [ x : _ |- _ ] ⇒ match x with
                          | pffail 2
                        end
    | _generalize pf; intro
  end.

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 : |- _ ] ⇒ destruct H
    | [ H : ?T, a : ?T |- _ ] ⇒ destruct (H a)
    | [ H : context[] |- _ ] ⇒ 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.

Ltac destruct_first_if_not_second a b :=
  (constr_eq a b; fail 1) || (let H := fresh in set (H := a : unit) in *; destruct H).

Ltac destruct_singleton_constructor c :=
  let t := type of c in
  repeat match goal with
           | [ H : t |- _ ] ⇒ destruct H
           | [ H : context[?e] |- _ ] ⇒ destruct_first_if_not_second e c
           | [ |- context[?e] ] ⇒ destruct_first_if_not_second e c
         end.

Ltac destruct_units := destruct_singleton_constructor tt.
Ltac destruct_Trues := destruct_singleton_constructor I.

Section True.
  Lemma True_singleton (u : True) : u = I.
    case u; reflexivity.
  Qed.

  Lemma True_eq (u u' : True) : u = u'.
    case u; case u'; reflexivity.
  Defined.

  Lemma True_eq_singleton (u u' : True) (H : u = u') : H = True_eq _ _.
    destruct u; destruct H; reflexivity.
  Defined.

  Lemma True_eq_eq (u u' : True) (H H' : u = u') : H = H'.
    transitivity (@True_eq u u');
    destruct_head @eq; subst_body; destruct_head True; reflexivity.
  Defined.

  Lemma True_JMeq (u u' : True) : u == u'.
    case u; case u'; reflexivity.
  Defined.

  Lemma False_eq (a b : False) : a = b.
    destruct a.
  Defined.

  Lemma False_JMeql (a : False) T (b : T) : a == b.
    destruct a.
  Defined.

  Lemma False_JMeqr T (a : T) (b : False) : a == b.
    destruct b.
  Defined.
End True.

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 : ) : a = b.
    destruct a.
  Defined.

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

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

Hint Rewrite True_singleton.
Hint Extern 0 (@eq True _ _) ⇒ apply True_eq.
Hint Extern 0 (@eq (@eq True _ _) _ _) ⇒ apply True_eq_eq.
Hint Extern 0 (@JMeq True _ True _) ⇒ apply True_JMeq.
Hint Extern 0 Trueconstructor.
Hint Extern 0 (@eq False _ _) ⇒ apply False_eq.
Hint Extern 0 (@JMeq False _ _ _) ⇒ apply False_JMeql.
Hint Extern 0 (@JMeq _ _ False _) ⇒ apply False_JMeqr.

Hint Rewrite unit_singleton.
Hint Extern 0 (@eq unit _ _) ⇒ apply unit_eq.
Hint Extern 0 (@eq (@eq unit _ _) _ _) ⇒ apply unit_eq_eq.
Hint Extern 0 (@JMeq unit _ unit _) ⇒ apply unit_JMeq.
Hint Extern 0 unitconstructor.
Hint Extern 0 (@eq _ _) ⇒ apply Empty_set_eq.
Hint Extern 0 (@JMeq _ _ _) ⇒ apply Empty_set_JMeql.
Hint Extern 0 (@JMeq _ _ _) ⇒ apply Empty_set_JMeqr.