# Library Tactics

Require Export Lvw.

Lemma proc_closed p : proc p -> closed p.

Proof.

firstorder intuition.

Qed.

Lemma proc_lambda p : proc p -> lambda p.

Proof.

firstorder intuition.

Qed.

Hint Resolve proc_closed proc_lambda : cbv.

Ltac rewrite_closed :=

match goal with

| H : proc _ |- _ => rewrite (proc_closed H)

| H : closed _ |- _ => rewrite H

end.

Ltac value := try match goal with

| [ |- proc _ ] => try eassumption; eauto with cbv; split; value

| [ |- lambda _ ] => try eassumption; eauto with cbv; eexists; reflexivity

| [ |- closed _ ] => try eassumption; eauto with cbv; intros k' r'; simpl; repeat rewrite_closed; autorewrite with cbv; reflexivity

end.

Ltac value2 := match goal with

| [ |- proc _ ] => try (( try eassumption); eauto with cbv; split; value2); fail

| [ |- lambda _ ] => try ((try eassumption); eauto with cbv; eexists; reflexivity); fail 1

| [ |- closed _ ] => try ( (try eassumption); eauto with cbv; intros k' r'; simpl; repeat rewrite_closed; autorewrite with cbv; reflexivity); fail 1

| [ |- _ ] => idtac

end.

Ltac stepsimpl_in A := cbv in A; autounfold with cbv in A; simpl in A; autorewrite with cbv in A.

Ltac stepsimpl := cbv; autounfold with cbv; simpl; autorewrite with cbv; repeat rewrite_closed.

Ltac tstep := stepsimpl;

match goal with

| [ |- step (app (lam _) (lam _) ) _ ] => eapply stepApp

| [ |- step (app (lam _) _ ) _ ] => (eapply step_value; try eassumption; now eauto with cbv) || eapply stepAppR

| [ |- step _ _ ] => eapply stepAppL

end.

Ltac reduce := repeat tstep; stepsimpl.

Lemma equiv_trans_r (s t t' : term) : t == t' -> s t == s t'.

Proof.

intros H; now rewrite H.

Qed.

Ltac rewrite_equiv :=

match goal with

| H : equiv ?s ?t |- _ => let H' := stepsimpl_in H in rewrite H

| H : star step ?s ?t |- _ => let H' := stepsimpl_in H in rewrite H

end.

Ltac reduction' :=

match goal with

| [ |- equiv (app ?s _) (app ?s _) ] => eapply eqRef || eapply equiv_trans_r

| [ |- equiv _ _ ] => eapply eqRef || (eapply eqTrans; [eapply eqStep; reduce|])

| [ |- star step (app ?s _) (app ?s _) ] => eapply starR || eapply star_trans_r

| [ |- star step _ _ ] => eapply starR || (eapply starC; reduce) end; stepsimpl.

Lemma database_dummy : I I I I I == I I I I I.

Proof.

reflexivity.

Qed.

Hint Rewrite database_dummy : cbv.

Ltac reductionE S := rewrite_equiv || (try (rewrite Eta with (s := S); value2)) || reduction'.

Ltac reduction := rewrite_equiv || reduction'.

Ltac crushE S := stepsimpl; repeat (reductionE S).

Ltac crush := stepsimpl; repeat reduction.