Library SKvTactics

Require Import L SKv.

Lemma proc_closed p : proc p → L.closed p.
Proof.
  firstorder intuition.
Qed.

Lemma proc_lambda p : proc p → lambda p.
Proof.
  firstorder intuition.
Qed.

Hint Resolve proc_closed proc_lambda : value.

Ltac fvalue :=intros;
  match goal with
    | [ |- proc _ ] ⇒ split;try fvalue
    | [ |- lambda _ ] ⇒ eexists; reflexivity
    | [ |- L.closed _ ] ⇒ vm_compute; reflexivity
  end.

Ltac value_lam' :=
  match goal with
    | |- lambda (match ?c with _ ⇒ _ end) ⇒ destruct c
    | |- lambda _ ⇒ tauto || (eexists;reflexivity) || auto with LProc
  end.

Ltac dvalue' :=
  match goal with
    | |- dclosed _ (L.app _ _) ⇒ constructor
    | |- dclosed _ (match ?c with _ ⇒ _ end) ⇒ destruct c
    | |- dclosed _ (L.lam _) ⇒ constructor
    | |- dclosed _ (L.var _) ⇒ solve [constructor;omega]
    | _ ⇒ assumption
  end.

Ltac dvalue := rewrite closed_dcl;repeat dvalue'.
Ltac value := auto 15 with value.
Hint Extern 8 (L.closed _) ⇒ dvalue : value.
Hint Extern 1 (lambda _) ⇒ value_lam' : value.

Lemma closed_dcl_x x s: L.closed s → dclosed x s.
Proof.
  intros. apply (@dclosed_ge 0). now apply closed_dcl. omega.
Qed.

Hint Extern 0 (dclosed _ _) ⇒ apply closed_dcl_x : value.

Ltac mp H :=
  let t := fresh "temp" in
  match type of H with
      ((?P) → _) ⇒ assert (t:P);[|specialize (H t);clear t]
  end.

Ltac sktopen s := unfold s.

Ltac sktstep :=
  match goal with
    | [ |- (app I _) >>> _] ⇒ unfold I at 1;sktstep
    | [ |- (app _ _) >>> _] ⇒ (now apply stepAppL;repeat sktstep)||(now apply stepAppR;repeat sktstep)
    | [ |- (app (app K _) _) >>> _ ] ⇒ now (apply stepK;value)
    | [ |- (app (app (app S _) _) _) >>> _ ] ⇒ now (apply stepS;value)
    | [ |- (app ?s _) >>> _ ] ⇒ sktopen s
    | [ |- (app (app ?s _) _) >>> _ ] ⇒ sktopen s
    | [ |- _ >>> _] ⇒ apply stepAppL || fail 2
  end.

Ltac skreduce :=
  match goal with
    | [ |- _ >>* _ ] ⇒ eapply starC;[now repeat sktstep|]
    | [ |- _ === _ ] ⇒ eapply eqTrans;[((now apply eqStep;repeat sktstep)||reflexivity)|];symmetry;eapply eqTrans;[((now apply eqStep;repeat sktstep)||reflexivity)|];symmetry
  end.

Ltac skreduction := (try now reflexivity); skreduce.

Ltac skCrush := repeat skreduction.