author  clasohm 
Thu, 29 Jun 1995 12:28:27 +0200  
changeset 1163  c080ff36d24e 
parent 975  6c280d1dac35 
child 3096  ccc2c92bb232 
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 \\ 
314  129 
\sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) & 
111  130 
\rm product $\prod@{x\in A}B[x]$ \\ 
314  131 
\sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) & 
111  132 
\rm sum $\sum@{x\in A}B[x]$ \\ 
104  133 
$A$ > $B$ & Prod($A$, $\lambda x.B$) & 
111  134 
\rm function space $A\to B$ \\ 
104  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 

172 
application, \hbox{\tt lam $x$.$b$} and $b{\tt`}a$. A {\CTT} 

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} 

181 
Quantification is expressed using general sums $\sum@{x\in A}B[x]$ and 

182 
products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt 

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)) 
284  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)) 
284  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)) 
284  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)) 
284  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} 

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

104  260 
PROD x:A.B(x) = PROD x:C.D(x) 
261 

314  262 
\tdx{ProdI} [ A type; !!x. x:A ==> b(x):B(x) 
104  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) 
104  265 
] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x) 
266 

314  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) 
104  271 
] ==> (lam x.b(x)) ` a = b(a) : B(a) 
272 

314  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} 

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

104  283 
] ==> SUM x:A.B(x) = SUM x:C.D(x) 
284 

314  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 

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

314  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>) 
284  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>) 
284  298 
] ==> split(<a,b>, \%x y.c(x,y)) = c(a,b) : C(<a,b>) 
104  299 

314  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)) 

284  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)) 

284  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)) 

284  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)) 

284  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 

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} 

314  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)) 

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 == 

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 == 
670 
rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v)) 

671 

672 

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

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

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

676 

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

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

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

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

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

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

104  686 

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

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

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

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

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

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

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

699 
\caption{The theory of arithmetic} \label{cttarith} 

104  700 
\end{ttbox} 
701 
\end{figure} 

702 

703 

704 
\section{A theory of arithmetic} 

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

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

709 
Figure~\ref{cttarith} presents the definitions and some of the key 

314  710 
theorems, including commutative, distributive, and associative laws. 
104  711 

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

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

716 

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

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

719 

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

722 
equality $succ(v)=b$. 

104  723 

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

104  726 

727 

728 

729 
\section{The examples directory} 

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

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

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

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

738 

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

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

314  745 
\end{ttdescription} 
104  746 

747 

748 
\section{Example: type inference} 

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

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

751 
initially 

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

753 
predecessor function on the natural numbers. 

754 
\begin{ttbox} 

284  755 
goal CTT.thy "lam n. rec(n, 0, \%x y.x) : ?A"; 
104  756 
{\out Level 0} 
284  757 
{\out lam n. rec(n,0,\%x y. x) : ?A} 
758 
{\out 1. lam n. rec(n,0,\%x y. x) : ?A} 

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

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

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

765 
by (resolve_tac [ProdI] 1); 

766 
{\out Level 1} 

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

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

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

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

778 
{\out Level 2} 

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

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

783 
\end{ttbox} 

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

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

789 
{\out Level 3} 

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

793 
\end{ttbox} 

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

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

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

802 
{\out Level 4} 

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

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

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

812 

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

815 
following invalid goal: 

816 
\begin{ttbox} 

817 
goal CTT.thy "lam n. rec(n, 0, \%x y.tt) : ?A"; 

818 
\end{ttbox} 

819 

820 

104  821 

822 
\section{An example of logical reasoning} 

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

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

826 
unknown and takes shape during the proof. 

827 

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

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

831 
\] 

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

834 
distributive law of Type Theory: 

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

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

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

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

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

843 
\] 

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

104  846 
\begin{ttbox} 
847 
val prems = goal CTT.thy 

848 
"[ A type; \ttback 

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

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

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

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

853 
{\out Level 0} 

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

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

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

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

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

861 
{\out : thm list} 

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

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

866 
calling 

867 
\begin{ttbox} 

868 
cut_facts_tac prems 1; 

869 
\end{ttbox} 

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

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

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

873 
resolve_tac}.\index{*SumE theorem} 

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

876 
{\out Level 1} 

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

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

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

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

881 
\end{ttbox} 

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

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

889 
{\out Level 2} 

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

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

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

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

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

899 
\end{ttbox} 

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

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

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

904 
\index{*PlusI_inl theorem} 

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

907 
{\out Level 3} 

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

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

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

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

916 
\end{ttbox} 

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

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

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

921 
\index{*SumI theorem} 

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

924 
{\out Level 4} 

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

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

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

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

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

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

933 
\end{ttbox} 

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

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

936 
\begin{ttbox} 

937 
by (assume_tac 1); 

938 
{\out Level 5} 

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

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

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

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

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

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

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

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

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

956 
\end{ttbox} 

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

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

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

962 
{\out Level 7} 

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

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

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

968 
\end{ttbox} 

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

971 
finally gets a fully instantiated proof object. 

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

974 
{\out Level 8} 

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

978 
\end{ttbox} 

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

980 
proves this theorem. 

981 

982 

983 
\section{Example: deriving a currying functional} 

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

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

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

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

990 

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

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

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

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

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

996 
explicit dependence upon~$f$. 

104  997 
\begin{ttbox} 
998 
val prems = goal CTT.thy 

284  999 
"[ A type; !!x. x:A ==> B(x) type; \ttback 
1000 
\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback 

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

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

1003 
\ttbreak 

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

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

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

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

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

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

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

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

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

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

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

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

1026 
{\out Level 1} 

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

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

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

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

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

1037 
{\out Level 2} 

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

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

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

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

1046 
by (intr_tac prems); 

1047 
{\out Level 3} 

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

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

1050 
{\out No subgoals!} 

1051 
\end{ttbox} 

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

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

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

1055 

1056 

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

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

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

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

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

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

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

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

1065 

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

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

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

1071 
\end{eqnarray*} 

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

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

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

1076 
prove the theorem in nine steps. 

104  1077 
\begin{ttbox} 
1078 
val prems = goal CTT.thy 

284  1079 
"[ A type; !!x. x:A ==> B(x) type; \ttback 
1080 
\ttback !!x y.[ x:A; y:B(x) ] ==> C(x,y) type \ttback 

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

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

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

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

1086 
{\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) >} 

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

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

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

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

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

1093 
{\out : thm list} 

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

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

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

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

1101 
{\out Level 1} 

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

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

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

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

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

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

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

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

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

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

1118 
proof. 

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

1122 
{\out Level 2} 

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

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

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

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

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

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

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

1134 
choice function. 

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

1137 
{\out Level 3} 

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

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

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

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

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

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

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

1150 
{\out Level 4} 

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

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

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

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

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

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

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

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

1166 
by (resolve_tac [subst_eqtyparg] 1); 

1167 
{\out Level 5} 

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

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

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

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

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

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

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

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

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

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

1190 
{\out Level 6} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1218 
{\out Level 7} 

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

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

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

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

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

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

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

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

1231 
{\out Level 8} 

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

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

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

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

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

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

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

1241 
to finish the type checking. 

1242 
\begin{ttbox} 

1243 
by (typechk_tac prems); 

1244 
{\out Level 9} 

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

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

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

1248 
{\out No subgoals!} 

1249 
\end{ttbox} 

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

1252 

1253 
\index{Constructive Type Theory)} 