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