Library CoLoR.Term.Lambda.LComp

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

Tait and Girard computability


Set Implicit Arguments.


Computability predicates.


Section cp.

  Variables F X : Type.

  Notation Te := (@Te F X).

  Variables (aeq R_aeq : relation Te) (neutral : set Te).

  Infix "=>R" := R_aeq (at level 70).

A computability predicate must be compatible with alpha-equivalence.

  Notation cp_aeq := (Proper (aeq ==> impl)) (only parsing).

A computability predicate contains strongly normalizing terms.

  Definition cp_sn (P : set Te) := forall u, P u -> SN R_aeq u.

A computability predicate is stable by reduction.

  Definition cp_red (P : set Te) := Proper (R_aeq ==> impl) P.

A computability predicate containing all the reducts of a neutral term u contains u too.

  Definition cp_neutral (P : set Te) :=
    forall u, neutral u -> (forall v, u =>R v -> P v) -> P u.

A computability predicate is a predicate satisfying the four conditions above.

  Class cp P := {
    cp1 : cp_aeq P;
    cp2 : cp_sn P;
    cp3 : cp_red P;
    cp4 : cp_neutral P }.

Interpretation of arrow types.

  Definition arr (P Q : set Te) : set Te :=
    fun u => forall v, P v -> Q (App u v).

End cp.

Structure on which we will define computability predicates.


