Library sflib

Useful tactics and notations.

Some interesting parts of SfLib.v from https://www.cis.upenn.edu/~bcpierce/sf/current/SfLib.v

Require Export Omega.
Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ ⇒ try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

Add Search Blacklist "_ind".
Add Search Blacklist "_rect".
Add Search Blacklist "_rec".
Add Search Blacklist "_equation".
Add Search Blacklist "R_".

Ltac decompose_ex H :=
  repeat match type of H with
           | ex (fun x ⇒ _) ⇒
             destruct H as [?x H]
         end.