Library CoLoR.Term.Lambda.LCompSimple

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

Termination of beta-reduction for simply-typed lambda-terms


Set Implicit Arguments.


Interpretation of simple types as computability predicates.


Module Export Def.

  Section int.

    Variables F X So : Type.

    Notation Te := (@Te F X).

    Variable I : So -> set Te.

    Fixpoint int T :=
      match T with
        | Base b => I b
        | Arr A B => arr (int A) (int B)
      end.

Computability of vectors of terms.
vint is defined in such a way that as much types Ts as there are terms ts must be given, but Ts can contain more types than necessary (i.e. the length n of Ts can be bigger than the length p of ts). However, the result does not depend on these extras types.

    Notation Tes := (vector Te).
    Notation Ty := (@Ty So).
    Notation Tys := (vector Ty).

    Fixpoint vint {n} (Ts : Tys n) {p} (ts : Tes p) :=
      match Ts, ts with
        | _, Vnil => True
        | Vcons T Ts', Vcons t ts' => int T t /\ vint Ts' ts'
        | _, _ => False
      end.


  End int.

End Def.

Functor providing a termination proof for any CP structure

assuming that every type constant is interpreted by a computability predicate, and every function symbol is computable.

Module Make (Export ST : ST_Struct)
  (Export CP : CP_Struct with Module L := ST.L).

  Module Export C := LComp.Make CP.
  Module Export T := LSimple.Make ST.

  Notation int := (@int F X So).
  Notation vint := (@vint F X So).

  Section int.

    Variables (I : So -> Te -> Prop) (cp_I : forall b, cp (I b)).

Properties of the interpretation of simple types


    Notation int := (int I).

    Lemma int_base b t : I b t <-> int (Base b) t.

The interpretation of a type is a computability predicate.

    Global Instance cp_int : forall T, cp (int T).


    Global Instance int_aeq : Proper (Logic.eq ==> aeq ==> impl) int.


    Lemma int_sn : forall T t, int T t -> SN R_aeq t.

    Lemma int_var : forall T x, int T (Var x).

A substitution is valid wrt an environment E if, for every mapping (x,T) in E, s x is in the interpretation of T.

    Definition valid E s := forall x T, MapsTo x T E -> int T (s x).

    Lemma valid_id : forall E, valid E id.

Termination proof assuming that function symbols are computable.


    Variable comp_fun : forall f, int (typ f) (Fun f).

    Lemma tr_int : forall v E V, E |- v ~: V ->
      forall s, valid E s -> int V (subs s v).

    Lemma tr_sn : forall E v V, E |- v ~: V -> SN R_aeq v.

Properties of vint.


    Notation vint := (vint I).

