104

1 
%% $Id$


2 
\chapter{Constructive Type Theory}


3 
MartinL\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can


4 
be viewed at many different levels. It is a formal system that embodies


5 
the principles of intuitionistic mathematics; it embodies the


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


7 
programs from proofs. The logic is complex and many authors have attempted


8 
to simplify it. Thompson~\cite{thompson91} is a readable and thorough


9 
account of the theory.


10 


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


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


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


14 
judgement was


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


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


17 
\]


18 
This sequent calculus was not satisfactory because assumptions like


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


20 
could not be formalized.


21 


22 
The directory~\ttindexbold{CTT} implements Constructive Type Theory, using


23 
natural deduction. The judgement above is expressed using $\Forall$ and


24 
$\Imp$:


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


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

111

27 
\List{x@1\in A@1;


28 
x@2\in A@2(x@1); \cdots \;


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

104

30 
& \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n)


31 
\end{array}


32 
\]


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


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


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


36 
To justify the {\CTT} formulation it is probably best to appeal directly


37 
to the semantic explanations of the rules~\cite{martinlof84}, rather than


38 
to the rules themselves. The order of assumptions no longer matters,


39 
unlike in standard Type Theory. Contexts, which are typical of many modern


40 
type theories, are difficult to represent in Isabelle. In particular, it


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


42 


43 
The theory has the {\ML} identifier \ttindexbold{CTT.thy}. It does not


44 
use polymorphism. Terms in {\CTT} have type~$i$, the type of individuals.


45 
Types in {\CTT} have type~$t$.


46 


47 
{\CTT} supports all of Type Theory apart from list types, well ordering


48 
types, and universes. Universes could be introduced {\em\`a la Tarski},


49 
adding new constants as names for types. The formulation {\em\`a la


50 
Russell}, where types denote themselves, is only possible if we identify


51 
the metatypes~$i$ and~$o$. Most published formulations of well ordering


52 
types have difficulties involving extensionality of functions; I suggest


53 
that you use some other method for defining recursive types. List types


54 
are easy to introduce by declaring new rules.


55 


56 
{\CTT} uses the 1982 version of Type Theory, with extensional equality.


57 
The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are


58 
interchangeable. Its rewriting tactics prove theorems of the form $a=b\in


59 
A$. It could be modified to have intensional equality, but rewriting


60 
tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the


61 
computation rules might require a second simplifier.


62 


63 


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


65 
\begin{center}


66 
\begin{tabular}{rrr}

111

67 
\it symbol & \it metatype & \it description \\


68 
\idx{Type} & $t \to prop$ & judgement form \\


69 
\idx{Eqtype} & $[t,t]\to prop$ & judgement form\\


70 
\idx{Elem} & $[i, t]\to prop$ & judgement form\\


71 
\idx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\


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

104

73 

111

74 
\idx{N} & $t$ & natural numbers type\\


75 
\idx{0} & $i$ & constructor\\


76 
\idx{succ} & $i\to i$ & constructor\\

104

77 
\idx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex]

111

78 
\idx{Prod} & $[t,i\to t]\to t$ & general product type\\


79 
\idx{lambda} & $(i\to i)\to i$ & constructor\\[2ex]


80 
\idx{Sum} & $[t, i\to t]\to t$ & general sum type\\


81 
\idx{pair} & $[i,i]\to i$ & constructor\\


82 
\idx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\


83 
\idx{fst} snd & $i\to i$ & projections\\[2ex]


84 
\idx{inl} inr & $i\to i$ & constructors for $+$\\

104

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

111

86 
\idx{Eq} & $[t,i,i]\to t$ & equality type\\


87 
\idx{eq} & $i$ & constructor\\[2ex]


88 
\idx{F} & $t$ & empty type\\


89 
\idx{contr} & $i\to i$ & eliminator\\[2ex]


90 
\idx{T} & $t$ & singleton type\\


91 
\idx{tt} & $i$ & constructor

104

92 
\end{tabular}


93 
\end{center}


94 
\caption{The constants of {\CTT}} \label{cttconstants}


95 
\end{figure}


96 


97 


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


99 
\begin{center}


100 
\begin{tabular}{llrrr}

111

101 
\it symbol &\it name &\it metatype & \it precedence & \it description \\

104

102 
\idx{lam} & \idx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$abstraction


103 
\end{tabular}


104 
\end{center}


105 
\subcaption{Binders}


106 


107 
\begin{center}


108 
\indexbold{*"`}


