Library LambdaJ_Rules


Set Implicit Arguments.
Require Import Metatheory LambdaES_Defs LambdaES_Infrastructure.
Require Import Rewriting_defs LambdaJ_ndr LambdaES_occ.

Rules of lambda j


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).

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).

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).

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).

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).

Lemmas

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.

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.

Induction scheme for nat, useful for the lambda_j reduction cases
Lemma nat_ind_lambda_j : forall (P : nat -> Prop), P(0) -> P(1)
    -> (forall n m, n > 0 -> m > 0 -> P(n) -> P(m) -> P(m+n))
    -> forall n, P(n).
Proof.
  intros P H0 H1 Hn n. induction n.
    assumption.
    case_eq n ; intros ; subst.
      assumption.
      apply (Hn (S n0) 1) ; auto. omega.
Qed.