THEOREM[expression termination]
  If C1 = {};{};P;L and |- C1 and C1 |- e1:t
  then all sequences of reduction steps e1-->e2-->e3-->...
    terminate at some en=vn
Proof:
The language Fwn is defined below.  Fwn is, roughly, a subset of the calculus of
inductive constructions (i.e. by lemma[expression type translation 2] every
well-typed Fwn program is a well-typed CIC program, by
lemma[expression simulation 2], every reduction in Fwn corresponds to
a reduction in CIC), and therefore all well-typed Fwn programs terminate.
(See Shao et al, "A Type System for Certified Binaries (Extended Version)",
for a concise definition of a variant of CIC, including definitions
of natural numbers, and a proof of strong normalization.)

Let Ck = {};{};P;L.  By preservation, |- Ck and Ck |- ek:t.
Let C1 |- e1:t~~> ~e1 and {} |- t:type~~> ~t (see definitions below).
By lemma[expression type translation 1], {};{} |- ~e1:~t.
Suppose e1 takes an infinite sequence of steps.  Then we can
show that e1' also takes an infinite number of steps, which contradicts
Fwn's termination:
  For each step that ek-->ek+1, lemma[expression simulation 1]
  shows that ~ek steps to ~(ek+1) in one or more steps.  Therefore,
  an infinite sequence of steps starting from e1 implies an
  infinite sequence of Fwn steps starting from ~e1.
Therefore, e1 can take only a finite number of steps to some en,
which can step no further.  By progress, en must be a value vn.

THEOREM[coercion termination]
  If C1 = {};{};P;L and |- C1 and C1 |- c1:t
  then all sequences of reduction steps c1-->c2-->c3-->...
    terminate at some en=vn
Proof by induction on structure of c1.
Case c1 = e: follows directly from theorem[expression termination].
Case c1 = #c:
  By inversion, c has type %t for some t.
  By induction, c reaches a value v in zero or more steps.
  By preservation, v has type %t.  By canonical forms, v = %e.
  Therefore, #c -->* #v and #v = #%e and #%e --> e.
  By theorem[expression termination], e terminates at some value.

The lemmas below make frequent use of lemma[type equivalence kinds] and lemma[expression kinds].

====================================================================

LEMMA[expression type translation 1]

 (1)  If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t'
      then D' |- t':~k
 (2)  If C = D;G;P;L and |- C ~~> D';G'
      and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and |- t1=t2
      then |- t1'=t2'
 (3)  If C = D;G;P;L and |- C ~~> D';G'
      then D' |- G'
 (4)  If C = D;G;P;L and |- C ~~> D';G' and D |- ta:k ~~> ta'
      and |- pat:ta => D'';G'' ; e':tb' ::> e'' and |- C D'';G'' ~~> D''';G''' and D''';G''' |- e':tb'
      then D';G' |- e'':ta'->tb'
 (5)  If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' and C |- e:t ~~> e'
      then D';G' |- e':t'


Define the target language "Fwn" for the translation ~~> as follows:

        D = {A->k}
        G = {x->t}
        C=D;G
        k = k->k | type | nat
        t = t -> t
          | 0 | s(t) | elim k t t t
          | A:k | all A:k.t | \A:k.t | t t
        e = x | \x:t.e | e e
          | induction t t e e
          | \A:k.e | e t

D |- t1:type
D |- t2:type
----------------
D |- t1 -> t2:type

D |- 0:nat

D |- t:nat
-------------
D |- s(t):nat

D |- tn:nat
D |- tz:k
D |- ts:nat->k->k
----------------------
D |- elim k tn tz ts:k

D,A:k |- (A:k):k

D,A:k |- t:type
-------------------
D |- all A:k.t : type

D,A:ka |- t:kb
---------------------
D |- \A:ka.t : ka->kb

D |- tf:ka->kb
D |- ta:ka
--------------
D |- tf ta:kb

|- t = t

|- t1 = t2
----------
|- t2 = t1

|- t1 = t2
|- t2 = t3
----------
|- t1 = t3