109 
\indexbold{*"+}


110 
\begin{tabular}{rrrr}


111 
\it symbol & \it metatype & \it precedence & \it description \\

111

112 
\tt ` & $[i,i]\to i$ & Left 55 & function application\\


113 
\tt + & $[t,t]\to t$ & Right 30 & sum of two types

104

114 
\end{tabular}


115 
\end{center}


116 
\subcaption{Infixes}


117 


118 
\indexbold{*"*}


119 
\indexbold{*""">}


120 
\begin{center} \tt\frenchspacing


121 
\begin{tabular}{rrr}

111

122 
\it external & \it internal & \it standard notation \\


123 
\idx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) &


124 
\rm product $\prod@{x\in A}B[x]$ \\


125 
\idx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) &


126 
\rm sum $\sum@{x\in A}B[x]$ \\

104

127 
$A$ > $B$ & Prod($A$, $\lambda x.B$) &

111

128 
\rm function space $A\to B$ \\

104

129 
$A$ * $B$ & Sum($A$, $\lambda x.B$) &

111

130 
\rm binary product $A\times B$

104

131 
\end{tabular}


132 
\end{center}


133 
\subcaption{Translations}


134 


135 
\indexbold{*"=}


136 
\begin{center}


137 
\dquotes


138 
\[ \begin{array}{rcl}

111

139 
prop & = & type " type" \\


140 
&  & type " = " type \\


141 
&  & term " : " type \\


142 
&  & term " = " term " : " type

104

143 
\\[2ex]

111

144 
type & = & \hbox{expression of type~$t$} \\


145 
&  & "PROD~" id " : " type " . " type \\


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

104

147 
\\[2ex]

111

148 
term & = & \hbox{expression of type~$i$} \\


149 
&  & "lam " id~id^* " . " term \\


150 
&  & "< " term " , " term " >"

104

151 
\end{array}


152 
\]


153 
\end{center}


154 
\subcaption{Grammar}


155 
\caption{Syntax of {\CTT}} \label{cttsyntax}


156 
\end{figure}


157 


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


159 


160 


161 
\section{Syntax}


162 
The constants are shown in Figure~\ref{cttconstants}. The infixes include


163 
the function application operator (sometimes called `apply'), and the


164 
2place type operators. Note that metalevel abstraction and application,


165 
$\lambda x.b$ and $f(a)$, differ from objectlevel abstraction and


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


167 
function~$f$ is simply an individual as far as Isabelle is concerned: its


168 
Isabelle type is~$i$, not say $i\To i$.


169 


170 
\indexbold{*F}\indexbold{*T}\indexbold{*SUM}\indexbold{*PROD}


171 
The empty type is called $F$ and the oneelement type is $T$; other finite


172 
sets are built as $T+T+T$, etc. The notation for~{\CTT}


173 
(Figure~\ref{cttsyntax}) is based on that of Nordstr\"om et


174 
al.~\cite{nordstrom90}. We can write


175 
\begin{ttbox}


176 
SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, %y. Prod(A, %x. C(x,y)))


177 
\end{ttbox}


178 
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$>$B$} abbreviate


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


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


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


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


183 


184 


185 
\begin{figure}


186 
\begin{ttbox}


187 
\idx{refl_type} A type ==> A = A


188 
\idx{refl_elem} a : A ==> a = a : A


189 


190 
\idx{sym_type} A = B ==> B = A


191 
\idx{sym_elem} a = b : A ==> b = a : A


192 


193 
\idx{trans_type} [ A = B; B = C ] ==> A = C


194 
\idx{trans_elem} [ a = b : A; b = c : A ] ==> a = c : A


195 


196 
\idx{equal_types} [ a : A; A = B ] ==> a : B


197 
\idx{equal_typesL} [ a = b : A; A = B ] ==> a = b : B


198 


199 
\idx{subst_type} [ a : A; !!z. z:A ==> B(z) type ] ==> B(a) type


200 
\idx{subst_typeL} [ a = c : A; !!z. z:A ==> B(z) = D(z)


201 
] ==> B(a) = D(c)


202 


203 
\idx{subst_elem} [ a : A; !!z. z:A ==> b(z):B(z) ] ==> b(a):B(a)


204 
\idx{subst_elemL} [ a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)


205 
] ==> b(a) = d(c) : B(a)


206 


207 
\idx{refl_red} Reduce(a,a)


208 
\idx{red_if_equal} a = b : A ==> Reduce(a,b)


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


210 
\end{ttbox}


211 
\caption{General equality rules} \label{cttequality}


212 
\end{figure}


213 


214 


215 
\begin{figure}


216 
\begin{ttbox}


217 
\idx{NF} N type


218 


219 
\idx{NI0} 0 : N


220 
\idx{NI_succ} a : N ==> succ(a) : N


221 
\idx{NI_succL} a = b : N ==> succ(a) = succ(b) : N


222 


223 
\idx{NE} [ p: N; a: C(0);


224 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u))


225 
] ==> rec(p, a, %u v.b(u,v)) : C(p)


226 


227 
\idx{NEL} [ p = q : N; a = c : C(0);


228 
!!u v. [ u: N; v: C(u) ] ==> b(u,v)=d(u,v): C(succ(u))


229 
] ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)


230 


231 
\idx{NC0} [ a: C(0);


232 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u))


233 
] ==> rec(0, a, %u v.b(u,v)) = a : C(0)


234 


235 
\idx{NC_succ} [ p: N; a: C(0);


236 
!!u v. [ u: N; v: C(u) ] ==> b(u,v): C(succ(u))


237 
] ==> rec(succ(p), a, %u v.b(u,v)) =


238 
b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))


239 


240 
\idx{zero_ne_succ} [ a: N; 0 = succ(a) : N ] ==> 0: F


241 
\end{ttbox}


242 
\caption{Rules for type~$N$} \label{cttN}


243 
\end{figure}


244 


245 


246 
\begin{figure}


247 
\begin{ttbox}


248 
\idx{ProdF} [ A type; !!x. x:A ==> B(x) type ] ==> PROD x:A.B(x) type


249 
\idx{ProdFL} [ A = C; !!x. x:A ==> B(x) = D(x) ] ==>


250 
PROD x:A.B(x) = PROD x:C.D(x)


251 


252 
\idx{ProdI} [ A type; !!x. x:A ==> b(x):B(x)


253 
] ==> lam x.b(x) : PROD x:A.B(x)


254 
\idx{ProdIL} [ A type; !!x. x:A ==> b(x) = c(x) : B(x)


255 
] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x)


256 


