Tactics_old
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_old := try match goal with
| [ |- proc _ ] => try eassumption; eauto with cbv; split; value_old
| [ |- lambda _ ] => try eassumption; eauto with cbv; eexists; reflexivity
| [ |- closed _ ] => try eassumption; eauto with cbv; intros k' r'; simpl; repeat rewrite_closed; autorewrite with cbv;auto; reflexivity
end.
Ltac value2_old := match goal with
| [ |- proc _ ] => try (( try eassumption); eauto with cbv; split; value2_old); 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; auto;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.
(* This is needed, since empty rewriting databases may raise errors *)
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_old)) || reduction'.
Ltac reduction := rewrite_equiv || reduction'.
Ltac crushE S := stepsimpl; repeat (reductionE S).
Ltac old_crush := stepsimpl; repeat reduction.