author  paulson 
Fri, 08 Jan 1999 14:02:04 +0100  
changeset 6072  5583261db33d 
parent 5151  1e944fe5ce96 
child 6170  9a59cf8ae9b5 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Constructive Type Theory} 

314  3 
\index{Constructive Type Theory(} 
4 

104  5 
MartinL\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can 
6 
be viewed at many different levels. It is a formal system that embodies 

7 
the principles of intuitionistic mathematics; it embodies the 

8 
interpretation of propositions as types; it is a vehicle for deriving 

314  9 
programs from proofs. 
10 

11 
Thompson's book~\cite{thompson91} gives a readable and thorough account of 

12 
Type Theory. Nuprl is an elaborate implementation~\cite{constable86}. 

13 
{\sc alf} is a more recent tool that allows proof terms to be edited 

14 
directly~\cite{alf}. 

104  15 

16 
Isabelle's original formulation of Type Theory was a kind of sequent 

17 
calculus, following MartinL\"of~\cite{martinlof84}. It included rules for 

18 
building the context, namely variable bindings with their types. A typical 

19 
judgement was 

20 
\[ a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \; 

21 
[ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n1}) ] 

22 
\] 

23 
This sequent calculus was not satisfactory because assumptions like 

24 
`suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$' 

25 
could not be formalized. 

26 

314  27 
The theory~\thydx{CTT} implements Constructive Type Theory, using 
104  28 
natural deduction. The judgement above is expressed using $\Forall$ and 
29 
$\Imp$: 

30 
\[ \begin{array}{r@{}l} 

31 
\Forall x@1\ldots x@n. & 

111  32 
\List{x@1\in A@1; 
33 
x@2\in A@2(x@1); \cdots \; 

34 
x@n\in A@n(x@1,\ldots,x@{n1})} \Imp \\ 

104  35 
& \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) 
36 
\end{array} 

37 
\] 

38 
Assumptions can use all the judgement forms, for instance to express that 

39 
$B$ is a family of types over~$A$: 

40 
\[ \Forall x . x\in A \Imp B(x)\;{\rm type} \] 

41 
To justify the {\CTT} formulation it is probably best to appeal directly 

42 
to the semantic explanations of the rules~\cite{martinlof84}, rather than 

43 
to the rules themselves. The order of assumptions no longer matters, 

44 
unlike in standard Type Theory. Contexts, which are typical of many modern 

45 
type theories, are difficult to represent in Isabelle. In particular, it 

46 
is difficult to enforce that all the variables in a context are distinct. 

314  47 
\index{assumptions!in {\CTT}} 
104  48 

314  49 
The theory does not use polymorphism. Terms in {\CTT} have type~\tydx{i}, the 
50 
type of individuals. Types in {\CTT} have type~\tydx{t}. 

51 

52 
\begin{figure} \tabcolsep=1em %wider spacing in tables 

53 
\begin{center} 

54 
\begin{tabular}{rrr} 

55 
\it name & \it metatype & \it description \\ 

56 
\cdx{Type} & $t \to prop$ & judgement form \\ 

57 
\cdx{Eqtype} & $[t,t]\to prop$ & judgement form\\ 

58 
\cdx{Elem} & $[i, t]\to prop$ & judgement form\\ 

59 
\cdx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\ 

60 
\cdx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex] 

104  61 

314  62 
\cdx{N} & $t$ & natural numbers type\\ 
63 
\cdx{0} & $i$ & constructor\\ 

64 
\cdx{succ} & $i\to i$ & constructor\\ 

65 
\cdx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex] 

66 
\cdx{Prod} & $[t,i\to t]\to t$ & general product type\\ 

67 
\cdx{lambda} & $(i\to i)\to i$ & constructor\\[2ex] 

68 
\cdx{Sum} & $[t, i\to t]\to t$ & general sum type\\ 

69 
\cdx{pair} & $[i,i]\to i$ & constructor\\ 

70 
\cdx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\ 

71 
\cdx{fst} \cdx{snd} & $i\to i$ & projections\\[2ex] 

72 
\cdx{inl} \cdx{inr} & $i\to i$ & constructors for $+$\\ 

73 
\cdx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex] 

74 
\cdx{Eq} & $[t,i,i]\to t$ & equality type\\ 

75 
\cdx{eq} & $i$ & constructor\\[2ex] 

76 
\cdx{F} & $t$ & empty type\\ 

77 
\cdx{contr} & $i\to i$ & eliminator\\[2ex] 

78 
\cdx{T} & $t$ & singleton type\\ 

79 
\cdx{tt} & $i$ & constructor 

80 
\end{tabular} 

81 
\end{center} 

82 
\caption{The constants of {\CTT}} \label{cttconstants} 

83 
\end{figure} 

84 

85 

86 
{\CTT} supports all of Type Theory apart from list types, wellordering 

104  87 
types, and universes. Universes could be introduced {\em\`a la Tarski}, 
88 
adding new constants as names for types. The formulation {\em\`a la 

314  89 
Russell}, where types denote themselves, is only possible if we identify 
90 
the metatypes~{\tt i} and~{\tt t}. Most published formulations of 

91 
wellordering types have difficulties involving extensionality of 

92 
functions; I suggest that you use some other method for defining recursive 

93 
types. List types are easy to introduce by declaring new rules. 

104  94 

95 
{\CTT} uses the 1982 version of Type Theory, with extensional equality. 

96 
The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are 

97 
interchangeable. Its rewriting tactics prove theorems of the form $a=b\in 

98 
A$. It could be modified to have intensional equality, but rewriting 

99 
tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the 

314  100 
computation rules might require a separate simplifier. 
104  101 

102 

103 
\begin{figure} \tabcolsep=1em %wider spacing in tables 

314  104 
\index{lambda abs@$\lambda$abstractions!in \CTT} 
104  105 
\begin{center} 
106 
\begin{tabular}{llrrr} 

314  107 
\it symbol &\it name &\it metatype & \it priority & \it description \\ 
108 
\sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$abstraction 

104  109 
\end{tabular} 
110 
\end{center} 

111 
\subcaption{Binders} 

112 

113 
\begin{center} 

314  114 
\index{*"` symbol}\index{function applications!in \CTT} 
115 
\index{*"+ symbol} 

104  116 
\begin{tabular}{rrrr} 
314  117 
\it symbol & \it metatype & \it priority & \it description \\ 
111  118 
\tt ` & $[i,i]\to i$ & Left 55 & function application\\ 
119 
\tt + & $[t,t]\to t$ & Right 30 & sum of two types 

104  120 
\end{tabular} 
121 
\end{center} 

122 
\subcaption{Infixes} 

123 

314  124 
\index{*"* symbol} 
125 
\index{*"""> symbol} 

104  126 
\begin{center} \tt\frenchspacing 
127 
\begin{tabular}{rrr} 

111  128 
\it external & \it internal & \it standard notation \\ 
5151  129 
\sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) & 
111  130 
\rm product $\prod@{x\in A}B[x]$ \\ 
5151  131 
\sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x. B[x]$) & 
111  132 
\rm sum $\sum@{x\in A}B[x]$ \\ 
5151  133 
$A$ > $B$ & Prod($A$, $\lambda x. B$) & 
111  134 
\rm function space $A\to B$ \\ 
5151  135 
$A$ * $B$ & Sum($A$, $\lambda x. B$) & 
111  136 
\rm binary product $A\times B$ 
104  137 
\end{tabular} 
138 
\end{center} 

139 
\subcaption{Translations} 

140 

314  141 
\index{*"= symbol} 
104  142 
\begin{center} 
143 
\dquotes 

144 
\[ \begin{array}{rcl} 

111  145 
prop & = & type " type" \\ 
146 
&  & type " = " type \\ 

147 
&  & term " : " type \\ 

148 
&  & term " = " term " : " type 

104  149 
\\[2ex] 
111  150 
type & = & \hbox{expression of type~$t$} \\ 
151 
&  & "PROD~" id " : " type " . " type \\ 

152 
&  & "SUM~~" id " : " type " . " type 

104  153 
\\[2ex] 
111  154 
term & = & \hbox{expression of type~$i$} \\ 
155 
&  & "lam " id~id^* " . " term \\ 

156 
&  & "< " term " , " term " >" 

104  157 
\end{array} 
158 
\] 

159 
\end{center} 

160 
\subcaption{Grammar} 

161 
\caption{Syntax of {\CTT}} \label{cttsyntax} 

162 
\end{figure} 

163 

164 
%%%%\section{Generic Packages} typedsimp.ML???????????????? 

165 

166 

167 
\section{Syntax} 

284  168 
The constants are shown in Fig.\ts\ref{cttconstants}. The infixes include 
104  169 
the function application operator (sometimes called `apply'), and the 
170 
2place type operators. Note that metalevel abstraction and application, 

171 
$\lambda x.b$ and $f(a)$, differ from objectlevel abstraction and 

5151  172 
application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT} 
104  173 
function~$f$ is simply an individual as far as Isabelle is concerned: its 
174 
Isabelle type is~$i$, not say $i\To i$. 