257 
\idx{ProdE} [ p : PROD x:A.B(x); a : A ] ==> p`a : B(a)


258 
\idx{ProdEL} [ p=q: PROD x:A.B(x); a=b : A ] ==> p`a = q`b : B(a)


259 


260 
\idx{ProdC} [ a : A; !!x. x:A ==> b(x) : B(x)


261 
] ==> (lam x.b(x)) ` a = b(a) : B(a)


262 


263 
\idx{ProdC2} p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)


264 
\end{ttbox}


265 
\caption{Rules for the product type $\prod@{x\in A}B[x]$} \label{cttprod}


266 
\end{figure}


267 


268 


269 
\begin{figure}


270 
\begin{ttbox}


271 
\idx{SumF} [ A type; !!x. x:A ==> B(x) type ] ==> SUM x:A.B(x) type


272 
\idx{SumFL} [ A = C; !!x. x:A ==> B(x) = D(x)


273 
] ==> SUM x:A.B(x) = SUM x:C.D(x)


274 


275 
\idx{SumI} [ a : A; b : B(a) ] ==> <a,b> : SUM x:A.B(x)


276 
\idx{SumIL} [ a=c:A; b=d:B(a) ] ==> <a,b> = <c,d> : SUM x:A.B(x)


277 


278 
\idx{SumE} [ p: SUM x:A.B(x);


279 
!!x y. [ x:A; y:B(x) ] ==> c(x,y): C(<x,y>)


280 
] ==> split(p, %x y.c(x,y)) : C(p)


281 


282 
\idx{SumEL} [ p=q : SUM x:A.B(x);


283 
!!x y. [ x:A; y:B(x) ] ==> c(x,y)=d(x,y): C(<x,y>)


284 
] ==> split(p, %x y.c(x,y)) = split(q, %x y.d(x,y)) : C(p)


285 


286 
\idx{SumC} [ a: A; b: B(a);


287 
!!x y. [ x:A; y:B(x) ] ==> c(x,y): C(<x,y>)


288 
] ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)


289 


290 
\idx{fst_def} fst(a) == split(a, %x y.x)


291 
\idx{snd_def} snd(a) == split(a, %x y.y)


292 
\end{ttbox}


293 
\caption{Rules for the sum type $\sum@{x\in A}B[x]$} \label{cttsum}


294 
\end{figure}


295 


296 


297 
\begin{figure}


298 
\begin{ttbox}


299 
\idx{PlusF} [ A type; B type ] ==> A+B type


300 
\idx{PlusFL} [ A = C; B = D ] ==> A+B = C+D


301 


302 
\idx{PlusI_inl} [ a : A; B type ] ==> inl(a) : A+B


303 
\idx{PlusI_inlL} [ a = c : A; B type ] ==> inl(a) = inl(c) : A+B


304 


305 
\idx{PlusI_inr} [ A type; b : B ] ==> inr(b) : A+B


306 
\idx{PlusI_inrL} [ A type; b = d : B ] ==> inr(b) = inr(d) : A+B


307 


308 
\idx{PlusE} [ p: A+B;


309 
!!x. x:A ==> c(x): C(inl(x));


310 
!!y. y:B ==> d(y): C(inr(y))


311 
] ==> when(p, %x.c(x), %y.d(y)) : C(p)


312 


313 
\idx{PlusEL} [ p = q : A+B;


314 
!!x. x: A ==> c(x) = e(x) : C(inl(x));


315 
!!y. y: B ==> d(y) = f(y) : C(inr(y))


316 
] ==> when(p, %x.c(x), %y.d(y)) =


317 
when(q, %x.e(x), %y.f(y)) : C(p)


318 


319 
\idx{PlusC_inl} [ a: A;


320 
!!x. x:A ==> c(x): C(inl(x));


321 
!!y. y:B ==> d(y): C(inr(y))


322 
] ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))


323 


324 
\idx{PlusC_inr} [ b: B;


325 
!!x. x:A ==> c(x): C(inl(x));


326 
!!y. y:B ==> d(y): C(inr(y))


327 
] ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))


328 
\end{ttbox}


329 
\caption{Rules for the binary sum type $A+B$} \label{cttplus}


330 
\end{figure}


331 


332 


333 
\begin{figure}


334 
\begin{ttbox}


335 
\idx{EqF} [ A type; a : A; b : A ] ==> Eq(A,a,b) type


336 
\idx{EqFL} [ A=B; a=c: A; b=d : A ] ==> Eq(A,a,b) = Eq(B,c,d)


337 
\idx{EqI} a = b : A ==> eq : Eq(A,a,b)


338 
\idx{EqE} p : Eq(A,a,b) ==> a = b : A


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


340 
\end{ttbox}


341 
\subcaption{The equality type $Eq(A,a,b)$}


342 


343 
\begin{ttbox}


344 
\idx{FF} F type


345 
\idx{FE} [ p: F; C type ] ==> contr(p) : C


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


347 
\end{ttbox}


348 
\subcaption{The empty type $F$}


349 


350 
\begin{ttbox}


351 
\idx{TF} T type


352 
\idx{TI} tt : T


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


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


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


356 
\end{ttbox}


357 
\subcaption{The unit type $T$}


358 


359 
\caption{Rules for other {\CTT} types} \label{cttothers}


360 
\end{figure}


361 


362 


363 


364 
\begin{figure}


365 
\begin{ttbox}


366 
\idx{replace_type} [ B = A; a : A ] ==> a : B


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


368 


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


370 
] ==> c(p`a): C(p`a)


371 


372 
\idx{SumIL2} [ c=a : A; d=b : B(a) ] ==> <c,d> = <a,b> : Sum(A,B)


373 


374 
\idx{SumE_fst} p : Sum(A,B) ==> fst(p) : A


375 


