doc-src/Logics/CTT.tex
 author haftmann Wed Dec 27 19:10:06 2006 +0100 (2006-12-27) changeset 21915 4e63c55f4cb4 parent 12679 8ed660138f83 child 42637 381fdcab0f36 permissions -rw-r--r--
different handling of type variable names
     1 %% $Id$

     2 \chapter{Constructive Type Theory}

     3 \index{Constructive Type Theory|(}

     4

     5 \underscoreoff %this file contains _ in rule names

     6

     7 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can

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

     9 the principles of intuitionistic mathematics; it embodies the

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

    11 programs from proofs.

    12

    13 Thompson's book~\cite{thompson91} gives a readable and thorough account of

    14 Type Theory.  Nuprl is an elaborate implementation~\cite{constable86}.

    15 {\sc alf} is a more recent tool that allows proof terms to be edited

    16 directly~\cite{alf}.

    17

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

    19 calculus, following Martin-L\"of~\cite{martinlof84}.  It included rules for

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

    21 judgement was

    22 $a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \;   23 [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]   24$

    25 This sequent calculus was not satisfactory because assumptions like

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

    27 could not be formalized.

    28

    29 The theory~\thydx{CTT} implements Constructive Type Theory, using

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

    31 $\Imp$:

    32 $\begin{array}{r@{}l}   33 \Forall x@1\ldots x@n. &   34 \List{x@1\in A@1;   35 x@2\in A@2(x@1); \cdots \;   36 x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\   37 & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n)   38 \end{array}   39$

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

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

    42 $\Forall x . x\in A \Imp B(x)\;{\rm type}$

    43 To justify the CTT formulation it is probably best to appeal directly to the

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

    45 rules themselves.  The order of assumptions no longer matters, unlike in

    46 standard Type Theory.  Contexts, which are typical of many modern type

    47 theories, are difficult to represent in Isabelle.  In particular, it is

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

    49 \index{assumptions!in CTT}

    50

    51 The theory does not use polymorphism.  Terms in CTT have type~\tydx{i}, the

    52 type of individuals.  Types in CTT have type~\tydx{t}.

    53

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

    55 \begin{center}

    56 \begin{tabular}{rrr}

    57   \it name      & \it meta-type         & \it description \\

    58   \cdx{Type}    & $t \to prop$          & judgement form \\

    59   \cdx{Eqtype}  & $[t,t]\to prop$       & judgement form\\

    60   \cdx{Elem}    & $[i, t]\to prop$      & judgement form\\

    61   \cdx{Eqelem}  & $[i, i, t]\to prop$   & judgement form\\

    62   \cdx{Reduce}  & $[i, i]\to prop$      & extra judgement form\$2ex]   63   64 \cdx{N} & t & natural numbers type\\   65 \cdx{0} & i & constructor\\   66 \cdx{succ} & i\to i & constructor\\   67 \cdx{rec} & [i,i,[i,i]\to i]\to i & eliminator\\[2ex]   68 \cdx{Prod} & [t,i\to t]\to t & general product type\\   69 \cdx{lambda} & (i\to i)\to i & constructor\\[2ex]   70 \cdx{Sum} & [t, i\to t]\to t & general sum type\\   71 \cdx{pair} & [i,i]\to i & constructor\\   72 \cdx{split} & [i,[i,i]\to i]\to i & eliminator\\   73 \cdx{fst} \cdx{snd} & i\to i & projections\\[2ex]   74 \cdx{inl} \cdx{inr} & i\to i & constructors for +\\   75 \cdx{when} & [i,i\to i, i\to i]\to i & eliminator for +\\[2ex]   76 \cdx{Eq} & [t,i,i]\to t & equality type\\   77 \cdx{eq} & i & constructor\\[2ex]   78 \cdx{F} & t & empty type\\   79 \cdx{contr} & i\to i & eliminator\\[2ex]   80 \cdx{T} & t & singleton type\\   81 \cdx{tt} & i & constructor   82 \end{tabular}   83 \end{center}   84 \caption{The constants of CTT} \label{ctt-constants}   85 \end{figure}   86   87   88 CTT supports all of Type Theory apart from list types, well-ordering types,   89 and universes. Universes could be introduced {\em\a la Tarski}, adding new   90 constants as names for types. The formulation {\em\a la Russell}, where   91 types denote themselves, is only possible if we identify the meta-types~{\tt   92 i} and~{\tt t}. Most published formulations of well-ordering types have   93 difficulties involving extensionality of functions; I suggest that you use   94 some other method for defining recursive types. List types are easy to   95 introduce by declaring new rules.   96   97 CTT uses the 1982 version of Type Theory, with extensional equality. The   98 computation a=b\in A and the equality c\in Eq(A,a,b) are interchangeable.   99 Its rewriting tactics prove theorems of the form a=b\in A. It could be   100 modified to have intensional equality, but rewriting tactics would have to   101 prove theorems of the form c\in Eq(A,a,b) and the computation rules might   102 require a separate simplifier.   103   104   105 \begin{figure} \tabcolsep=1em %wider spacing in tables   106 \index{lambda abs@\lambda-abstractions!in CTT}   107 \begin{center}   108 \begin{tabular}{llrrr}   109 \it symbol &\it name &\it meta-type & \it priority & \it description \\   110 \sdx{lam} & \cdx{lambda} & (i\To o)\To i & 10 & \lambda-abstraction   111 \end{tabular}   112 \end{center}   113 \subcaption{Binders}   114   115 \begin{center}   116 \index{*" symbol}\index{function applications!in CTT}   117 \index{*"+ symbol}   118 \begin{tabular}{rrrr}   119 \it symbol & \it meta-type & \it priority & \it description \\   120 \tt  & [i,i]\to i & Left 55 & function application\\   121 \tt + & [t,t]\to t & Right 30 & sum of two types   122 \end{tabular}   123 \end{center}   124 \subcaption{Infixes}   125   126 \index{*"* symbol}   127 \index{*"-"-"> symbol}   128 \begin{center} \tt\frenchspacing   129 \begin{tabular}{rrr}   130 \it external & \it internal & \it standard notation \\   131 \sdx{PROD} x:A . B[x] & Prod(A, \lambda x. B[x]) &   132 \rm product \prod@{x\in A}B[x] \\   133 \sdx{SUM} x:A . B[x] & Sum(A, \lambda x. B[x]) &   134 \rm sum \sum@{x\in A}B[x] \\   135 A --> B & Prod(A, \lambda x. B) &   136 \rm function space A\to B \\   137 A * B & Sum(A, \lambda x. B) &   138 \rm binary product A\times B   139 \end{tabular}   140 \end{center}   141 \subcaption{Translations}   142   143 \index{*"= symbol}   144 \begin{center}   145 \dquotes   146 \[ \begin{array}{rcl}   147 prop & = & type " type" \\   148 & | & type " = " type \\   149 & | & term " : " type \\   150 & | & term " = " term " : " type   151 \\[2ex]   152 type & = & \hbox{expression of type~t} \\   153 & | & "PROD~" id " : " type " . " type \\   154 & | & "SUM~~" id " : " type " . " type   155 \\[2ex]   156 term & = & \hbox{expression of type~i} \\   157 & | & "lam " id~id^* " . " term \\   158 & | & "< " term " , " term " >"   159 \end{array}   160$

   161 \end{center}

   162 \subcaption{Grammar}

   163 \caption{Syntax of CTT} \label{ctt-syntax}

   164 \end{figure}

   165

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

   167

   168

   169 \section{Syntax}

   170 The constants are shown in Fig.\ts\ref{ctt-constants}.  The infixes include

   171 the function application operator (sometimes called apply'), and the 2-place

   172 type operators.  Note that meta-level abstraction and application, $\lambda   173 x.b$ and $f(a)$, differ from object-level abstraction and application,

   174 \hbox{\tt lam $x$. $b$} and $b{\tt}a$.  A CTT function~$f$ is simply an

   175 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say

   176 $i\To i$.

   177

   178 The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om

   179 et al.~\cite{nordstrom90}.  The empty type is called $F$ and the one-element

   180 type is $T$; other finite types are built as $T+T+T$, etc.

   181

   182 \index{*SUM symbol}\index{*PROD symbol}

   183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and

   184 products $\prod@{x\in A}B[x]$.  Instead of {\tt Sum($A$,$B$)} and {\tt

   185   Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt

   186   PROD $x$:$A$.\ $B[x]$}.  For example, we may write

   187 \begin{ttbox}

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

   189 \end{ttbox}

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

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

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

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

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

   195

   196

   197 \begin{figure}

   198 \begin{ttbox}

   199 \tdx{refl_type}         A type ==> A = A

   200 \tdx{refl_elem}         a : A ==> a = a : A

   201

   202 \tdx{sym_type}          A = B ==> B = A

   203 \tdx{sym_elem}          a = b : A ==> b = a : A

   204

   205 \tdx{trans_type}        [| A = B;  B = C |] ==> A = C

   206 \tdx{trans_elem}        [| a = b : A;  b = c : A |] ==> a = c : A

   207

   208 \tdx{equal_types}       [| a : A;  A = B |] ==> a : B

   209 \tdx{equal_typesL}      [| a = b : A;  A = B |] ==> a = b : B

   210

   211 \tdx{subst_type}        [| a : A;  !!z. z:A ==> B(z) type |] ==> B(a) type

   212 \tdx{subst_typeL}       [| a = c : A;  !!z. z:A ==> B(z) = D(z)

   213                   |] ==> B(a) = D(c)

   214

   215 \tdx{subst_elem}        [| a : A;  !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)

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

   217                   |] ==> b(a) = d(c) : B(a)

   218

   219 \tdx{refl_red}          Reduce(a,a)

   220 \tdx{red_if_equal}      a = b : A ==> Reduce(a,b)

   221 \tdx{trans_red}         [| a = b : A;  Reduce(b,c) |] ==> a = c : A

   222 \end{ttbox}

   223 \caption{General equality rules} \label{ctt-equality}

   224 \end{figure}

   225

   226

   227 \begin{figure}

   228 \begin{ttbox}

   229 \tdx{NF}        N type

   230

   231 \tdx{NI0}       0 : N

   232 \tdx{NI_succ}   a : N ==> succ(a) : N

   233 \tdx{NI_succL}  a = b : N ==> succ(a) = succ(b) : N

   234

   235 \tdx{NE}        [| p: N;  a: C(0);

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

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

   238

   239 \tdx{NEL}       [| p = q : N;  a = c : C(0);

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

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

   242

   243 \tdx{NC0}       [| a: C(0);

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

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

   246

   247 \tdx{NC_succ}   [| p: N;  a: C(0);

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

   249           |] ==> rec(succ(p), a, \%u v. b(u,v)) =

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

   251

   252 \tdx{zero_ne_succ}      [| a: N;  0 = succ(a) : N |] ==> 0: F

   253 \end{ttbox}

   254 \caption{Rules for type~$N$} \label{ctt-N}

   255 \end{figure}

   256

   257

   258 \begin{figure}

   259 \begin{ttbox}

   260 \tdx{ProdF}     [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type

   261 \tdx{ProdFL}    [| A = C;  !!x. x:A ==> B(x) = D(x) |] ==>

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

   263

   264 \tdx{ProdI}     [| A type;  !!x. x:A ==> b(x):B(x)

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

   266 \tdx{ProdIL}    [| A type;  !!x. x:A ==> b(x) = c(x) : B(x)

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

   268

   269 \tdx{ProdE}     [| p : PROD x:A. B(x);  a : A |] ==> pa : B(a)

   270 \tdx{ProdEL}    [| p=q: PROD x:A. B(x);  a=b : A |] ==> pa = qb : B(a)

   271

   272 \tdx{ProdC}     [| a : A;  !!x. x:A ==> b(x) : B(x)

   273           |] ==> (lam x. b(x))  a = b(a) : B(a)

   274

   275 \tdx{ProdC2}    p : PROD x:A. B(x) ==> (lam x. px) = p : PROD x:A. B(x)

   276 \end{ttbox}

   277 \caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}

   278 \end{figure}

   279

   280

   281 \begin{figure}

   282 \begin{ttbox}

   283 \tdx{SumF}      [| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type

   284 \tdx{SumFL}     [| A = C;  !!x. x:A ==> B(x) = D(x)

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

   286

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

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

   289

   290 \tdx{SumE}      [| p: SUM x:A. B(x);

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

   292           |] ==> split(p, \%x y. c(x,y)) : C(p)

   293

   294 \tdx{SumEL}     [| p=q : SUM x:A. B(x);

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

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

   297

   298 \tdx{SumC}      [| a: A;  b: B(a);

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

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

   301

   302 \tdx{fst_def}   fst(a) == split(a, \%x y. x)

   303 \tdx{snd_def}   snd(a) == split(a, \%x y. y)

   304 \end{ttbox}

   305 \caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}

   306 \end{figure}

   307

   308

   309 \begin{figure}

   310 \begin{ttbox}

   311 \tdx{PlusF}       [| A type;  B type |] ==> A+B type

   312 \tdx{PlusFL}      [| A = C;  B = D |] ==> A+B = C+D

   313

   314 \tdx{PlusI_inl}   [| a : A;  B type |] ==> inl(a) : A+B

   315 \tdx{PlusI_inlL}  [| a = c : A;  B type |] ==> inl(a) = inl(c) : A+B

   316

   317 \tdx{PlusI_inr}   [| A type;  b : B |] ==> inr(b) : A+B

   318 \tdx{PlusI_inrL}  [| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B

   319

   320 \tdx{PlusE}     [| p: A+B;

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

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

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

   324

   325 \tdx{PlusEL}    [| p = q : A+B;

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

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

   328           |] ==> when(p, \%x. c(x), \%y. d(y)) =

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

   330

   331 \tdx{PlusC_inl} [| a: A;

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

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

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

   335

   336 \tdx{PlusC_inr} [| b: B;

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

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

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

   340 \end{ttbox}

   341 \caption{Rules for the binary sum type $A+B$} \label{ctt-plus}

   342 \end{figure}

   343

   344

   345 \begin{figure}

   346 \begin{ttbox}

   347 \tdx{FF}        F type

   348 \tdx{FE}        [| p: F;  C type |] ==> contr(p) : C

   349 \tdx{FEL}       [| p = q : F;  C type |] ==> contr(p) = contr(q) : C

   350

   351 \tdx{TF}        T type

   352 \tdx{TI}        tt : T

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

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

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

   356 \end{ttbox}

   357

   358 \caption{Rules for types $F$ and $T$} \label{ctt-ft}

   359 \end{figure}

   360

   361

   362 \begin{figure}

   363 \begin{ttbox}

   364 \tdx{EqF}       [| A type;  a : A;  b : A |] ==> Eq(A,a,b) type

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

   366 \tdx{EqI}       a = b : A ==> eq : Eq(A,a,b)

   367 \tdx{EqE}       p : Eq(A,a,b) ==> a = b : A

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

   369 \end{ttbox}

   370 \caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}

   371 \end{figure}

   372

   373

   374 \begin{figure}

   375 \begin{ttbox}

   376 \tdx{replace_type}    [| B = A;  a : A |] ==> a : B

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

   378

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

   380                 |] ==> c(pa): C(pa)

   381

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

   383

   384 \tdx{SumE_fst}  p : Sum(A,B) ==> fst(p) : A

   385

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

   387           |] ==> snd(p) : B(fst(p))

   388 \end{ttbox}

   389

   390 \caption{Derived rules for CTT} \label{ctt-derived}

   391 \end{figure}

   392

   393

   394 \section{Rules of inference}

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

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

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

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

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

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

   401 Introduction and computation rules are often further suffixed with

   402 constructor names.

   403

   404 Figure~\ref{ctt-equality} presents the equality rules.  Most of them are

   405 straightforward: reflexivity, symmetry, transitivity and substitution.  The

   406 judgement \cdx{Reduce} does not belong to Type Theory proper; it has

   407 been added to implement rewriting.  The judgement ${\tt Reduce}(a,b)$ holds

   408 when $a=b:A$ holds.  It also holds when $a$ and $b$ are syntactically

   409 identical, even if they are ill-typed, because rule {\tt refl_red} does

   410 not verify that $a$ belongs to $A$.

   411

   412 The {\tt Reduce} rules do not give rise to new theorems about the standard

   413 judgements.  The only rule with {\tt Reduce} in a premise is

   414 {\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus

   415 $c$) are well-typed.

   416

   417 Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.

   418 They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$.  This is

   419 the fourth Peano axiom and cannot be derived without universes \cite[page

   420 91]{martinlof84}.

   421

   422 The constant \cdx{rec} constructs proof terms when mathematical

   423 induction, rule~\tdx{NE}, is applied.  It can also express primitive

   424 recursion.  Since \cdx{rec} can be applied to higher-order functions,

   425 it can even express Ackermann's function, which is not primitive recursive

   426 \cite[page~104]{thompson91}.

   427

   428 Figure~\ref{ctt-prod} shows the rules for general product types, which

   429 include function types as a special case.  The rules correspond to the

   430 predicate calculus rules for universal quantifiers and implication.  They

   431 also permit reasoning about functions, with the rules of a typed

   432 $\lambda$-calculus.

   433

   434 Figure~\ref{ctt-sum} shows the rules for general sum types, which

   435 include binary product types as a special case.  The rules correspond to the

   436 predicate calculus rules for existential quantifiers and conjunction.  They

   437 also permit reasoning about ordered pairs, with the projections

   438 \cdx{fst} and~\cdx{snd}.

   439

   440 Figure~\ref{ctt-plus} shows the rules for binary sum types.  They

   441 correspond to the predicate calculus rules for disjunction.  They also

   442 permit reasoning about disjoint sums, with the injections \cdx{inl}

   443 and~\cdx{inr} and case analysis operator~\cdx{when}.

   444

   445 Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$

   446 and~$T$.  They correspond to the predicate calculus rules for absurdity and

   447 truth.

   448

   449 Figure~\ref{ctt-eq} shows the rules for equality types.  If $a=b\in A$ is

   450 provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,

   451 and vice versa.  These rules define extensional equality; the most recent

   452 versions of Type Theory use intensional equality~\cite{nordstrom90}.

   453

   454 Figure~\ref{ctt-derived} presents the derived rules.  The rule

   455 \tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use

   456 in backwards proof.  The rules \tdx{SumE_fst} and \tdx{SumE_snd}

   457 express the typing of~\cdx{fst} and~\cdx{snd}; together, they are

   458 roughly equivalent to~{\tt SumE} with the advantage of creating no

   459 parameters.  Section~\ref{ctt-choice} below demonstrates these rules in a

   460 proof of the Axiom of Choice.

   461

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

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

   464 rules for~$N$.  The expanded form permits Isabelle to preserve bound

   465 variable names during backward proof.  Names of bound variables in the

   466 conclusion (here, $u$ and~$v$) are matched with corresponding bound

   467 variables in the premises.

   468

   469

   470 \section{Rule lists}

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

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

   473 Theory rules against a proof state.  CTT defines lists --- each with

   474 type

   475 \hbox{\tt thm list} --- of related rules.

   476 \begin{ttdescription}

   477 \item[\ttindexbold{form_rls}]

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

   479 $F$, and $T$.

   480

   481 \item[\ttindexbold{formL_rls}]

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

   483 other types use \tdx{refl_type}.)

   484

   485 \item[\ttindexbold{intr_rls}]

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

   487 $T$.

   488

   489 \item[\ttindexbold{intrL_rls}]

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

   491 $T$ use \tdx{refl_elem}.)

   492

   493 \item[\ttindexbold{elim_rls}]

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

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

   496 eliminator.

   497

   498 \item[\ttindexbold{elimL_rls}]

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

   500

   501 \item[\ttindexbold{comp_rls}]

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

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

   504

   505 \item[\ttindexbold{basic_defs}]

   506 contains the definitions of {\tt fst} and {\tt snd}.

   507 \end{ttdescription}

   508

   509

   510 \section{Tactics for subgoal reordering}

   511 \begin{ttbox}

   512 test_assume_tac : int -> tactic

   513 typechk_tac     : thm list -> tactic

   514 equal_tac       : thm list -> tactic

   515 intr_tac        : thm list -> tactic

   516 \end{ttbox}

   517 Blind application of CTT rules seldom leads to a proof.  The elimination

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

   519 unify with anything, creating a huge search space.  The standard tactic

   520 \ttindex{filt_resolve_tac}

   521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%

   522         {\S\ref{filt_resolve_tac}})

   523 %

   524 fails for goals that are too flexible; so does the CTT tactic {\tt

   525   test_assume_tac}.  Used with the tactical \ttindex{REPEAT_FIRST} they

   526 achieve a simple kind of subgoal reordering: the less flexible subgoals are

   527 attempted first.  Do some single step proofs, or study the examples below,

   528 to see why this is necessary.

   529 \begin{ttdescription}

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

   531 uses {\tt assume_tac} to solve the subgoal by assumption, but only if

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

   533 Otherwise, it fails.

   534

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

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

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

   538 $a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it

   539 performs type inference.  The tactic can also solve goals of

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

   541

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

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

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

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

   546 tactic can also perform type-checking.

   547

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

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

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

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

   552 expressed as a type.

   553 \end{ttdescription}

   554

   555

   556

   557 \section{Rewriting tactics}

   558 \begin{ttbox}

   559 rew_tac     : thm list -> tactic

   560 hyp_rew_tac : thm list -> tactic

   561 \end{ttbox}

   562 Object-level simplification is accomplished through proof, using the {\tt

   563   CTT} equality rules and the built-in rewriting functor

   564 {\tt TSimpFun}.%

   565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt

   566     TSimpFun} is only useful for CTT and similar logics with type inference

   567   rules.  At present it is undocumented.}

   568 %

   569 The rewrites include the computation rules and other equations.  The long

   570 versions of the other rules permit rewriting of subterms and subtypes.

   571 Also used are transitivity and the extra judgement form \cdx{Reduce}.

   572 Meta-level simplification handles only definitional equality.

   573 \begin{ttdescription}

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

   575 applies $thms$ and the computation rules as left-to-right rewrites.  It

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

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

   578

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

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

   581 the assumptions.

   582 \end{ttdescription}

   583

   584

   585 \section{Tactics for logical reasoning}

   586 Interpreting propositions as types lets CTT express statements of

   587 intuitionistic logic.  However, Constructive Type Theory is not just another

   588 syntax for first-order logic.  There are fundamental differences.

   589

   590 \index{assumptions!in CTT}

   591 Can assumptions be deleted after use?  Not every occurrence of a type

   592 represents a proposition, and Type Theory assumptions declare variables.

   593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$

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

   595 can be deleted safely.  In Type Theory, $+$-elimination with the assumption

   596 $z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in   597 B$ (for arbitrary $x$ and $y$).  Deleting $z\in A+B$ when other assumptions

   598 refer to $z$ may render the subgoal unprovable: arguably,

   599 meaningless.

   600

   601 Isabelle provides several tactics for predicate calculus reasoning in CTT:

   602 \begin{ttbox}

   603 mp_tac       : int -> tactic

   604 add_mp_tac   : int -> tactic

   605 safestep_tac : thm list -> int -> tactic

   606 safe_tac     : thm list -> int -> tactic

   607 step_tac     : thm list -> int -> tactic

   608 pc_tac       : thm list -> int -> tactic

   609 \end{ttbox}

   610 These are loosely based on the intuitionistic proof procedures

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

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

   613 safe' tactics are misnamed.

   614 \begin{ttdescription}

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

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

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

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

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

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

   621

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

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

   624 avoids information loss but obviously loops if repeated.

   625

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

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

   628 (\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling

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

   630 which are typically premises of the rule being derived.

   631

   632 \item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by

   633   means of backtracking, using {\tt safestep_tac}.

   634

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

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

   637 rules.  It may produce multiple outcomes.

   638

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

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

   641 \end{ttdescription}

   642

   643

   644

   645 \begin{figure}

   646 \index{#+@{\tt\#+} symbol}

   647 \index{*"- symbol}

   648 \index{"|"-@{{\tt"|"-"|} symbol}}

   649 \index{#*@{\tt\#*} symbol}

   650 \index{*div symbol}

   651 \index{*mod symbol}

   652 \begin{constants}

   653   \it symbol  & \it meta-type & \it priority & \it description \\

   654   \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\

   655   \tt div       & $[i,i]\To i$  &  Left 70      & division\\

   656   \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\

   657   \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\

   658   \tt -         & $[i,i]\To i$  &  Left 65      & subtraction\\

   659   \verb'|-|'    & $[i,i]\To i$  &  Left 65      & absolute difference

   660 \end{constants}

   661

   662 \begin{ttbox}

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

   664 \tdx{diff_def}          a-b   == rec(b, a, \%u v. rec(v, 0, \%x y. x))

   665 \tdx{absdiff_def}       a|-|b == (a-b) #+ (b-a)

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

   667

   668 \tdx{mod_def}           a mod b ==

   669                   rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))

   670

   671 \tdx{div_def}           a div b ==

   672                   rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))

   673

   674 \tdx{add_typing}        [| a:N;  b:N |] ==> a #+ b : N

   675 \tdx{addC0}             b:N ==> 0 #+ b = b : N

   676 \tdx{addC_succ}         [| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N

   677

   678 \tdx{add_assoc}         [| a:N;  b:N;  c:N |] ==>

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

   680

   681 \tdx{add_commute}       [| a:N;  b:N |] ==> a #+ b = b #+ a : N

   682

   683 \tdx{mult_typing}       [| a:N;  b:N |] ==> a #* b : N

   684 \tdx{multC0}            b:N ==> 0 #* b = 0 : N

   685 \tdx{multC_succ}        [| a:N;  b:N |] ==> succ(a) #* b = b #+ (a#*b) : N

   686 \tdx{mult_commute}      [| a:N;  b:N |] ==> a #* b = b #* a : N

   687

   688 \tdx{add_mult_dist}     [| a:N;  b:N;  c:N |] ==>

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

   690

   691 \tdx{mult_assoc}        [| a:N;  b:N;  c:N |] ==>

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

   693

   694 \tdx{diff_typing}       [| a:N;  b:N |] ==> a - b : N

   695 \tdx{diffC0}            a:N ==> a - 0 = a : N

   696 \tdx{diff_0_eq_0}       b:N ==> 0 - b = 0 : N

   697 \tdx{diff_succ_succ}    [| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N

   698 \tdx{diff_self_eq_0}    a:N ==> a - a = 0 : N

   699 \tdx{add_inverse_diff}  [| a:N;  b:N;  b-a=0 : N |] ==> b #+ (a-b) = a : N

   700 \end{ttbox}

   701 \caption{The theory of arithmetic} \label{ctt_arith}

   702 \end{figure}

   703

   704

   705 \section{A theory of arithmetic}

   706 \thydx{Arith} is a theory of elementary arithmetic.  It proves the

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

   708 remainder, culminating in the theorem

   709 $a \bmod b + (a/b)\times b = a.$

   710 Figure~\ref{ctt_arith} presents the definitions and some of the key

   711 theorems, including commutative, distributive, and associative laws.

   712

   713 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'

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

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

   716 recursion, some of their definitions may be obscure.

   717

   718 The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where

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

   720

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

   722 as the successor of~$b-1$.  Absolute difference is used to test the

   723 equality $succ(v)=b$.

   724

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

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

   727

   728

   729

   730 \section{The examples directory}

   731 This directory contains examples and experimental proofs in CTT.

   732 \begin{ttdescription}

   733 \item[CTT/ex/typechk.ML]

   734 contains simple examples of type-checking and type deduction.

   735

   736 \item[CTT/ex/elim.ML]

   737 contains some examples from Martin-L\"of~\cite{martinlof84}, proved using

   738 {\tt pc_tac}.

   739

   740 \item[CTT/ex/equal.ML]

   741 contains simple examples of rewriting.

   742

   743 \item[CTT/ex/synth.ML]

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

   745 synthesis.

   746 \end{ttdescription}

   747

   748

   749 \section{Example: type inference}

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

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

   752 initially

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

   754 predecessor function on the natural numbers.

   755 \begin{ttbox}

   756 Goal "lam n. rec(n, 0, \%x y. x) : ?A";

   757 {\out Level 0}

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

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

   760 \end{ttbox}

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

   762 be confused with a meta-level abstraction), we apply the rule

   763 \tdx{ProdI}, for $\Pi$-introduction.  This instantiates~$\Var{A}$ to a

   764 product type of unknown domain and range.

   765 \begin{ttbox}

   766 by (resolve_tac [ProdI] 1);

   767 {\out Level 1}

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

   769 {\out  1. ?A1 type}

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

   771 \end{ttbox}

   772 Subgoal~1 is too flexible.  It can be solved by instantiating~$\Var{A@1}$

   773 to any type, but most instantiations will invalidate subgoal~2.  We

   774 therefore tackle the latter subgoal.  It asks the type of a term beginning

   775 with {\tt rec}, which can be found by $N$-elimination.%

   776 \index{*NE theorem}

   777 \begin{ttbox}

   778 by (eresolve_tac [NE] 2);

   779 {\out Level 2}

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

   781 {\out  1. N type}

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

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

   784 \end{ttbox}

   785 Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of

   786 natural numbers.  However, let us continue proving nontrivial subgoals.

   787 Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}

   788 \begin{ttbox}

   789 by (resolve_tac [NI0] 2);

   790 {\out Level 3}

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

   792 {\out  1. N type}

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

   794 \end{ttbox}

   795 The type~$\Var{A}$ is now fully determined.  It is the product type

   796 $\prod@{x\in N}N$, which is shown as the function type $N\to N$ because

   797 there is no dependence on~$x$.  But we must prove all the subgoals to show

   798 that the original term is validly typed.  Subgoal~2 is provable by

   799 assumption and the remaining subgoal falls by $N$-formation.%

   800 \index{*NF theorem}

   801 \begin{ttbox}

   802 by (assume_tac 2);

   803 {\out Level 4}

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

   805 {\out  1. N type}

   806 \ttbreak

   807 by (resolve_tac [NF] 1);

   808 {\out Level 5}

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

   810 {\out No subgoals!}

   811 \end{ttbox}

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

   813

   814 Even if the original term is ill-typed, one can infer a type for it, but

   815 unprovable subgoals will be left.  As an exercise, try to prove the

   816 following invalid goal:

   817 \begin{ttbox}

   818 Goal "lam n. rec(n, 0, \%x y. tt) : ?A";

   819 \end{ttbox}

   820

   821

   822

   823 \section{An example of logical reasoning}

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

   825 $\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands

   826 for its proof term, a value of type $A$.  The proof term is initially

   827 unknown and takes shape during the proof.

   828

   829 Our example expresses a theorem about quantifiers in a sorted logic:

   830 $\infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}   831 {\ex{x\in A}P(x)\disj Q(x)}   832$

   833 By the propositions-as-types principle, this is encoded

   834 using~$\Sigma$ and~$+$ types.  A special case of it expresses a

   835 distributive law of Type Theory:

   836 $\infer{(A\times B) + (A\times C)}{A\times(B+C)}$

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

   838 conditions explicit, yields the rule we must derive:

   839 $\infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}   840 {\hbox{A type} &   841 \infer*{\hbox{B(x) type}}{[x\in A]} &   842 \infer*{\hbox{C(x) type}}{[x\in A]} &   843 p\in \sum@{x\in A} B(x)+C(x)}   844$

   845 To begin, we bind the rule's premises --- returned by the~{\tt goal}

   846 command --- to the {\ML} variable~{\tt prems}.

   847 \begin{ttbox}

   848 val prems = Goal

   849     "[| A type;                       \ttback

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

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

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

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

   854 {\out Level 0}

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

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

   857 \ttbreak

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

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

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

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

   862 {\out             : thm list}

   863 \end{ttbox}

   864 The last premise involves the sum type~$\Sigma$.  Since it is a premise

   865 rather than the assumption of a goal, it cannot be found by {\tt

   866   eresolve_tac}.  We could insert it (and the other atomic premise) by

   867 calling

   868 \begin{ttbox}

   869 cut_facts_tac prems 1;

   870 \end{ttbox}

   871 A forward proof step is more straightforward here.  Let us resolve the

   872 $\Sigma$-elimination rule with the premises using~\ttindex{RL}.  This

   873 inference yields one result, which we supply to {\tt

   874   resolve_tac}.\index{*SumE theorem}

   875 \begin{ttbox}

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

   877 {\out Level 1}

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

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

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

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

   882 \end{ttbox}

   883 The subgoal has two new parameters, $x$ and~$y$.  In the main goal,

   884 $\Var{a}$ has been instantiated with a \cdx{split} term.  The

   885 assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and

   886 creating the parameter~$xa$.  This inference also inserts~\cdx{when}

   887 into the main goal.\index{*PlusE theorem}

   888 \begin{ttbox}

   889 by (eresolve_tac [PlusE] 1);

   890 {\out Level 2}

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

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

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

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

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

   896 \ttbreak

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

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

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

   900 \end{ttbox}

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

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

   903 a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left

   904 injection~(\cdx{inl}).

   905 \index{*PlusI_inl theorem}

   906 \begin{ttbox}

   907 by (resolve_tac [PlusI_inl] 1);

   908 {\out Level 3}

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

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

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

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

   913 \ttbreak

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

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

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

   917 \end{ttbox}

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

   919 Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.

   920 This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains

   921 an ordered pair, whose components are two new unknowns.%

   922 \index{*SumI theorem}

   923 \begin{ttbox}

   924 by (resolve_tac [SumI] 1);

   925 {\out Level 4}

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

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

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

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

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

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

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

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

   934 \end{ttbox}

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

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

   937 \begin{ttbox}

   938 by (assume_tac 1);

   939 {\out Level 5}

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

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

   942 \ttbreak

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

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

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

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

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

   948 \ttbreak

   949 by (assume_tac 1);

   950 {\out Level 6}

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

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

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

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

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

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

   957 \end{ttbox}

   958 Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.

   959 Such subgoals are usually trivial; this one yields to

   960 \ttindex{typechk_tac}, given the current list of premises.

   961 \begin{ttbox}

   962 by (typechk_tac prems);

   963 {\out Level 7}

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

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

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

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

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

   969 \end{ttbox}

   970 This subgoal is the other case from the $+$-elimination above, and can be

   971 proved similarly.  Quicker is to apply \ttindex{pc_tac}.  The main goal

   972 finally gets a fully instantiated proof object.

   973 \begin{ttbox}

   974 by (pc_tac prems 1);

   975 {\out Level 8}

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

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

   978 {\out No subgoals!}

   979 \end{ttbox}

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

   981 proves this theorem.

   982

   983

   984 \section{Example: deriving a currying functional}

   985 In simply-typed languages such as {\ML}, a currying functional has the type

   986 $(A\times B \to C) \to (A\to (B\to C)).$

   987 Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.

   988 The functional takes a function~$f$ that maps $z:\Sigma(A,B)$

   989 to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to

   990 $C(\langle x,y\rangle)$.

   991

   992 Formally, there are three typing premises.  $A$ is a type; $B$ is an

   993 $A$-indexed family of types; $C$ is a family of types indexed by

   994 $\Sigma(A,B)$.  The goal is expressed using \hbox{\tt PROD f} to ensure

   995 that the parameter corresponding to the functional's argument is really

   996 called~$f$; Isabelle echoes the type using \verb|-->| because there is no

   997 explicit dependence upon~$f$.

   998 \begin{ttbox}

   999 val prems = Goal

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

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

  1002 \ttback    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).      \ttback

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

  1004 \ttbreak

  1005 {\out Level 0}

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

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

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

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

  1010 \ttbreak

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

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

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

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

  1015 \end{ttbox}

  1016 This is a chance to demonstrate \ttindex{intr_tac}.  Here, the tactic

  1017 repeatedly applies $\Pi$-introduction and proves the rather

  1018 tiresome typing conditions.

  1019

  1020 Note that $\Var{a}$ becomes instantiated to three nested

  1021 $\lambda$-abstractions.  It would be easier to read if the bound variable

  1022 names agreed with the parameters in the subgoal.  Isabelle attempts to give

  1023 parameters the same names as corresponding bound variables in the goal, but

  1024 this does not always work.  In any event, the goal is logically correct.

  1025 \begin{ttbox}

  1026 by (intr_tac prems);

  1027 {\out Level 1}

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

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

  1030 {\out  1. !!f x y.}

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

  1032 {\out        ?b7(f,x,y) : C(<x,y>)}

  1033 \end{ttbox}

  1034 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.

  1035 \index{*ProdE theorem}

  1036 \begin{ttbox}

  1037 by (eresolve_tac [ProdE] 1);

  1038 {\out Level 2}

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

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

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

  1042 \end{ttbox}

  1043 Finally, we verify that the argument's type is suitable for the function

  1044 application.  This is straightforward using introduction rules.

  1045 \index{*intr_tac}

  1046 \begin{ttbox}

  1047 by (intr_tac prems);

  1048 {\out Level 3}

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

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

  1051 {\out No subgoals!}

  1052 \end{ttbox}

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

  1054 also prove an example by Martin-L\"of, related to $\disj$-elimination

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

  1056

  1057

  1058 \section{Example: proving the Axiom of Choice} \label{ctt-choice}

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

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

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

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

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

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

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

  1066

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

  1068 Theory.  The following definitions work:

  1069 \begin{eqnarray*}

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

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

  1072 \end{eqnarray*}

  1073 But a completely formal proof is hard to find.  The rules can be applied in

  1074 countless ways, yielding many higher-order unifiers.  The proof can get

  1075 bogged down in the details.  But with a careful selection of derived rules

  1076 (recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can

  1077 prove the theorem in nine steps.

  1078 \begin{ttbox}

  1079 val prems = Goal

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

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

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

  1083 \ttback                     (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, fx))";

  1084 {\out Level 0}

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

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

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

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

  1089 \ttbreak

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

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

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

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

  1094 {\out             : thm list}

  1095 \end{ttbox}

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

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

  1098 a $\lambda$-abstraction and an ordered pair.  The pair's components are

  1099 themselves $\lambda$-abstractions and there is a subgoal for each.

  1100 \begin{ttbox}

  1101 by (intr_tac prems);

  1102 {\out Level 1}

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

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

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

  1106 \ttbreak

  1107 {\out  1. !!h x.}

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

  1109 {\out        ?b7(h,x) : B(x)}

  1110 \ttbreak

  1111 {\out  2. !!h x.}

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

  1113 {\out        ?b8(h,x) : C(x,(lam x. ?b7(h,x))  x)}

  1114 \end{ttbox}

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

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

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

  1118 result lie in the relation~$C$.  This latter task will take up most of the

  1119 proof.

  1120 \index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}

  1121 \begin{ttbox}

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

  1123 {\out Level 2}

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

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

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

  1127 \ttbreak

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

  1129 {\out  2. !!h x.}

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

  1131 {\out        ?b8(h,x) : C(x,(lam x. fst(h  x))  x)}

  1132 \end{ttbox}

  1133 Above, we have composed {\tt fst} with the function~$h$.  Unification

  1134 has deduced that the function must be applied to $x\in A$.  We have our

  1135 choice function.

  1136 \begin{ttbox}

  1137 by (assume_tac 1);

  1138 {\out Level 3}

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

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

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

  1142 {\out  1. !!h x.}

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

  1144 {\out        ?b8(h,x) : C(x,(lam x. fst(h  x))  x)}

  1145 \end{ttbox}

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

  1147 simplified.  The derived rule \tdx{replace_type} lets us replace a type

  1148 by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:

  1149 \begin{ttbox}

  1150 by (resolve_tac [replace_type] 1);

  1151 {\out Level 4}

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

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

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

  1155 \ttbreak

  1156 {\out  1. !!h x.}

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

  1158 {\out        C(x,(lam x. fst(h  x))  x) = ?A13(h,x)}

  1159 \ttbreak

  1160 {\out  2. !!h x.}

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

  1162 {\out        ?b8(h,x) : ?A13(h,x)}

  1163 \end{ttbox}

  1164 The derived rule \tdx{subst_eqtyparg} lets us simplify a type's

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

  1166 \begin{ttbox}

  1167 by (resolve_tac [subst_eqtyparg] 1);

  1168 {\out Level 5}

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

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

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

  1172 \ttbreak

  1173 {\out  1. !!h x.}

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

  1175 {\out        (lam x. fst(h  x))  x = ?c14(h,x) : ?A14(h,x)}

  1176 \ttbreak

  1177 {\out  2. !!h x z.}

  1178 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}

  1179 {\out           z : ?A14(h,x) |] ==>}

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

  1181 \ttbreak

  1182 {\out  3. !!h x.}

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

  1184 {\out        ?b8(h,x) : C(x,?c14(h,x))}

  1185 \end{ttbox}

  1186 Subgoal~1 requires simply $\beta$-contraction, which is the rule

  1187 \tdx{ProdC}.  The term $\Var{c@{14}}(h,x)$ in the last subgoal

  1188 receives the contracted result.

  1189 \begin{ttbox}

  1190 by (resolve_tac [ProdC] 1);

  1191 {\out Level 6}

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

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

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

  1195 \ttbreak

  1196 {\out  1. !!h x.}

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

  1198 {\out        x : ?A15(h,x)}

  1199 \ttbreak

  1200 {\out  2. !!h x xa.}

  1201 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}

  1202 {\out           xa : ?A15(h,x) |] ==>}

  1203 {\out        fst(h  xa) : ?B15(h,x,xa)}

  1204 \ttbreak

  1205 {\out  3. !!h x z.}

  1206 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}

  1207 {\out           z : ?B15(h,x,x) |] ==>}

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

  1209 \ttbreak

  1210 {\out  4. !!h x.}

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

  1212 {\out        ?b8(h,x) : C(x,fst(h  x))}

  1213 \end{ttbox}

  1214 Routine type-checking goals proliferate in Constructive Type Theory, but

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

  1216 \tdx{SumE_fst} along with the premises.

  1217 \begin{ttbox}

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

  1219 {\out Level 7}

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

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

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

  1223 \ttbreak

  1224 {\out  1. !!h x.}

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

  1226 {\out        ?b8(h,x) : C(x,fst(h  x))}

  1227 \end{ttbox}

  1228 We are finally ready to compose {\tt snd} with~$h$.

  1229 \index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}

  1230 \begin{ttbox}

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

  1232 {\out Level 8}

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

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

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

  1236 \ttbreak

  1237 {\out  1. !!h x. x : A ==> x : A}

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

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

  1240 \end{ttbox}

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

  1242 to finish the type-checking.

  1243 \begin{ttbox}

  1244 by (typechk_tac prems);

  1245 {\out Level 9}

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

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

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

  1249 {\out No subgoals!}

  1250 \end{ttbox}

  1251 It might be instructive to compare this proof with Martin-L\"of's forward

  1252 proof of the Axiom of Choice \cite[page~50]{martinlof84}.

  1253

  1254 \index{Constructive Type Theory|)}
`