Library CoLoR.Term.Lambda.LEta

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

Eta-reduction


Set Implicit Arguments.


Definition of eta-top-reduction.

Section eta_top.

  Variables F X : Type.

  Notation Te := (@Te F X).

  Variable ens_X : Ens X.

  Notation In := (@Ens_In X ens_X).
  Notation fv := (@fv F X ens_X).
  Notation Var := (@Var F X).

  Inductive eta_top : relation Te :=
  | eta_top_intro : forall x u,
      ~In x (fv u) -> eta_top (Lam x (App u (Var x))) u.

End eta_top.

Properties of eta-reduction.


Module Make (Export L : L_Struct).

  Module Export A := LAlpha.Make L.

  Notation In := (@Ens_In X ens_X).

  Notation eta_top := (@eta_top F X ens_X).
  Infix "->eh" := eta_top (at level 70).

  Notation eta := (clos_mon eta_top).
  Infix "->e" := (clos_mon eta_top) (at level 70).

  Notation eta_aeq := (clos_aeq eta).
  Infix "=>e" := (clos_aeq eta) (at level 70).

Eta-reduction do not create free variables.

  Instance fv_eta_top_Equal : Proper (eta_top ==> Equal) fv.


  Instance fv_eta_top : Proper (eta_top --> Subset) fv.


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

  Lemma var_eta_aeq_l x u : ~Var x =>e u.

  Lemma fun_eta_aeq_l f u : ~Fun f =>e u.

  Lemma lam_eta_aeq_l x u v : Lam x u =>e v ->
    (exists v', u = App v' (Var x) /\ ~In x (fv v') /\ v' ~~ v)
    \/ (exists y w, v = Lam y w /\ (x=y \/ ~In y (fv u)) /\ u =>e rename y x w).

  Lemma app_eta_aeq_l u v w : App u v =>e w -> exists u' v',
    w = App u' v' /\ ((u =>e u' /\ v ~~ v') \/ (u ~~ u' /\ v =>e v')).

Inversion tactic for eta-reduction.

  Ltac inv_eta_aeq h :=
    match type of h with
      | Var _ =>e _ => apply var_eta_aeq_l in h; tauto
      | Fun _ =>e _ => apply fun_eta_aeq_l in h; tauto
      | App _ _ =>e _ =>
        let u := fresh "u" in let v := fresh "v" in let e := fresh "e" in
        let h1 := fresh "h" in let h2 := fresh "h" in
          destruct (app_eta_aeq_l h) as [u [v [e [[h1 h2]|[h1 h2]]]]]
| Lam _ _ =>e _ =>
        let y := fresh "x" in let v := fresh "v" in
        let h1 := fresh "h" in let h2 := fresh "h" in let h3 := fresh "h" in
          destruct (lam_eta_aeq_l h)
          as [[v [h1 [h2 h3]]]|[[y [v [h1 [h2 h3]]]]]]
| _ =>e _ => 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.

If apps u us eta-reduces to t, then t is of the form apps v vs with Vcons u us ==>b Vcons v vs.

  Infix "-->e" := (Vrel1 eta) (at level 70).
  Infix "==>e" := (clos_vaeq eta) (at level 70).

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


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


  Lemma eta_aeq_apps_fun f n (us : Tes n) t : apps (Fun f) us =>e t ->
    exists vs, t = apps (Fun f) vs /\ us ==>e vs.


End Make.