376 
\idx{SumE_snd} [ p: Sum(A,B); A type; !!x. x:A ==> B(x) type


377 
] ==> snd(p) : B(fst(p))


378 
\end{ttbox}


379 


380 
\caption{Derived rules for {\CTT}} \label{cttderived}


381 
\end{figure}


382 


383 


384 
\section{Rules of inference}


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


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


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


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


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


390 
called {\em long} rules; their names have the suffix~{\tt L}\@.


391 
Introduction and computation rules often are further suffixed with


392 
constructor names.


393 


394 
Figures~\ref{cttequality}\ref{cttothers} shows the rules. Those


395 
for~$N$ include \ttindex{zero_ne_succ}, $0\not=n+1$: the fourth Peano axiom


396 
cannot be derived without universes \cite[page 91]{martinlof84}.


397 
Figure~\ref{cttsum} shows the rules for general sums, which include binary


398 
products as a special case, with the projections \ttindex{fst}


399 
and~\ttindex{snd}.


400 


401 
The extra judgement \ttindex{Reduce} is used to implement rewriting. The


402 
judgement ${\tt Reduce}(a,b)$ holds when $a=b:A$ holds. It also holds


403 
when $a$ and $b$ are syntactically identical, even if they are illtyped,


404 
because rule \ttindex{refl_red} does not verify that $a$ belongs to $A$. These


405 
rules do not give rise to new theorems about the standard judgements 


406 
note that the only rule that makes use of {\tt Reduce} is \ttindex{trans_red},


407 
whose first premise ensures that $a$ and $b$ (and thus $c$) are welltyped.


408 


409 
Derived rules are shown in Figure~\ref{cttderived}. The rule


410 
\ttindex{subst_prodE} is derived from \ttindex{prodE}, and is easier to


411 
use in backwards proof. The rules \ttindex{SumE_fst} and


412 
\ttindex{SumE_snd} express the typing of~\ttindex{fst} and~\ttindex{snd};


413 
together, they are roughly equivalent to~\ttindex{SumE} with the advantage


414 
of creating no parameters. These rules are demonstrated in a proof of the


415 
Axiom of Choice~(\S\ref{cttchoice}).


416 


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


418 
occurrence of $\lambda u\,v.b(u,v)$ could be abbreviated to~$b$ in the


419 
rules for~$N$. This permits Isabelle to preserve bound variable names


420 
during backward proof. Names of bound variables in the conclusion (here,


421 
$u$ and~$v$) are matched with corresponding bound variables in the premises.


422 


423 


424 
\section{Rule lists}


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


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


427 
Theory rules against a proof state. {\CTT} defines lists  each with


428 
type


429 
\hbox{\tt thm list}  of related rules.


430 
\begin{description}


431 
\item[\ttindexbold{form_rls}]


432 
contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,


433 
$F$, and $T$.


434 


435 
\item[\ttindexbold{formL_rls}]


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


437 
other types use \ttindex{refl_type}.)


438 


439 
\item[\ttindexbold{intr_rls}]


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


441 
$T$.


442 


443 
\item[\ttindexbold{intrL_rls}]


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


445 
$T$ use \ttindex{refl_elem}.)


446 


447 
\item[\ttindexbold{elim_rls}]


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


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


450 
eliminator.


451 


452 
\item[\ttindexbold{elimL_rls}]


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


454 


455 
\item[\ttindexbold{comp_rls}]


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


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


458 


459 
\item[\ttindexbold{basic_defs}]


460 
contains the definitions of \ttindex{fst} and \ttindex{snd}.


461 
\end{description}


462 


463 


464 
\section{Tactics for subgoal reordering}


465 
\begin{ttbox}


466 
test_assume_tac : int > tactic


467 
typechk_tac : thm list > tactic


468 
equal_tac : thm list > tactic


469 
intr_tac : thm list > tactic


470 
\end{ttbox}


471 
Blind application of {\CTT} rules seldom leads to a proof. The elimination


472 
rules, especially, create subgoals containing new unknowns. These subgoals


473 
unify with anything, causing an undirectional search. The standard tactic


474 
\ttindex{filt_resolve_tac} (see the {\em Reference Manual}) can reject


475 
overly flexible goals; so does the {\CTT} tactic {\tt test_assume_tac}.


476 
Used with the tactical \ttindex{REPEAT_FIRST} they achieve a simple kind of


477 
subgoal reordering: the less flexible subgoals are attempted first. Do


478 
some single step proofs, or study the examples below, to see why this is


479 
necessary.


480 
\begin{description}


481 
\item[\ttindexbold{test_assume_tac} $i$]


482 
uses \ttindex{assume_tac} to solve the subgoal by assumption, but only if


483 
subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.


484 
Otherwise, it fails.


485 


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


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


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


489 
$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible. Thus it


490 
performs HindleyMilner type inference. The tactic can also solve goals of


491 
the form $A\;\rm type$.


492 


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


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


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


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


497 
tactic can also perform type checking.


498 


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


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


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


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


503 
expressed as a type.


504 
\end{description}


505 


506 


507 


508 
\section{Rewriting tactics}


509 
\begin{ttbox}


510 
rew_tac : thm list > tactic


511 
hyp_rew_tac : thm list > tactic


512 
\end{ttbox}


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


514 
CTT} equality rules and the builtin rewriting functor


515 
\ttindex{TSimpFun}.\footnote{This should not be confused with {\tt


516 
SimpFun}, which is the main rewriting functor; {\tt TSimpFun} is only


517 
useful for {\CTT} and similar logics with type inference rules.}


518 
The rewrites include the computation rules and other equations. The


