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))
673 \tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N
674 \tdx{addC0} b:N ==> 0 #+ b = b : N
675 \tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
677 \tdx{add_assoc} [| a:N; b:N; c:N |] ==>
678 (a #+ b) #+ c = a #+ (b #+ c) : N
680 \tdx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N
682 \tdx{mult_typing} [| a:N; b:N |] ==> a #* b : N
683 \tdx{multC0} b:N ==> 0 #* b = 0 : N
684 \tdx{multC_succ} [| a:N; b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
685 \tdx{mult_commute} [| a:N; b:N |] ==> a #* b = b #* a : N
687 \tdx{add_mult_dist} [| a:N; b:N; c:N |] ==>
688 (a #+ b) #* c = (a #* c) #+ (b #* c) : N
690 \tdx{mult_assoc} [| a:N; b:N; c:N |] ==>
691 (a #* b) #* c = a #* (b #* c) : N
693 \tdx{diff_typing} [| a:N; b:N |] ==> a - b : N
694 \tdx{diffC0} a:N ==> a - 0 = a : N
695 \tdx{diff_0_eq_0} b:N ==> 0 - b = 0 : N
696 \tdx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
697 \tdx{diff_self_eq_0} a:N ==> a - a = 0 : N
698 \tdx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N
699 \caption{The theory of arithmetic} \label{ctt-arith}
704 \section{A theory of arithmetic}
705 \thydx{Arith} is a theory of elementary arithmetic. It proves the
706 properties of addition, multiplication, subtraction, division, and
707 remainder, culminating in the theorem
708 \[ a \bmod b + (a/b)\times b = a. \]
709 Figure~\ref{ctt-arith} presents the definitions and some of the key
710 theorems, including commutative, distributive, and associative laws.
712 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
713 and~\verb'div' stand for sum, difference, absolute difference, product,
714 remainder and quotient, respectively. Since Type Theory has only primitive
715 recursion, some of their definitions may be obscure.
717 The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
718 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$.
720 The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
721 as the successor of~$b-1$. Absolute difference is used to test the
722 equality $succ(v)=b$.
724 The quotient $a/b$ is computed by adding one for every number $x$
725 such that $0\leq x \leq a$ and $x\bmod b = 0$.
729 \section{The examples directory}
730 This directory contains examples and experimental proofs in {\CTT}.
731 \begin{ttdescription}
732 \item[CTT/ex/typechk.ML]
733 contains simple examples of type checking and type deduction.
735 \item[CTT/ex/elim.ML]
736 contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
739 \item[CTT/ex/equal.ML]
740 contains simple examples of rewriting.
742 \item[CTT/ex/synth.ML]
743 demonstrates the use of unknowns with some trivial examples of program
748 \section{Example: type inference}
749 Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
750 is a term and $\Var{A}$ is an unknown standing for its type. The type,
752 unknown, takes shape in the course of the proof. Our example is the
753 predecessor function on the natural numbers.
755 goal CTT.thy "lam n. rec(n, 0, \%x y.x) : ?A";
757 {\out lam n. rec(n,0,\%x y. x) : ?A}
758 {\out 1. lam n. rec(n,0,\%x y. x) : ?A}
760 Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
761 be confused with a meta-level abstraction), we apply the rule
762 \tdx{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a
763 product type of unknown domain and range.
765 by (resolve_tac [ProdI] 1);
767 {\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)}
769 {\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)}
771 Subgoal~1 is too flexible. It can be solved by instantiating~$\Var{A@1}$
772 to any type, but most instantiations will invalidate subgoal~2. We
773 therefore tackle the latter subgoal. It asks the type of a term beginning
774 with {\tt rec}, which can be found by $N$-elimination.%
777 by (eresolve_tac [NE] 2);
779 {\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)}
781 {\out 2. !!n. 0 : ?C2(n,0)}
782 {\out 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))}
784 Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
785 natural numbers. However, let us continue proving nontrivial subgoals.
786 Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
788 by (resolve_tac [NI0] 2);
790 {\out lam n. rec(n,0,\%x y. x) : N --> N}
792 {\out 2. !!n x y. [| x : N; y : N |] ==> x : N}
794 The type~$\Var{A}$ is now fully determined. It is the product type
795 $\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
796 there is no dependence on~$x$. But we must prove all the subgoals to show
797 that the original term is validly typed. Subgoal~2 is provable by
798 assumption and the remaining subgoal falls by $N$-formation.%
803 {\out lam n. rec(n,0,\%x y. x) : N --> N}
806 by (resolve_tac [NF] 1);
808 {\out lam n. rec(n,0,\%x y. x) : N --> N}
811 Calling \ttindex{typechk_tac} can prove this theorem in one step.
813 Even if the original term is ill-typed, one can infer a type for it, but
814 unprovable subgoals will be left. As an exercise, try to prove the
815 following invalid goal:
817 goal CTT.thy "lam n. rec(n, 0, \%x y.tt) : ?A";
822 \section{An example of logical reasoning}
823 Logical reasoning in Type Theory involves proving a goal of the form
824 $\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands
825 for its proof term, a value of type $A$. The proof term is initially
826 unknown and takes shape during the proof.
828 Our example expresses a theorem about quantifiers in a sorted logic:
829 \[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
830 {\ex{x\in A}P(x)\disj Q(x)}
832 By the propositions-as-types principle, this is encoded
833 using~$\Sigma$ and~$+$ types. A special case of it expresses a
834 distributive law of Type Theory:
835 \[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
836 Generalizing this from $\times$ to $\Sigma$, and making the typing
837 conditions explicit, yields the rule we must derive:
838 \[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
840 \infer*{\hbox{$B(x)$ type}}{[x\in A]} &
841 \infer*{\hbox{$C(x)$ type}}{[x\in A]} &
842 p\in \sum@{x\in A} B(x)+C(x)}
844 To begin, we bind the rule's premises --- returned by the~{\tt goal}
845 command --- to the {\ML} variable~{\tt prems}.
847 val prems = goal CTT.thy
849 \ttback !!x. x:A ==> B(x) type; \ttback
850 \ttback !!x. x:A ==> C(x) type; \ttback
851 \ttback p: SUM x:A. B(x) + C(x) \ttback
852 \ttback |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
854 {\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
855 {\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
857 {\out val prems = ["A type [A type]",}
858 {\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
859 {\out "?x : A ==> C(?x) type [!!x. x : A ==> C(x) type]",}
860 {\out "p : SUM x:A. B(x) + C(x) [p : SUM x:A. B(x) + C(x)]"]}
863 The last premise involves the sum type~$\Sigma$. Since it is a premise
864 rather than the assumption of a goal, it cannot be found by {\tt
865 eresolve_tac}. We could insert it (and the other atomic premise) by
868 cut_facts_tac prems 1;
870 A forward proof step is more straightforward here. Let us resolve the
871 $\Sigma$-elimination rule with the premises using~\ttindex{RL}. This
872 inference yields one result, which we supply to {\tt
873 resolve_tac}.\index{*SumE theorem}
875 by (resolve_tac (prems RL [SumE]) 1);
877 {\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
879 {\out [| x : A; y : B(x) + C(x) |] ==>}
880 {\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
882 The subgoal has two new parameters, $x$ and~$y$. In the main goal,
883 $\Var{a}$ has been instantiated with a \cdx{split} term. The
884 assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
885 creating the parameter~$xa$. This inference also inserts~\cdx{when}
886 into the main goal.\index{*PlusE theorem}
888 by (eresolve_tac [PlusE] 1);
890 {\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))}
891 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
893 {\out [| x : A; xa : B(x) |] ==>}
894 {\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
897 {\out [| x : A; ya : C(x) |] ==>}
898 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
900 To complete the proof object for the main goal, we need to instantiate the
901 terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$. We attack subgoal~1 by
902 a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
903 injection~(\cdx{inl}).
904 \index{*PlusI_inl theorem}
906 by (resolve_tac [PlusI_inl] 1);
908 {\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
909 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
910 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
911 {\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
914 {\out [| x : A; ya : C(x) |] ==>}
915 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
917 A new subgoal~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
918 Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.
919 This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains
920 an ordered pair, whose components are two new unknowns.%
921 \index{*SumI theorem}
923 by (resolve_tac [SumI] 1);
925 {\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
926 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
927 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
928 {\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
929 {\out 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
931 {\out [| x : A; ya : C(x) |] ==>}
932 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
934 The two new subgoals both hold by assumption. Observe how the unknowns
935 $\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state.
939 {\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
940 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
942 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)}
943 {\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
945 {\out [| x : A; ya : C(x) |] ==>}
946 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
950 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
951 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
952 {\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
954 {\out [| x : A; ya : C(x) |] ==>}
955 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
957 Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.
958 Such subgoals are usually trivial; this one yields to
959 \ttindex{typechk_tac}, given the current list of premises.
961 by (typechk_tac prems);
963 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
964 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
966 {\out [| x : A; ya : C(x) |] ==>}
967 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
969 This subgoal is the other case from the $+$-elimination above, and can be
970 proved similarly. Quicker is to apply \ttindex{pc_tac}. The main goal
971 finally gets a fully instantiated proof object.
975 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))}
976 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
979 Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
983 \section{Example: deriving a currying functional}
984 In simply-typed languages such as {\ML}, a currying functional has the type
985 \[ (A\times B \to C) \to (A\to (B\to C)). \]
986 Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.
987 The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
988 to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
989 $C(\langle x,y\rangle)$.
991 Formally, there are three typing premises. $A$ is a type; $B$ is an
992 $A$-indexed family of types; $C$ is a family of types indexed by
993 $\Sigma(A,B)$. The goal is expressed using \hbox{\tt PROD f} to ensure
994 that the parameter corresponding to the functional's argument is really
995 called~$f$; Isabelle echoes the type using \verb|-->| because there is no
996 explicit dependence upon~$f$.
998 val prems = goal CTT.thy
999 "[| A type; !!x. x:A ==> B(x) type; \ttback
1000 \ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback
1001 \ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback
1002 \ttback (PROD x:A . PROD y:B(x) . C(<x,y>))";
1005 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
1006 {\out (PROD x:A. PROD y:B(x). C(<x,y>))}
1007 {\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
1008 {\out (PROD x:A. PROD y:B(x). C(<x,y>))}
1010 {\out val prems = ["A type [A type]",}
1011 {\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
1012 {\out "?z : SUM x:A. B(x) ==> C(?z) type}
1013 {\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
1015 This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic
1016 repeatedly applies $\Pi$-introduction and proves the rather
1017 tiresome typing conditions.
1019 Note that $\Var{a}$ becomes instantiated to three nested
1020 $\lambda$-abstractions. It would be easier to read if the bound variable
1021 names agreed with the parameters in the subgoal. Isabelle attempts to give
1022 parameters the same names as corresponding bound variables in the goal, but
1023 this does not always work. In any event, the goal is logically correct.
1025 by (intr_tac prems);
1027 {\out lam x xa xb. ?b7(x,xa,xb)}
1028 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
1030 {\out [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
1031 {\out ?b7(f,x,y) : C(<x,y>)}
1033 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
1034 \index{*ProdE theorem}
1036 by (eresolve_tac [ProdE] 1);
1038 {\out lam x xa xb. x ` <xa,xb>}
1039 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
1040 {\out 1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
1042 Finally, we verify that the argument's type is suitable for the function
1043 application. This is straightforward using introduction rules.
1046 by (intr_tac prems);
1048 {\out lam x xa xb. x ` <xa,xb>}
1049 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
1052 Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
1053 also prove an example by Martin-L\"of, related to $\disj$-elimination
1054 \cite[page~58]{martinlof84}.
1057 \section{Example: proving the Axiom of Choice} \label{ctt-choice}
1058 Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
1059 which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
1060 Interpreting propositions as types, this asserts that for all $x\in A$
1061 there exists $y\in B(x)$ such that $C(x,y)$. The Axiom of Choice asserts
1062 that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
1063 $C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
1064 function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
1066 In principle, the Axiom of Choice is simple to derive in Constructive Type
1067 Theory. The following definitions work:
1069 f & \equiv & {\tt fst} \circ h \\
1070 g & \equiv & {\tt snd} \circ h
1072 But a completely formal proof is hard to find. The rules can be applied in
1073 countless ways, yielding many higher-order unifiers. The proof can get
1074 bogged down in the details. But with a careful selection of derived rules
1075 (recall Fig.\ts\ref{ctt-derived}) and the type checking tactics, we can
1076 prove the theorem in nine steps.
1078 val prems = goal CTT.thy
1079 "[| A type; !!x. x:A ==> B(x) type; \ttback
1080 \ttback !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ttback
1081 \ttback |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ttback
1082 \ttback (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
1084 {\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1085 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1086 {\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1087 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1089 {\out val prems = ["A type [A type]",}
1090 {\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
1091 {\out "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
1092 {\out [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
1095 First, \ttindex{intr_tac} applies introduction rules and performs routine
1096 type checking. This instantiates~$\Var{a}$ to a construction involving
1097 a $\lambda$-abstraction and an ordered pair. The pair's components are
1098 themselves $\lambda$-abstractions and there is a subgoal for each.
1100 by (intr_tac prems);
1102 {\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
1103 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1104 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1107 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1108 {\out ?b7(h,x) : B(x)}
1111 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1112 {\out ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)}
1114 Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
1115 $\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof
1116 object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
1117 result lie in the relation~$C$. This latter task will take up most of the
1119 \index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}
1121 by (eresolve_tac [ProdE RS SumE_fst] 1);
1123 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
1124 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1125 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1127 {\out 1. !!h x. x : A ==> x : A}
1129 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1130 {\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
1132 Above, we have composed {\tt fst} with the function~$h$. Unification
1133 has deduced that the function must be applied to $x\in A$. We have our
1138 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
1139 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1140 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1142 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1143 {\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
1145 Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
1146 simplified. The derived rule \tdx{replace_type} lets us replace a type
1147 by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
1149 by (resolve_tac [replace_type] 1);
1151 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
1152 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1153 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1156 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1157 {\out C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)}
1160 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1161 {\out ?b8(h,x) : ?A13(h,x)}
1163 The derived rule \tdx{subst_eqtyparg} lets us simplify a type's
1164 argument (by currying, $C(x)$ is a unary type operator):
1166 by (resolve_tac [subst_eqtyparg] 1);
1168 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
1169 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1170 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1173 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1174 {\out (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)}
1177 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
1178 {\out z : ?A14(h,x) |] ==>}
1182 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1183 {\out ?b8(h,x) : C(x,?c14(h,x))}
1185 Subgoal~1 requires simply $\beta$-contraction, which is the rule
1186 \tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal
1187 receives the contracted result.
1189 by (resolve_tac [ProdC] 1);
1191 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
1192 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1193 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1196 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1197 {\out x : ?A15(h,x)}
1200 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
1201 {\out xa : ?A15(h,x) |] ==>}
1202 {\out fst(h ` xa) : ?B15(h,x,xa)}
1205 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
1206 {\out z : ?B15(h,x,x) |] ==>}
1210 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1211 {\out ?b8(h,x) : C(x,fst(h ` x))}
1213 Routine type checking goals proliferate in Constructive Type Theory, but
1214 \ttindex{typechk_tac} quickly solves them. Note the inclusion of
1215 \tdx{SumE_fst} along with the premises.
1217 by (typechk_tac (SumE_fst::prems));
1219 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
1220 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1221 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1224 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
1225 {\out ?b8(h,x) : C(x,fst(h ` x))}
1227 We are finally ready to compose {\tt snd} with~$h$.
1228 \index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}
1230 by (eresolve_tac [ProdE RS SumE_snd] 1);
1232 {\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
1233 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1234 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1236 {\out 1. !!h x. x : A ==> x : A}
1237 {\out 2. !!h x. x : A ==> B(x) type}
1238 {\out 3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
1240 The proof object has reached its final form. We call \ttindex{typechk_tac}
1241 to finish the type checking.
1243 by (typechk_tac prems);
1245 {\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
1246 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1247 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1250 It might be instructive to compare this proof with Martin-L\"of's forward
1251 proof of the Axiom of Choice \cite[page~50]{martinlof84}.
1253 \index{Constructive Type Theory|)}