Library Coqprime.Tactic.Tactic

Ltac finish := intros; auto; trivial; discriminate.


Ltac contradict name :=
     let term := type of name in (
     match term with
       (~_) =>
          match goal with
            |- ~ _ => let x := fresh in
                     (intros x; case name;
                      generalize x; clear x name;
                      intro name)
          | |- _ => case name; clear name
          end
     | _ =>
          match goal with
            |- ~ _ => let x := fresh in
                    (intros x; absurd term;
                       [idtac | exact name]; generalize x; clear x name;
                       intros name)
          | |- _ => generalize name; absurd term;
                       [idtac | exact name]; clear name
          end
     end).


Ltac case_eq name :=
  generalize (refl_equal name); pattern name at -1 in |- *; case name.


Ltac eq_tac :=
 match goal with
      |- (?g _ = ?g _) => apply f_equal with (f := g)
 | |- (?g ?X _ = ?g ?X _) => apply f_equal with (f := g X)
 | |- (?g _ _ = ?g _ _) => apply f_equal2 with (f := g)
 | |- (?g ?X ?Y _ = ?g ?X ?Y _) => apply f_equal with (f := g X Y)
 | |- (?g ?X _ _ = ?g ?X _ _) => apply f_equal2 with (f := g X)
 | |- (?g _ _ _ = ?g _ _ _) => apply f_equal3 with (f := g)
 | |- (?g ?X ?Y ?Z _ = ?g ?X ?Y ?Z _) => apply f_equal with (f := g X Y Z)
 | |- (?g ?X ?Y _ _ = ?g ?X ?Y _ _) => apply f_equal2 with (f := g X Y)
 | |- (?g ?X _ _ _ = ?g ?X _ _ _) => apply f_equal3 with (f := g X)
 | |- (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g)
 end.


Ltac sauto := (intros; apply sym_equal; auto; fail) || auto.