519 
long versions of the other rules permit rewriting of subterms and subtypes.


520 
Also used are transitivity and the extra judgement form \ttindex{Reduce}.


521 
Metalevel simplification handles only definitional equality.


522 
\begin{description}


523 
\item[\ttindexbold{rew_tac} $thms$]


524 
applies $thms$ and the computation rules as lefttoright rewrites. It


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


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


527 


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


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


530 
the assumptions.


531 
\end{description}


532 


533 


534 
\section{Tactics for logical reasoning}


535 
Interpreting propositions as types lets {\CTT} express statements of


536 
intuitionistic logic. However, Constructive Type Theory is not just


537 
another syntax for firstorder logic. A key question: can assumptions be


538 
deleted after use? Not every occurrence of a type represents a


539 
proposition, and Type Theory assumptions declare variables.


540 


541 
In firstorder logic, $\disj$elimination with the assumption $P\disj Q$


542 
creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$


543 
can be deleted. In Type Theory, $+$elimination with the assumption $z\in


544 
A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in B$


545 
(for arbitrary $x$ and $y$). Deleting $z\in A+B$ may render the subgoals


546 
unprovable if other assumptions refer to $z$. Some people might argue that


547 
such subgoals are not even meaningful.


548 
\begin{ttbox}


549 
mp_tac : int > tactic


550 
add_mp_tac : int > tactic


551 
safestep_tac : thm list > int > tactic


552 
safe_tac : thm list > int > tactic


553 
step_tac : thm list > int > tactic


554 
pc_tac : thm list > int > tactic


555 
\end{ttbox}


556 
These are loosely based on the intuitionistic proof procedures


557 
of~\ttindex{FOL}. For the reasons discussed above, a rule that is safe for


558 
propositional reasoning may be unsafe for type checking; thus, some of the


559 
``safe'' tactics are misnamed.


560 
\begin{description}


561 
\item[\ttindexbold{mp_tac} $i$]


562 
searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and


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


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


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


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


567 


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


569 
is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$.


570 


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


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


573 
(\ttindex{FE}, \ttindex{ProdI}, \ttindex{SumE}, \ttindex{PlusE}), calling


574 
{\tt mp_tac} when appropriate. It also uses~$thms$,


575 
which are typically premises of the rule being derived.


576 


577 
\item[\ttindexbold{safe_tac} $thms$ $i$]


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


579 


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


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


582 
rules. It may produce multiple outcomes.


583 


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


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


586 
\end{description}


587 


588 


589 


590 
\begin{figure}


591 
\begin{ttbox}


592 
\idx{add_def} a#+b == rec(a, b, %u v.succ(v))


593 
\idx{diff_def} ab == rec(b, a, %u v.rec(v, 0, %x y.x))


594 
\idx{absdiff_def} ab == (ab) #+ (ba)


595 
\idx{mult_def} a#*b == rec(a, 0, %u v. b #+ v)


596 

111

597 
\idx{mod_def} a mod b == rec(a, 0,

104

598 
%u v. rec(succ(v)  b, 0, %x y.succ(v)))


599 

111

600 
\idx{div_def} a div b == rec(a, 0,


601 
%u v. rec(succ(u) mod b, succ(v), %x y.v))

104

602 
\end{ttbox}


603 
\subcaption{Definitions of the operators}


604 


605 
\begin{ttbox}


606 
\idx{add_typing} [ a:N; b:N ] ==> a #+ b : N


607 
\idx{addC0} b:N ==> 0 #+ b = b : N


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


609 


610 
\idx{add_assoc} [ a:N; b:N; c:N ] ==>