175 

314  176 
The notation for~{\CTT} (Fig.\ts\ref{cttsyntax}) is based on that of 
177 
Nordstr\"om et al.~\cite{nordstrom90}. The empty type is called $F$ and 

178 
the oneelement type is $T$; other finite types are built as $T+T+T$, etc. 

179 

180 
\index{*SUM symbol}\index{*PROD symbol} 

6072  181 
Quantification is expressed by sums $\sum@{x\in A}B[x]$ and 
314  182 
products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt 
6072  183 
Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt 
184 
PROD $x$:$A$.\ $B[x]$}. For example, we may write 

104  185 
\begin{ttbox} 
284  186 
SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y))) 
104  187 
\end{ttbox} 
188 
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$>$B$} abbreviate 

189 
general sums and products over a constant family.\footnote{Unlike normal 

190 
infix operators, {\tt*} and {\tt>} merely define abbreviations; there are 

191 
no constants~{\tt op~*} and~\hbox{\tt op~>}.} Isabelle accepts these 

192 
abbreviations in parsing and uses them whenever possible for printing. 

193 

194 

195 
\begin{figure} 

196 
\begin{ttbox} 

314  197 
\tdx{refl_type} A type ==> A = A 
198 
\tdx{refl_elem} a : A ==> a = a : A 

104  199 

314  200 
\tdx{sym_type} A = B ==> B = A 
201 
\tdx{sym_elem} a = b : A ==> b = a : A 

104  202 

314  203 
\tdx{trans_type} [ A = B; B = C ] ==> A = C 
204 
\tdx{trans_elem} [ a = b : A; b = c : A ] ==> a = c : A 

104  205 

314  206 
\tdx{equal_types} [ a : A; A = B ] ==> a : B 
207 
\tdx{equal_typesL} [ a = b : A; A = B ] ==> a = b : B 

104  208 

314  209 
\tdx{subst_type} [ a : A; !!z. z:A ==> B(z) type ] ==> B(a) type 
210 
\tdx{subst_typeL} [ a = c : A; !!z. z:A ==> B(z) = D(z) 

104  211 
] ==> B(a) = D(c) 
212 

314  213 
\tdx{subst_elem} [ a : A; !!z. z:A ==> b(z):B(z) ] ==> b(a):B(a) 
214 
\tdx{subst_elemL} [ a = c : A; !!z. z:A ==> b(z) = d(z) : B(z) 

104  215 
] ==> b(a) = d(c) : B(a) 
216 

314  217 
\tdx{refl_red} Reduce(a,a) 
218 
\tdx{red_if_equal} a = b : A ==> Reduce(a,b) 

219 
\tdx{trans_red} [ a = b : A; Reduce(b,c) ] ==> a = c : A 

104  220 
\end{ttbox} 
221 
\caption{General equality rules} \label{cttequality} 

222 
\end{figure} 

223 

224 

225 
\begin{figure} 

226 
\begin{ttbox} 

314  227 
\tdx{NF} N type 
104  228 

314  229 
\tdx{NI0} 0 : N 
230 
\tdx{NI_succ} a : N ==> succ(a) : N 

231 
\tdx{NI_succL} a = b : N ==> succ(a) = succ(b) : N 

104  232 

314  233 
\tdx{NE} [ p: N; a: C(0); 
104  234 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u)) 
5151  235 
] ==> rec(p, a, \%u v. b(u,v)) : C(p) 
104  236 

314  237 
\tdx{NEL} [ p = q : N; a = c : C(0); 
104  238 
!!u v. [ u: N; v: C(u) ] ==> b(u,v)=d(u,v): C(succ(u)) 
5151  239 
] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p) 
104  240 

314  241 
\tdx{NC0} [ a: C(0); 
104  242 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u)) 
5151  243 
] ==> rec(0, a, \%u v. b(u,v)) = a : C(0) 
104  244 

314  245 
\tdx{NC_succ} [ p: N; a: C(0); 
104  246 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u)) 
5151  247 
] ==> rec(succ(p), a, \%u v. b(u,v)) = 
248 
b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p)) 

104  249 

314  250 
\tdx{zero_ne_succ} [ a: N; 0 = succ(a) : N ] ==> 0: F 
104  251 
\end{ttbox} 
252 
\caption{Rules for type~$N$} \label{cttN} 

253 
\end{figure} 

254 

255 

256 
\begin{figure} 

257 
\begin{ttbox} 

5151  258 
\tdx{ProdF} [ A type; !!x. x:A ==> B(x) type ] ==> PROD x:A. B(x) type 
314  259 
\tdx{ProdFL} [ A = C; !!x. x:A ==> B(x) = D(x) ] ==> 
5151  260 
PROD x:A. B(x) = PROD x:C. D(x) 
104  261 

314  262 
\tdx{ProdI} [ A type; !!x. x:A ==> b(x):B(x) 
5151  263 
] ==> lam x. b(x) : PROD x:A. B(x) 
314  264 
\tdx{ProdIL} [ A type; !!x. x:A ==> b(x) = c(x) : B(x) 
5151  265 
] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x) 
104  266 

5151  267 
\tdx{ProdE} [ p : PROD x:A. B(x); a : A ] ==> p`a : B(a) 
268 
\tdx{ProdEL} [ p=q: PROD x:A. B(x); a=b : A ] ==> p`a = q`b : B(a) 

104  269 

314  270 
\tdx{ProdC} [ a : A; !!x. x:A ==> b(x) : B(x) 
5151  271 
] ==> (lam x. b(x)) ` a = b(a) : B(a) 
104  272 

5151  273 
\tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x) 
104  274 
\end{ttbox} 
314  275 
\caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{cttprod} 
104  276 
\end{figure} 
277 

278 

279 
\begin{figure} 

280 
\begin{ttbox} 

5151  281 
\tdx{SumF} [ A type; !!x. x:A ==> B(x) type ] ==> SUM x:A. B(x) type 
314  282 
\tdx{SumFL} [ A = C; !!x. x:A ==> B(x) = D(x) 
5151  283 
] ==> SUM x:A. B(x) = SUM x:C. D(x) 
104  284 

5151  285 
\tdx{SumI} [ a : A; b : B(a) ] ==> <a,b> : SUM x:A. B(x) 
286 
\tdx{SumIL} [ a=c:A; b=d:B(a) ] ==> <a,b> = <c,d> : SUM x:A. B(x) 

104  287 

5151  288 
\tdx{SumE} [ p: SUM x:A. B(x); 
104  289 
!!x y. [ x:A; y:B(x) ] ==> c(x,y): C(<x,y>) 
5151  290 
] ==> split(p, \%x y. c(x,y)) : C(p) 
104  291 

5151  292 
\tdx{SumEL} [ p=q : SUM x:A. B(x); 
104  293 
!!x y. [ x:A; y:B(x) ] ==> c(x,y)=d(x,y): C(<x,y>) 
5151  294 
] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p) 
104  295 