Module Type CP_Struct.

  Declare Module Export L : L_Struct.

  Notation subs := (@subs F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation aeq := (@aeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation clos_aeq := (@clos_aeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation clos_vaeq :=
    (@clos_vaeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation beta_top := (@beta_top F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation eta_top := (@eta_top F X ens_X).

  Infix "->bh" := beta_top (at level 70).
  Infix "->eh" := eta_top (at level 70).

We assume given a relation ->Rh and a predicate neutral.

  Parameter Rh : relation Te.
  Infix "->Rh" := Rh (at level 70).

  Parameter neutral : set Te.

We then denote by ->R the monotone closure of ->Rh and by =>R the closure by alpha-equivalence of ->R.

  Notation R := (clos_mon Rh).
  Infix "->R" := (clos_mon Rh) (at level 70).

  Notation R_aeq := (clos_aeq R).
  Infix "=>R" := (clos_aeq R) (at level 70).

  Infix "==>R" := (clos_vaeq R) (at level 70).

Properties not involving reduction.

  Declare Instance neutral_aeq : Proper (aeq ==> impl) neutral.
  Parameter neutral_var : forall x, neutral (Var x).
  Parameter neutral_app : forall u v, neutral u -> neutral (App u v).
  Parameter not_neutral_lam : forall x u, ~neutral (Lam x u).
  Parameter neutral_beta : forall x u v, neutral (App (Lam x u) v).

Properties involving reduction.

  Declare Instance subs_R_aeq : Proper (Logic.eq ==> R_aeq ==> R_aeq) subs.
  Declare Instance fv_Rh : Proper (Rh --> Subset) fv.
  Parameter not_Rh_var : forall x u, ~ Var x ->Rh u.
  Parameter Rh_eh : forall x u w, Lam x u ->Rh w -> Lam x u ->eh w.
  Parameter Rh_bh : forall x u v w,
    App (Lam x u) v ->Rh w -> App (Lam x u) v ->bh w.
  Parameter not_Rh_app_neutral : forall u v w, neutral u -> ~ App u v ->Rh w.

Some notations.

  Notation cp_aeq := (Proper (aeq ==> impl)) (only parsing).
  Notation cp_sn := (@cp_sn F X R_aeq).
  Notation cp_red := (@cp_red F X R_aeq).
  Notation cp_neutral := (@cp_neutral F X R_aeq neutral).
  Notation cp := (@cp F X aeq R_aeq neutral).

End CP_Struct.

CP structure for beta-reduction alone.


Module CP_beta_eta (Import L : L_Struct) <: CP_Struct.

  Module L := L.

  Module Import B := LBeta.Make L.
  Module Import E := LEta.Make L.

  Definition Rh := beta_top U eta_top.
  Infix "->Rh" := Rh (at level 70).

  Notation R := (clos_mon Rh).
  Infix "->R" := (clos_mon Rh) (at level 70).

  Notation R_aeq := (clos_aeq R).
  Infix "=>R" := (clos_aeq R) (at level 70).

  Lemma R_aeq_alt : R_aeq == beta_aeq U eta_aeq.

A term is neutral if it is not a Lam.

  Definition neutral (u : Te) :=
    match u with
      | Def.Lam _ _ => False
      | _ => True
    end.

CP structure properties not involving reduction.

  Instance neutral_aeq : Proper (aeq ==> impl) neutral.


  Lemma neutral_var x : neutral (Var x).

  Lemma neutral_app u v : neutral u -> neutral (App u v).

  Lemma not_neutral_lam x u : ~neutral (Lam x u).

  Lemma neutral_beta x u v : neutral (App (Lam x u) v).

CP structure properties involving reduction.

  Instance subs_R_aeq : Proper (Logic.eq ==> R_aeq ==> R_aeq) subs.


  Lemma not_Rh_var x u : ~ Var x ->Rh u.

  Lemma Rh_eh x u w : Lam x u ->Rh w -> Lam x u ->eh w.

  Lemma Rh_bh x u v w : App (Lam x u) v ->Rh w -> App (Lam x u) v ->bh w.

  Lemma not_Rh_app_neutral u v w : neutral u -> ~ App u v ->Rh w.

  Instance fv_Rh : Proper (Rh --> Subset) fv.


Some notations.

  Notation cp_aeq := (Proper (aeq ==> impl)) (only parsing).
  Notation cp_sn := (@cp_sn F X R_aeq).
  Notation cp_red := (@cp_red F X R_aeq).
  Notation cp_neutral := (@cp_neutral F X R_aeq neutral).
  Notation cp := (@cp F X aeq R_aeq neutral).

Extra properties.

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


End CP_beta_eta.

Properties of CP structures.


Module Make (Export CP : CP_Struct).

  Notation arr := (@arr F X).

  Module Export B := LBeta.Make L.
  Module Export E := LEta.Make L.

Properties of R_aeq.

Variables are irreducible.

  Lemma not_R_var x u : ~ Var x ->R u.

  Lemma not_R_aeq_var x u : ~ Var x =>R u.

A reduct of an abstraction is either a top-eta-reduct or an non-top-reduct.

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

App u v is not head-reducible if u is neutral.

  Lemma R_app_neutral u v w : neutral u -> App u v ->R w ->
      (exists u', w = App u' v /\ u ->R u')
      \/ (exists v', w = App u v' /\ v ->R v').

  Lemma R_aeq_app_neutral u v w : neutral u -> App u v =>R w ->
      (exists u', w ~~ App u' v /\ u =>R u')
      \/ (exists v', w ~~ App u v' /\ v =>R v').

Extension of properties from App to apps.

  Lemma neutral_apps : forall n (us : Tes n) u,
      neutral u -> neutral (apps u us).

  Lemma neutral_apps_var x n (us : Tes n) : neutral (apps (Var x) us).

  Lemma R_aeq_apps_neutral : forall n (us : Tes n) u v, neutral u ->
    apps u us =>R v -> (exists u', v ~~ apps u' us /\ u =>R u')
    \/ (exists us', v ~~ apps u us' /\ Vrel1 R_aeq us us').


Alpha-transitive closure of =>R.

  Infix "=>R*" := (R_aeq*) (at level 70).

  Notation satc := (subs_rel (R_aeq*)).

  Lemma subs_satc u s s' : satc (fv u) s s' -> subs s u =>R* subs s' u.

Properties of SN R_aeq.

SN R_aeq is a computability predicate.

  Lemma cp_sn_SN : cp_sn (SN R_aeq).

  Lemma cp_red_SN : cp_red (SN R_aeq).

  Lemma cp_neutral_SN : cp_neutral (SN R_aeq).

  Lemma cp_SN : cp (SN R_aeq).

If u is SN , then Lam x u is SN too.

  Lemma sn_lam x u : SN R_aeq u -> SN R_aeq (Lam x u).

Computability properties are invariant wrt =.


  Instance cp_aeq_equiv : Proper (equiv ==> impl) cp_aeq.


  Instance cp_sn_equiv : Proper (equiv ==> impl) cp_sn.


  Instance cp_red_equiv : Proper (equiv ==> impl) cp_red.


  Instance cp_neutral_equiv : Proper (equiv ==> impl) cp_neutral.


  Instance cp_equiv : Proper (equiv ==> impl) cp.


Properties of computability predicates wrt variables.

A computability predicate contains every strongly normalizing term of the form x t1 .. tn.

  Lemma cp_var_app_sn : forall P, cp_aeq P -> cp_neutral P ->
    forall x n (us : Tes n), Vforall (SN R_aeq) us -> P (apps (Var x) us).

  Lemma cp_var : forall P, cp_aeq P -> cp_neutral P -> forall x, P (Var x).

Properties of arr.

Monotony properties of arr.
arr preserves cp_aeq.

  Instance cp_aeq_arr : forall P Q, cp_aeq Q -> cp_aeq (arr P Q).


arr preserves cp_sn.

  Lemma cp_sn_arr : forall P Q, cp_aeq P -> cp_sn P -> cp_neutral P ->
    cp_sn Q -> cp_sn (arr P Q).

arr preserves cp_red.

  Lemma cp_red_arr : forall P Q, cp_red Q -> cp_red (arr P Q).

arr preserves cp_neutral.

  Lemma cp_neutral_arr : forall P Q, cp_sn P -> cp_red P ->
    cp_aeq Q -> cp_neutral Q -> cp_neutral (arr P Q).

arr preserves cp.

  Lemma cp_arr : forall P Q, cp P -> cp Q -> cp (arr P Q).

Computability of an application.


  Lemma cp_app P Q : cp_aeq P -> cp_red P -> cp_sn P ->
                     cp_aeq Q -> cp_red Q -> cp_neutral Q ->
    forall t, (neutral t \/ exists x u, t = Lam x u) ->
              (forall t', t =>R t' -> arr P Q t') ->
              forall v, P v ->
                        (forall x u, t = Lam x u -> Q (subs (single x v) u)) ->
                        Q (App t v).

Computability of an abstraction.


  Lemma cp_lam P Q : cp_aeq P -> cp_red P -> cp_sn P -> cp_neutral P ->
                     cp_aeq Q -> cp_red Q -> cp_sn Q -> cp_neutral Q ->
    forall x u, (forall v, P v -> Q (subs (single x v) u)) ->
                arr P Q (Lam x u).

End Make.