|- (\A:k.tb) ta = [A<-ta]tb

|- elim k 0 tz ts = tz

|- elim k s(tm) tz ts = ts tm (elim k tm tz ts)

|- t1 = t1'
-----------------
|- T[t1] = T[t1']

|- t1 = t1'
|- t2 = t2'
------------------------
|- T[t1,t2] = T[t1',t2']

|- t1 = t1'
|- t2 = t2'
|- t3 = t3'
--------------------------------
|- T[t1,t2,t3'] = T[t1',t2',t3']

T[t1] = s(t1) | all A:k.t1 | \A:k.t1
T[t1,t2] = t1 -> t2 | t1 t2
T[t1,t2,t3] = elim k t1 t2 t3

C,x:t |- x:t

C,xa:ta |- e:tb
C |- tb:type
-----------------------
C |- \x:ta.e : ta -> tb

C |- ef:ta -> tb
C |- ea:ta
-------------
C |- ef ea:tb

C |- tn:nat
C |- tF:nat->type
C |- e0:tF 0
C |- es:all A:nat.tF A -> tF s(A)
---------------------------------
C |- induction tn tF e0 es: tF A

C,A:k |- e:t
-----------------------
C |- \A:k.e : all A:k.t

C |- e : all A:k.t'
C |- t:k
-------------------
C |- e t : t'

C |- e:t
C |- t = t'
-----------
C |- e:t'

forall x->t in G, D |- t:type
-----------------------------
D |- G

(\x:t.eb) ea --> [x<-ea]eb

|- tn = 0
----------------------------
induction tn tf e0 es --> e0

|- tn = s(tm)
---------------------------------------------------------
induction tn tf e0 !es --> es tm (induction tm tf e0 !es)

(\A:k.e) t --> [A<-t]e

E[e1] = \x:t.e1 | \A:k.e1 | e1 t
      | e1 e | e1,e | induction t t e1 e
      | e e1 | e,e1 | induction t t e e1

e-->e'
------------
E[e]-->E[e']



Define the translations ~~> as follows
(using the abbreviations ~e = e' for C |- e:t ~~> e' and ~t = t' for C |- t:k ~~> t'
where the surrounding judgments aren't immediately necessary)
Define the abbreviations True = all A:type.A->A and true = \A:type.\x:A.x

~(k1->k2) = ~k1->~k2
~nat = nat
~reg = type
~type = type

~(!t) = t
~(t1 -o t2) = ~t1->~t2
~(t1*t2) = all A:type.(~t1->~t2->(A:type))->(A:type)
~0 = 0
~s(t) = s(~t)
~(all A:k.t) = all A:~k.~t
~(exists A:k.t) = all B:type.(all A:~k.~t->(B:type))->(B:type)
~(\A:k.t) = \A:~k.~t
~(t1 t2) = ~t1 ~t2
~r = True
~(Reg t t) = True
~(Mem t t) = True
~(Code t t) = True

D,A:k |- A:k ~~> A:k

D |- tn:nat ~~> ~tn
D |- tz:k ~~> ~tz
D |- ts:nat->k->k ~~> ~ts
--------------------
D |- elim tn tz ts:k ~~> elim ~k ~tn ~tz ~ts

D |- t:k->k
-------------------
D |- rec t:k ~~> `k

D |- t:k
----------------
D |- %t:k ~~> `k

`(k1->k2) = \A:~k1.`k2
`nat = True
`reg = True
`type = True

|- x:t => {};{x:t} ; e:tb ::> \x:~t.e

|- !x:!t => {};{!x:t} ; e:tb ::> \x:~t.e

|- pat:t => D;G ; e:tb ::> e'
--------------------
|- !(pat):!t => D;G ; e:tb ::> e'

|- pat:t => D;G ; e:tb ::> e'
--------------------------------
|- A,pat:exists A:k.t => D,A:k;G ; e:tb ::> \x:~(exists A:k.t).x tb (\A:~k.e')

|- pat1:t1 => D1;G1 ; e':~t2->tb ::> e''
|- pat2:t2 => D2;G2 ; e:tb ::> e'
---------------------------------
|- pat1,pat2:t1*t2 => D1 D2;G1 G2  ; e ::> \x:~(t1*t2).x tb e''

|- pat:ta => D;G ; e' ::> e''
C D;G |- e:tb ~~> e'
C |- ta -o tb : type
-------------------------
C |- \pat:ta.e : ta -o tb ~~> e''

C |- e1:t1 ~~> e1'
|- pat:t1 => D;G ; e2' ::> e''
C D;G |- e2:t2 ~~> e2'
C |- t2:type
--------------------------
C |- let pat = e1 in e2:t2 ~~> e'' e1'

C1 |- e1:t1 ~~> e1'
C2 |- e2:t2 ~~> e2'
--------------------
C1,C2 |- e1,e2:t1*t2 ~~> \A:type.\x:(~t1->~t2->(A:type)).x e1' e2'

C |- t1:k ~~> t1'
C |- e:[A<-t1]t2 ~~> e'
-------------------------------
C |- pack t1,e as exists A:k.t2 ~~> \B:type.\x:(all A:~k.~t2->(B:type)).x t1' e'

C |- e:t ~~> e'
C |- t = t'
-----------
C |- e:t' ~~> e'

~x = x
~(!e) = ~e
~(e1 e2) = ~e1 ~e2
~(induction t1 t2 e1 e2) = induction ~t1 ~t2 ~e1 ~e2
~(\A:k.e) = \A:~k.~e
~(e t) = ~e ~t
~(%e) = true
~(e1 %<< e2) = (\_:True.~e2) ~e1
~fact = true
~(code(n)[t...t]) = true

LEMMA
 (1)  If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t'
      then D' |- t':~k

Induction on D |- t:k.  Also use following lemma:
  lemma: In any D, D |- `k:~k.
  proof: easy induction on k.

CASE

D |- t:k
----------------
D |- %t:k ~~> `k

By lemma, D' |- `k:~k.

CASE

D,A:ka |- t:kb ~~> ~t
---------------------
D |- \A:ka.t : ka->kb ~~> \A:~ka.~t

By induction, D',A:~ka |- ~t:~kb
By rule, D' |- (\A:~ka.~t):~ka->~kb
~ka->~kb = ~(ka->kb)

OTHER CASES SIMILAR



LEMMA
 (2)  If C = D;G;P;L and |- C ~~> D';G'
      and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and |- t1=t2
      then |- t1'=t2'

Induction on |- t1=t2

EASY CASES

|- t = t

|- t1 = t2
----------
|- t2 = t1

|- t1 = t2
|- t2 = t3
----------
|- t1 = t3

CASE

|- (\A:k.tb) ta = [A<-ta]tb

(\A:~k.~tb) ~ta = [A<-~ta]~tb
~((\A:k.tb) ta) = ~([A<-ta]tb)
where ~([A<-ta]tb) = [A<-~ta]~tb by induction on derivation of ~tb

CASES

|- elim 0 tz ts = tz
|- elim s(tm) tz ts = ts tm (elim tm tz ts)

~(elim 0 tz ts) = elim ~k 0 ~tz ~ts = ~tz
~(elim s(tm) tz ts) = elim ~k s(~tm) ~tz ~ts = ~ts ~tm (elim ~k ~tm ~tz ~ts) = ~(ts tm (elim tm tz ts))

CASE

|- rec t = %(t (rec t))

These are the only possible derivations of ~~> for rec t and %(t (rec t)):

D |- t:k->k
-------------------
D |- rec t:k ~~> `k

                 D |- t:k->k
                 ------------
D |- t:k->k      D |- rec t:k
-----------------------------
D |- t (rec t):k
--------------------------
D |- %(t (rec t)):k ~~> `k

Because the kinding rules are syntax directed,
there is only one possible derivation of D |- t:...,
so both `k must refer to the same k,
so the case is proven by:
  |- `k = `k

CASE

|- (%t1) t2 = %(t1 t2)

Only possible derivations:

D |- t1:ka->kb
---------------
D |- %t1:ka->kb ~~> `(ka->kb)    D |- t2:ka ~~> ~t2
-------------------------------------------
D |- (%t1) t2:kb ~~> `(ka->kb) ~t2

D |- t1:ka->kb    D |- t2:ka
----------------------------
D |- t1 t2:kb
----------------
D |- %(t1 t2):kb ~~> `kb

`(ka->kb) ~t2 = (\A:~ka.`kb) ~t2 = `kb

CONGRUENCE CASES

easy

LEMMA
 (3)  If C = D;G;P;L and |- C ~~> D';G'
      then D' |- G'

|- C implies forall x->t and !x->t in G, D |- t:type.
By lemma(1), forall x->t and !x->t in G, D' |- ~t:type.


LEMMA
 (4)  If C = D;G;P;L and |- C ~~> D';G' and D |- ta:k ~~> ta'
      and |- pat:ta => D'';G'' ; e':tb' ::> e'' and |- C D'';G'' ~~> D''';G''' and D''';G''' |- e':tb'
      then D';G' |- e'':ta'->tb'

CASE

|- x:ta => {x:ta} ; e':tb' ::> \x:~ta.e'

D'' = {}, so D''' = D'
G'' = {x:ta}, so G''' = G',x:~ta
D''';G''' |- e':tb'

D';G',x:ta' |- e':tb'
-------------------------------
D';G' |- \x:ta'.e':ta'->tb'

CASE

|- pat:t => D'';G'' ; e':tb' ::> e''
------------------------------------
|- A,pat:exists A:k.t => D'',A:k;G''; e':tb' ::> \x:~(exists A:k.t).x tb' (\A:~k.e'')

|- C,A:k ~~> D',A:~k;G'
D,A:k |- t:k ~~> t'
|- pat:t => D'';G'' ; e':tb' ::> e''
C'' = C D'',A:k;G''
|- C'' ~~> D''';G'''
D''' |- e':tb'
By induction, D',A:~k;G' |- e'':t'->tb'
D';G' |- (\A:~k.e''):all A:~k.t'->tb'
D';G',x:~(exists A:k.t) |- x tb' (\A:~k.e''):tb'
  since ~(exists A:k.t) = all B:type.(all A:~k.~t->(B:type))->(B:type)
D';G' |- \x:~(exists A:k.t).x (\A:~k.e'') : ta'->tb'


LEMMA
 (5)  If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' and C |- e:t ~~> e'
      then D';G' |- e':t'

By induction on C |- e:t ~~> e'.

CASE

|- pat:ta => D'';G'' ; e' ::> e''
C'' = C D'';G''
C'' |- e:tb ~~> e'
C |- ta -o tb:type
-------------------------
C |- \pat:ta.e : ta -o tb ~~> e''

|- C ~~> D';G'
D |- (ta -o tb):type ~~> ta'->tb'
C |- (\pat:ta.e):(ta -o tb) ~~> e''

C'' = D'';G'';P;L
|- C'' ~~> D''';G'''
By weakening, D'' |- tb:type ~~> tb'  // Yuck
C'' |- e:tb ~~> e'
By induction, D''';G''' |- e':tb'
By lemma(4), then D';G' |- e'':ta'->tb'

CASE

C |- e:t1 ~~> e'
C |- t1 = t2
-----------
C |- e:t2 ~~> e'

D |- t2:k ~~> t2'
By induction, D';G' |- e':t1'
By lemma 2, |- t1' = t2'
By rule, D';G' |- e':t2'

CASE

C |- e:t
----------
C |- %e:%t ~~> true

D |- %t:type ~~> True
D';G' |- true:True

CASE

C1 |- e1:%(ta -o tb) ~~> ~e1
C2 |- e2:%ta         ~~> ~e2
------------------------
C1,C2 |- e1 %<< e2 : %tb ~~> (\_:True.~e2) ~e1

D |- %ta:type ~~> True
D |- %(ta -o tb):type ~~> True
|- C1 ~~> D';G1'
|- C2 ~~> D';G2'
G' = G1',G2'
By induction, D';G1' |- ~e1:True
By induction, D';G2' |- ~e2:True
By weakening, D';G' |- ~e1:True
By weakening, D';G' |- ~e2:True
D';G' |- (\_:True.~e1):True->True
D';G' |- (\_:True.~e1) ~e2:True


OTHER CASES SIMILAR


====================================================================

LEMMA[expression simulation 1]
 (1) If |-pat:ta=>D';G';eb:tb::>ef and pat<-ea=>[s] and C |- ea:ta~~>eax
     then ef eax -->+ [~s]eb
 (2) If C |- e:t ~~> ex and C |- e':t ~~> ex' and e-->e' then ex -->+ ex'
(where -->+ indicates one or more steps)

Proof by induction on pat<-ea=>[s] and e-->e'.

CASE

x<-ea => [x<-ea]

|- x:ta => {};{x:ta} ; eb:tb ::> \x:~ta.eb
C |- ea:ta~~>eax

(\x:~ta.eb) eax --> [x<-eax]eb = [~(x<-ea)]eb


CASE

pat<-ea' => [s]
---------------------------------------
A,pat<-pack ta',ea' as ta => [s][A<-ta']

|- pat:t => D';G' ; eb:tb ::> e'
-----------------------------
|- A,pat:exists A:k.t => {A:k}D';G' ; eb:tb ::> \x:~(exists A:k.t).x tb (\A:~k.e')

C |- ta':k ~~> ta''
C |- ea':[A<-ta']t ~~> ea''
---------------------------------
C |- pack ta',ea' as exists A:k.t ~~> \B:type.\x:(all A:~k.~t->B).x ta'' ea''

|- pat:t => D';G' ; eb:tb ::> e'
|- pat:[A<-ta']t => D';[A<-ta']G' ; [A<-ta'']eb:tb ::> [A<-ta'']e' (easy induction)
pat<-ea' => [s]
C |- ea':[A<-ta']t ~~> ea''
By induction, ([A<-ta'']e') ea'' -->+ [~s][A<-ta'']eb

    (\x:~(exists A:k.t).x tb (\A:~k.e')) (\B:type.\x:(all A:~k.~t->B).x ta'' ea'')
--> (\B:type.\x:(all A:~k.~t->B).x ta'' ea'') tb (\A:~k.e')
--> (\x:(all A:~k.~t->tb).x ta'' ea'') (\A:~k.e')
--> (\A:~k.e') ta'' ea''
--> ([A<-ta'']e') ea''
-->+ [~s][A<-ta'']eb
  = [~s][~(A<-ta')]eb


CASE

pat<-ea => [s]
------------------------
(\pat:ta.eb) ea --> [s]eb

|- pat:ta => D';G' ; e' ::> e''
C' |- eb:tb ~~> e'
C |- ta -o tb : type
-------------------------
C |- \pat:ta.eb : ta -o tb ~~> e''
C |- (\pat:ta.eb) ea:t ~~> e'' ~ea

C |- [s]eb:t ~~> [~s]e'

By lemma(1), e'' ~ea -->+ [~s]e'


CASE

%ef %<< %ea --> %(ef ea)

C1 |- %ef:%(ta -o tb) ~~> ~%ef
C2 |- %ea:%ta         ~~> ~%ea
------------------------
C1,C2 |- %ef %<< %ea : %tb ~~> (\_:True.~%ea) ~%ef

~%ea = true (by inversion)
~(%(ef ea)) = true

(\_:True.~%ea) ~%ef --> ~%ea = true

OTHER CASES SIMILAR

====================================================================

LEMMA[expression type translation 2]

Target language ("TL", Shao et al's variant of CIC, omitting "Ext"):
        s = Kind | Kscm
        X = x | A
        D = {} | {},X:t
        t = s | X | \X:t.t | t t | #X:t.t
          | Ind(X:Kind){...t...}
          | Ctor(i,t)
          | Elim[t,t](t){...t...}
abbreviation: (t1->t2) = (#x:t1.t2) where x is not free in t2
abbreviation: (t1=>t2) = (#A:t1.t2) where A is not free in t2
abbreviation: nat = Ind(A:Kind){A;A->A}
abbreviation: 0 = Ctor(1,nat)
abbreviation: s(t) = Ctor(2,nat) t
note that nat's constructors are "small" ("small(A)" and "small(A->A)")
note that |- nat:Kind

S(k1->k2) = S(k2)
S(type) = Kscm
S(nat) = Kind

K(k1->k2) = K(k1)=>K(k2) where S(k1) = Kscm
K(k1->k2) = K(k1)->K(k2) where S(k1) = Kind
K(type) = Kind
K(nat) = nat

For each type variable "A", define a corresponding object variable "xA".
X(A,Kind) = xA
X(A,Kscm) = A

T(t1->t2) = T(t1)->T(t2)
T(0) = 0
T(s(t)) = s(T(t))
T(elim k tn tz ts) = Elim[nat,K(k)](T(tn)){T(tz);T(ts)} where S(k)=Kscm
T(elim k tn tz ts) = Elim[nat,\_:nat.K(k)](T(tn)){T(tz);T(ts)} where S(k)=Kind
T(A:k) = X(A,S(k))
T(\A:k.t) = \X(A,S(k)):K(k).T(t)
T(all A:k.t) = #X(A,S(k)):K(k).T(t)
T(t1 t2) = T(t1) T(t2)

E(x) = x
E(\x:t.e) = \x:T(t).E(e)
E(e1 e2) = E(e1) E(e2)
E(induction tf tn ez es) = Elim[nat,T(tf)](T(tn)){E(ez);E(es)}
E(\A:k.e) = \A:K(k).E(e)
E(e t) = E(e) T(t)

D(...A->k...} = ...X(A,S(k)):K(k)...
G(...x->t...} = ...x:T(t)...

Lemma: |- K(k):S(k)

By induction on k.
(Straightforward, since |- nat:Kind and |- Kind:Kscm
 and the rules assign #X:t1.t2 sort s2 if t2 has sort s2.)

Lemma: If |- t1:t2 then D(D) |- t1:t2

By induction on D.

Lemma: If D |- t:k then D(D) |- T(t):K(k)

By induction on derivation of D |- t:k.

CASE

D,A:ka |- t:kb
---------------------
D |- \A:ka.t : ka->kb
where S(ka)=S(kb)=Kind

By induction, D(D),X(A,S(ka)):K(ka) |- T(t):K(kb)
  So D(D),xA:K(ka) |- T(T):K(kb)
By lemma, |- K(ka->kb) : S(ka->kb)
  So |- K(ka)->K(kb) : Kind
  So |- #xA:K(ka).K(kb) : Kind  (since xA not free in K(kb))
By lemma, D(D) |- #xA:K(ka).K(kb) : Kind

D(D),xA:K(ka) |- T(t) : K(kb)
D(D) |- #xA:K(ka).K(kb) : Kind
---------------------------------------------------------
D(D),xA:K(ka) |- \X(A,S(ka)):K(ka).T(t) : #xA:K(ka).K(kb)

OTHER CASES SIMILAR

Lemma: If D |- G and D;G |- e:t then D(D),G(G) |- E(e):T(t)

By induction on derivation of D;G |- e:t.

LEMMA[expression simulation 2]
If C |- e:t ~~> tx and C |- e':t ~~> tx' and e-->e'
then tx -->+ tx' by beta-eta-iota reduction.
(where -->+ indicates one or more steps)

By induction on e-->e'.  The application rules are trivial,
but note that the rules for "induction", such as:

  |- tn = 0
  ----------------------------
  induction tn tf e0 es --> e0

take a single step in the source language, but it may take multiple
steps in the target language for tn to reduce to 0.  By confluence,
there is a sequence of steps tn=>tn'=>tn''=>...=>0, and
this sequence translates into a sequence ~tn -->* ~tn' -->* ... -->* 0
in the target language, where -->* indicates zero or more steps.