doc-src/Logics/CTT.tex
author haftmann
Wed Dec 27 19:10:06 2006 +0100 (2006-12-27)
changeset 21915 4e63c55f4cb4
parent 12679 8ed660138f83
child 42637 381fdcab0f36
permissions -rw-r--r--
different handling of type variable names
     1 %% $Id$
     2 \chapter{Constructive Type Theory}
     3 \index{Constructive Type Theory|(}
     4 
     5 \underscoreoff %this file contains _ in rule names
     6 
     7 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
     8 be viewed at many different levels.  It is a formal system that embodies
     9 the principles of intuitionistic mathematics; it embodies the
    10 interpretation of propositions as types; it is a vehicle for deriving
    11 programs from proofs.  
    12 
    13 Thompson's book~\cite{thompson91} gives a readable and thorough account of
    14 Type Theory.  Nuprl is an elaborate implementation~\cite{constable86}.
    15 {\sc alf} is a more recent tool that allows proof terms to be edited
    16 directly~\cite{alf}.
    17 
    18 Isabelle's original formulation of Type Theory was a kind of sequent
    19 calculus, following Martin-L\"of~\cite{martinlof84}.  It included rules for
    20 building the context, namely variable bindings with their types.  A typical
    21 judgement was
    22 \[   a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \; 
    23     [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]
    24 \]
    25 This sequent calculus was not satisfactory because assumptions like
    26 `suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$'
    27 could not be formalized.  
    28 
    29 The theory~\thydx{CTT} implements Constructive Type Theory, using
    30 natural deduction.  The judgement above is expressed using $\Forall$ and
    31 $\Imp$:
    32 \[ \begin{array}{r@{}l}
    33      \Forall x@1\ldots x@n. &
    34           \List{x@1\in A@1; 
    35                 x@2\in A@2(x@1); \cdots \; 
    36                 x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
    37      &  \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) 
    38     \end{array}
    39 \]
    40 Assumptions can use all the judgement forms, for instance to express that
    41 $B$ is a family of types over~$A$:
    42 \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
    43 To justify the CTT formulation it is probably best to appeal directly to the
    44 semantic explanations of the rules~\cite{martinlof84}, rather than to the
    45 rules themselves.  The order of assumptions no longer matters, unlike in
    46 standard Type Theory.  Contexts, which are typical of many modern type
    47 theories, are difficult to represent in Isabelle.  In particular, it is
    48 difficult to enforce that all the variables in a context are distinct.
    49 \index{assumptions!in CTT}
    50 
    51 The theory does not use polymorphism.  Terms in CTT have type~\tydx{i}, the
    52 type of individuals.  Types in CTT have type~\tydx{t}.
    53 
    54 \begin{figure} \tabcolsep=1em  %wider spacing in tables
    55 \begin{center}
    56 \begin{tabular}{rrr} 
    57   \it name      & \it meta-type         & \it description \\ 
    58   \cdx{Type}    & $t \to prop$          & judgement form \\
    59   \cdx{Eqtype}  & $[t,t]\to prop$       & judgement form\\
    60   \cdx{Elem}    & $[i, t]\to prop$      & judgement form\\
    61   \cdx{Eqelem}  & $[i, i, t]\to prop$   & judgement form\\
    62   \cdx{Reduce}  & $[i, i]\to prop$      & extra judgement form\\[2ex]
    63 
    64   \cdx{N}       &     $t$               & natural numbers type\\
    65   \cdx{0}       &     $i$               & constructor\\
    66   \cdx{succ}    & $i\to i$              & constructor\\
    67   \cdx{rec}     & $[i,i,[i,i]\to i]\to i$       & eliminator\\[2ex]
    68   \cdx{Prod}    & $[t,i\to t]\to t$     & general product type\\
    69   \cdx{lambda}  & $(i\to i)\to i$       & constructor\\[2ex]
    70   \cdx{Sum}     & $[t, i\to t]\to t$    & general sum type\\
    71   \cdx{pair}    & $[i,i]\to i$          & constructor\\
    72   \cdx{split}   & $[i,[i,i]\to i]\to i$ & eliminator\\
    73   \cdx{fst} \cdx{snd} & $i\to i$        & projections\\[2ex]
    74   \cdx{inl} \cdx{inr} & $i\to i$        & constructors for $+$\\
    75   \cdx{when}    & $[i,i\to i, i\to i]\to i$    & eliminator for $+$\\[2ex]
    76   \cdx{Eq}      & $[t,i,i]\to t$        & equality type\\
    77   \cdx{eq}      & $i$                   & constructor\\[2ex]
    78   \cdx{F}       & $t$                   & empty type\\
    79   \cdx{contr}   & $i\to i$              & eliminator\\[2ex]
    80   \cdx{T}       & $t$                   & singleton type\\
    81   \cdx{tt}      & $i$                   & constructor
    82 \end{tabular}
    83 \end{center}
    84 \caption{The constants of CTT} \label{ctt-constants}
    85 \end{figure}
    86 
    87 
    88 CTT supports all of Type Theory apart from list types, well-ordering types,
    89 and universes.  Universes could be introduced {\em\`a la Tarski}, adding new
    90 constants as names for types.  The formulation {\em\`a la Russell}, where
    91 types denote themselves, is only possible if we identify the meta-types~{\tt
    92   i} and~{\tt t}.  Most published formulations of well-ordering types have
    93 difficulties involving extensionality of functions; I suggest that you use
    94 some other method for defining recursive types.  List types are easy to
    95 introduce by declaring new rules.
    96 
    97 CTT uses the 1982 version of Type Theory, with extensional equality.  The
    98 computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
    99 Its rewriting tactics prove theorems of the form $a=b\in A$.  It could be
   100 modified to have intensional equality, but rewriting tactics would have to
   101 prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
   102 require a separate simplifier.
   103 
   104 
   105 \begin{figure} \tabcolsep=1em  %wider spacing in tables
   106 \index{lambda abs@$\lambda$-abstractions!in CTT}
   107 \begin{center}
   108 \begin{tabular}{llrrr} 
   109   \it symbol &\it name     &\it meta-type & \it priority & \it description \\
   110   \sdx{lam} & \cdx{lambda}  & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
   111 \end{tabular}
   112 \end{center}
   113 \subcaption{Binders} 
   114 
   115 \begin{center}
   116 \index{*"` symbol}\index{function applications!in CTT}
   117 \index{*"+ symbol}
   118 \begin{tabular}{rrrr} 
   119   \it symbol & \it meta-type    & \it priority & \it description \\ 
   120   \tt `         & $[i,i]\to i$  & Left 55       & function application\\
   121   \tt +         & $[t,t]\to t$  & Right 30      & sum of two types
   122 \end{tabular}
   123 \end{center}
   124 \subcaption{Infixes}
   125 
   126 \index{*"* symbol}
   127 \index{*"-"-"> symbol}
   128 \begin{center} \tt\frenchspacing
   129 \begin{tabular}{rrr} 
   130   \it external                  & \it internal  & \it standard notation \\ 
   131   \sdx{PROD} $x$:$A$ . $B[x]$   &  Prod($A$, $\lambda x. B[x]$) &
   132         \rm product $\prod@{x\in A}B[x]$ \\
   133   \sdx{SUM} $x$:$A$ . $B[x]$    & Sum($A$, $\lambda x. B[x]$) &
   134         \rm sum $\sum@{x\in A}B[x]$ \\
   135   $A$ --> $B$     &  Prod($A$, $\lambda x. B$) &
   136         \rm function space $A\to B$ \\
   137   $A$ * $B$       &  Sum($A$, $\lambda x. B$)  &
   138         \rm binary product $A\times B$
   139 \end{tabular}
   140 \end{center}
   141 \subcaption{Translations} 
   142 
   143 \index{*"= symbol}
   144 \begin{center}
   145 \dquotes
   146 \[ \begin{array}{rcl}
   147 prop    & = &  type " type"       \\
   148         & | & type " = " type     \\
   149         & | & term " : " type        \\
   150         & | & term " = " term " : " type 
   151 \\[2ex]
   152 type    & = & \hbox{expression of type~$t$} \\
   153         & | & "PROD~" id " : " type " . " type  \\
   154         & | & "SUM~~" id " : " type " . " type 
   155 \\[2ex]
   156 term    & = & \hbox{expression of type~$i$} \\
   157         & | & "lam " id~id^* " . " term   \\
   158         & | & "< " term " , " term " >"
   159 \end{array} 
   160 \]
   161 \end{center}
   162 \subcaption{Grammar}
   163 \caption{Syntax of CTT} \label{ctt-syntax}
   164 \end{figure}
   165 
   166 %%%%\section{Generic Packages}  typedsimp.ML????????????????
   167 
   168 
   169 \section{Syntax}
   170 The constants are shown in Fig.\ts\ref{ctt-constants}.  The infixes include
   171 the function application operator (sometimes called `apply'), and the 2-place
   172 type operators.  Note that meta-level abstraction and application, $\lambda
   173 x.b$ and $f(a)$, differ from object-level abstraction and application,
   174 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$.  A CTT function~$f$ is simply an
   175 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
   176 $i\To i$.
   177 
   178 The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
   179 et al.~\cite{nordstrom90}.  The empty type is called $F$ and the one-element
   180 type is $T$; other finite types are built as $T+T+T$, etc.
   181 
   182 \index{*SUM symbol}\index{*PROD symbol}
   183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
   184 products $\prod@{x\in A}B[x]$.  Instead of {\tt Sum($A$,$B$)} and {\tt
   185   Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
   186   PROD $x$:$A$.\ $B[x]$}.  For example, we may write
   187 \begin{ttbox}
   188 SUM y:B. PROD x:A. C(x,y)   {\rm for}   Sum(B, \%y. Prod(A, \%x. C(x,y)))
   189 \end{ttbox}
   190 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate
   191 general sums and products over a constant family.\footnote{Unlike normal
   192 infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are
   193 no constants~{\tt op~*} and~\hbox{\tt op~-->}.}  Isabelle accepts these
   194 abbreviations in parsing and uses them whenever possible for printing.
   195 
   196 
   197 \begin{figure} 
   198 \begin{ttbox}
   199 \tdx{refl_type}         A type ==> A = A
   200 \tdx{refl_elem}         a : A ==> a = a : A
   201 
   202 \tdx{sym_type}          A = B ==> B = A
   203 \tdx{sym_elem}          a = b : A ==> b = a : A
   204 
   205 \tdx{trans_type}        [| A = B;  B = C |] ==> A = C
   206 \tdx{trans_elem}        [| a = b : A;  b = c : A |] ==> a = c : A
   207 
   208 \tdx{equal_types}       [| a : A;  A = B |] ==> a : B
   209 \tdx{equal_typesL}      [| a = b : A;  A = B |] ==> a = b : B
   210 
   211 \tdx{subst_type}        [| a : A;  !!z. z:A ==> B(z) type |] ==> B(a) type
   212 \tdx{subst_typeL}       [| a = c : A;  !!z. z:A ==> B(z) = D(z) 
   213                   |] ==> B(a) = D(c)
   214 
   215 \tdx{subst_elem}        [| a : A;  !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
   216 \tdx{subst_elemL}       [| a = c : A;  !!z. z:A ==> b(z) = d(z) : B(z) 
   217                   |] ==> b(a) = d(c) : B(a)
   218 
   219 \tdx{refl_red}          Reduce(a,a)
   220 \tdx{red_if_equal}      a = b : A ==> Reduce(a,b)
   221 \tdx{trans_red}         [| a = b : A;  Reduce(b,c) |] ==> a = c : A
   222 \end{ttbox}
   223 \caption{General equality rules} \label{ctt-equality}
   224 \end{figure}
   225 
   226 
   227 \begin{figure} 
   228 \begin{ttbox}
   229 \tdx{NF}        N type
   230 
   231 \tdx{NI0}       0 : N
   232 \tdx{NI_succ}   a : N ==> succ(a) : N
   233 \tdx{NI_succL}  a = b : N ==> succ(a) = succ(b) : N
   234 
   235 \tdx{NE}        [| p: N;  a: C(0);  
   236              !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) 
   237           |] ==> rec(p, a, \%u v. b(u,v)) : C(p)
   238 
   239 \tdx{NEL}       [| p = q : N;  a = c : C(0);  
   240              !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
   241           |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p)
   242 
   243 \tdx{NC0}       [| a: C(0);  
   244              !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
   245           |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0)
   246 
   247 \tdx{NC_succ}   [| p: N;  a: C(0);  
   248              !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) 
   249           |] ==> rec(succ(p), a, \%u v. b(u,v)) =
   250                  b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p))
   251 
   252 \tdx{zero_ne_succ}      [| a: N;  0 = succ(a) : N |] ==> 0: F
   253 \end{ttbox}
   254 \caption{Rules for type~$N$} \label{ctt-N}
   255 \end{figure}
   256 
   257 
   258 \begin{figure} 
   259 \begin{ttbox}
   260 \tdx{ProdF}     [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
   261 \tdx{ProdFL}    [| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
   262           PROD x:A. B(x) = PROD x:C. D(x)
   263 
   264 \tdx{ProdI}     [| A type;  !!x. x:A ==> b(x):B(x)
   265           |] ==> lam x. b(x) : PROD x:A. B(x)
   266 \tdx{ProdIL}    [| A type;  !!x. x:A ==> b(x) = c(x) : B(x)
   267           |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)
   268 
   269 \tdx{ProdE}     [| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)
   270 \tdx{ProdEL}    [| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)
   271 
   272 \tdx{ProdC}     [| a : A;  !!x. x:A ==> b(x) : B(x)
   273           |] ==> (lam x. b(x)) ` a = b(a) : B(a)
   274 
   275 \tdx{ProdC2}    p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)
   276 \end{ttbox}
   277 \caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}
   278 \end{figure}
   279 
   280 
   281 \begin{figure} 
   282 \begin{ttbox}
   283 \tdx{SumF}      [| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
   284 \tdx{SumFL}     [| A = C;  !!x. x:A ==> B(x) = D(x) 
   285           |] ==> SUM x:A. B(x) = SUM x:C. D(x)
   286 
   287 \tdx{SumI}      [| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)
   288 \tdx{SumIL}     [| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)
   289 
   290 \tdx{SumE}      [| p: SUM x:A. B(x);  
   291              !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) 
   292           |] ==> split(p, \%x y. c(x,y)) : C(p)
   293 
   294 \tdx{SumEL}     [| p=q : SUM x:A. B(x); 
   295              !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
   296           |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p)
   297 
   298 \tdx{SumC}      [| a: A;  b: B(a);
   299              !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
   300           |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>)
   301 
   302 \tdx{fst_def}   fst(a) == split(a, \%x y. x)
   303 \tdx{snd_def}   snd(a) == split(a, \%x y. y)
   304 \end{ttbox}
   305 \caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
   306 \end{figure}
   307 
   308 
   309 \begin{figure} 
   310 \begin{ttbox}
   311 \tdx{PlusF}       [| A type;  B type |] ==> A+B type
   312 \tdx{PlusFL}      [| A = C;  B = D |] ==> A+B = C+D
   313 
   314 \tdx{PlusI_inl}   [| a : A;  B type |] ==> inl(a) : A+B
   315 \tdx{PlusI_inlL}  [| a = c : A;  B type |] ==> inl(a) = inl(c) : A+B
   316 
   317 \tdx{PlusI_inr}   [| A type;  b : B |] ==> inr(b) : A+B
   318 \tdx{PlusI_inrL}  [| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B
   319 
   320 \tdx{PlusE}     [| p: A+B;
   321              !!x. x:A ==> c(x): C(inl(x));  
   322              !!y. y:B ==> d(y): C(inr(y))
   323           |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p)
   324 
   325 \tdx{PlusEL}    [| p = q : A+B;
   326              !!x. x: A ==> c(x) = e(x) : C(inl(x));   
   327              !!y. y: B ==> d(y) = f(y) : C(inr(y))
   328           |] ==> when(p, \%x. c(x), \%y. d(y)) = 
   329                  when(q, \%x. e(x), \%y. f(y)) : C(p)
   330 
   331 \tdx{PlusC_inl} [| a: A;
   332              !!x. x:A ==> c(x): C(inl(x));  
   333              !!y. y:B ==> d(y): C(inr(y))
   334           |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a))
   335 
   336 \tdx{PlusC_inr} [| b: B;
   337              !!x. x:A ==> c(x): C(inl(x));  
   338              !!y. y:B ==> d(y): C(inr(y))
   339           |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b))
   340 \end{ttbox}
   341 \caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
   342 \end{figure}
   343 
   344 
   345 \begin{figure} 
   346 \begin{ttbox}
   347 \tdx{FF}        F type
   348 \tdx{FE}        [| p: F;  C type |] ==> contr(p) : C
   349 \tdx{FEL}       [| p = q : F;  C type |] ==> contr(p) = contr(q) : C
   350 
   351 \tdx{TF}        T type
   352 \tdx{TI}        tt : T
   353 \tdx{TE}        [| p : T;  c : C(tt) |] ==> c : C(p)
   354 \tdx{TEL}       [| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)
   355 \tdx{TC}        p : T ==> p = tt : T)
   356 \end{ttbox}
   357 
   358 \caption{Rules for types $F$ and $T$} \label{ctt-ft}
   359 \end{figure}
   360 
   361 
   362 \begin{figure} 
   363 \begin{ttbox}
   364 \tdx{EqF}       [| A type;  a : A;  b : A |] ==> Eq(A,a,b) type
   365 \tdx{EqFL}      [| A=B;  a=c: A;  b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
   366 \tdx{EqI}       a = b : A ==> eq : Eq(A,a,b)
   367 \tdx{EqE}       p : Eq(A,a,b) ==> a = b : A
   368 \tdx{EqC}       p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
   369 \end{ttbox}
   370 \caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}
   371 \end{figure}
   372 
   373 
   374 \begin{figure} 
   375 \begin{ttbox}
   376 \tdx{replace_type}    [| B = A;  a : A |] ==> a : B
   377 \tdx{subst_eqtyparg}  [| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
   378 
   379 \tdx{subst_prodE}     [| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z)
   380                 |] ==> c(p`a): C(p`a)
   381 
   382 \tdx{SumIL2}    [| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
   383 
   384 \tdx{SumE_fst}  p : Sum(A,B) ==> fst(p) : A
   385 
   386 \tdx{SumE_snd}  [| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type
   387           |] ==> snd(p) : B(fst(p))
   388 \end{ttbox}
   389 
   390 \caption{Derived rules for CTT} \label{ctt-derived}
   391 \end{figure}
   392 
   393 
   394 \section{Rules of inference}
   395 The rules obey the following naming conventions.  Type formation rules have
   396 the suffix~{\tt F}\@.  Introduction rules have the suffix~{\tt I}\@.
   397 Elimination rules have the suffix~{\tt E}\@.  Computation rules, which
   398 describe the reduction of eliminators, have the suffix~{\tt C}\@.  The
   399 equality versions of the rules (which permit reductions on subterms) are
   400 called {\bf long} rules; their names have the suffix~{\tt L}\@.
   401 Introduction and computation rules are often further suffixed with
   402 constructor names.
   403 
   404 Figure~\ref{ctt-equality} presents the equality rules.  Most of them are
   405 straightforward: reflexivity, symmetry, transitivity and substitution.  The
   406 judgement \cdx{Reduce} does not belong to Type Theory proper; it has
   407 been added to implement rewriting.  The judgement ${\tt Reduce}(a,b)$ holds
   408 when $a=b:A$ holds.  It also holds when $a$ and $b$ are syntactically
   409 identical, even if they are ill-typed, because rule {\tt refl_red} does
   410 not verify that $a$ belongs to $A$.  
   411 
   412 The {\tt Reduce} rules do not give rise to new theorems about the standard
   413 judgements.  The only rule with {\tt Reduce} in a premise is
   414 {\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus
   415 $c$) are well-typed.
   416 
   417 Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.
   418 They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$.  This is
   419 the fourth Peano axiom and cannot be derived without universes \cite[page
   420 91]{martinlof84}.  
   421 
   422 The constant \cdx{rec} constructs proof terms when mathematical
   423 induction, rule~\tdx{NE}, is applied.  It can also express primitive
   424 recursion.  Since \cdx{rec} can be applied to higher-order functions,
   425 it can even express Ackermann's function, which is not primitive recursive
   426 \cite[page~104]{thompson91}.
   427 
   428 Figure~\ref{ctt-prod} shows the rules for general product types, which
   429 include function types as a special case.  The rules correspond to the
   430 predicate calculus rules for universal quantifiers and implication.  They
   431 also permit reasoning about functions, with the rules of a typed
   432 $\lambda$-calculus.
   433 
   434 Figure~\ref{ctt-sum} shows the rules for general sum types, which
   435 include binary product types as a special case.  The rules correspond to the
   436 predicate calculus rules for existential quantifiers and conjunction.  They
   437 also permit reasoning about ordered pairs, with the projections
   438 \cdx{fst} and~\cdx{snd}.
   439 
   440 Figure~\ref{ctt-plus} shows the rules for binary sum types.  They
   441 correspond to the predicate calculus rules for disjunction.  They also
   442 permit reasoning about disjoint sums, with the injections \cdx{inl}
   443 and~\cdx{inr} and case analysis operator~\cdx{when}.
   444 
   445 Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$
   446 and~$T$.  They correspond to the predicate calculus rules for absurdity and
   447 truth.
   448 
   449 Figure~\ref{ctt-eq} shows the rules for equality types.  If $a=b\in A$ is
   450 provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,
   451 and vice versa.  These rules define extensional equality; the most recent
   452 versions of Type Theory use intensional equality~\cite{nordstrom90}.
   453 
   454 Figure~\ref{ctt-derived} presents the derived rules.  The rule
   455 \tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use
   456 in backwards proof.  The rules \tdx{SumE_fst} and \tdx{SumE_snd}
   457 express the typing of~\cdx{fst} and~\cdx{snd}; together, they are
   458 roughly equivalent to~{\tt SumE} with the advantage of creating no
   459 parameters.  Section~\ref{ctt-choice} below demonstrates these rules in a
   460 proof of the Axiom of Choice.
   461 
   462 All the rules are given in $\eta$-expanded form.  For instance, every
   463 occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the
   464 rules for~$N$.  The expanded form permits Isabelle to preserve bound
   465 variable names during backward proof.  Names of bound variables in the
   466 conclusion (here, $u$ and~$v$) are matched with corresponding bound
   467 variables in the premises.
   468 
   469 
   470 \section{Rule lists}
   471 The Type Theory tactics provide rewriting, type inference, and logical
   472 reasoning.  Many proof procedures work by repeatedly resolving certain Type
   473 Theory rules against a proof state.  CTT defines lists --- each with
   474 type
   475 \hbox{\tt thm list} --- of related rules. 
   476 \begin{ttdescription}
   477 \item[\ttindexbold{form_rls}] 
   478 contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
   479 $F$, and $T$.
   480 
   481 \item[\ttindexbold{formL_rls}] 
   482 contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$.  (For
   483 other types use \tdx{refl_type}.)
   484 
   485 \item[\ttindexbold{intr_rls}] 
   486 contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
   487 $T$.
   488 
   489 \item[\ttindexbold{intrL_rls}] 
   490 contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$.  (For
   491 $T$ use \tdx{refl_elem}.)
   492 
   493 \item[\ttindexbold{elim_rls}] 
   494 contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
   495 $F$.  The rules for $Eq$ and $T$ are omitted because they involve no
   496 eliminator.
   497 
   498 \item[\ttindexbold{elimL_rls}] 
   499 contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$.
   500 
   501 \item[\ttindexbold{comp_rls}] 
   502 contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$.
   503 Those for $Eq$ and $T$ involve no eliminator.
   504 
   505 \item[\ttindexbold{basic_defs}] 
   506 contains the definitions of {\tt fst} and {\tt snd}.  
   507 \end{ttdescription}
   508 
   509 
   510 \section{Tactics for subgoal reordering}
   511 \begin{ttbox}
   512 test_assume_tac : int -> tactic
   513 typechk_tac     : thm list -> tactic
   514 equal_tac       : thm list -> tactic
   515 intr_tac        : thm list -> tactic
   516 \end{ttbox}
   517 Blind application of CTT rules seldom leads to a proof.  The elimination
   518 rules, especially, create subgoals containing new unknowns.  These subgoals
   519 unify with anything, creating a huge search space.  The standard tactic
   520 \ttindex{filt_resolve_tac}
   521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
   522         {\S\ref{filt_resolve_tac}})
   523 %
   524 fails for goals that are too flexible; so does the CTT tactic {\tt
   525   test_assume_tac}.  Used with the tactical \ttindex{REPEAT_FIRST} they
   526 achieve a simple kind of subgoal reordering: the less flexible subgoals are
   527 attempted first.  Do some single step proofs, or study the examples below,
   528 to see why this is necessary.
   529 \begin{ttdescription}
   530 \item[\ttindexbold{test_assume_tac} $i$] 
   531 uses {\tt assume_tac} to solve the subgoal by assumption, but only if
   532 subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.
   533 Otherwise, it fails.
   534 
   535 \item[\ttindexbold{typechk_tac} $thms$] 
   536 uses $thms$ with formation, introduction, and elimination rules to check
   537 the typing of constructions.  It is designed to solve goals of the form
   538 $a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
   539 performs type inference.  The tactic can also solve goals of
   540 the form $A\;\rm type$.
   541 
   542 \item[\ttindexbold{equal_tac} $thms$]
   543 uses $thms$ with the long introduction and elimination rules to solve goals
   544 of the form $a=b\in A$, where $a$ is rigid.  It is intended for deriving
   545 the long rules for defined constants such as the arithmetic operators.  The
   546 tactic can also perform type-checking.
   547 
   548 \item[\ttindexbold{intr_tac} $thms$]
   549 uses $thms$ with the introduction rules to break down a type.  It is
   550 designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
   551 rigid.  These typically arise when trying to prove a proposition~$A$,
   552 expressed as a type.
   553 \end{ttdescription}
   554 
   555 
   556 
   557 \section{Rewriting tactics}
   558 \begin{ttbox}
   559 rew_tac     : thm list -> tactic
   560 hyp_rew_tac : thm list -> tactic
   561 \end{ttbox}
   562 Object-level simplification is accomplished through proof, using the {\tt
   563   CTT} equality rules and the built-in rewriting functor
   564 {\tt TSimpFun}.%
   565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt
   566     TSimpFun} is only useful for CTT and similar logics with type inference
   567   rules.  At present it is undocumented.}
   568 %
   569 The rewrites include the computation rules and other equations.  The long
   570 versions of the other rules permit rewriting of subterms and subtypes.
   571 Also used are transitivity and the extra judgement form \cdx{Reduce}.
   572 Meta-level simplification handles only definitional equality.
   573 \begin{ttdescription}
   574 \item[\ttindexbold{rew_tac} $thms$]
   575 applies $thms$ and the computation rules as left-to-right rewrites.  It
   576 solves the goal $a=b\in A$ by rewriting $a$ to $b$.  If $b$ is an unknown
   577 then it is assigned the rewritten form of~$a$.  All subgoals are rewritten.
   578 
   579 \item[\ttindexbold{hyp_rew_tac} $thms$]
   580 is like {\tt rew_tac}, but includes as rewrites any equations present in
   581 the assumptions.
   582 \end{ttdescription}
   583 
   584 
   585 \section{Tactics for logical reasoning}
   586 Interpreting propositions as types lets CTT express statements of
   587 intuitionistic logic.  However, Constructive Type Theory is not just another
   588 syntax for first-order logic.  There are fundamental differences.
   589 
   590 \index{assumptions!in CTT}
   591 Can assumptions be deleted after use?  Not every occurrence of a type
   592 represents a proposition, and Type Theory assumptions declare variables.
   593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
   594 creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
   595 can be deleted safely.  In Type Theory, $+$-elimination with the assumption
   596 $z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in
   597 B$ (for arbitrary $x$ and $y$).  Deleting $z\in A+B$ when other assumptions
   598 refer to $z$ may render the subgoal unprovable: arguably,
   599 meaningless.
   600 
   601 Isabelle provides several tactics for predicate calculus reasoning in CTT:
   602 \begin{ttbox}
   603 mp_tac       : int -> tactic
   604 add_mp_tac   : int -> tactic
   605 safestep_tac : thm list -> int -> tactic
   606 safe_tac     : thm list -> int -> tactic
   607 step_tac     : thm list -> int -> tactic
   608 pc_tac       : thm list -> int -> tactic
   609 \end{ttbox}
   610 These are loosely based on the intuitionistic proof procedures
   611 of~\thydx{FOL}.  For the reasons discussed above, a rule that is safe for
   612 propositional reasoning may be unsafe for type-checking; thus, some of the
   613 `safe' tactics are misnamed.
   614 \begin{ttdescription}
   615 \item[\ttindexbold{mp_tac} $i$] 
   616 searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
   617 $a\in A$, where~$A$ may be found by unification.  It replaces
   618 $f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter.  The tactic
   619 can produce multiple outcomes for each suitable pair of assumptions.  In
   620 short, {\tt mp_tac} performs Modus Ponens among the assumptions.
   621 
   622 \item[\ttindexbold{add_mp_tac} $i$]
   623 is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$.  It
   624 avoids information loss but obviously loops if repeated.
   625 
   626 \item[\ttindexbold{safestep_tac} $thms$ $i$]
   627 attacks subgoal~$i$ using formation rules and certain other `safe' rules
   628 (\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling
   629 {\tt mp_tac} when appropriate.  It also uses~$thms$,
   630 which are typically premises of the rule being derived.
   631 
   632 \item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by
   633   means of backtracking, using {\tt safestep_tac}.
   634 
   635 \item[\ttindexbold{step_tac} $thms$ $i$]
   636 tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe
   637 rules.  It may produce multiple outcomes.
   638 
   639 \item[\ttindexbold{pc_tac} $thms$ $i$]
   640 tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}.
   641 \end{ttdescription}
   642 
   643 
   644 
   645 \begin{figure} 
   646 \index{#+@{\tt\#+} symbol}
   647 \index{*"- symbol}
   648 \index{"|"-@{{\tt"|"-"|} symbol}}
   649 \index{#*@{\tt\#*} symbol}
   650 \index{*div symbol}
   651 \index{*mod symbol}
   652 \begin{constants}
   653   \it symbol  & \it meta-type & \it priority & \it description \\ 
   654   \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\
   655   \tt div       & $[i,i]\To i$  &  Left 70      & division\\
   656   \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\
   657   \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\
   658   \tt -         & $[i,i]\To i$  &  Left 65      & subtraction\\
   659   \verb'|-|'    & $[i,i]\To i$  &  Left 65      & absolute difference
   660 \end{constants}
   661 
   662 \begin{ttbox}
   663 \tdx{add_def}           a#+b  == rec(a, b, \%u v. succ(v))  
   664 \tdx{diff_def}          a-b   == rec(b, a, \%u v. rec(v, 0, \%x y. x))  
   665 \tdx{absdiff_def}       a|-|b == (a-b) #+ (b-a)  
   666 \tdx{mult_def}          a#*b  == rec(a, 0, \%u v. b #+ v)  
   667 
   668 \tdx{mod_def}           a mod b ==
   669                   rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
   670 
   671 \tdx{div_def}           a div b ==
   672                   rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
   673 
   674 \tdx{add_typing}        [| a:N;  b:N |] ==> a #+ b : N
   675 \tdx{addC0}             b:N ==> 0 #+ b = b : N
   676 \tdx{addC_succ}         [| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
   677 
   678 \tdx{add_assoc}         [| a:N;  b:N;  c:N |] ==> 
   679                   (a #+ b) #+ c = a #+ (b #+ c) : N
   680 
   681 \tdx{add_commute}       [| a:N;  b:N |] ==> a #+ b = b #+ a : N
   682 
   683 \tdx{mult_typing}       [| a:N;  b:N |] ==> a #* b : N
   684 \tdx{multC0}            b:N ==> 0 #* b = 0 : N
   685 \tdx{multC_succ}        [| a:N;  b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
   686 \tdx{mult_commute}      [| a:N;  b:N |] ==> a #* b = b #* a : N
   687 
   688 \tdx{add_mult_dist}     [| a:N;  b:N;  c:N |] ==> 
   689                   (a #+ b) #* c = (a #* c) #+ (b #* c) : N
   690 
   691 \tdx{mult_assoc}        [| a:N;  b:N;  c:N |] ==> 
   692                   (a #* b) #* c = a #* (b #* c) : N
   693 
   694 \tdx{diff_typing}       [| a:N;  b:N |] ==> a - b : N
   695 \tdx{diffC0}            a:N ==> a - 0 = a : N
   696 \tdx{diff_0_eq_0}       b:N ==> 0 - b = 0 : N
   697 \tdx{diff_succ_succ}    [| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N
   698 \tdx{diff_self_eq_0}    a:N ==> a - a = 0 : N
   699 \tdx{add_inverse_diff}  [| a:N;  b:N;  b-a=0 : N |] ==> b #+ (a-b) = a : N
   700 \end{ttbox}
   701 \caption{The theory of arithmetic} \label{ctt_arith}
   702 \end{figure}
   703 
   704 
   705 \section{A theory of arithmetic}
   706 \thydx{Arith} is a theory of elementary arithmetic.  It proves the
   707 properties of addition, multiplication, subtraction, division, and
   708 remainder, culminating in the theorem
   709 \[ a \bmod b + (a/b)\times b = a. \]
   710 Figure~\ref{ctt_arith} presents the definitions and some of the key
   711 theorems, including commutative, distributive, and associative laws.
   712 
   713 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
   714 and~\verb'div' stand for sum, difference, absolute difference, product,
   715 remainder and quotient, respectively.  Since Type Theory has only primitive
   716 recursion, some of their definitions may be obscure.  
   717 
   718 The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
   719 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
   720 
   721 The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
   722 as the successor of~$b-1$.  Absolute difference is used to test the
   723 equality $succ(v)=b$.
   724 
   725 The quotient $a/b$ is computed by adding one for every number $x$
   726 such that $0\leq x \leq a$ and $x\bmod b = 0$.
   727 
   728 
   729 
   730 \section{The examples directory}
   731 This directory contains examples and experimental proofs in CTT.
   732 \begin{ttdescription}
   733 \item[CTT/ex/typechk.ML]
   734 contains simple examples of type-checking and type deduction.
   735 
   736 \item[CTT/ex/elim.ML]
   737 contains some examples from Martin-L\"of~\cite{martinlof84}, proved using 
   738 {\tt pc_tac}.
   739 
   740 \item[CTT/ex/equal.ML]
   741 contains simple examples of rewriting.
   742 
   743 \item[CTT/ex/synth.ML]
   744 demonstrates the use of unknowns with some trivial examples of program
   745 synthesis. 
   746 \end{ttdescription}
   747 
   748 
   749 \section{Example: type inference}
   750 Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
   751 is a term and $\Var{A}$ is an unknown standing for its type.  The type,
   752 initially
   753 unknown, takes shape in the course of the proof.  Our example is the
   754 predecessor function on the natural numbers.
   755 \begin{ttbox}
   756 Goal "lam n. rec(n, 0, \%x y. x) : ?A";
   757 {\out Level 0}
   758 {\out lam n. rec(n,0,\%x y. x) : ?A}
   759 {\out  1. lam n. rec(n,0,\%x y. x) : ?A}
   760 \end{ttbox}
   761 Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
   762 be confused with a meta-level abstraction), we apply the rule
   763 \tdx{ProdI}, for $\Pi$-introduction.  This instantiates~$\Var{A}$ to a
   764 product type of unknown domain and range.
   765 \begin{ttbox}
   766 by (resolve_tac [ProdI] 1);
   767 {\out Level 1}
   768 {\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)}
   769 {\out  1. ?A1 type}
   770 {\out  2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)}
   771 \end{ttbox}
   772 Subgoal~1 is too flexible.  It can be solved by instantiating~$\Var{A@1}$
   773 to any type, but most instantiations will invalidate subgoal~2.  We
   774 therefore tackle the latter subgoal.  It asks the type of a term beginning
   775 with {\tt rec}, which can be found by $N$-elimination.%
   776 \index{*NE theorem}
   777 \begin{ttbox}
   778 by (eresolve_tac [NE] 2);
   779 {\out Level 2}
   780 {\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)}
   781 {\out  1. N type}
   782 {\out  2. !!n. 0 : ?C2(n,0)}
   783 {\out  3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))}
   784 \end{ttbox}
   785 Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
   786 natural numbers.  However, let us continue proving nontrivial subgoals.
   787 Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
   788 \begin{ttbox}
   789 by (resolve_tac [NI0] 2);
   790 {\out Level 3}
   791 {\out lam n. rec(n,0,\%x y. x) : N --> N}
   792 {\out  1. N type}
   793 {\out  2. !!n x y. [| x : N; y : N |] ==> x : N}
   794 \end{ttbox}
   795 The type~$\Var{A}$ is now fully determined.  It is the product type
   796 $\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
   797 there is no dependence on~$x$.  But we must prove all the subgoals to show
   798 that the original term is validly typed.  Subgoal~2 is provable by
   799 assumption and the remaining subgoal falls by $N$-formation.%
   800 \index{*NF theorem}
   801 \begin{ttbox}
   802 by (assume_tac 2);
   803 {\out Level 4}
   804 {\out lam n. rec(n,0,\%x y. x) : N --> N}
   805 {\out  1. N type}
   806 \ttbreak
   807 by (resolve_tac [NF] 1);
   808 {\out Level 5}
   809 {\out lam n. rec(n,0,\%x y. x) : N --> N}
   810 {\out No subgoals!}
   811 \end{ttbox}
   812 Calling \ttindex{typechk_tac} can prove this theorem in one step.
   813 
   814 Even if the original term is ill-typed, one can infer a type for it, but
   815 unprovable subgoals will be left.  As an exercise, try to prove the
   816 following invalid goal:
   817 \begin{ttbox}
   818 Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
   819 \end{ttbox}
   820 
   821 
   822 
   823 \section{An example of logical reasoning}
   824 Logical reasoning in Type Theory involves proving a goal of the form
   825 $\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands
   826 for its proof term, a value of type $A$.  The proof term is initially
   827 unknown and takes shape during the proof.  
   828 
   829 Our example expresses a theorem about quantifiers in a sorted logic:
   830 \[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
   831          {\ex{x\in A}P(x)\disj Q(x)} 
   832 \]
   833 By the propositions-as-types principle, this is encoded
   834 using~$\Sigma$ and~$+$ types.  A special case of it expresses a
   835 distributive law of Type Theory: 
   836 \[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
   837 Generalizing this from $\times$ to $\Sigma$, and making the typing
   838 conditions explicit, yields the rule we must derive:
   839 \[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
   840          {\hbox{$A$ type} &
   841           \infer*{\hbox{$B(x)$ type}}{[x\in A]}  &
   842           \infer*{\hbox{$C(x)$ type}}{[x\in A]}  &
   843           p\in \sum@{x\in A} B(x)+C(x)} 
   844 \]
   845 To begin, we bind the rule's premises --- returned by the~{\tt goal}
   846 command --- to the {\ML} variable~{\tt prems}.
   847 \begin{ttbox}
   848 val prems = Goal
   849     "[| A type;                       \ttback
   850 \ttback       !!x. x:A ==> B(x) type;       \ttback
   851 \ttback       !!x. x:A ==> C(x) type;       \ttback
   852 \ttback       p: SUM x:A. B(x) + C(x)       \ttback
   853 \ttback    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
   854 {\out Level 0}
   855 {\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   856 {\out  1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   857 \ttbreak
   858 {\out val prems = ["A type  [A type]",}
   859 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
   860 {\out              "?x : A ==> C(?x) type  [!!x. x : A ==> C(x) type]",}
   861 {\out              "p : SUM x:A. B(x) + C(x)  [p : SUM x:A. B(x) + C(x)]"]}
   862 {\out             : thm list}
   863 \end{ttbox}
   864 The last premise involves the sum type~$\Sigma$.  Since it is a premise
   865 rather than the assumption of a goal, it cannot be found by {\tt
   866   eresolve_tac}.  We could insert it (and the other atomic premise) by
   867 calling
   868 \begin{ttbox}
   869 cut_facts_tac prems 1;
   870 \end{ttbox}
   871 A forward proof step is more straightforward here.  Let us resolve the
   872 $\Sigma$-elimination rule with the premises using~\ttindex{RL}.  This
   873 inference yields one result, which we supply to {\tt
   874   resolve_tac}.\index{*SumE theorem}
   875 \begin{ttbox}
   876 by (resolve_tac (prems RL [SumE]) 1);
   877 {\out Level 1}
   878 {\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   879 {\out  1. !!x y.}
   880 {\out        [| x : A; y : B(x) + C(x) |] ==>}
   881 {\out        ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   882 \end{ttbox}
   883 The subgoal has two new parameters, $x$ and~$y$.  In the main goal,
   884 $\Var{a}$ has been instantiated with a \cdx{split} term.  The
   885 assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
   886 creating the parameter~$xa$.  This inference also inserts~\cdx{when}
   887 into the main goal.\index{*PlusE theorem}
   888 \begin{ttbox}
   889 by (eresolve_tac [PlusE] 1);
   890 {\out Level 2}
   891 {\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))}
   892 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   893 {\out  1. !!x y xa.}
   894 {\out        [| x : A; xa : B(x) |] ==>}
   895 {\out        ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   896 \ttbreak
   897 {\out  2. !!x y ya.}
   898 {\out        [| x : A; ya : C(x) |] ==>}
   899 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   900 \end{ttbox}
   901 To complete the proof object for the main goal, we need to instantiate the
   902 terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$.  We attack subgoal~1 by
   903 a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
   904 injection~(\cdx{inl}).
   905 \index{*PlusI_inl theorem}
   906 \begin{ttbox}
   907 by (resolve_tac [PlusI_inl] 1);
   908 {\out Level 3}
   909 {\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
   910 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   911 {\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
   912 {\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
   913 \ttbreak
   914 {\out  3. !!x y ya.}
   915 {\out        [| x : A; ya : C(x) |] ==>}
   916 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   917 \end{ttbox}
   918 A new subgoal~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
   919 Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.
   920 This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains
   921 an ordered pair, whose components are two new unknowns.%
   922 \index{*SumI theorem}
   923 \begin{ttbox}
   924 by (resolve_tac [SumI] 1);
   925 {\out Level 4}
   926 {\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
   927 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   928 {\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
   929 {\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
   930 {\out  3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
   931 {\out  4. !!x y ya.}
   932 {\out        [| x : A; ya : C(x) |] ==>}
   933 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   934 \end{ttbox}
   935 The two new subgoals both hold by assumption.  Observe how the unknowns
   936 $\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state.
   937 \begin{ttbox}
   938 by (assume_tac 1);
   939 {\out Level 5}
   940 {\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
   941 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   942 \ttbreak
   943 {\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)}
   944 {\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
   945 {\out  3. !!x y ya.}
   946 {\out        [| x : A; ya : C(x) |] ==>}
   947 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   948 \ttbreak
   949 by (assume_tac 1);
   950 {\out Level 6}
   951 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
   952 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   953 {\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
   954 {\out  2. !!x y ya.}
   955 {\out        [| x : A; ya : C(x) |] ==>}
   956 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   957 \end{ttbox}
   958 Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.
   959 Such subgoals are usually trivial; this one yields to
   960 \ttindex{typechk_tac}, given the current list of premises.
   961 \begin{ttbox}
   962 by (typechk_tac prems);
   963 {\out Level 7}
   964 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
   965 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   966 {\out  1. !!x y ya.}
   967 {\out        [| x : A; ya : C(x) |] ==>}
   968 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   969 \end{ttbox}
   970 This subgoal is the other case from the $+$-elimination above, and can be
   971 proved similarly.  Quicker is to apply \ttindex{pc_tac}.  The main goal
   972 finally gets a fully instantiated proof object.
   973 \begin{ttbox}
   974 by (pc_tac prems 1);
   975 {\out Level 8}
   976 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))}
   977 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
   978 {\out No subgoals!}
   979 \end{ttbox}
   980 Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
   981 proves this theorem.
   982 
   983 
   984 \section{Example: deriving a currying functional}
   985 In simply-typed languages such as {\ML}, a currying functional has the type 
   986 \[ (A\times B \to C) \to (A\to (B\to C)). \]
   987 Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.  
   988 The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
   989 to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
   990 $C(\langle x,y\rangle)$.
   991 
   992 Formally, there are three typing premises.  $A$ is a type; $B$ is an
   993 $A$-indexed family of types; $C$ is a family of types indexed by
   994 $\Sigma(A,B)$.  The goal is expressed using \hbox{\tt PROD f} to ensure
   995 that the parameter corresponding to the functional's argument is really
   996 called~$f$; Isabelle echoes the type using \verb|-->| because there is no
   997 explicit dependence upon~$f$.
   998 \begin{ttbox}
   999 val prems = Goal
  1000     "[| A type; !!x. x:A ==> B(x) type;                           \ttback
  1001 \ttback               !!z. z: (SUM x:A. B(x)) ==> C(z) type             \ttback
  1002 \ttback    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).      \ttback
  1003 \ttback                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
  1004 \ttbreak
  1005 {\out Level 0}
  1006 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
  1007 {\out      (PROD x:A. PROD y:B(x). C(<x,y>))}
  1008 {\out  1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
  1009 {\out          (PROD x:A. PROD y:B(x). C(<x,y>))}
  1010 \ttbreak
  1011 {\out val prems = ["A type  [A type]",}
  1012 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
  1013 {\out              "?z : SUM x:A. B(x) ==> C(?z) type}
  1014 {\out               [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
  1015 \end{ttbox}
  1016 This is a chance to demonstrate \ttindex{intr_tac}.  Here, the tactic
  1017 repeatedly applies $\Pi$-introduction and proves the rather
  1018 tiresome typing conditions.  
  1019 
  1020 Note that $\Var{a}$ becomes instantiated to three nested
  1021 $\lambda$-abstractions.  It would be easier to read if the bound variable
  1022 names agreed with the parameters in the subgoal.  Isabelle attempts to give
  1023 parameters the same names as corresponding bound variables in the goal, but
  1024 this does not always work.  In any event, the goal is logically correct.
  1025 \begin{ttbox}
  1026 by (intr_tac prems);
  1027 {\out Level 1}
  1028 {\out lam x xa xb. ?b7(x,xa,xb)}
  1029 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
  1030 {\out  1. !!f x y.}
  1031 {\out        [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
  1032 {\out        ?b7(f,x,y) : C(<x,y>)}
  1033 \end{ttbox}
  1034 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
  1035 \index{*ProdE theorem}
  1036 \begin{ttbox}
  1037 by (eresolve_tac [ProdE] 1);
  1038 {\out Level 2}
  1039 {\out lam x xa xb. x ` <xa,xb>}
  1040 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
  1041 {\out  1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
  1042 \end{ttbox}
  1043 Finally, we verify that the argument's type is suitable for the function
  1044 application.  This is straightforward using introduction rules.
  1045 \index{*intr_tac}
  1046 \begin{ttbox}
  1047 by (intr_tac prems);
  1048 {\out Level 3}
  1049 {\out lam x xa xb. x ` <xa,xb>}
  1050 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
  1051 {\out No subgoals!}
  1052 \end{ttbox}
  1053 Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
  1054 also prove an example by Martin-L\"of, related to $\disj$-elimination
  1055 \cite[page~58]{martinlof84}.
  1056 
  1057 
  1058 \section{Example: proving the Axiom of Choice} \label{ctt-choice}
  1059 Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
  1060 which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
  1061 Interpreting propositions as types, this asserts that for all $x\in A$
  1062 there exists $y\in B(x)$ such that $C(x,y)$.  The Axiom of Choice asserts
  1063 that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
  1064 $C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
  1065 function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
  1066 
  1067 In principle, the Axiom of Choice is simple to derive in Constructive Type
  1068 Theory.  The following definitions work:
  1069 \begin{eqnarray*}
  1070     f & \equiv & {\tt fst} \circ h \\
  1071     g & \equiv & {\tt snd} \circ h
  1072 \end{eqnarray*}
  1073 But a completely formal proof is hard to find.  The rules can be applied in
  1074 countless ways, yielding many higher-order unifiers.  The proof can get
  1075 bogged down in the details.  But with a careful selection of derived rules
  1076 (recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
  1077 prove the theorem in nine steps.
  1078 \begin{ttbox}
  1079 val prems = Goal
  1080     "[| A type;  !!x. x:A ==> B(x) type;                    \ttback
  1081 \ttback       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type            \ttback
  1082 \ttback    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    \ttback
  1083 \ttback                     (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
  1084 {\out Level 0}
  1085 {\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1086 {\out      (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1087 {\out  1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1088 {\out          (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1089 \ttbreak
  1090 {\out val prems = ["A type  [A type]",}
  1091 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
  1092 {\out              "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
  1093 {\out               [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
  1094 {\out             : thm list}
  1095 \end{ttbox}
  1096 First, \ttindex{intr_tac} applies introduction rules and performs routine
  1097 type-checking.  This instantiates~$\Var{a}$ to a construction involving
  1098 a $\lambda$-abstraction and an ordered pair.  The pair's components are
  1099 themselves $\lambda$-abstractions and there is a subgoal for each.
  1100 \begin{ttbox}
  1101 by (intr_tac prems);
  1102 {\out Level 1}
  1103 {\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
  1104 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1105 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1106 \ttbreak
  1107 {\out  1. !!h x.}
  1108 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1109 {\out        ?b7(h,x) : B(x)}
  1110 \ttbreak
  1111 {\out  2. !!h x.}
  1112 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1113 {\out        ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)}
  1114 \end{ttbox}
  1115 Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
  1116 $\Var{b@7}(h,x)\in B(x)$.  Subgoal~2 asks, given $x\in A$, for a proof
  1117 object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
  1118 result lie in the relation~$C$.  This latter task will take up most of the
  1119 proof.
  1120 \index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}
  1121 \begin{ttbox}
  1122 by (eresolve_tac [ProdE RS SumE_fst] 1);
  1123 {\out Level 2}
  1124 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
  1125 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1126 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1127 \ttbreak
  1128 {\out  1. !!h x. x : A ==> x : A}
  1129 {\out  2. !!h x.}
  1130 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1131 {\out        ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
  1132 \end{ttbox}
  1133 Above, we have composed {\tt fst} with the function~$h$.  Unification
  1134 has deduced that the function must be applied to $x\in A$.  We have our
  1135 choice function.
  1136 \begin{ttbox}
  1137 by (assume_tac 1);
  1138 {\out Level 3}
  1139 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
  1140 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1141 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1142 {\out  1. !!h x.}
  1143 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1144 {\out        ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
  1145 \end{ttbox}
  1146 Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
  1147 simplified.  The derived rule \tdx{replace_type} lets us replace a type
  1148 by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
  1149 \begin{ttbox}
  1150 by (resolve_tac [replace_type] 1);
  1151 {\out Level 4}
  1152 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
  1153 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1154 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1155 \ttbreak
  1156 {\out  1. !!h x.}
  1157 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1158 {\out        C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)}
  1159 \ttbreak
  1160 {\out  2. !!h x.}
  1161 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1162 {\out        ?b8(h,x) : ?A13(h,x)}
  1163 \end{ttbox}
  1164 The derived rule \tdx{subst_eqtyparg} lets us simplify a type's
  1165 argument (by currying, $C(x)$ is a unary type operator):
  1166 \begin{ttbox}
  1167 by (resolve_tac [subst_eqtyparg] 1);
  1168 {\out Level 5}
  1169 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
  1170 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1171 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1172 \ttbreak
  1173 {\out  1. !!h x.}
  1174 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1175 {\out        (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)}
  1176 \ttbreak
  1177 {\out  2. !!h x z.}
  1178 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
  1179 {\out           z : ?A14(h,x) |] ==>}
  1180 {\out        C(x,z) type}
  1181 \ttbreak
  1182 {\out  3. !!h x.}
  1183 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1184 {\out        ?b8(h,x) : C(x,?c14(h,x))}
  1185 \end{ttbox}
  1186 Subgoal~1 requires simply $\beta$-contraction, which is the rule
  1187 \tdx{ProdC}.  The term $\Var{c@{14}}(h,x)$ in the last subgoal
  1188 receives the contracted result.
  1189 \begin{ttbox}
  1190 by (resolve_tac [ProdC] 1);
  1191 {\out Level 6}
  1192 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
  1193 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1194 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1195 \ttbreak
  1196 {\out  1. !!h x.}
  1197 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1198 {\out        x : ?A15(h,x)}
  1199 \ttbreak
  1200 {\out  2. !!h x xa.}
  1201 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
  1202 {\out           xa : ?A15(h,x) |] ==>}
  1203 {\out        fst(h ` xa) : ?B15(h,x,xa)}
  1204 \ttbreak
  1205 {\out  3. !!h x z.}
  1206 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
  1207 {\out           z : ?B15(h,x,x) |] ==>}
  1208 {\out        C(x,z) type}
  1209 \ttbreak
  1210 {\out  4. !!h x.}
  1211 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1212 {\out        ?b8(h,x) : C(x,fst(h ` x))}
  1213 \end{ttbox}
  1214 Routine type-checking goals proliferate in Constructive Type Theory, but
  1215 \ttindex{typechk_tac} quickly solves them.  Note the inclusion of
  1216 \tdx{SumE_fst} along with the premises.
  1217 \begin{ttbox}
  1218 by (typechk_tac (SumE_fst::prems));
  1219 {\out Level 7}
  1220 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
  1221 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1222 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1223 \ttbreak
  1224 {\out  1. !!h x.}
  1225 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1226 {\out        ?b8(h,x) : C(x,fst(h ` x))}
  1227 \end{ttbox}
  1228 We are finally ready to compose {\tt snd} with~$h$.
  1229 \index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}
  1230 \begin{ttbox}
  1231 by (eresolve_tac [ProdE RS SumE_snd] 1);
  1232 {\out Level 8}
  1233 {\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
  1234 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1235 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1236 \ttbreak
  1237 {\out  1. !!h x. x : A ==> x : A}
  1238 {\out  2. !!h x. x : A ==> B(x) type}
  1239 {\out  3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
  1240 \end{ttbox}
  1241 The proof object has reached its final form.  We call \ttindex{typechk_tac}
  1242 to finish the type-checking.
  1243 \begin{ttbox}
  1244 by (typechk_tac prems);
  1245 {\out Level 9}
  1246 {\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
  1247 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1248 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
  1249 {\out No subgoals!}
  1250 \end{ttbox}
  1251 It might be instructive to compare this proof with Martin-L\"of's forward
  1252 proof of the Axiom of Choice \cite[page~50]{martinlof84}.
  1253 
  1254 \index{Constructive Type Theory|)}