author  wenzelm 
Wed, 15 Apr 2009 11:14:48 +0200  
changeset 30895  bad26d8f0adf 
parent 12679  8ed660138f83 
child 42637  381fdcab0f36 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Constructive Type Theory} 

314  3 
\index{Constructive Type Theory(} 
4 

7159
b009afd1ace5
\underscoreoff needed because of \underscoreon in previous file
paulson
parents:
6170
diff
changeset

5 
\underscoreoff %this file contains _ in rule names 
b009afd1ace5
\underscoreoff needed because of \underscoreon in previous file
paulson
parents:
6170
diff
changeset

6 

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

9 
the principles of intuitionistic mathematics; it embodies the 

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

314  11 
programs from proofs. 
12 

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

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

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

16 
directly~\cite{alf}. 

104  17 

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

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

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

21 
judgement was 

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

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

24 
\] 

25 
This sequent calculus was not satisfactory because assumptions like 

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

27 
could not be formalized. 

28 

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

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

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

111  34 
\List{x@1\in A@1; 
35 
x@2\in A@2(x@1); \cdots \; 

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

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

39 
\] 

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

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

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

9695  43 
To justify the CTT formulation it is probably best to appeal directly to the 
44 
semantic explanations of the rules~\cite{martinlof84}, rather than to the 

45 
rules themselves. The order of assumptions no longer matters, unlike in 

46 
standard Type Theory. Contexts, which are typical of many modern type 

47 
theories, are difficult to represent in Isabelle. In particular, it is 

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

49 
\index{assumptions!in CTT} 

104  50 

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

314  53 

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

55 
\begin{center} 

56 
\begin{tabular}{rrr} 

57 
\it name & \it metatype & \it description \\ 

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

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

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

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

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

104  63 

314  64 
\cdx{N} & $t$ & natural numbers type\\ 
65 
\cdx{0} & $i$ & constructor\\ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

82 
\end{tabular} 

83 
\end{center} 

9695  84 
\caption{The constants of CTT} \label{cttconstants} 
314  85 
\end{figure} 
86 

87 