611 
(a #+ b) #+ c = a #+ (b #+ c) : N


612 


613 
\idx{add_commute} [ a:N; b:N ] ==> a #+ b = b #+ a : N


614 


615 
\idx{mult_typing} [ a:N; b:N ] ==> a #* b : N


616 
\idx{multC0} b:N ==> 0 #* b = 0 : N


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


618 
\idx{mult_commute} [ a:N; b:N ] ==> a #* b = b #* a : N


619 


620 
\idx{add_mult_dist} [ a:N; b:N; c:N ] ==>


621 
(a #+ b) #* c = (a #* c) #+ (b #* c) : N


622 


623 
\idx{mult_assoc} [ a:N; b:N; c:N ] ==>


624 
(a #* b) #* c = a #* (b #* c) : N


625 


626 
\idx{diff_typing} [ a:N; b:N ] ==> a  b : N


627 
\idx{diffC0} a:N ==> a  0 = a : N


628 
\idx{diff_0_eq_0} b:N ==> 0  b = 0 : N


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


630 
\idx{diff_self_eq_0} a:N ==> a  a = 0 : N


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


632 
\end{ttbox}


633 
\subcaption{Some theorems of arithmetic}


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


635 
\end{figure}


636 


637 


638 
\section{A theory of arithmetic}


639 
{\CTT} contains a theory of elementary arithmetic. It proves the


640 
properties of addition, multiplication, subtraction, division, and


641 
remainder, culminating in the theorem


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


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


644 
theorems, including commutative, distributive, and associative laws. The


645 
theory has the {\ML} identifier \ttindexbold{arith.thy}. All proofs are on


646 
the file \ttindexbold{CTT/arith.ML}.


647 

111

648 
The operators~\verb'#+', \verb'', \verb'', \verb'#*', \verb'mod'


649 
and~\verb'div' stand for sum, difference, absolute difference, product,

104

650 
remainder and quotient, respectively. Since Type Theory has only primitive


651 
recursion, some of their definitions may be obscure.


652 


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


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


655 

111

656 
The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0


657 
as the successor of~$b1$. Absolute difference is used to test the


658 
equality $succ(v)=b$.

104

659 

111

660 
The quotient $a/b$ is computed by adding one for every number $x$


661 
such that $0\leq x \leq a$ and $x\bmod b = 0$.

104

662 


663 


664 


665 
\section{The examples directory}


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


667 
\begin{description}


668 
\item[\ttindexbold{CTT/ex/typechk.ML}]


669 
contains simple examples of type checking and type deduction.


670 


671 
\item[\ttindexbold{CTT/ex/elim.ML}]


672 
contains some examples from MartinL\"of~\cite{martinlof84}, proved using


673 
{\tt pc_tac}.


674 


675 
\item[\ttindexbold{CTT/ex/equal.ML}]


676 
contains simple examples of rewriting.


677 


678 
\item[\ttindexbold{CTT/ex/synth.ML}]


679 
demonstrates the use of unknowns with some trivial examples of program


680 
synthesis.


681 
\end{description}


682 


683 


684 
\section{Example: type inference}


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


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


687 
initially


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


689 
predecessor function on the natural numbers.


690 
\begin{ttbox}


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


692 
{\out Level 0}


693 
{\out lam n. rec(n,0,%x y. x) : ?A}


694 
{\out 1. lam n. rec(n,0,%x y. x) : ?A}


695 
\end{ttbox}


696 
Since the term is a Constructive Type Theory $\lambda$abstraction (not to


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


698 
\ttindex{ProdI}, for $\Pi$introduction. This instantiates~$\Var{A}$ to a


699 
product type of unknown domain and range.


700 
\begin{ttbox}


701 
by (resolve_tac [ProdI] 1);


702 
{\out Level 1}


703 
{\out lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)}


704 
{\out 1. ?A1 type}


705 
{\out 2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)}


706 
\end{ttbox}


707 
Subgoal~1 can be solved by instantiating~$\Var{A@1}$ to any type, but this


708 
could invalidate subgoal~2. We therefore tackle the latter subgoal. It


709 
asks the type of a term beginning with {\tt rec}, which can be found by


710 
$N$elimination.\index{*NE}


711 
\begin{ttbox}


712 
by (eresolve_tac [NE] 2);


713 
{\out Level 2}


714 
{\out lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)}


715 
{\out 1. N type}


716 
{\out 2. !!n. 0 : ?C2(n,0)}


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


718 
\end{ttbox}


719 
We now know~$\Var{A@1}$ is the type of natural numbers. However, let us


720 
continue with subgoal~2. What is the type of~0?\index{*NIO}


721 
\begin{ttbox}


722 
by (resolve_tac [NI0] 2);


723 
{\out Level 3}


724 
{\out lam n. rec(n,0,%x y. x) : N > N}


725 
{\out 1. N type}


726 
{\out 2. !!n x y. [ x : N; y : N ] ==> x : N}


727 
\end{ttbox}


728 
The type~$\Var{A}$ is now determined. It is $\prod@{n\in N}N$, which is


729 
equivalent to $N\to N$. But we must prove all the subgoals to show that


730 
the original term is validly typed. Subgoal~2 is provable by assumption


731 
and the remaining subgoal falls by $N$formation.\index{*NF}


732 
\begin{ttbox}


733 
by (assume_tac 2);


734 
{\out Level 4}


735 
{\out lam n. rec(n,0,%x y. x) : N > N}


736 
{\out 1. N type}


737 
by (resolve_tac [NF] 1);


738 
{\out Level 5}


739 
{\out lam n. rec(n,0,%x y. x) : N > N}


740 
{\out No subgoals!}


741 
\end{ttbox}


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


743 


744 


745 
\section{An example of logical reasoning}


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


747 
$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ is an


748 
unknown standing


749 
for its proof term: a value of type $A$. This term is initially unknown, as


750 
with type inference, and takes shape during the proof. Our example


751 
expresses, by propositionsastypes, a theorem about quantifiers in a


752 
sorted logic:


753 
\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}


754 
{\ex{x\in A}P(x)\disj Q(x)}


755 
\]


756 
It it related to a distributive law of Type Theory:


757 
\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]


758 
Generalizing this from $\times$ to $\Sigma$, and making the typing


759 
conditions explicit, yields


760 
\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}


761 
{\hbox{$A$ type} &


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


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


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


765 
\]


766 
To derive this rule, we bind its premises  returned by~\ttindex{goal}


767 
 to the {\ML} variable~{\tt prems}.


768 
\begin{ttbox}


769 
val prems = goal CTT.thy


770 
"[ A type; \ttback


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


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


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


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


775 
{\out Level 0}


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


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

114

778 
\ttbreak

111

779 
{\out val prems = ["A type [A type]",}


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


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


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


783 
{\out : thm list}

104

784 
\end{ttbox}


785 
One of the premises involves summation ($\Sigma$). Since it is a premise


786 
rather than the assumption of a goal, it cannot be found by


787 
\ttindex{eresolve_tac}. We could insert it by calling


788 
\hbox{\tt \ttindex{cut_facts_tac} prems 1}. Instead, let us resolve the


789 
$\Sigma$elimination rule with the premises; this yields one result, which


790 
we supply to \ttindex{resolve_tac}.\index{*SumE}\index{*RL}


791 
\begin{ttbox}


792 
by (resolve_tac (prems RL [SumE]) 1);


793 
{\out Level 1}


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


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


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


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


798 
\end{ttbox}


799 
The subgoal has two new parameters. In the main goal, $\Var{a}$ has been


800 
instantiated with a \ttindex{split} term. The assumption $y\in B(x) + C(x)$ is


801 
eliminated next, causing a case split and a new parameter. The main goal


802 
now contains~\ttindex{when}.


803 
\index{*PlusE}


804 
\begin{ttbox}


805 
by (eresolve_tac [PlusE] 1);


806 
{\out Level 2}


807 
{\out split(p,%x y. when(y,?c2(x,y),?d2(x,y)))}


808 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}


