From Undecidability.L Require Export Util.L_facts.
From Undecidability.L.Tactics Require Import Lproc Lbeta Lrewrite Reflection mixedTactics.
Require Import ListTactics.
Import L_Notations.
Local Ltac wLsimpl' _n := intros;try reflexivity';try standardizeGoal _n ; try reflexivity'.
Local Ltac wLsimpl := wLsimpl' 100.
Ltac Lsimpl' :=
match goal with
| |- eval ?s _ => assert (lambda s) by Lproc;split;[ (exact (starR _ _);fail 1)|Lproc]
| |- eval ?s _ => (progress (eapply eval_helper;[Lsimpl';reflexivity|]))
| _ => try Lrewrite;try wLsimpl' 100
end.
Ltac Lreduce :=
repeat progress ( (Lrewrite;try Lbeta) || Lbeta).
Ltac Lsimpl_old :=intros;
once lazymatch goal with
| |- _ >(<= _ ) _ => Lreduce;try Lreflexivity
| |- _ ⇓(_ ) _ => repeat progress Lbeta;try Lreflexivity
| |- _ ⇓(<= _ ) _ => Lreduce;try Lreflexivity
| |- _ >(_) _ => repeat progress Lbeta;try Lreflexivity
| |- _ >* _ => Lreduce;try Lreflexivity
| |- eval _ _ => Lreduce;try Lreflexivity
| |- _ == _ => repeat Lsimpl';try reflexivity'
end.
Ltac Lsimpl :=
lazymatch goal with
| |- _ >( _ ) _ => Lsimpl_old
| |- _ => LrewriteSimpl
end.
Ltac LsimplHypo := standardizeHypo 100.
Tactic Notation "closedRewrite" :=
match goal with
| [ |- context[subst ?s _ _] ] =>
let cl := fresh "cl" in assert (cl:closed s);[Lproc|rewrite !cl;clear cl]
end.
Tactic Notation "closedRewrite" "in" hyp(h):=
match type of h with
| context[subst ?s _ _] =>
let cl := fresh "cl" in assert (cl:closed s);[Lproc|rewrite !cl in h;clear cl]
end.
Tactic Notation "redStep" "at" integer(pos) := rewrite step_Lproc at pos;[simpl;try closedRewrite|Lproc].
Tactic Notation "redStep" "in" hyp(h) "at" integer(pos) := rewrite step_Lproc in h at pos;[simpl in h;try closedRewrite in h|Lproc].
Tactic Notation "redStep" "in" hyp(h) := redStep in h at 1.
Lemma rho_correct s t : proc s -> lambda t -> rho s t >* s (rho s) t.
Proof.
intros. unfold rho,r. redStep at 1. apply star_trans_l. now Lsimpl.
Qed.
Lemma rho_correctPow s t : proc s -> lambda t -> rho s t >(3) s (rho s) t.
Proof.
intros. unfold rho,r. change 3 with (1+2). apply pow_add.
eexists;split. apply (rcomp_1 step). now inv H0.
cbn. closedRewrite. apply pow_step_congL;[|reflexivity]. now Lbeta.
Qed.
Lemma rho_inj s t: rho s = rho t -> s = t.
Proof.
unfold rho,r. congruence.
Qed.
Hint Resolve rho_lambda rho_cls : LProc.
Tactic Notation "recStep" constr(P) "at" integer(i):=
match eval lazy [P] in P with
| rho ?rP => unfold P;rewrite rho_correct at i;[|Lproc..];fold P;try unfold rP
end.
Tactic Notation "recStep" constr(P) :=
intros;recStep P at 1.
Lemma I_proc : proc I.
Proof.
fLproc.
Qed.
Lemma K_proc : proc K.
Proof.
fLproc.
Qed.
Lemma omega_proc : proc omega.
Proof.
fLproc.
Qed.
Lemma Omega_closed : closed Omega.
Proof.
fLproc.
Qed.
Hint Resolve I_proc K_proc omega_proc Omega_closed: LProc.
Hint Extern 0 (I >(_) _)=> unfold I;reflexivity : Lrewrite.
Hint Extern 0 (K >(_) _)=> unfold K;reflexivity : Lrewrite.
Lemma Omega_diverge t: ~ eval Omega t.
Proof.
intros (?&?). remember Omega as s eqn:HO. induction H;subst.
-inv H0. easy.
-unfold Omega in H. inv H. cbn in *. eauto. all:easy.
Qed.
From Undecidability.L.Tactics Require Import Lproc Lbeta Lrewrite Reflection mixedTactics.
Require Import ListTactics.
Import L_Notations.
Local Ltac wLsimpl' _n := intros;try reflexivity';try standardizeGoal _n ; try reflexivity'.
Local Ltac wLsimpl := wLsimpl' 100.
Ltac Lsimpl' :=
match goal with
| |- eval ?s _ => assert (lambda s) by Lproc;split;[ (exact (starR _ _);fail 1)|Lproc]
| |- eval ?s _ => (progress (eapply eval_helper;[Lsimpl';reflexivity|]))
| _ => try Lrewrite;try wLsimpl' 100
end.
Ltac Lreduce :=
repeat progress ( (Lrewrite;try Lbeta) || Lbeta).
Ltac Lsimpl_old :=intros;
once lazymatch goal with
| |- _ >(<= _ ) _ => Lreduce;try Lreflexivity
| |- _ ⇓(_ ) _ => repeat progress Lbeta;try Lreflexivity
| |- _ ⇓(<= _ ) _ => Lreduce;try Lreflexivity
| |- _ >(_) _ => repeat progress Lbeta;try Lreflexivity
| |- _ >* _ => Lreduce;try Lreflexivity
| |- eval _ _ => Lreduce;try Lreflexivity
| |- _ == _ => repeat Lsimpl';try reflexivity'
end.
Ltac Lsimpl :=
lazymatch goal with
| |- _ >( _ ) _ => Lsimpl_old
| |- _ => LrewriteSimpl
end.
Ltac LsimplHypo := standardizeHypo 100.
Tactic Notation "closedRewrite" :=
match goal with
| [ |- context[subst ?s _ _] ] =>
let cl := fresh "cl" in assert (cl:closed s);[Lproc|rewrite !cl;clear cl]
end.
Tactic Notation "closedRewrite" "in" hyp(h):=
match type of h with
| context[subst ?s _ _] =>
let cl := fresh "cl" in assert (cl:closed s);[Lproc|rewrite !cl in h;clear cl]
end.
Tactic Notation "redStep" "at" integer(pos) := rewrite step_Lproc at pos;[simpl;try closedRewrite|Lproc].
Tactic Notation "redStep" "in" hyp(h) "at" integer(pos) := rewrite step_Lproc in h at pos;[simpl in h;try closedRewrite in h|Lproc].
Tactic Notation "redStep" "in" hyp(h) := redStep in h at 1.
Lemma rho_correct s t : proc s -> lambda t -> rho s t >* s (rho s) t.
Proof.
intros. unfold rho,r. redStep at 1. apply star_trans_l. now Lsimpl.
Qed.
Lemma rho_correctPow s t : proc s -> lambda t -> rho s t >(3) s (rho s) t.
Proof.
intros. unfold rho,r. change 3 with (1+2). apply pow_add.
eexists;split. apply (rcomp_1 step). now inv H0.
cbn. closedRewrite. apply pow_step_congL;[|reflexivity]. now Lbeta.
Qed.
Lemma rho_inj s t: rho s = rho t -> s = t.
Proof.
unfold rho,r. congruence.
Qed.
Hint Resolve rho_lambda rho_cls : LProc.
Tactic Notation "recStep" constr(P) "at" integer(i):=
match eval lazy [P] in P with
| rho ?rP => unfold P;rewrite rho_correct at i;[|Lproc..];fold P;try unfold rP
end.
Tactic Notation "recStep" constr(P) :=
intros;recStep P at 1.
Lemma I_proc : proc I.
Proof.
fLproc.
Qed.
Lemma K_proc : proc K.
Proof.
fLproc.
Qed.
Lemma omega_proc : proc omega.
Proof.
fLproc.
Qed.
Lemma Omega_closed : closed Omega.
Proof.
fLproc.
Qed.
Hint Resolve I_proc K_proc omega_proc Omega_closed: LProc.
Hint Extern 0 (I >(_) _)=> unfold I;reflexivity : Lrewrite.
Hint Extern 0 (K >(_) _)=> unfold K;reflexivity : Lrewrite.
Lemma Omega_diverge t: ~ eval Omega t.
Proof.
intros (?&?). remember Omega as s eqn:HO. induction H;subst.
-inv H0. easy.
-unfold Omega in H. inv H. cbn in *. eauto. all:easy.
Qed.