314  296 
\tdx{SumC} [ a: A; b: B(a); 
104  297 
!!x y. [ x:A; y:B(x) ] ==> c(x,y): C(<x,y>) 
5151  298 
] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>) 
104  299 

5151  300 
\tdx{fst_def} fst(a) == split(a, \%x y. x) 
301 
\tdx{snd_def} snd(a) == split(a, \%x y. y) 

104  302 
\end{ttbox} 
314  303 
\caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{cttsum} 
104  304 
\end{figure} 
305 

306 

307 
\begin{figure} 

308 
\begin{ttbox} 

314  309 
\tdx{PlusF} [ A type; B type ] ==> A+B type 
310 
\tdx{PlusFL} [ A = C; B = D ] ==> A+B = C+D 

104  311 

314  312 
\tdx{PlusI_inl} [ a : A; B type ] ==> inl(a) : A+B 
313 
\tdx{PlusI_inlL} [ a = c : A; B type ] ==> inl(a) = inl(c) : A+B 

104  314 

314  315 
\tdx{PlusI_inr} [ A type; b : B ] ==> inr(b) : A+B 
316 
\tdx{PlusI_inrL} [ A type; b = d : B ] ==> inr(b) = inr(d) : A+B 

104  317 

314  318 
\tdx{PlusE} [ p: A+B; 
104  319 
!!x. x:A ==> c(x): C(inl(x)); 
320 
!!y. y:B ==> d(y): C(inr(y)) 

5151  321 
] ==> when(p, \%x. c(x), \%y. d(y)) : C(p) 
104  322 

314  323 
\tdx{PlusEL} [ p = q : A+B; 
104  324 
!!x. x: A ==> c(x) = e(x) : C(inl(x)); 
325 
!!y. y: B ==> d(y) = f(y) : C(inr(y)) 

5151  326 
] ==> when(p, \%x. c(x), \%y. d(y)) = 
327 
when(q, \%x. e(x), \%y. f(y)) : C(p) 

104  328 

314  329 
\tdx{PlusC_inl} [ a: A; 
104  330 
!!x. x:A ==> c(x): C(inl(x)); 
331 
!!y. y:B ==> d(y): C(inr(y)) 

5151  332 
] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a)) 
104  333 

314  334 
\tdx{PlusC_inr} [ b: B; 
104  335 
!!x. x:A ==> c(x): C(inl(x)); 
336 
!!y. y:B ==> d(y): C(inr(y)) 

5151  337 
] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b)) 
104  338 
\end{ttbox} 
339 
\caption{Rules for the binary sum type $A+B$} \label{cttplus} 

340 
\end{figure} 

341 

342 

343 
\begin{figure} 

344 
\begin{ttbox} 

314  345 
\tdx{FF} F type 
346 
\tdx{FE} [ p: F; C type ] ==> contr(p) : C 

347 
\tdx{FEL} [ p = q : F; C type ] ==> contr(p) = contr(q) : C 

104  348 

314  349 
\tdx{TF} T type 
350 
\tdx{TI} tt : T 

351 
\tdx{TE} [ p : T; c : C(tt) ] ==> c : C(p) 

352 
\tdx{TEL} [ p = q : T; c = d : C(tt) ] ==> c = d : C(p) 

353 
\tdx{TC} p : T ==> p = tt : T) 

104  354 
\end{ttbox} 
355 

314  356 
\caption{Rules for types $F$ and $T$} \label{cttft} 
104  357 
\end{figure} 
358 

359 

360 
\begin{figure} 

361 
\begin{ttbox} 

314  362 
\tdx{EqF} [ A type; a : A; b : A ] ==> Eq(A,a,b) type 
363 
\tdx{EqFL} [ A=B; a=c: A; b=d : A ] ==> Eq(A,a,b) = Eq(B,c,d) 

364 
\tdx{EqI} a = b : A ==> eq : Eq(A,a,b) 

365 
\tdx{EqE} p : Eq(A,a,b) ==> a = b : A 

366 
\tdx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b) 

367 
\end{ttbox} 

368 
\caption{Rules for the equality type $Eq(A,a,b)$} \label{ctteq} 

369 
\end{figure} 

104  370 

314  371 

372 
\begin{figure} 

373 
\begin{ttbox} 

374 
\tdx{replace_type} [ B = A; a : A ] ==> a : B 

375 
\tdx{subst_eqtyparg} [ a=c : A; !!z. z:A ==> B(z) type ] ==> B(a)=B(c) 

376 

377 
\tdx{subst_prodE} [ p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) 

104  378 
] ==> c(p`a): C(p`a) 
379 

314  380 
\tdx{SumIL2} [ c=a : A; d=b : B(a) ] ==> <c,d> = <a,b> : Sum(A,B) 
104  381 

314  382 
\tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A 
104  383 

314  384 
\tdx{SumE_snd} [ p: Sum(A,B); A type; !!x. x:A ==> B(x) type 
104  385 
] ==> snd(p) : B(fst(p)) 
386 
\end{ttbox} 

387 

388 
\caption{Derived rules for {\CTT}} \label{cttderived} 

389 
\end{figure} 

390 

391 

392 
\section{Rules of inference} 

393 
The rules obey the following naming conventions. Type formation rules have 

394 
the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@. 

395 
Elimination rules have the suffix~{\tt E}\@. Computation rules, which 

396 
describe the reduction of eliminators, have the suffix~{\tt C}\@. The 

397 
equality versions of the rules (which permit reductions on subterms) are 

333  398 
called {\bf long} rules; their names have the suffix~{\tt L}\@. 
399 
Introduction and computation rules are often further suffixed with 

104  400 
constructor names. 
401 

314  402 
Figure~\ref{cttequality} presents the equality rules. Most of them are 
403 
straightforward: reflexivity, symmetry, transitivity and substitution. The 

404 
judgement \cdx{Reduce} does not belong to Type Theory proper; it has 

405 
been added to implement rewriting. The judgement ${\tt Reduce}(a,b)$ holds 

406 
when $a=b:A$ holds. It also holds when $a$ and $b$ are syntactically 

407 
identical, even if they are illtyped, because rule {\tt refl_red} does 

408 
not verify that $a$ belongs to $A$. 

409 

410 
The {\tt Reduce} rules do not give rise to new theorems about the standard 

411 
judgements. The only rule with {\tt Reduce} in a premise is 

412 
{\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus 

413 
$c$) are welltyped. 

414 

415 
Figure~\ref{cttN} presents the rules for~$N$, the type of natural numbers. 

416 
They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$. This is 

417 
the fourth Peano axiom and cannot be derived without universes \cite[page 

418 
91]{martinlof84}. 

419 

420 
The constant \cdx{rec} constructs proof terms when mathematical 

421 
induction, rule~\tdx{NE}, is applied. It can also express primitive 

422 
recursion. Since \cdx{rec} can be applied to higherorder functions, 

423 
it can even express Ackermann's function, which is not primitive recursive 

424 
\cite[page~104]{thompson91}. 

104  425 

314  426 
Figure~\ref{cttprod} shows the rules for general product types, which 
427 
include function types as a special case. The rules correspond to the 

428 
predicate calculus rules for universal quantifiers and implication. They 

429 
also permit reasoning about functions, with the rules of a typed 

430 
$\lambda$calculus. 

431 

432 
Figure~\ref{cttsum} shows the rules for general sum types, which 

433 
include binary product types as a special case. The rules correspond to the 

434 
predicate calculus rules for existential quantifiers and conjunction. They 

435 
also permit reasoning about ordered pairs, with the projections 

436 
\cdx{fst} and~\cdx{snd}. 

437 

438 
Figure~\ref{cttplus} shows the rules for binary sum types. They 

439 
correspond to the predicate calculus rules for disjunction. They also 

440 
permit reasoning about disjoint sums, with the injections \cdx{inl} 

441 
and~\cdx{inr} and case analysis operator~\cdx{when}. 

104  442 

