% Universe of types.
LF tp : type =
| i : tp % base type
| arr : tp → tp → tp % function type
;
--name tp T.
% Intrinsically typed terms, indexed by their type.
LF tm : tp → type =
| c : tm i % constants, of base type
| lam : (tm T1 → tm T2) → tm (arr T1 T2) % abstractions
| app : tm (arr T1 T2) → tm T1 → tm T2 % applications
;
--name tm M.
% single-step judgment.
LF step : tm A → tm A → type =
| s_beta : step (app (lam M) N) (M N) % beta reduction
| s_app : step M M' → step (app M N) (app M' N) % congruence
;
--name step S.
% multi-step judgment.
LF mstep : tm A → tm A → type =
| m_refl : mstep M M
| m_sing : step M M' → mstep M' N → mstep M N
;
--name mstep MS.
% values.
LF value : tm A → type =
| v_c : value c
| v_lam : value (lam M)
;
--name value V.
% A term halts if it has a reduction sequence to a value.
LF halts : tm A → type =
| eval : mstep M N → value N → halts M
;
% Now we can define reducibility.
% Reducibility needs a strong function space, so it is defined as a
% computation-level datatype.
% It is not a strictly positive definition: it is *stratified*,
% meaning that the recursion is not structural, but rather takes place
% on an index.
% We say that a term M is reducible at base type `i` if it halts.
% And a term M is reducible at function type `arr T1 T2` if it halts
% *and* if for any reducible term N at type T1, the application
% `app M N` is reducible at type T2.
stratified Reducible : {T : [ ⊢ tp ]} { M : [ ⊢ tm A ] } ctype =
| I : [ ⊢ halts M ] → Reducible [ ⊢ i ] [ ⊢ M ]
| Arr : [ ⊢ halts M ] →
({ N : [ ⊢ tm T1 ]} Reducible [ ⊢ T1 ] [ ⊢ N ] →
Reducible [ ⊢ T2 ] [ ⊢ app M N ]) →
Reducible [ ⊢ arr T1 T2 ] [ ⊢ M ]
;
% Now some lemmas. First, we need to show that halts is preserved when
% we add one more step.
rec halts_step : [ ⊢ step M N ] → [ ⊢ halts N ] → [ ⊢ halts M ] =
/ total (halts_step) /
fn s => fn h =>
let [ ⊢ S ] = s in
let [ |- eval MS V] = h in
% This is easy: h shows that N halts.
% Since halting means that there is a reduction sequence (MS)
% taking N to a value V, we can extend the reduction sequence with
% one my step (by rule m_sing) to get M reducing to V.
[ ⊢ eval (m_sing S MS) V ]
;
% Now we want to show that reducibility is "backwards closed", under
% stepping.
% If M1 steps to M2 and M2 is reducible at type T, then M1 is
% reducible at type T.
rec backwards_closed' : { T : [ ⊢ tp ] }
{ M1 : [ ⊢ tm T ] }
{ M2 : [ ⊢ tm T ] }
[ ⊢ step M1 M2 ] →
Reducible [ ⊢ T ] [ ⊢ M2 ] →
Reducible [ ⊢ T ] [ ⊢ M1 ] =
/ total a (backwards_closed' a s r1 r2) /
mlam T => mlam M1 => mlam M2 => fn s => fn r =>
(case [ |- T] of
| [ |- i] =>
let I v = r in
let v' = halts_step s v in
I v'
| [ |- arr T1 T2] =>
let Arr h nr = r in
Arr (halts_step s h)
(mlam N ⇒ fn rN ⇒
let [ ⊢ S ] = s in
let r' = nr [ ⊢ N ] rN in
backwards_closed' [ ⊢ T2 ] [ ⊢ _ ] [ ⊢ _ ]
[ ⊢ s_app S ]
r'
)
)
;
% Any reducible term halts.
% This is easy because each Reducible constructor includes a halts proof.
rec reduce_halts : Reducible [ ⊢ T ] [ ⊢ M ] → [ ⊢ halts M ] =
/ total r (reduce_halts r) /
fn r =>
(case r of
| I h => h
| Arr h nr => h
)
;
% Since we use intrinsically-typed terms, our contexts will store the
% terms themselves, since the terms contain their types in their
% index.
schema ctx = tm T;
inductive ReducibleSub : {γ : ctx} { #S : [ ⊢ γ ] } ctype =
| Nil : ReducibleSub [ ] [ ⊢ ^ ]
| Cons : ReducibleSub [γ] [ ⊢ #S ] → Reducible [ ⊢ T ] [ ⊢ M ] →
ReducibleSub [γ, x : tm T[]] [ ⊢ #S, M ]
;
% If we have a context and a variable in that context as well as a
% reducible substitution variable S in that context, then looking up
% the variable inside the substitution variable gives us a reducible
% term.
rec lookup : {γ : ctx} {#p : [ γ ⊢ tm T[] ]} ReducibleSub [γ] [ ⊢ #S ] →
Reducible [ ⊢ T ] [ ⊢ #p[#S] ] =
/ total γ (lookup γ _ _) /
mlam γ => mlam #p => fn rs =>
(case [γ] of
% impossible because the variable #p can't exist in an empty context!
| [] => impossible [ ⊢ #p ]
| [γ', x : tm T] =>
% notice rs : ReducibleSub [γ', x : tm T ] [ ⊢ #S[] ]
% so we can invert
let Cons rs' rN = rs in
(case [γ', x : tm T |- #p] of
% if #p is a variable other than x
| [γ', x : tm T |- #q[..]] =>
% strengthen #q since it isn't x,
% and recurse on the smaller substitution variable
lookup [γ'] [ γ' ⊢ #q ] rs'
% if #p is x
| [γ', x : tm T |- x] =>
rN
)
)
;
% Main lemma: if M is an open term in context γ of type A and σ is a
% reducible substitution, (i.e. σ takes variables in γ to reducible
% terms,) then M[σ] is reducible at type A.
rec main : {γ : ctx} {M : [γ ⊢ tm A[]]} ReducibleSub [γ] [ ⊢ #S ] →
Reducible [ ⊢ A ] [ ⊢ M[#S] ] =
/ total m (main _ _ _ m) / % extra _ for implicits!
mlam γ => mlam M => fn rs =>
(case [γ |- M] of
% in case of a variable, just look it up
| [γ |- #p] => lookup [γ] [ γ ⊢ #p ] rs
| [γ |- c] => I [ ⊢ eval m_refl v_c ]
| [γ |- lam (\x. M')] =>
Arr [ ⊢ eval m_refl v_lam ] % halts b/c lambda
mlam N => fn rN =>
let ih =
% reducible in extended context with extra variable
main [γ, x : tm _ ] [ γ, x ⊢ M' ] (Cons rs rN) in
% still reducible after converting back to application form
backwards_closed' [ ⊢ _ ] [ ⊢ _ ] [ ⊢ _ ]
[ ⊢ s_beta ]
ih
| [γ |- app M1 M2] =>
% apply IH to function; get out f
let Arr h f = main [γ] [ γ ⊢ M1 ] rs in
% apply IH to arg; get reducible arg
let r = main [γ] [ γ ⊢ M2 ] rs in
% apply f to reducible arg to get reducible result
f [ ⊢ _ ] r
)
;
% Theorem: all well-typed terms halt.
rec thm : {M : [ ⊢ tm T ]} [ ⊢ halts M ] =
/ total m (thm m) /
% This is easy since by the main lemma, M is reducible at type A, and
% reducibility implies halting.
mlam M ⇒ reduce_halts (main [] [ ⊢ M ] Nil)
;