# Library Tactics

Require Export Lvw.

# Tactics for closedness and abstractions

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.

# Simplifying goals

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.

# Solving reductions

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.

# Solving equivalences

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.