314  443 
Figure~\ref{cttft} shows the rules for the empty and unit types, $F$ 
444 
and~$T$. They correspond to the predicate calculus rules for absurdity and 

445 
truth. 

446 

447 
Figure~\ref{ctteq} shows the rules for equality types. If $a=b\in A$ is 

448 
provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$, 

449 
and vice versa. These rules define extensional equality; the most recent 

450 
versions of Type Theory use intensional equality~\cite{nordstrom90}. 

451 

452 
Figure~\ref{cttderived} presents the derived rules. The rule 

453 
\tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use 

454 
in backwards proof. The rules \tdx{SumE_fst} and \tdx{SumE_snd} 

455 
express the typing of~\cdx{fst} and~\cdx{snd}; together, they are 

456 
roughly equivalent to~{\tt SumE} with the advantage of creating no 

457 
parameters. Section~\ref{cttchoice} below demonstrates these rules in a 

458 
proof of the Axiom of Choice. 

104  459 

460 
All the rules are given in $\eta$expanded form. For instance, every 

5151  461 
occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the 
314  462 
rules for~$N$. The expanded form permits Isabelle to preserve bound 
463 
variable names during backward proof. Names of bound variables in the 

464 
conclusion (here, $u$ and~$v$) are matched with corresponding bound 

465 
variables in the premises. 

104  466 

467 

468 
\section{Rule lists} 

469 
The Type Theory tactics provide rewriting, type inference, and logical 

470 
reasoning. Many proof procedures work by repeatedly resolving certain Type 

471 
Theory rules against a proof state. {\CTT} defines lists  each with 

472 
type 

473 
\hbox{\tt thm list}  of related rules. 

314  474 
\begin{ttdescription} 
104  475 
\item[\ttindexbold{form_rls}] 
476 
contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$, 

477 
$F$, and $T$. 

478 

479 
\item[\ttindexbold{formL_rls}] 

480 
contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$. (For 

314  481 
other types use \tdx{refl_type}.) 
104  482 

483 
\item[\ttindexbold{intr_rls}] 

484 
contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and 

485 
$T$. 

486 

487 
\item[\ttindexbold{intrL_rls}] 

488 
contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$. (For 

314  489 
$T$ use \tdx{refl_elem}.) 
104  490 

491 
\item[\ttindexbold{elim_rls}] 

492 
contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and 

493 
$F$. The rules for $Eq$ and $T$ are omitted because they involve no 

494 
eliminator. 

495 

496 
\item[\ttindexbold{elimL_rls}] 

497 
contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$. 

498 

499 
\item[\ttindexbold{comp_rls}] 

500 
contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$. 

501 
Those for $Eq$ and $T$ involve no eliminator. 

502 

503 
\item[\ttindexbold{basic_defs}] 

314  504 
contains the definitions of {\tt fst} and {\tt snd}. 
505 
\end{ttdescription} 

104  506 

507 

508 
\section{Tactics for subgoal reordering} 

509 
\begin{ttbox} 

510 
test_assume_tac : int > tactic 

511 
typechk_tac : thm list > tactic 

512 
equal_tac : thm list > tactic 

513 
intr_tac : thm list > tactic 

514 
\end{ttbox} 

515 
Blind application of {\CTT} rules seldom leads to a proof. The elimination 

516 
rules, especially, create subgoals containing new unknowns. These subgoals 

333  517 
unify with anything, creating a huge search space. The standard tactic 
314  518 
\ttindex{filt_resolve_tac} 
519 
(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% 

520 
{\S\ref{filt_resolve_tac}}) 

521 
% 

333  522 
fails for goals that are too flexible; so does the {\CTT} tactic {\tt 
314  523 
test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they 
524 
achieve a simple kind of subgoal reordering: the less flexible subgoals are 

525 
attempted first. Do some single step proofs, or study the examples below, 

526 
to see why this is necessary. 

527 
\begin{ttdescription} 

104  528 
\item[\ttindexbold{test_assume_tac} $i$] 
314  529 
uses {\tt assume_tac} to solve the subgoal by assumption, but only if 
104  530 
subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown. 
531 
Otherwise, it fails. 

532 

533 
\item[\ttindexbold{typechk_tac} $thms$] 

534 
uses $thms$ with formation, introduction, and elimination rules to check 

535 
the typing of constructions. It is designed to solve goals of the form 

975
6c280d1dac35
Corrected faulty reference to HindleyMilner type inference
lcp
parents:
333
diff
changeset

536 
$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it 
6c280d1dac35
Corrected faulty reference to HindleyMilner type inference
lcp
parents:
333
diff
changeset

537 
performs type inference. The tactic can also solve goals of 
104  538 
the form $A\;\rm type$. 
539 

540 
\item[\ttindexbold{equal_tac} $thms$] 

541 
uses $thms$ with the long introduction and elimination rules to solve goals 

542 
of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving 

543 
the long rules for defined constants such as the arithmetic operators. The 

544 
tactic can also perform type checking. 

545 

546 
\item[\ttindexbold{intr_tac} $thms$] 

547 
uses $thms$ with the introduction rules to break down a type. It is 

548 
designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$ 

549 
rigid. These typically arise when trying to prove a proposition~$A$, 

550 
expressed as a type. 

314  551 
\end{ttdescription} 
104  552 

553 

554 

555 
\section{Rewriting tactics} 

556 
\begin{ttbox} 

557 
rew_tac : thm list > tactic 

558 
hyp_rew_tac : thm list > tactic 

559 
\end{ttbox} 

560 
Objectlevel simplification is accomplished through proof, using the {\tt 

314  561 
CTT} equality rules and the builtin rewriting functor 
562 
{\tt TSimpFun}.% 

563 
\footnote{This should not be confused with Isabelle's main simplifier; {\tt 

564 
TSimpFun} is only useful for {\CTT} and similar logics with type 

565 
inference rules. At present it is undocumented.} 

566 
% 

567 
The rewrites include the computation rules and other equations. The long 

568 
versions of the other rules permit rewriting of subterms and subtypes. 

569 
Also used are transitivity and the extra judgement form \cdx{Reduce}. 

104  570 
Metalevel simplification handles only definitional equality. 
314  571 
\begin{ttdescription} 
104  572 
\item[\ttindexbold{rew_tac} $thms$] 
573 
applies $thms$ and the computation rules as lefttoright rewrites. It 

574 
solves the goal $a=b\in A$ by rewriting $a$ to $b$. If $b$ is an unknown 

575 
then it is assigned the rewritten form of~$a$. All subgoals are rewritten. 

576 

577 
\item[\ttindexbold{hyp_rew_tac} $thms$] 

578 
is like {\tt rew_tac}, but includes as rewrites any equations present in 

579 
the assumptions. 

314  580 
\end{ttdescription} 
104  581 

582 

583 
\section{Tactics for logical reasoning} 

584 
Interpreting propositions as types lets {\CTT} express statements of 

585 
intuitionistic logic. However, Constructive Type Theory is not just 

314  586 
another syntax for firstorder logic. There are fundamental differences. 
104  587 

314  588 
\index{assumptions!in {\CTT}} 
589 
Can assumptions be deleted after use? Not every occurrence of a type 

590 
represents a proposition, and Type Theory assumptions declare variables. 

104  591 
In firstorder logic, $\disj$elimination with the assumption $P\disj Q$ 
592 
creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$ 

314  593 
can be deleted safely. In Type Theory, $+$elimination with the assumption 
594 
$z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in 

595 
B$ (for arbitrary $x$ and $y$). Deleting $z\in A+B$ when other assumptions 

596 
refer to $z$ may render the subgoal unprovable: arguably, 

597 
meaningless. 

598 

599 
Isabelle provides several tactics for predicate calculus reasoning in \CTT: 

104  600 
\begin{ttbox} 
601 
mp_tac : int > tactic 

602 
add_mp_tac : int > tactic 

603 
safestep_tac : thm list > int > tactic 

604 
safe_tac : thm list > int > tactic 

605 
step_tac : thm list > int > tactic 

