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