Basic properties of vint.

    Lemma vint_le : forall n (Ts : Tys n) p (ts : Tes p),
      vint Ts ts -> p <= n.


    Lemma vint_le' : forall n (Ts : Tys n) p (ts : Tes p),
      vint Ts ts -> 0+p <= n.

    Lemma vint_typs_eq : forall n (Ts Us : Tys n) p (ts : Tes p),
      vint Us ts -> Us = Ts -> vint Ts ts.

    Lemma vint_typs_eq_cast : forall n (Ts : Tys n) m (Us : Tys m)
      (h : n=m) p (ts : Tes p), vint Us ts -> Us = Vcast Ts h -> vint Ts ts.

    Lemma vint_elim_nth : forall n (Ts : Tys n) p (ts : Tes p),
      vint Ts ts ->
      forall j (jn : j<n) (jp : j<p), int (Vnth Ts jn) (Vnth ts jp).

    Lemma vint_intro_nth : forall n (Ts : Tys n) p (ts : Tes p), p <= n ->
      (forall j (jn : j<n) (jp : j<p), int (Vnth Ts jn) (Vnth ts jp))
      -> vint Ts ts.

    Lemma vint_eq : forall n (Ts : Tys n) p (ts : Tes p), p <= n ->
      (vint Ts ts
        <-> (forall j (jn : j<n) (jp : j<p), int (Vnth Ts jn) (Vnth ts jp))).

    Lemma vint_sub_intro : forall n (Ts : Tys n) p (ts : Tes p),
      vint Ts ts -> forall i k (h : i+k<=n) k' (h' : i+k'<= p), k'<=k ->
        vint (Vsub Ts h) (Vsub ts h').

    Lemma vint_sub_typ_elim : forall n (Ts : Tys n) p (ts : Tes p) (h : 0+p<=n),
      vint (Vsub Ts h) ts -> vint Ts ts.

    Lemma vint_sub_typ_intro : forall n (Ts : Tys n) p (ts : Tes p)
      (h : 0+p<=n), vint Ts ts -> vint (Vsub Ts h) ts.

    Lemma vint_sub_term_intro : forall n (Ts : Tys n) p (ts : Tes p)
      q (h : 0+q<=p), vint Ts ts -> vint Ts (Vsub ts h).

    Lemma vint_cast_typ : forall n (Ts : Tys n) n' (h : n=n') p (ts : Tes p),
      vint (Vcast Ts h) ts <-> vint Ts ts.

    Lemma vint_cast_term : forall n (Ts : Tys n) p (ts : Tes p) p' (h : p=p'),
      vint Ts (Vcast ts h) <-> vint Ts ts.

    Lemma vint_app_term_elim_l : forall n (Ts : Tys n) p (ts : Tes p)
      q (us : Tes q), vint Ts (Vapp ts us) -> vint Ts ts.

    Lemma vint_app_term_elim_r : forall n (Ts : Tys n) p (ts : Tes p)
      q (us : Tes q) (h : vint Ts (Vapp ts us)), vint (Vsub Ts (vint_le h)) us.

    Lemma vint_app_intro : forall n (Ts : Tys n) p (ts : Tes p)
      q (us : Tes q) (h : p+q <= n), vint Ts ts -> vint (Vsub Ts h) us ->
      vint Ts (Vapp ts us).

    Lemma vint_forall_sn : forall n (Ts : Tys n) p (ts : Tes p),
      vint Ts ts -> Vforall (SN R_aeq) ts.

    Global Instance vint_vaeq n (Ts : Tys n) p :
      Proper (vaeq ==> impl) (vint Ts (p:=p)).


v is computable if, for every vector vs computable wrt the input types of v, apps v vs is computable.

    Lemma int_arrow : forall V v n, n <= arity V ->
      (forall vs : Tes n, vint (inputs V) vs -> int (output V n) (apps v vs))
      -> int V v.

apps v vs is computable if v and vs so are.

    Lemma int_apps : forall n (vs : Tes n) v (Vs : Tys n) A,
      vint Vs vs -> int (arrow Vs A) v -> int A (apps v vs).

Computability of vectors of terms is preserved by reduction.

    Global Instance vint_clos_vaeq n (Ts : Tys n) p :
      Proper (clos_vaeq R ==> impl) (vint Ts (p:=p)).


  End int.


Monotony properties of int and vint.


  Import SetUtil.

  Lemma int_equiv : forall I J T,
    (forall a, occurs a T -> I a [=] J a) -> int I T [=] int J T.

  Lemma int_equiv' : forall I J T,
    (forall a, occurs a T -> I a [=] J a) -> int I T [<=] int J T.

  Section mon.

    Variables (eq_dec : forall x y : So, {x=y}+{~x=y})
      (I J : So -> set Te) (a : So) (IJa : I a [<=] J a)
      (IJna : forall b, b <> a -> I b [=] J b).

    Lemma int_mon : forall T,
      (pos a T -> int I T [<=] int J T) /\ (neg a T -> int J T [<=] int I T).

    Lemma int_pos : forall T, pos a T -> int I T [<=] int J T.

    Lemma int_neg : forall T, neg a T -> int J T [<=] int I T.

    Lemma vint_mon : forall n (Ts : Tys n) p (ts : Tes p),
      (Vforall (pos a) Ts -> vint I Ts ts -> vint J Ts ts)
      /\ (Vforall (neg a) Ts -> vint J Ts ts -> vint I Ts ts).

    Lemma vint_pos : forall n (Ts : Tys n) p (ts : Tes p),
      Vforall (pos a) Ts -> vint I Ts ts -> vint J Ts ts.

    Lemma vint_neg : forall n (Ts : Tys n) p (ts : Tes p),
      Vforall (neg a) Ts -> vint J Ts ts -> vint I Ts ts.

  End mon.

End Make.

Termination of beta-eta-reduction.


Module SN_beta_eta (Export ST : ST_Struct).

  Module Import CP := CP_beta_eta ST.L.
  Module Import SN := Make ST CP.

  Lemma neutral_apps_fun : forall f n (us : Tes n), neutral (apps (Fun f) us).

  Lemma tr_sn_beta_aeq : forall E v V, E |- v ~: V -> SN R_aeq v.

End SN_beta_eta.