Module Tactics

Load Param.

Ltac changeall v f P :=
match P with
| v => f
| forall x : ?T, ?b => let T2 := changeall v f T with b2 := changeall v f b in
  constr:(forall x : T2, b2)
| exists x : ?T, ?b => let T2 := changeall v f T with b2 := changeall v f b in
  constr:(exists x : T2, b2)
| (fun x : ?T => ?b) => let T2 := changeall v f T with b2 := changeall v f b in
  constr:(fun x : T2 => b2)
| (?a ?b) => let a2 := changeall v f a with b2 := changeall v f b in
  constr:(a2 b2)
| (?a -> ?b) => let a2 := changeall v f a with b2 := changeall v f b in
  constr:(a2 -> b2)
| _ => P
end.

Ltac setvar v f H :=
match goal with
| [|- ?P] =>
  let P2 := changeall f v P in
  cut (forall v, f = v -> P2) ;
  [intro H ; apply (H (f) (refl_equal _)) | intros v H ]
end.

Ltac var1 v f :=
 let H := fresh "H" in
 setvar v f H
.

Ltac var0 f :=
 let v := fresh "v" in
 let H := fresh "H" in
 setvar v f H
.

Ltac var f :=
 let v := fresh "v" in
 let H := fresh "H" in
 setvar v f H ; (rewrite H || idtac)
.

Ltac genclear H := generalize H ; clear H.

Ltac econtr := eapply False_rect ; eauto.

Ltac invert_all :=
match goal with
| [ |- ?Q ] =>
 match type of Q with
  | Prop => match goal with
    | [ H : exists x, _ |- _ ] => inversion_clear H
    end
 | _ =>
  match goal with
    | [ H : _ /\ _ |- _ ] => inversion_clear H
    | [ H : _ <-> _ |- _ ] => inversion_clear H
    | [ H : { x : _ & _ } |- _ ] => inversion_clear H
    | [ H : { x : _ | _ } |- _ ] => inversion_clear H
  end
 end
end.

Ltac invall := repeat invert_all.

Ltac discr :=
match goal with
| [ H1 : ?k = _ , H2 : ?k = _ |- _ ] => rewrite H2 in H1 ; clear H2 ; discr
| [ H1 : ?k = _ , H2 : _ = ?k |- _ ] => rewrite <- H2 in H1 ; clear H2 ; discr
| _ => discriminate
end.


Goal forall (A : Set) (a b c : A) (H1 : a = b) (H2 : a = c), True.
intros.
discr || eauto.
Save.