2 \chapter{Constructive Type Theory}
3 \index{Constructive Type Theory|(}
5 \underscoreoff %this file contains _ in rule names
7 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
8 be viewed at many different levels. It is a formal system that embodies
9 the principles of intuitionistic mathematics; it embodies the
10 interpretation of propositions as types; it is a vehicle for deriving
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
18 Isabelle's original formulation of Type Theory was a kind of sequent
19 calculus, following Martin-L\"of~\cite{martinlof84}. It included rules for
20 building the context, namely variable bindings with their types. A typical
22 \[ a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \;
23 [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]
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.
29 The theory~\thydx{CTT} implements Constructive Type Theory, using
30 natural deduction. The judgement above is expressed using $\Forall$ and
32 \[ \begin{array}{r@{}l}
33 \Forall x@1\ldots x@n. &
35 x@2\in A@2(x@1); \cdots \;
36 x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
37 & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n)
40 Assumptions can use all the judgement forms, for instance to express that
41 $B$ is a family of types over~$A$:
42 \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
43 To justify the CTT formulation it is probably best to appeal directly to the
44 semantic explanations of the rules~\cite{martinlof84}, rather than to the
45 rules themselves. The order of assumptions no longer matters, unlike in
46 standard Type Theory. Contexts, which are typical of many modern type
47 theories, are difficult to represent in Isabelle. In particular, it is
48 difficult to enforce that all the variables in a context are distinct.
49 \index{assumptions!in CTT}
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}.
54 \begin{figure} \tabcolsep=1em %wider spacing in tables
57 \it name & \it meta-type & \it description \\
58 \cdx{Type} & $t \to prop$ & judgement form \\
59 \cdx{Eqtype} & $[t,t]\to prop$ & judgement form\\
60 \cdx{Elem} & $[i, t]\to prop$ & judgement form\\
61 \cdx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\
62 \cdx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex]
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
84 \caption{The constants of CTT} \label{ctt-constants}
88 CTT supports all of Type Theory apart from list types, well-ordering types,
89 and universes. Universes could be introduced {\em\`a la Tarski}, adding new
90 constants as names for types. The formulation {\em\`a la Russell}, where
91 types denote themselves, is only possible if we identify the meta-types~{\tt
92 i} and~{\tt t}. Most published formulations of well-ordering types have
93 difficulties involving extensionality of functions; I suggest that you use
94 some other method for defining recursive types. List types are easy to
95 introduce by declaring new rules.
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.
105 \begin{figure} \tabcolsep=1em %wider spacing in tables
106 \index{lambda abs@$\lambda$-abstractions!in CTT}
108 \begin{tabular}{llrrr}
109 \it symbol &\it name &\it meta-type & \it priority & \it description \\
110 \sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
116 \index{*"` symbol}\index{function applications!in CTT}
118 \begin{tabular}{rrrr}
119 \it symbol & \it meta-type & \it priority & \it description \\
120 \tt ` & $[i,i]\to i$ & Left 55 & function application\\
121 \tt + & $[t,t]\to t$ & Right 30 & sum of two types
127 \index{*"-"-"> symbol}
128 \begin{center} \tt\frenchspacing
130 \it external & \it internal & \it standard notation \\
131 \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) &
132 \rm product $\prod@{x\in A}B[x]$ \\
133 \sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x. B[x]$) &
134 \rm sum $\sum@{x\in A}B[x]$ \\
135 $A$ --> $B$ & Prod($A$, $\lambda x. B$) &
136 \rm function space $A\to B$ \\
137 $A$ * $B$ & Sum($A$, $\lambda x. B$) &
138 \rm binary product $A\times B$
141 \subcaption{Translations}
146 \[ \begin{array}{rcl}
147 prop & = & type " type" \\
148 & | & type " = " type \\
149 & | & term " : " type \\
150 & | & term " = " term " : " type
152 type & = & \hbox{expression of type~$t$} \\
153 & | & "PROD~" id " : " type " . " type \\
154 & | & "SUM~~" id " : " type " . " type
156 term & = & \hbox{expression of type~$i$} \\
157 & | & "lam " id~id^* " . " term \\
158 & | & "< " term " , " term " >"
163 \caption{Syntax of CTT} \label{ctt-syntax}
166 %%%%\section{Generic Packages} typedsimp.ML????????????????
170 The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include
171 the function application operator (sometimes called `apply'), and the 2-place
172 type operators. Note that meta-level abstraction and application, $\lambda
173 x.b$ and $f(a)$, differ from object-level abstraction and application,
174 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
175 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
178 The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
179 et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element
180 type is $T$; other finite types are built as $T+T+T$, etc.
182 \index{*SUM symbol}\index{*PROD symbol}
183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
184 products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt
185 Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
186 PROD $x$:$A$.\ $B[x]$}. For example, we may write
188 SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y)))
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.
199 \tdx{refl_type} A type ==> A = A
200 \tdx{refl_elem} a : A ==> a = a : A
202 \tdx{sym_type} A = B ==> B = A
203 \tdx{sym_elem} a = b : A ==> b = a : A
205 \tdx{trans_type} [| A = B; B = C |] ==> A = C
206 \tdx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A
208 \tdx{equal_types} [| a : A; A = B |] ==> a : B
209 \tdx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B
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)
215 \tdx{subst_elem} [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
216 \tdx{subst_elemL} [| a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)
217 |] ==> b(a) = d(c) : B(a)
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
223 \caption{General equality rules} \label{ctt-equality}
232 \tdx{NI_succ} a : N ==> succ(a) : N
233 \tdx{NI_succL} a = b : N ==> succ(a) = succ(b) : N
235 \tdx{NE} [| p: N; a: C(0);
236 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
237 |] ==> rec(p, a, \%u v. b(u,v)) : C(p)
239 \tdx{NEL} [| p = q : N; a = c : C(0);
240 !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
241 |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p)
243 \tdx{NC0} [| a: C(0);
244 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
245 |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0)
247 \tdx{NC_succ} [| p: N; a: C(0);
248 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
249 |] ==> rec(succ(p), a, \%u v. b(u,v)) =
250 b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p))
252 \tdx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F
254 \caption{Rules for type~$N$} \label{ctt-N}
260 \tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
261 \tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
262 PROD x:A. B(x) = PROD x:C. D(x)
264 \tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x)
265 |] ==> lam x. b(x) : PROD x:A. B(x)
266 \tdx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x)
267 |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)
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)
272 \tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x)
273 |] ==> (lam x. b(x)) ` a = b(a) : B(a)
275 \tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)
277 \caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}
283 \tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
284 \tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x)
285 |] ==> SUM x:A. B(x) = SUM x:C. D(x)
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)
290 \tdx{SumE} [| p: SUM x:A. B(x);
291 !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
292 |] ==> split(p, \%x y. c(x,y)) : C(p)
294 \tdx{SumEL} [| p=q : SUM x:A. B(x);
295 !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
296 |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p)
298 \tdx{SumC} [| a: A; b: B(a);
299 !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
300 |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>)
302 \tdx{fst_def} fst(a) == split(a, \%x y. x)
303 \tdx{snd_def} snd(a) == split(a, \%x y. y)
305 \caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
311 \tdx{PlusF} [| A type; B type |] ==> A+B type
312 \tdx{PlusFL} [| A = C; B = D |] ==> A+B = C+D
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
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
320 \tdx{PlusE} [| p: A+B;
321 !!x. x:A ==> c(x): C(inl(x));
322 !!y. y:B ==> d(y): C(inr(y))
323 |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p)
325 \tdx{PlusEL} [| p = q : A+B;
326 !!x. x: A ==> c(x) = e(x) : C(inl(x));
327 !!y. y: B ==> d(y) = f(y) : C(inr(y))
328 |] ==> when(p, \%x. c(x), \%y. d(y)) =
329 when(q, \%x. e(x), \%y. f(y)) : C(p)
331 \tdx{PlusC_inl} [| a: A;
332 !!x. x:A ==> c(x): C(inl(x));
333 !!y. y:B ==> d(y): C(inr(y))
334 |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a))
336 \tdx{PlusC_inr} [| b: B;
337 !!x. x:A ==> c(x): C(inl(x));
338 !!y. y:B ==> d(y): C(inr(y))
339 |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b))
341 \caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
348 \tdx{FE} [| p: F; C type |] ==> contr(p) : C
349 \tdx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C
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)
358 \caption{Rules for types $F$ and $T$} \label{ctt-ft}
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)
370 \caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}
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)
379 \tdx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z)
380 |] ==> c(p`a): C(p`a)
382 \tdx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
384 \tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A
386 \tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type
387 |] ==> snd(p) : B(fst(p))
390 \caption{Derived rules for CTT} \label{ctt-derived}
394 \section{Rules of inference}
395 The rules obey the following naming conventions. Type formation rules have
396 the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@.
397 Elimination rules have the suffix~{\tt E}\@. Computation rules, which
398 describe the reduction of eliminators, have the suffix~{\tt C}\@. The
399 equality versions of the rules (which permit reductions on subterms) are
400 called {\bf long} rules; their names have the suffix~{\tt L}\@.
401 Introduction and computation rules are often further suffixed with
404 Figure~\ref{ctt-equality} presents the equality rules. Most of them are
405 straightforward: reflexivity, symmetry, transitivity and substitution. The
406 judgement \cdx{Reduce} does not belong to Type Theory proper; it has
407 been added to implement rewriting. The judgement ${\tt Reduce}(a,b)$ holds
408 when $a=b:A$ holds. It also holds when $a$ and $b$ are syntactically
409 identical, even if they are ill-typed, because rule {\tt refl_red} does
410 not verify that $a$ belongs to $A$.
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
417 Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.
418 They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$. This is
419 the fourth Peano axiom and cannot be derived without universes \cite[page
422 The constant \cdx{rec} constructs proof terms when mathematical
423 induction, rule~\tdx{NE}, is applied. It can also express primitive
424 recursion. Since \cdx{rec} can be applied to higher-order functions,
425 it can even express Ackermann's function, which is not primitive recursive
426 \cite[page~104]{thompson91}.
428 Figure~\ref{ctt-prod} shows the rules for general product types, which
429 include function types as a special case. The rules correspond to the
430 predicate calculus rules for universal quantifiers and implication. They
431 also permit reasoning about functions, with the rules of a typed
434 Figure~\ref{ctt-sum} shows the rules for general sum types, which
435 include binary product types as a special case. The rules correspond to the
436 predicate calculus rules for existential quantifiers and conjunction. They
437 also permit reasoning about ordered pairs, with the projections
438 \cdx{fst} and~\cdx{snd}.
440 Figure~\ref{ctt-plus} shows the rules for binary sum types. They
441 correspond to the predicate calculus rules for disjunction. They also
442 permit reasoning about disjoint sums, with the injections \cdx{inl}
443 and~\cdx{inr} and case analysis operator~\cdx{when}.
445 Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$
446 and~$T$. They correspond to the predicate calculus rules for absurdity and
449 Figure~\ref{ctt-eq} shows the rules for equality types. If $a=b\in A$ is
450 provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,
451 and vice versa. These rules define extensional equality; the most recent
452 versions of Type Theory use intensional equality~\cite{nordstrom90}.
454 Figure~\ref{ctt-derived} presents the derived rules. The rule
455 \tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use
456 in backwards proof. The rules \tdx{SumE_fst} and \tdx{SumE_snd}
457 express the typing of~\cdx{fst} and~\cdx{snd}; together, they are
458 roughly equivalent to~{\tt SumE} with the advantage of creating no
459 parameters. Section~\ref{ctt-choice} below demonstrates these rules in a
460 proof of the Axiom of Choice.
462 All the rules are given in $\eta$-expanded form. For instance, every
463 occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the
464 rules for~$N$. The expanded form permits Isabelle to preserve bound
465 variable names during backward proof. Names of bound variables in the
466 conclusion (here, $u$ and~$v$) are matched with corresponding bound
467 variables in the premises.
471 The Type Theory tactics provide rewriting, type inference, and logical
472 reasoning. Many proof procedures work by repeatedly resolving certain Type
473 Theory rules against a proof state. CTT defines lists --- each with
475 \hbox{\tt thm list} --- of related rules.
476 \begin{ttdescription}
477 \item[\ttindexbold{form_rls}]
478 contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
481 \item[\ttindexbold{formL_rls}]
482 contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$. (For
483 other types use \tdx{refl_type}.)
485 \item[\ttindexbold{intr_rls}]
486 contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
489 \item[\ttindexbold{intrL_rls}]
490 contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$. (For
491 $T$ use \tdx{refl_elem}.)
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
498 \item[\ttindexbold{elimL_rls}]
499 contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$.
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.
505 \item[\ttindexbold{basic_defs}]
506 contains the definitions of {\tt fst} and {\tt snd}.
510 \section{Tactics for subgoal reordering}
512 test_assume_tac : int -> tactic
513 typechk_tac : thm list -> tactic
514 equal_tac : thm list -> tactic
515 intr_tac : thm list -> tactic
517 Blind application of CTT rules seldom leads to a proof. The elimination
518 rules, especially, create subgoals containing new unknowns. These subgoals
519 unify with anything, creating a huge search space. The standard tactic
520 \ttindex{filt_resolve_tac}
521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
522 {\S\ref{filt_resolve_tac}})
524 fails for goals that are too flexible; so does the CTT tactic {\tt
525 test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they
526 achieve a simple kind of subgoal reordering: the less flexible subgoals are
527 attempted first. Do some single step proofs, or study the examples below,
528 to see why this is necessary.
529 \begin{ttdescription}
530 \item[\ttindexbold{test_assume_tac} $i$]
531 uses {\tt assume_tac} to solve the subgoal by assumption, but only if
532 subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.
535 \item[\ttindexbold{typechk_tac} $thms$]
536 uses $thms$ with formation, introduction, and elimination rules to check
537 the typing of constructions. It is designed to solve goals of the form
538 $a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
539 performs type inference. The tactic can also solve goals of
540 the form $A\;\rm type$.
542 \item[\ttindexbold{equal_tac} $thms$]
543 uses $thms$ with the long introduction and elimination rules to solve goals
544 of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving
545 the long rules for defined constants such as the arithmetic operators. The
546 tactic can also perform type-checking.
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$,
557 \section{Rewriting tactics}
559 rew_tac : thm list -> tactic
560 hyp_rew_tac : thm list -> tactic
562 Object-level simplification is accomplished through proof, using the {\tt
563 CTT} equality rules and the built-in rewriting functor
565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt
566 TSimpFun} is only useful for CTT and similar logics with type inference
567 rules. At present it is undocumented.}
569 The rewrites include the computation rules and other equations. The long
570 versions of the other rules permit rewriting of subterms and subtypes.
571 Also used are transitivity and the extra judgement form \cdx{Reduce}.
572 Meta-level simplification handles only definitional equality.
573 \begin{ttdescription}
574 \item[\ttindexbold{rew_tac} $thms$]
575 applies $thms$ and the computation rules as left-to-right rewrites. It
576 solves the goal $a=b\in A$ by rewriting $a$ to $b$. If $b$ is an unknown
577 then it is assigned the rewritten form of~$a$. All subgoals are rewritten.
579 \item[\ttindexbold{hyp_rew_tac} $thms$]
580 is like {\tt rew_tac}, but includes as rewrites any equations present in
585 \section{Tactics for logical reasoning}
586 Interpreting propositions as types lets CTT express statements of
587 intuitionistic logic. However, Constructive Type Theory is not just another
588 syntax for first-order logic. There are fundamental differences.
590 \index{assumptions!in CTT}
591 Can assumptions be deleted after use? Not every occurrence of a type
592 represents a proposition, and Type Theory assumptions declare variables.
593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
594 creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
595 can be deleted safely. In Type Theory, $+$-elimination with the assumption
596 $z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in
597 B$ (for arbitrary $x$ and $y$). Deleting $z\in A+B$ when other assumptions
598 refer to $z$ may render the subgoal unprovable: arguably,
601 Isabelle provides several tactics for predicate calculus reasoning in CTT:
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
610 These are loosely based on the intuitionistic proof procedures
611 of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for
612 propositional reasoning may be unsafe for type-checking; thus, some of the
613 `safe' tactics are misnamed.
614 \begin{ttdescription}
615 \item[\ttindexbold{mp_tac} $i$]
616 searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
617 $a\in A$, where~$A$ may be found by unification. It replaces
618 $f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter. The tactic
619 can produce multiple outcomes for each suitable pair of assumptions. In
620 short, {\tt mp_tac} performs Modus Ponens among the assumptions.
622 \item[\ttindexbold{add_mp_tac} $i$]
623 is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. It
624 avoids information loss but obviously loops if repeated.
626 \item[\ttindexbold{safestep_tac} $thms$ $i$]
627 attacks subgoal~$i$ using formation rules and certain other `safe' rules
628 (\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling
629 {\tt mp_tac} when appropriate. It also uses~$thms$,
630 which are typically premises of the rule being derived.
632 \item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by
633 means of backtracking, using {\tt safestep_tac}.
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.
639 \item[\ttindexbold{pc_tac} $thms$ $i$]
640 tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}.
646 \index{#+@{\tt\#+} symbol}
648 \index{"|"-@{{\tt"|"-"|} symbol}}
649 \index{#*@{\tt\#*} symbol}
653 \it symbol & \it meta-type & \it priority & \it description \\
654 \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\
655 \tt div & $[i,i]\To i$ & Left 70 & division\\
656 \tt mod & $[i,i]\To i$ & Left 70 & modulus\\
657 \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\
658 \tt - & $[i,i]\To i$ & Left 65 & subtraction\\
659 \verb'|-|' & $[i,i]\To i$ & Left 65 & absolute difference
663 \tdx{add_def} a#+b == rec(a, b, \%u v. succ(v))
664 \tdx{diff_def} a-b == rec(b, a, \%u v. rec(v, 0, \%x y. x))
665 \tdx{absdiff_def} a|-|b == (a-b) #+ (b-a)
666 \tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v)
668 \tdx{mod_def} a mod b ==
669 rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
671 \tdx{div_def} a div b ==
672 rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
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
678 \tdx{add_assoc} [| a:N; b:N; c:N |] ==>
679 (a #+ b) #+ c = a #+ (b #+ c) : N
681 \tdx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N
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
688 \tdx{add_mult_dist} [| a:N; b:N; c:N |] ==>
689 (a #+ b) #* c = (a #* c) #+ (b #* c) : N
691 \tdx{mult_assoc} [| a:N; b:N; c:N |] ==>
692 (a #* b) #* c = a #* (b #* c) : N
694 \tdx{diff_typing} [| a:N; b:N |] ==> a - b : N
695 \tdx{diffC0} a:N ==> a - 0 = a : N
696 \tdx{diff_0_eq_0} b:N ==> 0 - b = 0 : N
697 \tdx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
698 \tdx{diff_self_eq_0} a:N ==> a - a = 0 : N
699 \tdx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N
701 \caption{The theory of arithmetic} \label{ctt_arith}
705 \section{A theory of arithmetic}
706 \thydx{Arith} is a theory of elementary arithmetic. It proves the
707 properties of addition, multiplication, subtraction, division, and
708 remainder, culminating in the theorem
709 \[ a \bmod b + (a/b)\times b = a. \]
710 Figure~\ref{ctt_arith} presents the definitions and some of the key
711 theorems, including commutative, distributive, and associative laws.
713 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
714 and~\verb'div' stand for sum, difference, absolute difference, product,
715 remainder and quotient, respectively. Since Type Theory has only primitive
716 recursion, some of their definitions may be obscure.
718 The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
719 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
721 The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
722 as the successor of~$b-1$. Absolute difference is used to test the
723 equality $succ(v)=b$.
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$.
730 \section{The examples directory}
731 This directory contains examples and experimental proofs in CTT.
732 \begin{ttdescription}
733 \item[CTT/ex/typechk.ML]
734 contains simple examples of type-checking and type deduction.
736 \item[CTT/ex/elim.ML]
737 contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
740 \item[CTT/ex/equal.ML]
741 contains simple examples of rewriting.
743 \item[CTT/ex/synth.ML]
744 demonstrates the use of unknowns with some trivial examples of program
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,
753 unknown, takes shape in the course of the proof. Our example is the
754 predecessor function on the natural numbers.
756 Goal "lam n. rec(n, 0, \%x y. x) : ?A";
758 {\out lam n. rec(n,0,\%x y. x) : ?A}
759 {\out 1. lam n. rec(n,0,\%x y. x) : ?A}
761 Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
762 be confused with a meta-level abstraction), we apply the rule
763 \tdx{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a
764 product type of unknown domain and range.
766 by (resolve_tac [ProdI] 1);
768 {\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)}
770 {\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)}
772 Subgoal~1 is too flexible. It can be solved by instantiating~$\Var{A@1}$
773 to any type, but most instantiations will invalidate subgoal~2. We
774 therefore tackle the latter subgoal. It asks the type of a term beginning
775 with {\tt rec}, which can be found by $N$-elimination.%
778 by (eresolve_tac [NE] 2);
780 {\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)}
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))}
785 Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
786 natural numbers. However, let us continue proving nontrivial subgoals.
787 Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
789 by (resolve_tac [NI0] 2);
791 {\out lam n. rec(n,0,\%x y. x) : N --> N}
793 {\out 2. !!n x y. [| x : N; y : N |] ==> x : N}
795 The type~$\Var{A}$ is now fully determined. It is the product type
796 $\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
797 there is no dependence on~$x$. But we must prove all the subgoals to show
798 that the original term is validly typed. Subgoal~2 is provable by
799 assumption and the remaining subgoal falls by $N$-formation.%
804 {\out lam n. rec(n,0,\%x y. x) : N --> N}
807 by (resolve_tac [NF] 1);
809 {\out lam n. rec(n,0,\%x y. x) : N --> N}
812 Calling \ttindex{typechk_tac} can prove this theorem in one step.
814 Even if the original term is ill-typed, one can infer a type for it, but
815 unprovable subgoals will be left. As an exercise, try to prove the
816 following invalid goal:
818 Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
823 \section{An example of logical reasoning}
824 Logical reasoning in Type Theory involves proving a goal of the form
825 $\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands
826 for its proof term, a value of type $A$. The proof term is initially
827 unknown and takes shape during the proof.
829 Our example expresses a theorem about quantifiers in a sorted logic:
830 \[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
831 {\ex{x\in A}P(x)\disj Q(x)}
833 By the propositions-as-types principle, this is encoded
834 using~$\Sigma$ and~$+$ types. A special case of it expresses a
835 distributive law of Type Theory:
836 \[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
837 Generalizing this from $\times$ to $\Sigma$, and making the typing
838 conditions explicit, yields the rule we must derive:
839 \[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
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)}
845 To begin, we bind the rule's premises --- returned by the~{\tt goal}
846 command --- to the {\ML} variable~{\tt prems}.
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))";
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))}
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)]"]}
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
869 cut_facts_tac prems 1;
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}
876 by (resolve_tac (prems RL [SumE]) 1);
878 {\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
880 {\out [| x : A; y : B(x) + C(x) |] ==>}
881 {\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
883 The subgoal has two new parameters, $x$ and~$y$. In the main goal,
884 $\Var{a}$ has been instantiated with a \cdx{split} term. The
885 assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
886 creating the parameter~$xa$. This inference also inserts~\cdx{when}
887 into the main goal.\index{*PlusE theorem}
889 by (eresolve_tac [PlusE] 1);
891 {\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))}
892 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
894 {\out [| x : A; xa : B(x) |] ==>}
895 {\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
898 {\out [| x : A; ya : C(x) |] ==>}
899 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
901 To complete the proof object for the main goal, we need to instantiate the
902 terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$. We attack subgoal~1 by
903 a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
904 injection~(\cdx{inl}).
905 \index{*PlusI_inl theorem}
907 by (resolve_tac [PlusI_inl] 1);
909 {\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
910 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
911 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
912 {\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
915 {\out [| x : A; ya : C(x) |] ==>}
916 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
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}
924 by (resolve_tac [SumI] 1);
926 {\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
927 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
928 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
929 {\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
930 {\out 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
932 {\out [| x : A; ya : C(x) |] ==>}
933 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
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.
940 {\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
941 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
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}
946 {\out [| x : A; ya : C(x) |] ==>}
947 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
951 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
952 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
953 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
955 {\out [| x : A; ya : C(x) |] ==>}
956 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
958 Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.
959 Such subgoals are usually trivial; this one yields to
960 \ttindex{typechk_tac}, given the current list of premises.
962 by (typechk_tac prems);
964 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
965 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
967 {\out [| x : A; ya : C(x) |] ==>}
968 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
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.
976 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))}
977 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
980 Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
984 \section{Example: deriving a currying functional}
985 In simply-typed languages such as {\ML}, a currying functional has the type
986 \[ (A\times B \to C) \to (A\to (B\to C)). \]
987 Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.
988 The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
989 to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
990 $C(\langle x,y\rangle)$.
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$.
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>))";
1006 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
1007 {\out (PROD x:A. PROD y:B(x). C(<x,y>))}
1008 {\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
1009 {\out (PROD x:A. PROD y:B(x). C(<x,y>))}
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}
1016 This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic
1017 repeatedly applies $\Pi$-introduction and proves the rather
1018 tiresome typing conditions.
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.
1026 by (intr_tac prems);
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>))}
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>)}
1034 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
1035 \index{*ProdE theorem}
1037 by (eresolve_tac [ProdE] 1);
1039 {\out lam x xa xb. x ` <xa,xb>}
1040 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
1041 {\out 1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
1043 Finally, we verify that the argument's type is suitable for the function
1044 application. This is straightforward using introduction rules.
1047 by (intr_tac prems);
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>))}
1053 Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
1054 also prove an example by Martin-L\"of, related to $\disj$-elimination
1055 \cite[page~58]{martinlof84}.
1058 \section{Example: proving the Axiom of Choice} \label{ctt-choice}
1059 Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
1060 which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
1061 Interpreting propositions as types, this asserts that for all $x\in A$
1062 there exists $y\in B(x)$ such that $C(x,y)$. The Axiom of Choice asserts
1063 that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
1064 $C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
1065 function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
1067 In principle, the Axiom of Choice is simple to derive in Constructive Type
1068 Theory. The following definitions work:
1070 f & \equiv & {\tt fst} \circ h \\
1071 g & \equiv & {\tt snd} \circ h
1073 But a completely formal proof is hard to find. The rules can be applied in
1074 countless ways, yielding many higher-order unifiers. The proof can get
1075 bogged down in the details. But with a careful selection of derived rules
1076 (recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
1077 prove the theorem in nine steps.
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))";
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))}
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]"]}
1096 First, \ttindex{intr_tac} applies introduction rules and performs routine
1097 type-checking. This instantiates~$\Var{a}$ to a construction involving
1098 a $\lambda$-abstraction and an ordered pair. The pair's components are
1099 themselves $\lambda$-abstractions and there is a subgoal for each.
1101 by (intr_tac prems);
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))}
1108 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1109 {\out ?b7(h,x) : B(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)}
1115 Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
1116 $\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof
1117 object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
1118 result lie in the relation~$C$. This latter task will take up most of the
1120 \index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}
1122 by (eresolve_tac [ProdE RS SumE_fst] 1);
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))}
1128 {\out 1. !!h x. x : A ==> x : A}
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)}
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
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))}
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)}
1146 Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
1147 simplified. The derived rule \tdx{replace_type} lets us replace a type
1148 by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
1150 by (resolve_tac [replace_type] 1);
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))}
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)}
1161 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1162 {\out ?b8(h,x) : ?A13(h,x)}
1164 The derived rule \tdx{subst_eqtyparg} lets us simplify a type's
1165 argument (by currying, $C(x)$ is a unary type operator):
1167 by (resolve_tac [subst_eqtyparg] 1);
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))}
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)}
1178 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
1179 {\out z : ?A14(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))}
1186 Subgoal~1 requires simply $\beta$-contraction, which is the rule
1187 \tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal
1188 receives the contracted result.
1190 by (resolve_tac [ProdC] 1);
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))}
1197 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1198 {\out x : ?A15(h,x)}
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)}
1206 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
1207 {\out z : ?B15(h,x,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))}
1214 Routine type-checking goals proliferate in Constructive Type Theory, but
1215 \ttindex{typechk_tac} quickly solves them. Note the inclusion of
1216 \tdx{SumE_fst} along with the premises.
1218 by (typechk_tac (SumE_fst::prems));
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))}
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))}
1228 We are finally ready to compose {\tt snd} with~$h$.
1229 \index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}
1231 by (eresolve_tac [ProdE RS SumE_snd] 1);
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))}
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}
1241 The proof object has reached its final form. We call \ttindex{typechk_tac}
1242 to finish the type-checking.
1244 by (typechk_tac prems);
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))}
1251 It might be instructive to compare this proof with Martin-L\"of's forward
1252 proof of the Axiom of Choice \cite[page~50]{martinlof84}.
1254 \index{Constructive Type Theory|)}