# Library CoLoR.Term.Lambda.LCompSimple

CoLoR, a Coq library on rewriting and termination.
• 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.