606 
pc_tac : thm list > int > tactic 

607 
\end{ttbox} 

608 
These are loosely based on the intuitionistic proof procedures 

314  609 
of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for 
104  610 
propositional reasoning may be unsafe for type checking; thus, some of the 
314  611 
`safe' tactics are misnamed. 
612 
\begin{ttdescription} 

104  613 
\item[\ttindexbold{mp_tac} $i$] 
614 
searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and 

615 
$a\in A$, where~$A$ may be found by unification. It replaces 

616 
$f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter. The tactic 

617 
can produce multiple outcomes for each suitable pair of assumptions. In 

618 
short, {\tt mp_tac} performs Modus Ponens among the assumptions. 

619 

620 
\item[\ttindexbold{add_mp_tac} $i$] 

314  621 
is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. It 
622 
avoids information loss but obviously loops if repeated. 

104  623 

624 
\item[\ttindexbold{safestep_tac} $thms$ $i$] 

625 
attacks subgoal~$i$ using formation rules and certain other `safe' rules 

333  626 
(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling 
104  627 
{\tt mp_tac} when appropriate. It also uses~$thms$, 
628 
which are typically premises of the rule being derived. 

629 

314  630 
\item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by 
631 
means of backtracking, using {\tt safestep_tac}. 

104  632 

633 
\item[\ttindexbold{step_tac} $thms$ $i$] 

634 
tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe 

635 
rules. It may produce multiple outcomes. 

636 

637 
\item[\ttindexbold{pc_tac} $thms$ $i$] 

638 
tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}. 

314  639 
\end{ttdescription} 
104  640 

641 

642 

643 
\begin{figure} 