809 
{\out 1. !!x y xa.}


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


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

114

812 
\ttbreak

104

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


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


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


816 
\end{ttbox}


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


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


819 
introduction of~$+$; since it assumes $xa\in B(x)$, we take the left


820 
injection~(\ttindex{inl}).


821 
\index{*PlusI_inl}


822 
\begin{ttbox}


823 
by (resolve_tac [PlusI_inl] 1);


824 
{\out Level 3}


825 
{\out split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y)))}


826 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}


827 
{\out 1. !!x y xa. [ x : A; xa : B(x) ] ==> ?a3(x,y,xa) : SUM x:A. B(x)}


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

114

829 
\ttbreak

104

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


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


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


833 
\end{ttbox}


834 
A new subgoal has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.


835 
Continuing with subgoal~1, we apply $\Sigma$introduction. The main goal


836 
now contains an ordered pair.


837 
\index{*SumI}


838 
\begin{ttbox}


839 
by (resolve_tac [SumI] 1);


840 
{\out Level 4}


841 
{\out split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}


842 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}


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


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


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


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


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


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


849 
\end{ttbox}


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


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


852 
\begin{ttbox}


853 
by (assume_tac 1);


854 
{\out Level 5}


855 
{\out split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}


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


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


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


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


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


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


862 
by (assume_tac 1);


863 
{\out Level 6}


864 
{\out split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))}


865 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}


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


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


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


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


870 
\end{ttbox}


871 
Subgoal~1 is just type checking. It yields to \ttindex{typechk_tac},


872 
supplied with the current list of premises.


873 
\begin{ttbox}


874 
by (typechk_tac prems);


875 
{\out Level 7}


876 
{\out split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))}


877 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}


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


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


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


881 
\end{ttbox}


882 
The other case is similar. Let us prove it by \ttindex{pc_tac}, and note


883 
the final proof object.


884 
\begin{ttbox}


885 
by (pc_tac prems 1);


886 
{\out Level 8}


887 
{\out split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))}


888 
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}


889 
{\out No subgoals!}


890 
\end{ttbox}


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


892 
proves this theorem.


893 


894 


895 
\section{Example: deriving a currying functional}


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


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


898 
Let us generalize this to~$\Sigma$ and~$\Pi$. The argument of the


899 
functional is a function that maps $z:\Sigma(A,B)$ to~$C(z)$; the resulting


900 
function maps $x\in A$ and $y\in B(x)$ to $C(\langle x,y\rangle)$. Here


901 
$B$ is a family over~$A$, while $C$ is a family over $\Sigma(A,B)$.


902 
\begin{ttbox}


903 
val prems = goal CTT.thy


904 
"[ A type; !!x. x:A ==> B(x) type; \ttback


905 
\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type ] \ttback


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


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


908 
{\out Level 0}


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


910 
{\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) >}


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

114

912 
\ttbreak

111

913 
{\out val prems = ["A type [A type]",}


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


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


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

104

917 
\end{ttbox}


918 
This is an opportunity to demonstrate \ttindex{intr_tac}. Here, the tactic


919 
repeatedly applies $\Pi$introduction, automatically proving the rather


920 
tiresome typing conditions. Note that $\Var{a}$ becomes instantiated to


921 
three nested $\lambda$abstractions.


922 
\begin{ttbox}


923 
by (intr_tac prems);


924 
{\out Level 1}


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


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


927 
{\out 1. !!uu x y.}


928 
{\out [ uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) ] ==>}


929 
{\out ?b7(uu,x,y) : C(<x,y>)}


930 
\end{ttbox}


931 
Using $\Pi$elimination, we solve subgoal~1 by applying the function~$uu$.


932 
\index{*ProdE}


933 
\begin{ttbox}


934 
by (eresolve_tac [ProdE] 1);


935 
{\out Level 2}


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


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


938 
{\out 1. !!uu x y. [ x : A; y : B(x) ] ==> <x,y> : SUM x:A. B(x)}


939 
\end{ttbox}


940 
Finally, we exhibit a suitable argument for the function application. This


941 
is straightforward using introduction rules.


942 
\index{*intr_tac}


943 
\begin{ttbox}


944 
by (intr_tac prems);


945 
{\out Level 3}


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


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


948 
{\out No subgoals!}


949 
\end{ttbox}


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


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


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


953 


954 


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


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


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


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


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


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


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


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


963 


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


965 
Theory \cite[page~50]{martinlof84}. The following definitions work:


966 
\begin{eqnarray*}


967 
f & \equiv & {\tt fst} \circ h \\


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


969 
\end{eqnarray*}


970 
But a completely formal proof is hard to find. Many of the rules can be


971 
applied in a multiplicity of ways, yielding a large number of higherorder


972 
unifiers. The proof can get bogged down in the details. But with a


973 
careful selection of derived rules (recall Figure~\ref{cttderived}) and


974 
the type checking tactics, we can prove the theorem in nine steps.


975 
\begin{ttbox}


976 
val prems = goal CTT.thy


977 
"[ A type; !!x. x:A ==> B(x) type; \ttback


978 
\ttback !!x y.[ x:A; y:B(x) ] ==> C(x,y) type \ttback


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


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


981 
{\out Level 0}


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


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


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


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

