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