314  644 
\index{#+@{\tt\#+} symbol} 
645 
\index{*" symbol} 

646 
\index{*""" symbol} 

647 
\index{#*@{\tt\#*} symbol} 

648 
\index{*div symbol} 

649 
\index{*mod symbol} 

650 
\begin{constants} 

651 
\it symbol & \it metatype & \it priority & \it description \\ 

652 
\tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ 

653 
\tt div & $[i,i]\To i$ & Left 70 & division\\ 

654 
\tt mod & $[i,i]\To i$ & Left 70 & modulus\\ 

655 
\tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ 

656 
\tt  & $[i,i]\To i$ & Left 65 & subtraction\\ 

657 
\verb'' & $[i,i]\To i$ & Left 65 & absolute difference 

658 
\end{constants} 

104  659 

660 
\begin{ttbox} 

5151  661 
\tdx{add_def} a#+b == rec(a, b, \%u v. succ(v)) 
662 
\tdx{diff_def} ab == rec(b, a, \%u v. rec(v, 0, \%x y. x)) 

314  663 
\tdx{absdiff_def} ab == (ab) #+ (ba) 
664 
\tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v) 

665 

666 
\tdx{mod_def} a mod b == 

5151  667 
rec(a, 0, \%u v. rec(succ(v)  b, 0, \%x y. succ(v))) 
104  668 

314  669 
\tdx{div_def} a div b == 
5151  670 
rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v)) 
314  671 

672 
\tdx{add_typing} [ a:N; b:N ] ==> a #+ b : N 

673 
\tdx{addC0} b:N ==> 0 #+ b = b : N 

674 
\tdx{addC_succ} [ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N 

675 

676 
\tdx{add_assoc} [ a:N; b:N; c:N ] ==> 

104  677 
(a #+ b) #+ c = a #+ (b #+ c) : N 
678 

314  679 
\tdx{add_commute} [ a:N; b:N ] ==> a #+ b = b #+ a : N 
104  680 

314  681 
\tdx{mult_typing} [ a:N; b:N ] ==> a #* b : N 
682 
\tdx{multC0} b:N ==> 0 #* b = 0 : N 

683 
\tdx{multC_succ} [ a:N; b:N ] ==> succ(a) #* b = b #+ (a#*b) : N 

684 
\tdx{mult_commute} [ a:N; b:N ] ==> a #* b = b #* a : N 

104  685 

314  686 
\tdx{add_mult_dist} [ a:N; b:N; c:N ] ==> 
104  687 
(a #+ b) #* c = (a #* c) #+ (b #* c) : N 
688 

314  689 
\tdx{mult_assoc} [ a:N; b:N; c:N ] ==> 
104  690 
(a #* b) #* c = a #* (b #* c) : N 
691 

314  692 
\tdx{diff_typing} [ a:N; b:N ] ==> a  b : N 
693 
\tdx{diffC0} a:N ==> a  0 = a : N 

694 
\tdx{diff_0_eq_0} b:N ==> 0  b = 0 : N 

695 
\tdx{diff_succ_succ} [ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N 

696 
\tdx{diff_self_eq_0} a:N ==> a  a = 0 : N 

697 
\tdx{add_inverse_diff} [ a:N; b:N; ba=0 : N ] ==> b #+ (ab) = a : N 

3136  698 
\end{ttbox} 
3096  699 
\caption{The theory of arithmetic} \label{ctt_arith} 
104  700 
\end{figure} 
701 

702 

703 
\section{A theory of arithmetic} 

314  704 
\thydx{Arith} is a theory of elementary arithmetic. It proves the 
104  705 
properties of addition, multiplication, subtraction, division, and 
706 
remainder, culminating in the theorem 

707 
\[ a \bmod b + (a/b)\times b = a. \] 

3096  708 
Figure~\ref{ctt_arith} presents the definitions and some of the key 
314  709 
theorems, including commutative, distributive, and associative laws. 
104  710 

111  711 
The operators~\verb'#+', \verb'', \verb'', \verb'#*', \verb'mod' 
712 
and~\verb'div' stand for sum, difference, absolute difference, product, 

104  713 
remainder and quotient, respectively. Since Type Theory has only primitive 
714 
recursion, some of their definitions may be obscure. 

715 

716 
The difference~$ab$ is computed by taking $b$ predecessors of~$a$, where 

5151  717 
the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$. 
104  718 

111  719 
The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0 
720 
as the successor of~$b1$. Absolute difference is used to test the 

721 
equality $succ(v)=b$. 

104  722 

111  723 
The quotient $a/b$ is computed by adding one for every number $x$ 
724 
such that $0\leq x \leq a$ and $x\bmod b = 0$. 

104  725 

726 

727 

728 
\section{The examples directory} 

729 
This directory contains examples and experimental proofs in {\CTT}. 

314  730 
\begin{ttdescription} 
731 
\item[CTT/ex/typechk.ML] 

104  732 
contains simple examples of type checking and type deduction. 
733 

314  734 
\item[CTT/ex/elim.ML] 
104  735 
contains some examples from MartinL\"of~\cite{martinlof84}, proved using 
736 
{\tt pc_tac}. 

737 

314  738 
\item[CTT/ex/equal.ML] 
104  739 
contains simple examples of rewriting. 
740 

314  741 
\item[CTT/ex/synth.ML] 
104  742 
demonstrates the use of unknowns with some trivial examples of program 
743 
synthesis. 

314  744 
\end{ttdescription} 
104  745 

746 

747 
\section{Example: type inference} 

748 
Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$ 

749 
is a term and $\Var{A}$ is an unknown standing for its type. The type, 

750 
initially 

751 
unknown, takes shape in the course of the proof. Our example is the 

752 
predecessor function on the natural numbers. 

753 
\begin{ttbox} 

5151  754 
Goal "lam n. rec(n, 0, \%x y. x) : ?A"; 
104  755 
{\out Level 0} 
284  756 
{\out lam n. rec(n,0,\%x y. x) : ?A} 
757 
{\out 1. lam n. rec(n,0,\%x y. x) : ?A} 

104  758 
\end{ttbox} 
759 
Since the term is a Constructive Type Theory $\lambda$abstraction (not to 

760 
be confused with a metalevel abstraction), we apply the rule 

314  761 
\tdx{ProdI}, for $\Pi$introduction. This instantiates~$\Var{A}$ to a 
104  762 
product type of unknown domain and range. 
763 
\begin{ttbox} 

764 
by (resolve_tac [ProdI] 1); 

765 
{\out Level 1} 

284  766 
{\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)} 
104  767 
{\out 1. ?A1 type} 
284  768 
{\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)} 
104  769 
\end{ttbox} 
284  770 
Subgoal~1 is too flexible. It can be solved by instantiating~$\Var{A@1}$ 
771 
to any type, but most instantiations will invalidate subgoal~2. We 

772 
therefore tackle the latter subgoal. It asks the type of a term beginning 

314  773 
with {\tt rec}, which can be found by $N$elimination.% 
774 
\index{*NE theorem} 

104  775 
\begin{ttbox} 
776 
by (eresolve_tac [NE] 2); 

777 
{\out Level 2} 

284  778 
{\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)} 
104  779 
{\out 1. N type} 
780 
{\out 2. !!n. 0 : ?C2(n,0)} 

781 
{\out 3. !!n x y. [ x : N; y : ?C2(n,x) ] ==> x : ?C2(n,succ(x))} 

782 
\end{ttbox} 

284  783 
Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of 
784 
natural numbers. However, let us continue proving nontrivial subgoals. 

314  785 
Subgoal~2 asks, what is the type of~0?\index{*NIO theorem} 
104  786 
\begin{ttbox} 
787 
by (resolve_tac [NI0] 2); 

788 
{\out Level 3} 

284  789 
{\out lam n. rec(n,0,\%x y. x) : N > N} 
104  790 
{\out 1. N type} 
791 
{\out 2. !!n x y. [ x : N; y : N ] ==> x : N} 

792 
\end{ttbox} 

284  793 
The type~$\Var{A}$ is now fully determined. It is the product type 
314  794 
$\prod@{x\in N}N$, which is shown as the function type $N\to N$ because 
284  795 
there is no dependence on~$x$. But we must prove all the subgoals to show 
796 
that the original term is validly typed. Subgoal~2 is provable by 

314  797 
assumption and the remaining subgoal falls by $N$formation.% 
798 
\index{*NF theorem} 

104  799 
\begin{ttbox} 
800 
by (assume_tac 2); 

801 
{\out Level 4} 

284  802 
{\out lam n. rec(n,0,\%x y. x) : N > N} 
104  803 
{\out 1. N type} 
284  804 
\ttbreak 
104  805 
by (resolve_tac [NF] 1); 
806 
{\out Level 5} 

284  807 
{\out lam n. rec(n,0,\%x y. x) : N > N} 
104  808 
{\out No subgoals!} 
809 
\end{ttbox} 

810 
Calling \ttindex{typechk_tac} can prove this theorem in one step. 

811 

284  812 
Even if the original term is illtyped, one can infer a type for it, but 
813 
unprovable subgoals will be left. As an exercise, try to prove the 

814 
following invalid goal: 

815 
\begin{ttbox} 

5151  816 
Goal "lam n. rec(n, 0, \%x y. tt) : ?A"; 
284  817 
\end{ttbox} 
818 

819 

104  820 

821 
\section{An example of logical reasoning} 

822 
Logical reasoning in Type Theory involves proving a goal of the form 

314  823 
$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands 
824 
for its proof term, a value of type $A$. The proof term is initially 

825 
unknown and takes shape during the proof. 

826 

827 
Our example expresses a theorem about quantifiers in a sorted logic: 

104  828 
\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))} 
829 
{\ex{x\in A}P(x)\disj Q(x)} 

830 
\] 

314  831 
By the propositionsastypes principle, this is encoded 
832 
using~$\Sigma$ and~$+$ types. A special case of it expresses a 

833 
distributive law of Type Theory: 

104  834 
\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \] 
835 
Generalizing this from $\times$ to $\Sigma$, and making the typing 

314  836 
conditions explicit, yields the rule we must derive: 
104  837 
\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))} 
838 
{\hbox{$A$ type} & 

839 
\infer*{\hbox{$B(x)$ type}}{[x\in A]} & 

840 
\infer*{\hbox{$C(x)$ type}}{[x\in A]} & 

841 
p\in \sum@{x\in A} B(x)+C(x)} 

842 
\] 

314  843 
To begin, we bind the rule's premises  returned by the~{\tt goal} 
844 
command  to the {\ML} variable~{\tt prems}. 

104  845 
\begin{ttbox} 
5151  846 
val prems = Goal 
104  847 
"[ A type; \ttback 
848 
\ttback !!x. x:A ==> B(x) type; \ttback 

849 
\ttback !!x. x:A ==> C(x) type; \ttback 

850 
\ttback p: SUM x:A. B(x) + C(x) \ttback 

851 
\ttback ] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))"; 

852 
{\out Level 0} 

853 
{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

854 
{\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

114  855 
\ttbreak 
111  856 
{\out val prems = ["A type [A type]",} 
857 
{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} 

858 
{\out "?x : A ==> C(?x) type [!!x. x : A ==> C(x) type]",} 

859 
{\out "p : SUM x:A. B(x) + C(x) [p : SUM x:A. B(x) + C(x)]"]} 

860 
{\out : thm list} 

104  861 
\end{ttbox} 
314  862 
The last premise involves the sum type~$\Sigma$. Since it is a premise 
863 
rather than the assumption of a goal, it cannot be found by {\tt 

864 
eresolve_tac}. We could insert it (and the other atomic premise) by 

865 
calling 

866 
\begin{ttbox} 

867 
cut_facts_tac prems 1; 

868 
\end{ttbox} 

869 
A forward proof step is more straightforward here. Let us resolve the 

870 
$\Sigma$elimination rule with the premises using~\ttindex{RL}. This 

871 
inference yields one result, which we supply to {\tt 

872 
resolve_tac}.\index{*SumE theorem} 

104  873 
\begin{ttbox} 
874 
by (resolve_tac (prems RL [SumE]) 1); 

875 
{\out Level 1} 

876 
{\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

877 
{\out 1. !!x y.} 

878 
{\out [ x : A; y : B(x) + C(x) ] ==>} 

879 
{\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

880 
\end{ttbox} 

284  881 
The subgoal has two new parameters, $x$ and~$y$. In the main goal, 
314  882 
$\Var{a}$ has been instantiated with a \cdx{split} term. The 
284  883 
assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and 
314  884 
creating the parameter~$xa$. This inference also inserts~\cdx{when} 
885 
into the main goal.\index{*PlusE theorem} 

104  886 
\begin{ttbox} 
887 
by (eresolve_tac [PlusE] 1); 

888 
{\out Level 2} 

284  889 
{\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))} 
104  890 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
891 
{\out 1. !!x y xa.} 

892 
{\out [ x : A; xa : B(x) ] ==>} 

893 
{\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

114  894 
\ttbreak 
104  895 
{\out 2. !!x y ya.} 
896 
{\out [ x : A; ya : C(x) ] ==>} 

897 
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

898 
\end{ttbox} 

899 
To complete the proof object for the main goal, we need to instantiate the 

900 
terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$. We attack subgoal~1 by 

314  901 
a~$+$introduction rule; since the goal assumes $xa\in B(x)$, we take the left 
902 
injection~(\cdx{inl}). 

903 
\index{*PlusI_inl theorem} 

104  904 
\begin{ttbox} 
905 
by (resolve_tac [PlusI_inl] 1); 

906 
{\out Level 3} 

284  907 
{\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))} 
104  908 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
909 
{\out 1. !!x y xa. [ x : A; xa : B(x) ] ==> ?a3(x,y,xa) : SUM x:A. B(x)} 

910 
{\out 2. !!x y xa. [ x : A; xa : B(x) ] ==> SUM x:A. C(x) type} 

114  911 
\ttbreak 
104  912 
{\out 3. !!x y ya.} 
913 
{\out [ x : A; ya : C(x) ] ==>} 

914 
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

915 
\end{ttbox} 

314  916 
A new subgoal~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type. 
917 
Continuing to work on subgoal~1, we apply the $\Sigma$introduction rule. 

918 
This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains 

919 
an ordered pair, whose components are two new unknowns.% 

920 
\index{*SumI theorem} 

104  921 
\begin{ttbox} 
922 
by (resolve_tac [SumI] 1); 

923 
{\out Level 4} 

284  924 
{\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))} 
104  925 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
926 
{\out 1. !!x y xa. [ x : A; xa : B(x) ] ==> ?a4(x,y,xa) : A} 

927 
{\out 2. !!x y xa. [ x : A; xa : B(x) ] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))} 

928 
{\out 3. !!x y xa. [ x : A; xa : B(x) ] ==> SUM x:A. C(x) type} 

929 
{\out 4. !!x y ya.} 

930 
{\out [ x : A; ya : C(x) ] ==>} 

931 
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

932 
\end{ttbox} 

933 
The two new subgoals both hold by assumption. Observe how the unknowns 

934 
$\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state. 

935 
\begin{ttbox} 

936 
by (assume_tac 1); 

937 
{\out Level 5} 

284  938 
{\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))} 
104  939 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
284  940 
\ttbreak 
104  941 
{\out 1. !!x y xa. [ x : A; xa : B(x) ] ==> ?b4(x,y,xa) : B(x)} 
942 
{\out 2. !!x y xa. [ x : A; xa : B(x) ] ==> SUM x:A. C(x) type} 

943 
{\out 3. !!x y ya.} 

944 
{\out [ x : A; ya : C(x) ] ==>} 

945 
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

284  946 
\ttbreak 
104  947 
by (assume_tac 1); 
948 
{\out Level 6} 

284  949 
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))} 
104  950 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
951 
{\out 1. !!x y xa. [ x : A; xa : B(x) ] ==> SUM x:A. C(x) type} 

952 
{\out 2. !!x y ya.} 

953 
{\out [ x : A; ya : C(x) ] ==>} 

954 
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

955 
\end{ttbox} 

314  956 
Subgoal~1 is an example of a wellformedness subgoal~\cite{constable86}. 
957 
Such subgoals are usually trivial; this one yields to 

958 
\ttindex{typechk_tac}, given the current list of premises. 

104  959 
\begin{ttbox} 
960 
by (typechk_tac prems); 

961 
{\out Level 7} 

284  962 
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))} 
104  963 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
964 
{\out 1. !!x y ya.} 

965 
{\out [ x : A; ya : C(x) ] ==>} 

966 
{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} 

967 
\end{ttbox} 

314  968 
This subgoal is the other case from the $+$elimination above, and can be 
969 
proved similarly. Quicker is to apply \ttindex{pc_tac}. The main goal 

970 
finally gets a fully instantiated proof object. 

104  971 
\begin{ttbox} 
972 
by (pc_tac prems 1); 

973 
{\out Level 8} 

284  974 
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))} 
104  975 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} 
976 
{\out No subgoals!} 

977 
\end{ttbox} 

978 
Calling \ttindex{pc_tac} after the first $\Sigma$elimination above also 

979 
proves this theorem. 

980 

981 

982 
\section{Example: deriving a currying functional} 

983 
In simplytyped languages such as {\ML}, a currying functional has the type 

984 
\[ (A\times B \to C) \to (A\to (B\to C)). \] 

314  985 
Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$. 
284  986 
The functional takes a function~$f$ that maps $z:\Sigma(A,B)$ 
987 
to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to 

988 
$C(\langle x,y\rangle)$. 

989 

990 
Formally, there are three typing premises. $A$ is a type; $B$ is an 

991 
$A$indexed family of types; $C$ is a family of types indexed by 

992 
$\Sigma(A,B)$. The goal is expressed using \hbox{\tt PROD f} to ensure 

993 
that the parameter corresponding to the functional's argument is really 

994 
called~$f$; Isabelle echoes the type using \verb> because there is no 

995 
explicit dependence upon~$f$. 

104  996 
\begin{ttbox} 
5151  997 
val prems = Goal 
284  998 
"[ A type; !!x. x:A ==> B(x) type; \ttback 
999 
\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback 

1000 
\ttback ] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback 

1001 
\ttback (PROD x:A . PROD y:B(x) . C(<x,y>))"; 

1002 
\ttbreak 

104  1003 
{\out Level 0} 
284  1004 
{\out ?a : (PROD z:SUM x:A. B(x). C(z)) >} 
1005 
{\out (PROD x:A. PROD y:B(x). C(<x,y>))} 

104  1006 
{\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) >} 
1007 
{\out (PROD x:A. PROD y:B(x). C(<x,y>))} 

114  1008 
\ttbreak 
111  1009 
{\out val prems = ["A type [A type]",} 
1010 
{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} 

1011 
{\out "?z : SUM x:A. B(x) ==> C(?z) type} 

1012 
{\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list} 

104  1013 
\end{ttbox} 
284  1014 
This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic 
314  1015 
repeatedly applies $\Pi$introduction and proves the rather 
284  1016 
tiresome typing conditions. 
1017 

1018 
Note that $\Var{a}$ becomes instantiated to three nested 

1019 
$\lambda$abstractions. It would be easier to read if the bound variable 

1020 
names agreed with the parameters in the subgoal. Isabelle attempts to give 

1021 
parameters the same names as corresponding bound variables in the goal, but 

1022 
this does not always work. In any event, the goal is logically correct. 

104  1023 
\begin{ttbox} 
1024 
by (intr_tac prems); 

1025 
{\out Level 1} 

1026 
{\out lam x xa xb. ?b7(x,xa,xb)} 

1027 
{\out : (PROD z:SUM x:A. B(x). C(z)) > (PROD x:A. PROD y:B(x). C(<x,y>))} 

284  1028 
{\out 1. !!f x y.} 
1029 
{\out [ f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) ] ==>} 

1030 
{\out ?b7(f,x,y) : C(<x,y>)} 

104  1031 
\end{ttbox} 
284  1032 
Using $\Pi$elimination, we solve subgoal~1 by applying the function~$f$. 
314  1033 
\index{*ProdE theorem} 
104  1034 
\begin{ttbox} 
1035 
by (eresolve_tac [ProdE] 1); 

1036 
{\out Level 2} 

1037 
{\out lam x xa xb. x ` <xa,xb>} 

1038 
{\out : (PROD z:SUM x:A. B(x). C(z)) > (PROD x:A. PROD y:B(x). C(<x,y>))} 

284  1039 
{\out 1. !!f x y. [ x : A; y : B(x) ] ==> <x,y> : SUM x:A. B(x)} 
104  1040 
\end{ttbox} 
314  1041 
Finally, we verify that the argument's type is suitable for the function 
1042 
application. This is straightforward using introduction rules. 

104  1043 
\index{*intr_tac} 
1044 
\begin{ttbox} 

1045 
by (intr_tac prems); 

1046 
{\out Level 3} 

1047 
{\out lam x xa xb. x ` <xa,xb>} 

1048 
{\out : (PROD z:SUM x:A. B(x). C(z)) > (PROD x:A. PROD y:B(x). C(<x,y>))} 

1049 
{\out No subgoals!} 

1050 
\end{ttbox} 

1051 
Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can 

1052 
also prove an example by MartinL\"of, related to $\disj$elimination 

1053 
\cite[page~58]{martinlof84}. 

1054 

1055 

1056 
\section{Example: proving the Axiom of Choice} \label{cttchoice} 

1057 
Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$, 

1058 
which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$. 

1059 
Interpreting propositions as types, this asserts that for all $x\in A$ 

1060 
there exists $y\in B(x)$ such that $C(x,y)$. The Axiom of Choice asserts 

1061 
that we can construct a function $f\in \prod@{x\in A}B(x)$ such that 

1062 
$C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a 

1063 
function $g\in \prod@{x\in A}C(x,f{\tt`}x)$. 

1064 

1065 
In principle, the Axiom of Choice is simple to derive in Constructive Type 

333  1066 
Theory. The following definitions work: 
104  1067 
\begin{eqnarray*} 
1068 
f & \equiv & {\tt fst} \circ h \\ 

1069 
g & \equiv & {\tt snd} \circ h 

1070 
\end{eqnarray*} 

314  1071 
But a completely formal proof is hard to find. The rules can be applied in 
1072 
countless ways, yielding many higherorder unifiers. The proof can get 

1073 
bogged down in the details. But with a careful selection of derived rules 

1074 
(recall Fig.\ts\ref{cttderived}) and the type checking tactics, we can 

1075 
prove the theorem in nine steps. 

104  1076 
\begin{ttbox} 
5151  1077 
val prems = Goal 
284  1078 
"[ A type; !!x. x:A ==> B(x) type; \ttback 
1079 
\ttback !!x y.[ x:A; y:B(x) ] ==> C(x,y) type \ttback 

1080 
\ttback ] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ttback 

1081 
\ttback (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; 

104  1082 
{\out Level 0} 
1083 
{\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1084 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

1085 
{\out 1. ?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))} 

111  1087 
\ttbreak 
1088 
{\out val prems = ["A type [A type]",} 

1089 
{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} 

1090 
{\out "[ ?x : A; ?y : B(?x) ] ==> C(?x, ?y) type} 

1091 
{\out [!!x y. [ x : A; y : B(x) ] ==> C(x, y) type]"]} 

1092 
{\out : thm list} 

104  1093 
\end{ttbox} 
1094 
First, \ttindex{intr_tac} applies introduction rules and performs routine 

1095 
type checking. This instantiates~$\Var{a}$ to a construction involving 

314  1096 
a $\lambda$abstraction and an ordered pair. The pair's components are 
1097 
themselves $\lambda$abstractions and there is a subgoal for each. 

104  1098 
\begin{ttbox} 
1099 
by (intr_tac prems); 

1100 
{\out Level 1} 

1101 
{\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>} 

1102 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1103 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

114  1104 
\ttbreak 
284  1105 
{\out 1. !!h x.} 
1106 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1107 
{\out ?b7(h,x) : B(x)} 

114  1108 
\ttbreak 
284  1109 
{\out 2. !!h x.} 
1110 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1111 
{\out ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)} 

104  1112 
\end{ttbox} 
1113 
Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some 

284  1114 
$\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof 
1115 
object $\Var{b@8}(h,x)$ to witness that the choice function's argument and 

1116 
result lie in the relation~$C$. This latter task will take up most of the 

1117 
proof. 

314  1118 
\index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS} 
104  1119 
\begin{ttbox} 
1120 
by (eresolve_tac [ProdE RS SumE_fst] 1); 

1121 
{\out Level 2} 

1122 
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} 

1123 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1124 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

114  1125 
\ttbreak 
284  1126 
{\out 1. !!h x. x : A ==> x : A} 
1127 
{\out 2. !!h x.} 

1128 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1129 
{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)} 

104  1130 
\end{ttbox} 
314  1131 
Above, we have composed {\tt fst} with the function~$h$. Unification 
1132 
has deduced that the function must be applied to $x\in A$. We have our 

1133 
choice function. 

104  1134 
\begin{ttbox} 
1135 
by (assume_tac 1); 

1136 
{\out Level 3} 

1137 
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} 

1138 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1139 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

284  1140 
{\out 1. !!h x.} 
1141 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1142 
{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)} 

104  1143 
\end{ttbox} 
314  1144 
Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be 
1145 
simplified. The derived rule \tdx{replace_type} lets us replace a type 

284  1146 
by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$: 
104  1147 
\begin{ttbox} 
1148 
by (resolve_tac [replace_type] 1); 

1149 
{\out Level 4} 

1150 
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} 

1151 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1152 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

114  1153 
\ttbreak 
284  1154 
{\out 1. !!h x.} 
1155 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1156 
{\out C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)} 

114  1157 
\ttbreak 
284  1158 
{\out 2. !!h x.} 
1159 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1160 
{\out ?b8(h,x) : ?A13(h,x)} 

104  1161 
\end{ttbox} 
314  1162 
The derived rule \tdx{subst_eqtyparg} lets us simplify a type's 
104  1163 
argument (by currying, $C(x)$ is a unary type operator): 
1164 
\begin{ttbox} 

1165 
by (resolve_tac [subst_eqtyparg] 1); 

1166 
{\out Level 5} 

1167 
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} 

1168 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1169 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

114  1170 
\ttbreak 
284  1171 
{\out 1. !!h x.} 
1172 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1173 
{\out (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)} 

114  1174 
\ttbreak 
284  1175 
{\out 2. !!h x z.} 
1176 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A;} 

1177 
{\out z : ?A14(h,x) ] ==>} 

104  1178 
{\out C(x,z) type} 
114  1179 
\ttbreak 
284  1180 
{\out 3. !!h x.} 
1181 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1182 
{\out ?b8(h,x) : C(x,?c14(h,x))} 

104  1183 
\end{ttbox} 
284  1184 
Subgoal~1 requires simply $\beta$contraction, which is the rule 
314  1185 
\tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal 
284  1186 
receives the contracted result. 
104  1187 
\begin{ttbox} 
1188 
by (resolve_tac [ProdC] 1); 

1189 
{\out Level 6} 

1190 
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} 

1191 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1192 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

114  1193 
\ttbreak 
284  1194 
{\out 1. !!h x.} 
1195 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1196 
{\out x : ?A15(h,x)} 

114  1197 
\ttbreak 
284  1198 
{\out 2. !!h x xa.} 
1199 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A;} 

1200 
{\out xa : ?A15(h,x) ] ==>} 

1201 
{\out fst(h ` xa) : ?B15(h,x,xa)} 

114  1202 
\ttbreak 
284  1203 
{\out 3. !!h x z.} 
1204 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A;} 

1205 
{\out z : ?B15(h,x,x) ] ==>} 

104  1206 
{\out C(x,z) type} 
114  1207 
\ttbreak 
284  1208 
{\out 4. !!h x.} 
1209 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1210 
{\out ?b8(h,x) : C(x,fst(h ` x))} 

104  1211 
\end{ttbox} 
1212 
Routine type checking goals proliferate in Constructive Type Theory, but 

1213 
\ttindex{typechk_tac} quickly solves them. Note the inclusion of 

314  1214 
\tdx{SumE_fst} along with the premises. 
104  1215 
\begin{ttbox} 
1216 
by (typechk_tac (SumE_fst::prems)); 

1217 
{\out Level 7} 

1218 
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} 

1219 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1220 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

284  1221 
\ttbreak 
1222 
{\out 1. !!h x.} 

1223 
{\out [ h : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==>} 

1224 
{\out ?b8(h,x) : C(x,fst(h ` x))} 

104  1225 
\end{ttbox} 
314  1226 
We are finally ready to compose {\tt snd} with~$h$. 
1227 
\index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS} 

104  1228 
\begin{ttbox} 
1229 
by (eresolve_tac [ProdE RS SumE_snd] 1); 

1230 
{\out Level 8} 

1231 
{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>} 

1232 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1233 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

284  1234 
\ttbreak 
1235 
{\out 1. !!h x. x : A ==> x : A} 

1236 
{\out 2. !!h x. x : A ==> B(x) type} 

1237 
{\out 3. !!h x xa. [ x : A; xa : B(x) ] ==> C(x,xa) type} 

104  1238 
\end{ttbox} 
1239 
The proof object has reached its final form. We call \ttindex{typechk_tac} 

1240 
to finish the type checking. 

1241 
\begin{ttbox} 

1242 
by (typechk_tac prems); 

1243 
{\out Level 9} 

1244 
{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>} 

1245 
{\out : (PROD x:A. SUM y:B(x). C(x,y)) >} 

1246 
{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} 

1247 
{\out No subgoals!} 

1248 
\end{ttbox} 

314  1249 
It might be instructive to compare this proof with MartinL\"of's forward 
1250 
proof of the Axiom of Choice \cite[page~50]{martinlof84}. 

1251 

1252 
\index{Constructive Type Theory)} 