111

986 
\ttbreak


987 
{\out val prems = ["A type [A type]",}


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


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


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


991 
{\out : thm list}

104

992 
\end{ttbox}


993 
First, \ttindex{intr_tac} applies introduction rules and performs routine


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


995 
three $\lambda$abstractions and an ordered pair.


996 
\begin{ttbox}


997 
by (intr_tac prems);


998 
{\out Level 1}


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


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


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

114

1002 
\ttbreak

104

1003 
{\out 1. !!uu x.}


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


1005 
{\out ?b7(uu,x) : B(x)}

114

1006 
\ttbreak

104

1007 
{\out 2. !!uu x.}


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


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


1010 
\end{ttbox}


1011 
Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some


1012 
$\Var{b@7}(uu,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof


1013 
object $\Var{b@8}(uu,x)$ to witness that the choice function's argument


1014 
and result lie in the relation~$C$.


1015 
\index{*ProdE}\index{*SumE_fst}\index{*RS}


1016 
\begin{ttbox}


1017 
by (eresolve_tac [ProdE RS SumE_fst] 1);


1018 
{\out Level 2}


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


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


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

114

1022 
\ttbreak

104

1023 
{\out 1. !!uu x. x : A ==> x : A}


1024 
{\out 2. !!uu x.}


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


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


1027 
\end{ttbox}


1028 
Above, we have composed \ttindex{fst} with the function~$h$ (named~$uu$ in


1029 
the assumptions). Unification has deduced that the function must be


1030 
applied to $x\in A$.


1031 
\begin{ttbox}


1032 
by (assume_tac 1);


1033 
{\out Level 3}


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


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


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


1037 
{\out 1. !!uu x.}


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


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


1040 
\end{ttbox}


1041 
Before we can compose \ttindex{snd} with~$h$, the arguments of $C$ must be


1042 
simplified. The derived rule \ttindex{replace_type} lets us replace a type


1043 
by any equivalent type:


1044 
\begin{ttbox}


1045 
by (resolve_tac [replace_type] 1);


1046 
{\out Level 4}


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


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


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

114

1050 
\ttbreak

104

1051 
{\out 1. !!uu x.}


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


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

114

1054 
\ttbreak

104

1055 
{\out 2. !!uu x.}


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


1057 
{\out ?b8(uu,x) : ?A13(uu,x)}


1058 
\end{ttbox}


1059 
The derived rule \ttindex{subst_eqtyparg} lets us simplify a type's


1060 
argument (by currying, $C(x)$ is a unary type operator):


1061 
\begin{ttbox}


1062 
by (resolve_tac [subst_eqtyparg] 1);


1063 
{\out Level 5}


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


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


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

114

1067 
\ttbreak

104

1068 
{\out 1. !!uu x.}


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


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

114

1071 
\ttbreak

104

1072 
{\out 2. !!uu x z.}


1073 
{\out [ uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}


1074 
{\out z : ?A14(uu,x) ] ==>}


1075 
{\out C(x,z) type}

114

1076 
\ttbreak

104

1077 
{\out 3. !!uu x.}


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


1079 
{\out ?b8(uu,x) : C(x,?c14(uu,x))}


1080 
\end{ttbox}


1081 
The rule \ttindex{ProdC} is simply $\beta$reduction. The term


1082 
$\Var{c@{14}}(uu,x)$ receives the simplified form, $f{\tt`}x$.


1083 
\begin{ttbox}


1084 
by (resolve_tac [ProdC] 1);


1085 
{\out Level 6}


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


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


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

114

1089 
\ttbreak

104

1090 
{\out 1. !!uu x.}


1091 
{\out [ uu : PROD x:A. SUM y:B(x). C(x,y); x : A ] ==> x : ?A15(uu,x)}

114

1092 
\ttbreak

104

1093 
{\out 2. !!uu x xa.}


1094 
{\out [ uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}


1095 
{\out xa : ?A15(uu,x) ] ==>}


1096 
{\out fst(uu ` xa) : ?B15(uu,x,xa)}

114

1097 
\ttbreak

104

1098 
{\out 3. !!uu x z.}


1099 
{\out [ uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}


1100 
{\out z : ?B15(uu,x,x) ] ==>}


1101 
{\out C(x,z) type}

114

1102 
\ttbreak

104

1103 
{\out 4. !!uu x.}


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


1105 
{\out ?b8(uu,x) : C(x,fst(uu ` x))}


1106 
\end{ttbox}


1107 
Routine type checking goals proliferate in Constructive Type Theory, but


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


1109 
\ttindex{SumE_fst}.


1110 
\begin{ttbox}


1111 
by (typechk_tac (SumE_fst::prems));


1112 
{\out Level 7}


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


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


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


1116 
{\out 1. !!uu x.}


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


1118 
{\out ?b8(uu,x) : C(x,fst(uu ` x))}


1119 
\end{ttbox}


1120 
We are finally ready to compose \ttindex{snd} with~$h$.


1121 
\index{*ProdE}\index{*SumE_snd}\index{*RS}


1122 
\begin{ttbox}


1123 
by (eresolve_tac [ProdE RS SumE_snd] 1);


1124 
{\out Level 8}


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


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


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


1128 
{\out 1. !!uu x. x : A ==> x : A}


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


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


1131 
\end{ttbox}


1132 
The proof object has reached its final form. We call \ttindex{typechk_tac}


1133 
to finish the type checking.


1134 
\begin{ttbox}


1135 
by (typechk_tac prems);


1136 
{\out Level 9}


1137 
{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(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))}


1140 
{\out No subgoals!}


1141 
\end{ttbox}
