Library LambdaJ_Rules
Set Implicit Arguments.
Require Import Metatheory LambdaES_Defs LambdaES_Infrastructure.
Require Import Rewriting_defs LambdaJ_ndr LambdaES_occ.
Rule B
Inductive B_red : pterm -> pterm -> Prop :=
| rule_B : forall t s, body t -> term s -> B_red (pterm_app (pterm_abs t) s) (t[s]).
Notation "t ->B u" := (B_red t u) (at level 66).
| rule_B : forall t s, body t -> term s -> B_red (pterm_app (pterm_abs t) s) (t[s]).
Notation "t ->B u" := (B_red t u) (at level 66).
Contextual closure of the rule B
Definition B_ctxt_red t u := (contextual_closure B_red) t u.
Notation "t -->B u" := (B_ctxt_red t u) (at level 66).
Notation "t -->B u" := (B_ctxt_red t u) (at level 66).
Rules j
Inductive j_red : pterm -> pterm -> Prop :=
| rule_w : forall t s, body t -> term s -> bv_occ t = 0 -> j_red (t[s]) t
| rule_d: forall t s, body t-> term s -> bv_occ t = 1 -> j_red (t[s]) (t^^s)
| rule_c : forall t s x y t', body t -> term s ->
bv_occ t >= 2 ->
x \notin fv t ->
y \notin fv t ->
ndr (t^x) x y t' ->
j_red (t[s]) ((close ((close t' x)[s]) y) [s]).
Notation "t ->j u" := (j_red t u) (at level 66).
| rule_w : forall t s, body t -> term s -> bv_occ t = 0 -> j_red (t[s]) t
| rule_d: forall t s, body t-> term s -> bv_occ t = 1 -> j_red (t[s]) (t^^s)
| rule_c : forall t s x y t', body t -> term s ->
bv_occ t >= 2 ->
x \notin fv t ->
y \notin fv t ->
ndr (t^x) x y t' ->
j_red (t[s]) ((close ((close t' x)[s]) y) [s]).
Notation "t ->j u" := (j_red t u) (at level 66).
Contextual closure of the rules j
Definition j_ctxt_red t u := (contextual_closure j_red) t u.
Notation "t -->j u" := (j_ctxt_red t u) (at level 66).
Notation "t -->j u" := (j_ctxt_red t u) (at level 66).
Transitive closure of (the contextual closure) of j
Definition j_full_reduction t u := star_closure (contextual_closure j_red) t u.
Notation "t -->j* u" := (j_full_reduction t u) (at level 66).
Notation "t -->j* u" := (j_full_reduction t u) (at level 66).
After a -->B reduction, we still have a locally closed term
Lemma preservation_terms_after_B : forall t t', term t -> t -->B t' -> term t'.
Proof. intros t t' term_t red. induction red ; solve [inversion* H |inversion* term_t]. Qed.
Proof. intros t t' term_t red. induction red ; solve [inversion* H |inversion* term_t]. Qed.
After a ->j reduction, we still have a locally closed term
Lemma preservation_terms_after_j : forall t t', term t -> t -->j t' -> term t'.
Proof.
intros t t' term_t red. induction red ; try (now inversion* term_t).
inversion* H ; subst ; inversion* H ; subst ; term_solver.
Qed.
Proof.
intros t t' term_t red. induction red ; try (now inversion* term_t).
inversion* H ; subst ; inversion* H ; subst ; term_solver.
Qed.
Induction scheme for nat, useful for the lambda_j reduction cases