Lvc.Infra.AutoIndTac

Ltac revert_except E :=
  repeat match goal with
           [H : _ |- _] ⇒
           match H with
             | E ⇒ fail 1
             | _ ⇒ revert H
               end
         end.

Ltac clear_except E :=
  repeat match goal with
           [H : _ |- _] ⇒
           match H with
             | E ⇒ fail
             | _ ⇒ clear H
               end
         end.

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

Ltac revert_all :=
  repeat match goal with
           [H : _ |- _] ⇒ revert H
         end.


Ltac remember_arguments E :=
  let tac x := (try (is_var x; fail 1); remember (x)) in
  repeat (match type of E with
    | ?t ?x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ _ ⇒ tac x
    | ?t ?x _ _ _ ⇒ tac x
    | ?t ?x _ _ ⇒ tac x
    | ?t ?x _ ⇒ tac x
    | ?t ?x ⇒ tac x
  end).

Ltac clear_dup :=
  match goal with
    | [ H : ?X |- _ ] ⇒
      match goal with
        | [ H´ : ?Y |- _ ] ⇒
          match H with
            | H´ ⇒ fail 2
            | _ ⇒ unify X Y ; (clear H´ || clear H)
          end
      end
  end.

Ltac inv_eqs :=
  repeat (match goal with
              | [ H : @eq _ ?x ?x |- _ ] ⇒ fail
              | [ H : @eq _ ?x ?y |- _ ] ⇒ progress (inversion H; subst; try clear_dup)
            end).

Ltac clear_trivial_eqs :=
  repeat (progress (match goal with
              | [ H : @eq _ ?x ?x |- _ ] ⇒ clear H
            end)).

Tactic Notation "general" "induction" hyp(H) :=
  remember_arguments H; revert_except H;
  induction H; intros; (try inv_eqs); (try clear_trivial_eqs).

Module Test.
Require Import List.

Inductive decreasing : list nat → Prop :=
  | base : decreasing nil
  | step m n L : decreasing (n::L) → n ≤ m → decreasing (m :: n :: L).

Lemma all_zero_by_hand L
  : decreasing (0::L) → ∀ x, In x L → x = 0.

Lemma all_zero L
  : decreasing (0::L) → ∀ x, In x L → x = 0.
End Test.