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

match expr with
| _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).

| Tidtac
end.

| Tidtac
end.

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