Library LambdaES_Tactics


Require Import LambdaES_Defs.

Ltac elim_zero_one :=
match goal with
| H : 0 = 1 |- _ =>
  let Hfresh := fresh H in
  assert (0 = 1 -> False) as Hfresh by omega ; elim Hfresh ; auto
| H : 1 = 0 |- _ =>
  let Hfresh := fresh H in
  assert (1 = 0 -> False) as Hfresh by omega ; elim Hfresh ; auto
| H : 1 = 0 |- _ =>
  let Hfresh := fresh H in
  assert (1 = 0 -> False) as Hfresh by omega ; elim Hfresh ; auto
end.

Ltac stupid_arith :=
match goal with
| H : 0 = 1 |- _ =>
  let Hfresh := fresh H in
  let T := type of H in
  assert (T -> False) as Hfresh by omega ; elim Hfresh ; auto
end.

Ltac elim_stupid H :=
  let typeH := type of H in
  let Hfresh := fresh H in
  try (assert (typeH -> False) as Hfresh by (try omega ; intuition) ; elim Hfresh ; assumption).

Ltac stupid_hyp :=
match goal with
| H : _ |- _ => elim_stupid H
end.

Performs an induction on the term t and basic test to solve the cases
Ltac easy_pterm_induction t Prefix Tac :=
  match (type of t) with
  | pterm => induction t as [| |? IHt|? IHt1 ? IHt2|? IHt1 ? IHt2] ;
      intros ; simpl ; try (Prefix ; solve[
            stupid_hyp
          | reflexivity
          | try rewrite IHt ; auto ; try omega
          | try rewrite IHt1 ; try rewrite IHt2 ; auto ; try omega
          | try rewrite <-IHt ; auto ; try omega
          | try rewrite <-IHt1 ; try rewrite <-IHt2 ; auto ; try omega
          | Tac
        ])
  end.

Notations to call easy_pterm_induction with prefixing or special tactic options
Tactic Notation "basic_pterm_induction" constr(t) "using" tactic(T) :=
easy_pterm_induction t idtac T.
Tactic Notation "basic_pterm_induction" constr(t) :=
easy_pterm_induction t idtac idtac.
Tactic Notation "basic_pterm_induction" constr(t) "prefixed_by" tactic(Prefix):=
easy_pterm_induction t Prefix idtac.
Tactic Notation "basic_pterm_induction" constr(t) "prefixed_by" tactic(Prefix) "using" tactic(T):=
easy_pterm_induction t Prefix T.