9695  88 
CTT supports all of Type Theory apart from list types, wellordering types, 
89 
and universes. Universes could be introduced {\em\`a la Tarski}, adding new 

90 
constants as names for types. The formulation {\em\`a la Russell}, where 

91 
types denote themselves, is only possible if we identify the metatypes~{\tt 

92 
i} and~{\tt t}. Most published formulations of wellordering types have 

93 
difficulties involving extensionality of functions; I suggest that you use 

94 
some other method for defining recursive types. List types are easy to 

95 
introduce by declaring new rules. 

104  96 

9695  97 
CTT uses the 1982 version of Type Theory, with extensional equality. The 
98 
computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable. 

99 
Its rewriting tactics prove theorems of the form $a=b\in A$. It could be 

100 
modified to have intensional equality, but rewriting tactics would have to 

101 
prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might 

102 
require a separate simplifier. 

104  103 

104 

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

9695  106 
\index{lambda abs@$\lambda$abstractions!in CTT} 
104  107 
\begin{center} 
108 
\begin{tabular}{llrrr} 

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

104  111 
\end{tabular} 
112 
\end{center} 

113 
\subcaption{Binders} 

114 

115 
\begin{center} 

9695  116 
\index{*"` symbol}\index{function applications!in CTT} 
314  117 
\index{*"+ symbol} 
104  118 
\begin{tabular}{rrrr} 
314  119 
\it symbol & \it metatype & \it priority & \it description \\ 
111  120 
\tt ` & $[i,i]\to i$ & Left 55 & function application\\ 
121 
\tt + & $[t,t]\to t$ & Right 30 & sum of two types 

104  122 
\end{tabular} 
123 
\end{center} 

124 
\subcaption{Infixes} 

125 

314  126 
\index{*"* symbol} 
127 
\index{*"""> symbol} 

104  128 
\begin{center} \tt\frenchspacing 
129 
\begin{tabular}{rrr} 

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

141 
\subcaption{Translations} 

142 

314  143 
\index{*"= symbol} 
104  144 
\begin{center} 
145 
\dquotes 

146 
\[ \begin{array}{rcl} 

111  147 
prop & = & type " type" \\ 
148 
&  & type " = " type \\ 

149 
&  & term " : " type \\ 

150 
&  & term " = " term " : " type 

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

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

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

158 
&  & "< " term " , " term " >" 

104  159 
\end{array} 
160 
\] 

161 
\end{center} 

162 
\subcaption{Grammar} 

9695  163 
\caption{Syntax of CTT} \label{cttsyntax} 
104  164 
\end{figure} 
165 

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

167 

168 

169 
\section{Syntax} 

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

173 
x.b$ and $f(a)$, differ from objectlevel abstraction and application, 

174 
\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an 

175 
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say 

176 
$i\To i$. 

104  177 

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

180 
type is $T$; other finite types are built as $T+T+T$, etc. 

314  181 

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

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

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

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

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

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

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

195 

196 

197 
\begin{figure} 

198 
\begin{ttbox} 

314  199 
\tdx{refl_type} A type ==> A = A 
200 
\tdx{refl_elem} a : A ==> a = a : A 

104  201 

314  202 
\tdx{sym_type} A = B ==> B = A 
203 
\tdx{sym_elem} a = b : A ==> b = a : A 

104  204 

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

104  207 

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

104  210 

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

104  213 
] ==> B(a) = D(c) 
214 

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

104  217 
] ==> b(a) = d(c) : B(a) 
218 

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

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

104  222 
\end{ttbox} 
223 
\caption{General equality rules} \label{cttequality} 

224 
\end{figure} 

225 

226 

227 
\begin{figure} 

228 
\begin{ttbox} 

314  229 
\tdx{NF} N type 
104  230 

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

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

104  234 

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

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

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

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

104  251 

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

255 
\end{figure} 

256 

257 

258 
\begin{figure} 

259 
\begin{ttbox} 

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

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

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

104  271 

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

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

280 

281 
\begin{figure} 

282 
\begin{ttbox} 

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

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

104  289 

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

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

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

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

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

308 

309 
\begin{figure} 

310 
\begin{ttbox} 

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

104  313 

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

104  316 

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

104  319 

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

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

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

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

104  330 

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

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

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

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

342 
\end{figure} 

343 

344 

345 
\begin{figure} 

346 
\begin{ttbox} 

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

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

104  350 

314  351 
\tdx{TF} T type 
352 
\tdx{TI} tt : T 

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

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

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

104  356 
\end{ttbox} 
357 

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

361 

362 
\begin{figure} 

363 
\begin{ttbox} 

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

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

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

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

369 
\end{ttbox} 

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

371 
\end{figure} 

104  372 

314  373 

374 
\begin{figure} 

375 
\begin{ttbox} 

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

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

378 

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

104  380 
] ==> c(p`a): C(p`a) 
381 

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

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

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

389 

9695  390 
\caption{Derived rules for CTT} \label{cttderived} 
104  391 
\end{figure} 
392 

393 

394 
\section{Rules of inference} 

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

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

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

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

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

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

104  402 
constructor names. 
403 

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

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

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

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

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

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

411 

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

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

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

415 
$c$) are welltyped. 

416 

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

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

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

420 
91]{martinlof84}. 

421 

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

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

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

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

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

104  427 

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

430 
predicate calculus rules for universal quantifiers and implication. They 

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

432 
$\lambda$calculus. 

433 

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

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

436 
predicate calculus rules for existential quantifiers and conjunction. They 

437 
also permit reasoning about ordered pairs, with the projections 

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

439 

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

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

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

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

104  444 

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

447 
truth. 

448 

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

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

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

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

453 

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

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

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

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

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

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

460 
proof of the Axiom of Choice. 

104  461 

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

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

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

467 
variables in the premises. 

104  468 

469 

470 
\section{Rule lists} 

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

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

9695  473 
Theory rules against a proof state. CTT defines lists  each with 
104  474 
type 
475 
\hbox{\tt thm list}  of related rules. 

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

479 
$F$, and $T$. 

480 

481 
\item[\ttindexbold{formL_rls}] 

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

314  483 
other types use \tdx{refl_type}.) 
104  484 

485 
\item[\ttindexbold{intr_rls}] 

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

487 
$T$. 

488 

489 
\item[\ttindexbold{intrL_rls}] 

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

314  491 
$T$ use \tdx{refl_elem}.) 
104  492 

493 
\item[\ttindexbold{elim_rls}] 

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

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

496 
eliminator. 

497 

498 
\item[\ttindexbold{elimL_rls}] 

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

500 

501 
\item[\ttindexbold{comp_rls}] 

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

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

504 

505 
\item[\ttindexbold{basic_defs}] 

314  506 
contains the definitions of {\tt fst} and {\tt snd}. 
507 
\end{ttdescription} 

104  508 

509 

510 
\section{Tactics for subgoal reordering} 

511 
\begin{ttbox} 

512 
test_assume_tac : int > tactic 

513 
typechk_tac : thm list > tactic 

514 
equal_tac : thm list > tactic 

515 
intr_tac : thm list > tactic 

516 
\end{ttbox} 

9695  517 
Blind application of CTT rules seldom leads to a proof. The elimination 
104  518 
rules, especially, create subgoals containing new unknowns. These subgoals 
333  519 
unify with anything, creating a huge search space. The standard tactic 
9695  520 
\ttindex{filt_resolve_tac} 
314  521 
(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% 
522 
{\S\ref{filt_resolve_tac}}) 

523 
% 

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

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

528 
to see why this is necessary. 

529 
\begin{ttdescription} 

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

534 

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

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

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

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

538 
$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

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

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

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

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

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

6170  546 
tactic can also perform typechecking. 
104  547 

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

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

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

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

552 
expressed as a type. 

314  553 
\end{ttdescription} 
104  554 

555 

556 

557 
\section{Rewriting tactics} 

558 
\begin{ttbox} 

559 
rew_tac : thm list > tactic 

560 
hyp_rew_tac : thm list > tactic 

561 
\end{ttbox} 

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

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

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

9695  566 
TSimpFun} is only useful for CTT and similar logics with type inference 
567 
rules. At present it is undocumented.} 

314  568 
% 
569 
The rewrites include the computation rules and other equations. The long 

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

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

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

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

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

578 

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

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

581 
the assumptions. 

314  582 
\end{ttdescription} 
104  583 

584 

585 
\section{Tactics for logical reasoning} 

9695  586 
Interpreting propositions as types lets CTT express statements of 
587 
intuitionistic logic. However, Constructive Type Theory is not just another 

588 
syntax for firstorder logic. There are fundamental differences. 

104  589 

9695  590 
\index{assumptions!in CTT} 
314  591 
Can assumptions be deleted after use? Not every occurrence of a type 
592 
represents a proposition, and Type Theory assumptions declare variables. 

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

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

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

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

599 
meaningless. 

600 

9695  601 
Isabelle provides several tactics for predicate calculus reasoning in CTT: 
104  602 
\begin{ttbox} 
603 
mp_tac : int > tactic 

604 
add_mp_tac : int > tactic 

605 
safestep_tac : thm list > int > tactic 

606 
safe_tac : thm list > int > tactic 

607 
step_tac : thm list > int > tactic 

608 
pc_tac : thm list > int > tactic 

609 
\end{ttbox} 

610 
These are loosely based on the intuitionistic proof procedures 

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

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

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

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

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

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

621 

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

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

104  625 

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

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

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

631 

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

104  634 

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

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

637 
rules. It may produce multiple outcomes. 

638 

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

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

314  641 
\end{ttdescription} 
104  642 

643 

644 

645 
\begin{figure} 

314  646 
\index{#+@{\tt\#+} symbol} 
647 
\index{*" symbol} 

12679
8ed660138f83
changed the index sort key from  to just  because pdflatex can't cope
paulson
parents:
9695
diff
changeset

648 
\index{""@{{\tt"""} symbol}} 
314  649 
\index{#*@{\tt\#*} symbol} 
650 
\index{*div symbol} 

651 
\index{*mod symbol} 

652 
\begin{constants} 

653 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

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

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

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

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

660 
\end{constants} 

104  661 

662 
\begin{ttbox} 

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

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

667 

668 
\tdx{mod_def} a mod b == 

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

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

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

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

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

677 

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

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

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

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

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

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

104  687 

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

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

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

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

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

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

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

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

704 

705 
\section{A theory of arithmetic} 

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

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

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

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

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

717 

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

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

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

723 
equality $succ(v)=b$. 

104  724 

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

104  727 

728 

729 

730 
\section{The examples directory} 

9695  731 
This directory contains examples and experimental proofs in CTT. 
314  732 
\begin{ttdescription} 
733 
\item[CTT/ex/typechk.ML] 

6170  734 
contains simple examples of typechecking and type deduction. 
104  735 

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

739 

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

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

314  746 
\end{ttdescription} 
104  747 

748 

749 
\section{Example: type inference} 

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

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

752 
initially 

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

754 
predecessor function on the natural numbers. 

755 
\begin{ttbox} 

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

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

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

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

766 
by (resolve_tac [ProdI] 1); 

767 
{\out Level 1} 

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

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

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

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

779 
{\out Level 2} 

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

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

784 
\end{ttbox} 

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

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

790 
{\out Level 3} 

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

794 
\end{ttbox} 

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

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

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

803 
{\out Level 4} 

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

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

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

813 

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

816 
following invalid goal: 

817 
\begin{ttbox} 

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

821 

104  822 

823 
\section{An example of logical reasoning} 

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

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

827 
unknown and takes shape during the proof. 

828 

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

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

832 
\] 

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

835 
distributive law of Type Theory: 

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

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

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

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

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

844 
\] 

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

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

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

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

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

854 
{\out Level 0} 

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

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

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

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

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

862 
{\out : thm list} 

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

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

867 
calling 

868 
\begin{ttbox} 

869 
cut_facts_tac prems 1; 

870 
\end{ttbox} 

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

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

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

874 
resolve_tac}.\index{*SumE theorem} 

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

877 
{\out Level 1} 

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

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

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

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

882 
\end{ttbox} 

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

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

890 
{\out Level 2} 

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

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

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

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

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

900 
\end{ttbox} 

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

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

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

905 
\index{*PlusI_inl theorem} 

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

908 
{\out Level 3} 

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

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

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

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

917 
\end{ttbox} 

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

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

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

922 
\index{*SumI theorem} 

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

925 
{\out Level 4} 

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

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

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

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

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

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

934 
\end{ttbox} 

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

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

937 
\begin{ttbox} 

938 
by (assume_tac 1); 

939 
{\out Level 5} 

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

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

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

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

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

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

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

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

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

957 
\end{ttbox} 

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

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

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

963 
{\out Level 7} 

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

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

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

969 
\end{ttbox} 

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

972 
finally gets a fully instantiated proof object. 

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

975 
{\out Level 8} 

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

979 
\end{ttbox} 

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

981 
proves this theorem. 

982 

983 

984 
\section{Example: deriving a currying functional} 

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

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

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

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

991 

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

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

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

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

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

997 
explicit dependence upon~$f$. 

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

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

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

1004 
\ttbreak 

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

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

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

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

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

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

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

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

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

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

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

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

1027 
{\out Level 1} 

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

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

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

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

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

1038 
{\out Level 2} 

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

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

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

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

1047 
by (intr_tac prems); 

1048 
{\out Level 3} 

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

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

1051 
{\out No subgoals!} 

1052 
\end{ttbox} 

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

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

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

1056 

1057 

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

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

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

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

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

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

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

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

1066 

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

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

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

1072 
\end{eqnarray*} 

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

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

6170  1076 
(recall Fig.\ts\ref{cttderived}) and the typechecking tactics, we can 
314  1077 
prove the theorem in nine steps. 
104  1078 
\begin{ttbox} 
5151  1079 
val prems = Goal 
284  1080 
"[ A type; !!x. x:A ==> B(x) type; \ttback 
1081 
\ttback !!x y.[ x:A; y:B(x) ] ==> C(x,y) type \ttback 

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

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

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

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

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

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

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

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

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

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

1094 
{\out : thm list} 

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

6170  1097 
typechecking. This instantiates~$\Var{a}$ to a construction involving 
314  1098 
a $\lambda$abstraction and an ordered pair. The pair's components are 
1099 
themselves $\lambda$abstractions and there is a subgoal for each. 

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

1102 
{\out Level 1} 

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

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

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

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

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

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

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

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

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

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

1119 
proof. 

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

1123 
{\out Level 2} 

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

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

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

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

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

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

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

1135 
choice function. 

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

1138 
{\out Level 3} 

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

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

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

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

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

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

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

1151 
{\out Level 4} 

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

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

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

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

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

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

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

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

1167 
by (resolve_tac [subst_eqtyparg] 1); 

1168 
{\out Level 5} 

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

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

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

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

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

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

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

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

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

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

1191 
{\out Level 6} 

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

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

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

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

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

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

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

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

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

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

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

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

104  1213 
\end{ttbox} 
6170  1214 
Routine typechecking goals proliferate in Constructive Type Theory, but 
104  1215 
\ttindex{typechk_tac} quickly solves them. Note the inclusion of 
314  1216 
\tdx{SumE_fst} along with the premises. 
104  1217 
\begin{ttbox} 
1218 
by (typechk_tac (SumE_fst::prems)); 

1219 
{\out Level 7} 

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

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

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

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

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

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

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

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

1232 
{\out Level 8} 

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

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

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

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

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

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

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

6170  1242 
to finish the typechecking. 
104  1243 
\begin{ttbox} 
1244 
by (typechk_tac prems); 

1245 
{\out Level 9} 

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

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

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

1249 
{\out No subgoals!} 

1250 
\end{ttbox} 

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

1253 

1254 
\index{Constructive Type Theory)} 