Library Termination

Termination

Require Import Substitution Reduction.
Implicit Types x y z : var.
Implicit Types F G H : basetype.
Implicit Types A B C : inttype.
Implicit Types U V W : type.
Implicit Types Gamma Delta : context.

Reducible terms have a non-zero reduction bound

Lemma step_n {n Gamma s A} : ty n Gamma s A -> forall {s'}, step s s' -> n > 0.
remember (A : type) as U.
intros tys.
revert A HeqU.
assert (forall n m, n > 0 -> n + m > 0) by (intros x y ; omega).
induction tys ; intros A' e' s' ; inversion 1 ; subst ; eauto.
Qed.

Every reduction step reduces the reduction bound by one

Lemma step_ty {n Gamma s A} : ty n Gamma s A -> forall s', step s s' -> ty (pred n) Gamma s' A.
remember (A : type) as U.
intros tys.
revert A HeqU.
induction tys ; intros A' e' s' ; subst ; simpl in * ; eauto.
- inversion 1.
- inversion 1. eauto.
- intros st. rewrite <- e.
  inversion st as [ ? ? | ? ? ? sts | ? ? ? stt | ? ? sL ] ; subst.
  + inversion tys1 ; subst.
    eauto using tysubst, tycsub, tysub_beta, csub_comm.
  + assert (H' := step_n tys1 sts).
    destruct n ; simpl in * ; eauto.
  + assert (H' := step_n tys2 stt).
    replace (n + m) with (S (n + pred m)) ; eauto.
- intros st.
  assert (H1 := step_n tys1 st).
  assert (H2 := step_n tys2 st).
  replace (pred (n + m)) with (S (pred n + pred m)) ; eauto using tymon.
Qed.

The target system is terminating
Theorem sn_system n Gamma t A : ty n Gamma t A -> SN t.
revert t A.
induction n ; intros t A tyt ; constructor ; intros t' st.
- assert (bogus := step_n tyt st). omega.
- apply IHn with A. now apply (step_ty tyt).
Qed.