doc-src/Logics/CTT.tex
 author wenzelm Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) changeset 48497 ba61aceaa18a parent 43049 99985426c0bb permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     1 \chapter{Constructive Type Theory}

     2 \index{Constructive Type Theory|(}

     3

     4 \underscoreoff %this file contains _ in rule names

     5

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

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

     8 the principles of intuitionistic mathematics; it embodies the

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

    10 programs from proofs.

    11

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

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

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

    15 directly~\cite{alf}.

    16

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

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

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

    20 judgement 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$

    24 This 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$'

    26 could not be formalized.

    27

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

    29 natural 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$

    39 Assumptions 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}$

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

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

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

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

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

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

    48 \index{assumptions!in CTT}

    49

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

    51 type 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   87 CTT supports all of Type Theory apart from list types, well-ordering types,   88 and universes. Universes could be introduced {\em\a la Tarski}, adding new   89 constants as names for types. The formulation {\em\a la Russell}, where   90 types 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   92 difficulties involving extensionality of functions; I suggest that you use   93 some other method for defining recursive types. List types are easy to   94 introduce by declaring new rules.   95   96 CTT uses the 1982 version of Type Theory, with extensional equality. The   97 computation a=b\in A and the equality c\in Eq(A,a,b) are interchangeable.   98 Its rewriting tactics prove theorems of the form a=b\in A. It could be   99 modified to have intensional equality, but rewriting tactics would have to   100 prove theorems of the form c\in Eq(A,a,b) and the computation rules might   101 require 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}   146 prop & = & type " type" \\   147 & | & type " = " type \\   148 & | & term " : " type \\   149 & | & term " = " term " : " type   150 \\[2ex]   151 type & = & \hbox{expression of type~t} \\   152 & | & "PROD~" id " : " type " . " type \\   153 & | & "SUM~~" id " : " type " . " type   154 \\[2ex]   155 term & = & \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}

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

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

   171 type operators.  Note that meta-level abstraction and application, $\lambda   172 x.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

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

   175 $i\To i$.

   176

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

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

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

   180

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

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

   183 products $\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}

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

   188 \end{ttbox}

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

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

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

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

   193 abbreviations 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 |] ==> pa : B(a)

   269 \tdx{ProdEL}    [| p=q: PROD x:A. B(x);  a=b : A |] ==> pa = qb : 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. px) = 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(pa): C(pa)

   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}

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

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

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

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

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

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

   400 Introduction and computation rules are often further suffixed with

   401 constructor names.

   402

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

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

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

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

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

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

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

   410

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

   412 judgements.  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

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

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

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

   419 91]{martinlof84}.

   420

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

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

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

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

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

   426

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

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

   429 predicate calculus rules for universal quantifiers and implication.  They

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

   431 $\lambda$-calculus.

   432

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

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

   435 predicate calculus rules for existential quantifiers and conjunction.  They

   436 also permit reasoning about ordered pairs, with the projections

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

   438

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

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

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

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

   443

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

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

   446 truth.

   447

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

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

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

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

   452

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

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

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

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

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

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

   459 proof of the Axiom of Choice.

   460

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

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

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

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

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

   466 variables in the premises.

   467

   468

   469 \section{Rule lists}

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

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

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

   473 type

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

   475 \begin{ttdescription}

   476 \item[\ttindexbold{form_rls}]

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

   478 $F$, and $T$.

   479

   480 \item[\ttindexbold{formL_rls}]

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

   482 other types use \tdx{refl_type}.)

   483

   484 \item[\ttindexbold{intr_rls}]

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

   486 $T$.

   487

   488 \item[\ttindexbold{intrL_rls}]

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

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

   491

   492 \item[\ttindexbold{elim_rls}]

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

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

   495 eliminator.

   496

   497 \item[\ttindexbold{elimL_rls}]

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

   499

   500 \item[\ttindexbold{comp_rls}]

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

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

   503

   504 \item[\ttindexbold{basic_defs}]

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

   506 \end{ttdescription}

   507

   508

   509 \section{Tactics for subgoal reordering}

   510 \begin{ttbox}

   511 test_assume_tac : int -> tactic

   512 typechk_tac     : thm list -> tactic

   513 equal_tac       : thm list -> tactic

   514 intr_tac        : thm list -> tactic

   515 \end{ttbox}

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

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

   518 unify 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 %

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

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

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

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

   527 to see why this is necessary.

   528 \begin{ttdescription}

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

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

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

   532 Otherwise, it fails.

   533

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

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

   536 the 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

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

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

   540

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

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

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

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

   545 tactic can also perform type-checking.

   546

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

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

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

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

   551 expressed as a type.

   552 \end{ttdescription}

   553

   554

   555

   556 \section{Rewriting tactics}

   557 \begin{ttbox}

   558 rew_tac     : thm list -> tactic

   559 hyp_rew_tac : thm list -> tactic

   560 \end{ttbox}

   561 Object-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 %

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

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

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

   571 Meta-level simplification handles only definitional equality.

   572 \begin{ttdescription}

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

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

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

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

   577

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

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

   580 the assumptions.

   581 \end{ttdescription}

   582

   583

   584 \section{Tactics for logical reasoning}

   585 Interpreting propositions as types lets CTT express statements of

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

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

   588

   589 \index{assumptions!in CTT}

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

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

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

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

   594 can 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   596 B$ (for arbitrary $x$ and $y$).  Deleting $z\in A+B$ when other assumptions

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

   598 meaningless.

   599

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

   601 \begin{ttbox}

   602 mp_tac       : int -> tactic

   603 add_mp_tac   : int -> tactic

   604 safestep_tac : thm list -> int -> tactic

   605 safe_tac     : thm list -> int -> tactic

   606 step_tac     : thm list -> int -> tactic

   607 pc_tac       : thm list -> int -> tactic

   608 \end{ttbox}

   609 These are loosely based on the intuitionistic proof procedures

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

   611 propositional 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$]

   615 searches 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

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

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

   620

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

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

   623 avoids information loss but obviously loops if repeated.

   624

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

   626 attacks 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$,

   629 which 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$]

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

   636 rules.  It may produce multiple outcomes.

   637

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

   639 tries 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

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

   711 remainder, culminating in the theorem

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

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

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

   715

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

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

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

   719 recursion, some of their definitions may be obscure.

   720

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

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

   723

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

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

   726 equality $succ(v)=b$.

   727

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

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

   730

   731

   732

   733 \section{The examples directory}

   734 This directory contains examples and experimental proofs in CTT.

   735 \begin{ttdescription}

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

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

   738

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

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

   741 {\tt pc_tac}.

   742

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

   744 contains simple examples of rewriting.

   745

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

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

   748 synthesis.

   749 \end{ttdescription}

   750

   751

   752 \section{Example: type inference}

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

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

   755 initially

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

   757 predecessor function on the natural numbers.

   758 \begin{ttbox}

   759 Goal "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}

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

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

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

   767 product type of unknown domain and range.

   768 \begin{ttbox}

   769 by (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}

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

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

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

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

   779 \index{*NE theorem}

   780 \begin{ttbox}

   781 by (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}

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

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

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

   791 \begin{ttbox}

   792 by (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}

   798 The 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

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

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

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

   803 \index{*NF theorem}

   804 \begin{ttbox}

   805 by (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

   810 by (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}

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

   816

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

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

   819 following invalid goal:

   820 \begin{ttbox}

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

   822 \end{ttbox}

   823

   824

   825

   826 \section{An example of logical reasoning}

   827 Logical 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

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

   830 unknown and takes shape during the proof.

   831

   832 Our 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$

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

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

   838 distributive law of Type Theory:

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

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

   841 conditions 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$

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

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

   850 \begin{ttbox}

   851 val 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}

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

   868 rather 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

   870 calling

   871 \begin{ttbox}

   872 cut_facts_tac prems 1;

   873 \end{ttbox}

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

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

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

   877   resolve_tac}.\index{*SumE theorem}

   878 \begin{ttbox}

   879 by (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}

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

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

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

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

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

   891 \begin{ttbox}

   892 by (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}

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

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

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

   907 injection~(\cdx{inl}).

   908 \index{*PlusI_inl theorem}

   909 \begin{ttbox}

   910 by (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}

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

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

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

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

   925 \index{*SumI theorem}

   926 \begin{ttbox}

   927 by (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}

   938 The 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}

   941 by (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

   952 by (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}

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

   962 Such subgoals are usually trivial; this one yields to

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

   964 \begin{ttbox}

   965 by (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}

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

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

   975 finally gets a fully instantiated proof object.

   976 \begin{ttbox}

   977 by (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}

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

   984 proves this theorem.

   985

   986

   987 \section{Example: deriving a currying functional}

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

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

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

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

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

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

   994

   995 Formally, 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

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

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

  1000 explicit dependence upon~$f$.

  1001 \begin{ttbox}

  1002 val 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}

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

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

  1021 tiresome typing conditions.

  1022

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

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

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

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

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

  1028 \begin{ttbox}

  1029 by (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}

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

  1038 \index{*ProdE theorem}

  1039 \begin{ttbox}

  1040 by (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}

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

  1047 application.  This is straightforward using introduction rules.

  1048 \index{*intr_tac}

  1049 \begin{ttbox}

  1050 by (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}

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

  1057 also 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}

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

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

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

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

  1066 that 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

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

  1069

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

  1071 Theory.  The following definitions work:

  1072 \begin{eqnarray*}

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

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

  1075 \end{eqnarray*}

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

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

  1078 bogged 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

  1080 prove the theorem in nine steps.

  1081 \begin{ttbox}

  1082 val 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, fx))";

  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}

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

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

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

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

  1103 \begin{ttbox}

  1104 by (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}

  1118 Subgoal~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

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

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

  1122 proof.

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

  1124 \begin{ttbox}

  1125 by (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}

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

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

  1138 choice function.

  1139 \begin{ttbox}

  1140 by (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}

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

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

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

  1152 \begin{ttbox}

  1153 by (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}

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

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

  1169 \begin{ttbox}

  1170 by (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}

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

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

  1191 receives the contracted result.

  1192 \begin{ttbox}

  1193 by (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}

  1217 Routine 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}

  1221 by (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}

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

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

  1233 \begin{ttbox}

  1234 by (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}

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

  1245 to finish the type-checking.

  1246 \begin{ttbox}

  1247 by (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}

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

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

  1256

  1257 \index{Constructive Type Theory|)}
`