# Library SKvTactics

Require Import L SKv.

Lemma proc_closed p : proc p L.closed p.

Lemma proc_lambda p : proc p lambda p.

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.

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.