THEOREM[expression termination]
  If C1 = {};U1;R1;{};P;L and |- C1 and C1 |- e1:t
  then all sequences of reduction steps U1;R1;e1-->U2;R2;e2-->U3;R3;e3-->...
    terminate at some Un;Rn;vn
Proof:
The language Fwn is defined below.  Fwn is a subset of the calculus of
inductive constructions (i.e. every well-typed Fwn program is a well-typed
CIC program, and every reduction rule in Fwn is 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 = {};Uk;Rk;{};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 U1;R1;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 Uk;Rk;ek-->Uk+1;Rk+1;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 U1;R1;e1 implies an
  infinite sequence of Fwn steps starting from ~e1.
Therefore, U1;R1;e1 can take only a finite number of steps to some Un;Rn;en,
which can step no further.  By progress, en must be a value vn.

THEOREM[coercion termination]
  If C1 = {};U1;R1;{};P;L and |- C1 and C1 |- c1:t
  then all sequences of reduction steps U1;R1;c1-->U2;R2;c2-->U3;R3;c3-->...
    terminate at some Un;Rn;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;U;R;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t'
      then D' |- t':~k
 (2)  If C = D;U;R;G;P;L and |- C ~~> D';G'
      and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and R |- t1=t2
      then |- t1'=t2'
 (3)  If C = D;U;R;G;P;L and |- C ~~> D';G'
      then D' |- G'
 (4)  If C = D;U;R;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;U;R;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) | if0 t t t
          | A | 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
-------------------
D |- if0 tn tz ts:k

D,A:k |- A: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

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

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

R |- t1 = t1'
R |- t2 = t2'
R |- t3 = t3'
-----------------------------------
R |- 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] = if0 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'

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)->A
~0 = 0
~s(t) = s(~t)
~(if0 t1 t2 t3) = if0 ~t1 ~t2 ~t3
~A = A
~(all A:k.t) = all A:~k.~t
~(exists A:k.t) = all B:type.(all A:~k.~t->B)->B
~(\A:k.t) = \A:~k.~t
~(t1 t2) = ~t1 ~t2
~(Delay t) = True
~q_k = `k
~r = True
~(Reg t t) = True
~(Mem t t) = True
~(Code t t) = True

D |- t:k
---------------------
D |- type(t):k ~~> `k

D |- t:k
-------------------
D |- pf(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 |- 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).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).x t1' e'

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

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

~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
~(delay k) = (\_:True.true) true
~(commit[t=type(t)] e) = (\_:True.true) ~e
~(%e) = true
~(e1 >>* e2) = (\_:True.~e2) ~e1
~fact = true
~(code(n)[t...t]) = true

LEMMA
 (1)  If C = D;U;R;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 |- type(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;U;R;G;P;L and |- C ~~> D';G'
      and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and R |- t1=t2
      then |- t1'=t2'

Induction on R |- t1=t2

EASY CASES

R |- t = t

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

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

CASE

R |- (\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

R |- if0 0 tz ts = tz
R |- if0 s(tm) tz ts = ts tm

~(if0 0 tz ts) = if0 0 ~tz ~ts = ~tz
~(if0 s(tm) tz ts) = if0 s(~tm) ~tz ~ts = ~ts ~tm = ~(ts tm)

CASE

R,q_k->t |- type(q_k) = type(t)

D |- type(q_k):k
D |- type(t):k
~type(q_k) = `k
~type(t) = `k

CASE

R |- (type(t1)) t2 = type(t1 t2)

D |- (type(t1)):ka->kb
D |- t2:ka
--------------
D |- (type(t1)) t2:kb

D |- type(t1 t2):kb

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

CASE

R |- (pf(t1)) t2 = pf(t1 t2)
see previous case

CONGRUENCE CASES

easy

LEMMA
 (3)  If C = D;U;R;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;U;R;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)->B
D';G' |- \x:~(exists A:k.t).x (\A:~k.e'') : ta'->tb'


LEMMA
 (5)  If C = D;U;R;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 |- 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'';U;R;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 ~~> e1'
C2 |- e2:ta -o tb ~~> e2'
------------------------
C1,C2 |- e1 >>@ e2 : %tb ~~> (\_:~ta->~tb.e1') e2'

D |- %ta:type ~~> True
D |- (ta -o tb):type ~~> ta'->tb'
|- C1 ~~> D';G1'
|- C2 ~~> D';G2'
G' = G1',G2'
By induction, D';G1' |- e1':True
By induction, D';G2' |- e2':ta'->tb'
By weakening, D';G' |- e1':True
By weakening, D';G' |- e2':ta'->tb'
D';G' |- (\_:~ta->~tb.e1'):(ta'->tb')->True
D';G' |- (\_:~ta->~tb.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'
 (3) If C |- e:t ~~> ex and C |- e':t ~~> ex' and U;R;e-->U';R';e' then ex -->+ ex'
(where -->+ indicates one or more steps)

Proof by induction on pat<-ea=>[s] and e-->e' and U;R;e-->U';R';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 |- 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 

e-->e'
------------------
(U;R;e)-->(U;R;e')

By induction, ex -->+ ex'

CASE

(U;R; %ea >>@ vf) --> (U;R; %(vf ea))

C1 |- %ea:%ta ~~> e1'
C2 |- vf:ta -o tb ~~> e2'
------------------------
C1,C2 |- %ea >>@ vf : %tb ~~> (\_:~ta->~tb.e1') e2'

e1' = true (by inversion)
~(%(vf ea)) = true

(\_:~ta->~tb.e1') e2' --> e1' = true

CASE

(U;R; delay k) --> (U,q_k;R; %pack q_k,fact as exists A:k.Delay type(A))  where q_k is fresh
~(delay k) = (\_:True.true) true --> true = ~(%pack q_k,fact as exists A:k.Delay type(A))


CASE

R |- t=type(q_k)
-----------------------------------------------------------------------------------
(U,q_k;R; commit[t=type(t')] fact) --> (U;R,q_k->t'; %!\F:k->type.\x:F type(q_k).x)

~(commit[t=type(t')] e) = (\_:True.true) ~e --> true = ~(%!\F:k->type.\x:F q_k.x)

OTHER CASES SIMILAR