Library Util

Require Import Coq.Setoids.Setoid List.

Set Implicit Arguments.
Unset Printing Records.

Tactic Notation "inv" hyp(H) := inversion H; subst.
Tactic Notation "inv" integer(H) := inversion H; subst.

Ltac invt ty :=
  match goal with
      | h: ty |- _ ⇒ inv h
      | h: ty _ |- _ ⇒ inv h
      | h: ty _ _ |- _ ⇒ inv h
      | h: ty _ _ _ |- _ ⇒ inv h
      | h: ty _ _ _ _ |- _ ⇒ inv h
      | h: ty _ _ _ _ _ |- _ ⇒ inv h
      | h: ty _ _ _ _ _ _ |- _ ⇒ inv h
      | h: ty _ _ _ _ _ _ _ |- _ ⇒ inv h
      | h: ty _ _ _ _ _ _ _ _ |- _ ⇒ inv h
      | h: ty _ _ _ _ _ _ _ _ _ |- _ ⇒ inv h
  end.

Ltac isabsurd :=
  try now (hnf; intros; match goal with
                 [ H : _ |- _ ] ⇒ exfalso; inversion H; try congruence
               end).

Lemma modus_ponens P Q
: P → (P → Q) → Q.
tauto.
Defined.

Ltac exploit H :=
  eapply modus_ponens;
  [
    let H' := fresh "exploitH" in
    pose proof H as H'; hnf in H';
      eapply H'; clear H'
  | intros].

Tactic Notation "dcr" :=
  repeat (
      match goal with
      | H: _ |- _ ⇒ progress (decompose record H); clear H
      end).