Library CoLoR.Term.Lambda.LBeta

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2012-04-05

Beta-reduction


Set Implicit Arguments.


Definition of beta-top-reduction.

Section beta_top.

  Variables F X : Type.

  Notation Te := (@Te F X).

  Variable eq_fun_dec : forall f g : F, {f=g}+{~f=g}.
  Variable eq_var_dec : forall x y : X, {x=y}+{~x=y}.

  Notation eq_term_dec := (@eq_term_dec F X eq_fun_dec eq_var_dec).
  Notation beq_term := (bool_of_rel eq_term_dec).

  Variable ens_X : Ens X.

  Notation fv := (@fv F X ens_X).

  Variable var_notin : Ens_type ens_X -> X.

  Notation single := (@single F X eq_var_dec).
  Notation subs := (@subs F X eq_fun_dec eq_var_dec ens_X var_notin).

  Inductive beta_top : relation Te :=
  | beta_top_intro : forall x u v,
    beta_top (App (Lam x u) v) (subs (single x v) u).

End beta_top.

Properties of beta-reduction.


Module Make (Export L : L_Struct).

  Module Export A := LAlpha.Make L.

  Notation beta_top := (@beta_top F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Infix "->bh" := beta_top (at level 70).

  Notation beta := (clos_mon beta_top).
  Infix "->b" := (clos_mon beta_top) (at level 70).

Note that, because subs may rename some bound variables, ->b cannot be stable by substitution, syntactically. We therefore define beta-reduction =>b as the closure by alpha-equivalence of ->b.

  Notation beta_aeq := (clos_aeq beta).
  Infix "=>b" := (clos_aeq beta) (at level 70).

Beta-reduction is stable by substitution.
Inversion lemmas for beta-reduction.

  Lemma var_beta_aeq_l x u : ~Var x =>b u.

  Lemma fun_beta_aeq_l f u : ~Fun f =>b u.

  Lemma lam_beta_aeq_l x u v :
    Lam x u =>b v -> exists y w, v = Lam y w /\ u =>b rename y x w.

  Lemma app_beta_aeq_l u v w : App u v =>b w ->
    (exists u', w ~~ App u' v /\ u =>b u')
    \/ (exists v', w ~~ App u v' /\ v =>b v')
    \/ (exists x, exists a, u = Lam x a /\ w ~~ subs (single x v) a).

Inversion tactic for beta-reduction.

  Ltac inv_beta_aeq h :=
    match type of h with
      | Var _ =>b _ => apply var_beta_aeq_l in h; tauto
      | Fun _ =>b _ => apply fun_beta_aeq_l in h; tauto
      | App _ _ =>b _ => let x := fresh "x" in let u := fresh "u" in
        let h1 := fresh "h" in let h2 := fresh "h" in
          destruct (app_beta_aeq_l h)
            as [[u [h1 h2]]|[[u [h1 h2]]|[x [u [h1 h2]]]]]
| Lam _ _ =>b _ => let x := fresh "x" in let u := fresh "u" in
        let h1 := fresh "h" in let h2 := fresh "h" in
          destruct (lam_beta_aeq_l h) as [x [u [h1 h2]]]
| _ =>b _ => let u := fresh "u" in let v := fresh "v" in
        let h1 := fresh "h" in let h2 := fresh "h" in let h3 := fresh "h" in
          destruct h as [u [h1 [v [h2 h3]]]]
end.

Beta-reduction do not create free variables.

  Instance fv_beta_top : Proper (beta_top --> Subset) fv.


If apps u us beta-reduces to t and u is not an abstraction, then t is of the form apps v vs with Vcons u us ==>b Vcons v vs.

  Infix "-->b" := (Vrel1 beta) (at level 70).
  Infix "==>b" := (clos_vaeq beta) (at level 70).

  Lemma beta_apps_no_lam : forall n (us : Tes n) u t,
    not_lam u -> apps u us ->b t ->
    exists v vs, t = apps v vs /\ Vcons u us -->b Vcons v vs.


  Lemma beta_aeq_apps_no_lam : forall n (us : Tes n) u t,
    not_lam u -> apps u us =>b t ->
    exists v vs, t = apps v vs /\ clos_vaeq beta (Vcons u us) (Vcons v vs).


  Lemma beta_aeq_apps_fun f n (us : Tes n) t : apps (Fun f) us =>b t ->
    exists vs, t = apps (Fun f) vs /\ clos_vaeq beta us vs.


apps (Fun f) us is strongly normalizing wrt beta-reduction if every element of us is strongly normalizing wrt beta-reduction.

  Lemma sn_beta_apps_fun f n (us : Tes n) :
    Vforall (SN beta_aeq) us -> SN beta_aeq (apps (Fun f) us).

End Make.