author | haftmann |
Thu, 12 Nov 2009 15:49:01 +0100 | |
changeset 33633 | 9f7280e0c231 |
parent 12679 | 8ed660138f83 |
child 42637 | 381fdcab0f36 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
2 |
\chapter{Constructive Type Theory} |
|
314 | 3 |
\index{Constructive Type Theory|(} |
4 |
||
7159
b009afd1ace5
\underscoreoff needed because of \underscoreon in previous file
paulson
parents:
6170
diff
changeset
|
5 |
\underscoreoff %this file contains _ in rule names |
b009afd1ace5
\underscoreoff needed because of \underscoreon in previous file
paulson
parents:
6170
diff
changeset
|
6 |
|
104 | 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 |
|
314 | 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}. |
|
104 | 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 |
||
314 | 29 |
The theory~\thydx{CTT} implements Constructive Type Theory, using |
104 | 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. & |
|
111 | 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 \\ |
|
104 | 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} \] |
|
9695 | 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} |
|
104 | 50 |
|
9695 | 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}. |
|
314 | 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] |
|
104 | 63 |
|
314 | 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} |
|
9695 | 84 |
\caption{The constants of CTT} \label{ctt-constants} |
314 | 85 |
\end{figure} |
86 |
||
87 |
||
9695 | 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. |
|
104 | 96 |
|
9695 | 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. |
|
104 | 103 |
|
104 |
||
105 |
\begin{figure} \tabcolsep=1em %wider spacing in tables |
|
9695 | 106 |
\index{lambda abs@$\lambda$-abstractions!in CTT} |
104 | 107 |
\begin{center} |
108 |
\begin{tabular}{llrrr} |
|
314 | 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 |
|
104 | 111 |
\end{tabular} |
112 |
\end{center} |
|
113 |
\subcaption{Binders} |
|
114 |
||
115 |
\begin{center} |
|
9695 | 116 |
\index{*"` symbol}\index{function applications!in CTT} |
314 | 117 |
\index{*"+ symbol} |
104 | 118 |
\begin{tabular}{rrrr} |
314 | 119 |
\it symbol & \it meta-type & \it priority & \it description \\ |
111 | 120 |
\tt ` & $[i,i]\to i$ & Left 55 & function application\\ |
121 |
\tt + & $[t,t]\to t$ & Right 30 & sum of two types |
|
104 | 122 |
\end{tabular} |
123 |
\end{center} |
|
124 |
\subcaption{Infixes} |
|
125 |
||
314 | 126 |
\index{*"* symbol} |
127 |
\index{*"-"-"> symbol} |
|
104 | 128 |
\begin{center} \tt\frenchspacing |
129 |
\begin{tabular}{rrr} |
|
111 | 130 |
\it external & \it internal & \it standard notation \\ |
5151 | 131 |
\sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) & |
111 | 132 |
\rm product $\prod@{x\in A}B[x]$ \\ |
5151 | 133 |
\sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x. B[x]$) & |
111 | 134 |
\rm sum $\sum@{x\in A}B[x]$ \\ |
5151 | 135 |
$A$ --> $B$ & Prod($A$, $\lambda x. B$) & |
111 | 136 |
\rm function space $A\to B$ \\ |
5151 | 137 |
$A$ * $B$ & Sum($A$, $\lambda x. B$) & |
111 | 138 |
\rm binary product $A\times B$ |
104 | 139 |
\end{tabular} |
140 |
\end{center} |
|
141 |
\subcaption{Translations} |
|
142 |
||
314 | 143 |
\index{*"= symbol} |
104 | 144 |
\begin{center} |
145 |
\dquotes |
|
146 |
\[ \begin{array}{rcl} |
|
111 | 147 |
prop & = & type " type" \\ |
148 |
& | & type " = " type \\ |
|
149 |
& | & term " : " type \\ |
|
150 |
& | & term " = " term " : " type |
|
104 | 151 |
\\[2ex] |
111 | 152 |
type & = & \hbox{expression of type~$t$} \\ |
153 |
& | & "PROD~" id " : " type " . " type \\ |
|
154 |
& | & "SUM~~" id " : " type " . " type |
|
104 | 155 |
\\[2ex] |
111 | 156 |
term & = & \hbox{expression of type~$i$} \\ |
157 |
& | & "lam " id~id^* " . " term \\ |
|
158 |
& | & "< " term " , " term " >" |
|
104 | 159 |
\end{array} |
160 |
\] |
|
161 |
\end{center} |
|
162 |
\subcaption{Grammar} |
|
9695 | 163 |
\caption{Syntax of CTT} \label{ctt-syntax} |
104 | 164 |
\end{figure} |
165 |
||
166 |
%%%%\section{Generic Packages} typedsimp.ML???????????????? |
|
167 |
||
168 |
||
169 |
\section{Syntax} |
|
284 | 170 |
The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include |
9695 | 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$. |
|
104 | 177 |
|
9695 | 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. |
|
314 | 181 |
|
182 |
\index{*SUM symbol}\index{*PROD symbol} |
|
6072 | 183 |
Quantification is expressed by sums $\sum@{x\in A}B[x]$ and |
314 | 184 |
products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt |
6072 | 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 |
|
104 | 187 |
\begin{ttbox} |
284 | 188 |
SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y))) |
104 | 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} |
|
314 | 199 |
\tdx{refl_type} A type ==> A = A |
200 |
\tdx{refl_elem} a : A ==> a = a : A |
|
104 | 201 |
|
314 | 202 |
\tdx{sym_type} A = B ==> B = A |
203 |
\tdx{sym_elem} a = b : A ==> b = a : A |
|
104 | 204 |
|
314 | 205 |
\tdx{trans_type} [| A = B; B = C |] ==> A = C |
206 |
\tdx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A |
|
104 | 207 |
|
314 | 208 |
\tdx{equal_types} [| a : A; A = B |] ==> a : B |
209 |
\tdx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B |
|
104 | 210 |
|
314 | 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) |
|
104 | 213 |
|] ==> B(a) = D(c) |
214 |
||
314 | 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) |
|
104 | 217 |
|] ==> b(a) = d(c) : B(a) |
218 |
||
314 | 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 |
|
104 | 222 |
\end{ttbox} |
223 |
\caption{General equality rules} \label{ctt-equality} |
|
224 |
\end{figure} |
|
225 |
||
226 |
||
227 |
\begin{figure} |
|
228 |
\begin{ttbox} |
|
314 | 229 |
\tdx{NF} N type |
104 | 230 |
|
314 | 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 |
|
104 | 234 |
|
314 | 235 |
\tdx{NE} [| p: N; a: C(0); |
104 | 236 |
!!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
5151 | 237 |
|] ==> rec(p, a, \%u v. b(u,v)) : C(p) |
104 | 238 |
|
314 | 239 |
\tdx{NEL} [| p = q : N; a = c : C(0); |
104 | 240 |
!!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u)) |
5151 | 241 |
|] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p) |
104 | 242 |
|
314 | 243 |
\tdx{NC0} [| a: C(0); |
104 | 244 |
!!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
5151 | 245 |
|] ==> rec(0, a, \%u v. b(u,v)) = a : C(0) |
104 | 246 |
|
314 | 247 |
\tdx{NC_succ} [| p: N; a: C(0); |
104 | 248 |
!!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
5151 | 249 |
|] ==> rec(succ(p), a, \%u v. b(u,v)) = |
250 |
b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p)) |
|
104 | 251 |
|
314 | 252 |
\tdx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F |
104 | 253 |
\end{ttbox} |
254 |
\caption{Rules for type~$N$} \label{ctt-N} |
|
255 |
\end{figure} |
|
256 |
||
257 |
||
258 |
\begin{figure} |
|
259 |
\begin{ttbox} |
|
5151 | 260 |
\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type |
314 | 261 |
\tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==> |
5151 | 262 |
PROD x:A. B(x) = PROD x:C. D(x) |
104 | 263 |
|
314 | 264 |
\tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x) |
5151 | 265 |
|] ==> lam x. b(x) : PROD x:A. B(x) |
314 | 266 |
\tdx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x) |
5151 | 267 |
|] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x) |
104 | 268 |
|
5151 | 269 |
\tdx{ProdE} [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a) |
270 |
\tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a) |
|
104 | 271 |
|
314 | 272 |
\tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x) |
5151 | 273 |
|] ==> (lam x. b(x)) ` a = b(a) : B(a) |
104 | 274 |
|
5151 | 275 |
\tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x) |
104 | 276 |
\end{ttbox} |
314 | 277 |
\caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod} |
104 | 278 |
\end{figure} |
279 |
||
280 |
||
281 |
\begin{figure} |
|
282 |
\begin{ttbox} |
|
5151 | 283 |
\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type |
314 | 284 |
\tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x) |
5151 | 285 |
|] ==> SUM x:A. B(x) = SUM x:C. D(x) |
104 | 286 |
|
5151 | 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) |
|
104 | 289 |
|
5151 | 290 |
\tdx{SumE} [| p: SUM x:A. B(x); |
104 | 291 |
!!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |
5151 | 292 |
|] ==> split(p, \%x y. c(x,y)) : C(p) |
104 | 293 |
|
5151 | 294 |
\tdx{SumEL} [| p=q : SUM x:A. B(x); |
104 | 295 |
!!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>) |
5151 | 296 |
|] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p) |
104 | 297 |
|
314 | 298 |
\tdx{SumC} [| a: A; b: B(a); |
104 | 299 |
!!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |
5151 | 300 |
|] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>) |
104 | 301 |
|
5151 | 302 |
\tdx{fst_def} fst(a) == split(a, \%x y. x) |
303 |
\tdx{snd_def} snd(a) == split(a, \%x y. y) |
|
104 | 304 |
\end{ttbox} |
314 | 305 |
\caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum} |
104 | 306 |
\end{figure} |
307 |
||
308 |
||
309 |
\begin{figure} |
|
310 |
\begin{ttbox} |
|
314 | 311 |
\tdx{PlusF} [| A type; B type |] ==> A+B type |
312 |
\tdx{PlusFL} [| A = C; B = D |] ==> A+B = C+D |
|
104 | 313 |
|
314 | 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 |
|
104 | 316 |
|
314 | 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 |
|
104 | 319 |
|
314 | 320 |
\tdx{PlusE} [| p: A+B; |
104 | 321 |
!!x. x:A ==> c(x): C(inl(x)); |
322 |
!!y. y:B ==> d(y): C(inr(y)) |
|
5151 | 323 |
|] ==> when(p, \%x. c(x), \%y. d(y)) : C(p) |
104 | 324 |
|
314 | 325 |
\tdx{PlusEL} [| p = q : A+B; |
104 | 326 |
!!x. x: A ==> c(x) = e(x) : C(inl(x)); |
327 |
!!y. y: B ==> d(y) = f(y) : C(inr(y)) |
|
5151 | 328 |
|] ==> when(p, \%x. c(x), \%y. d(y)) = |
329 |
when(q, \%x. e(x), \%y. f(y)) : C(p) |
|
104 | 330 |
|
314 | 331 |
\tdx{PlusC_inl} [| a: A; |
104 | 332 |
!!x. x:A ==> c(x): C(inl(x)); |
333 |
!!y. y:B ==> d(y): C(inr(y)) |
|
5151 | 334 |
|] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a)) |
104 | 335 |
|
314 | 336 |
\tdx{PlusC_inr} [| b: B; |
104 | 337 |
!!x. x:A ==> c(x): C(inl(x)); |
338 |
!!y. y:B ==> d(y): C(inr(y)) |
|
5151 | 339 |
|] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b)) |
104 | 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} |
|
314 | 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 |
|
104 | 350 |
|
314 | 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) |
|
104 | 356 |
\end{ttbox} |
357 |
||
314 | 358 |
\caption{Rules for types $F$ and $T$} \label{ctt-ft} |
104 | 359 |
\end{figure} |
360 |
||
361 |
||
362 |
\begin{figure} |
|
363 |
\begin{ttbox} |
|
314 | 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} |
|
104 | 372 |
|
314 | 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) |
|
104 | 380 |
|] ==> c(p`a): C(p`a) |
381 |
||
314 | 382 |
\tdx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B) |
104 | 383 |
|
314 | 384 |
\tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A |
104 | 385 |
|
314 | 386 |
\tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type |
104 | 387 |
|] ==> snd(p) : B(fst(p)) |
388 |
\end{ttbox} |
|
389 |
||
9695 | 390 |
\caption{Derived rules for CTT} \label{ctt-derived} |
104 | 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 |
|
333 | 400 |
called {\bf long} rules; their names have the suffix~{\tt L}\@. |
401 |
Introduction and computation rules are often further suffixed with |
|
104 | 402 |
constructor names. |
403 |
||
314 | 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}. |
|
104 | 427 |
|
314 | 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}. |
|
104 | 444 |
|
314 | 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. |
|
104 | 461 |
|
462 |
All the rules are given in $\eta$-expanded form. For instance, every |
|
5151 | 463 |
occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the |
314 | 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. |
|
104 | 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 |
|
9695 | 473 |
Theory rules against a proof state. CTT defines lists --- each with |
104 | 474 |
type |
475 |
\hbox{\tt thm list} --- of related rules. |
|
314 | 476 |
\begin{ttdescription} |
104 | 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 |
|
314 | 483 |
other types use \tdx{refl_type}.) |
104 | 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 |
|
314 | 491 |
$T$ use \tdx{refl_elem}.) |
104 | 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}] |
|
314 | 506 |
contains the definitions of {\tt fst} and {\tt snd}. |
507 |
\end{ttdescription} |
|
104 | 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} |
|
9695 | 517 |
Blind application of CTT rules seldom leads to a proof. The elimination |
104 | 518 |
rules, especially, create subgoals containing new unknowns. These subgoals |
333 | 519 |
unify with anything, creating a huge search space. The standard tactic |
9695 | 520 |
\ttindex{filt_resolve_tac} |
314 | 521 |
(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% |
522 |
{\S\ref{filt_resolve_tac}}) |
|
523 |
% |
|
9695 | 524 |
fails for goals that are too flexible; so does the CTT tactic {\tt |
314 | 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} |
|
104 | 530 |
\item[\ttindexbold{test_assume_tac} $i$] |
314 | 531 |
uses {\tt assume_tac} to solve the subgoal by assumption, but only if |
104 | 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 |
|
975
6c280d1dac35
Corrected faulty reference to Hindley-Milner type inference
lcp
parents:
333
diff
changeset
|
538 |
$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it |
6c280d1dac35
Corrected faulty reference to Hindley-Milner type inference
lcp
parents:
333
diff
changeset
|
539 |
performs type inference. The tactic can also solve goals of |
104 | 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 |
|
6170 | 546 |
tactic can also perform type-checking. |
104 | 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. |
|
314 | 553 |
\end{ttdescription} |
104 | 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 |
|
314 | 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 |
|
9695 | 566 |
TSimpFun} is only useful for CTT and similar logics with type inference |
567 |
rules. At present it is undocumented.} |
|
314 | 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}. |
|
104 | 572 |
Meta-level simplification handles only definitional equality. |
314 | 573 |
\begin{ttdescription} |
104 | 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. |
|
314 | 582 |
\end{ttdescription} |
104 | 583 |
|
584 |
||
585 |
\section{Tactics for logical reasoning} |
|
9695 | 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. |
|
104 | 589 |
|
9695 | 590 |
\index{assumptions!in CTT} |
314 | 591 |
Can assumptions be deleted after use? Not every occurrence of a type |
592 |
represents a proposition, and Type Theory assumptions declare variables. |
|
104 | 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$ |
|
314 | 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 |
||
9695 | 601 |
Isabelle provides several tactics for predicate calculus reasoning in CTT: |
104 | 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 |
|
314 | 611 |
of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for |
6170 | 612 |
propositional reasoning may be unsafe for type-checking; thus, some of the |
314 | 613 |
`safe' tactics are misnamed. |
614 |
\begin{ttdescription} |
|
104 | 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$] |
|
314 | 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. |
|
104 | 625 |
|
626 |
\item[\ttindexbold{safestep_tac} $thms$ $i$] |
|
627 |
attacks subgoal~$i$ using formation rules and certain other `safe' rules |
|
333 | 628 |
(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling |
104 | 629 |
{\tt mp_tac} when appropriate. It also uses~$thms$, |
630 |
which are typically premises of the rule being derived. |
|
631 |
||
314 | 632 |
\item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by |
633 |
means of backtracking, using {\tt safestep_tac}. |
|
104 | 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}. |
|
314 | 641 |
\end{ttdescription} |
104 | 642 |
|
643 |
||
644 |
||
645 |
\begin{figure} |
|
314 | 646 |
\index{#+@{\tt\#+} symbol} |
647 |
\index{*"- symbol} |
|
12679
8ed660138f83
changed the index sort key from |-| to just |- because pdflatex can't cope
paulson
parents:
9695
diff
changeset
|
648 |
\index{"|"-@{{\tt"|"-"|} symbol}} |
314 | 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} |
|
104 | 661 |
|
662 |
\begin{ttbox} |
|
5151 | 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)) |
|
314 | 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 == |
|
5151 | 669 |
rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v))) |
104 | 670 |
|
314 | 671 |
\tdx{div_def} a div b == |
5151 | 672 |
rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v)) |
314 | 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 |] ==> |
|
104 | 679 |
(a #+ b) #+ c = a #+ (b #+ c) : N |
680 |
||
314 | 681 |
\tdx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N |
104 | 682 |
|
314 | 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 |
|
104 | 687 |
|
314 | 688 |
\tdx{add_mult_dist} [| a:N; b:N; c:N |] ==> |
104 | 689 |
(a #+ b) #* c = (a #* c) #+ (b #* c) : N |
690 |
||
314 | 691 |
\tdx{mult_assoc} [| a:N; b:N; c:N |] ==> |
104 | 692 |
(a #* b) #* c = a #* (b #* c) : N |
693 |
||
314 | 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 |
|
3136 | 700 |
\end{ttbox} |
3096 | 701 |
\caption{The theory of arithmetic} \label{ctt_arith} |
104 | 702 |
\end{figure} |
703 |
||
704 |
||
705 |
\section{A theory of arithmetic} |
|
314 | 706 |
\thydx{Arith} is a theory of elementary arithmetic. It proves the |
104 | 707 |
properties of addition, multiplication, subtraction, division, and |
708 |
remainder, culminating in the theorem |
|
709 |
\[ a \bmod b + (a/b)\times b = a. \] |
|
3096 | 710 |
Figure~\ref{ctt_arith} presents the definitions and some of the key |
314 | 711 |
theorems, including commutative, distributive, and associative laws. |
104 | 712 |
|
111 | 713 |
The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod' |
714 |
and~\verb'div' stand for sum, difference, absolute difference, product, |
|
104 | 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 |
|
5151 | 719 |
the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$. |
104 | 720 |
|
111 | 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$. |
|
104 | 724 |
|
111 | 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$. |
|
104 | 727 |
|
728 |
||
729 |
||
730 |
\section{The examples directory} |
|
9695 | 731 |
This directory contains examples and experimental proofs in CTT. |
314 | 732 |
\begin{ttdescription} |
733 |
\item[CTT/ex/typechk.ML] |
|
6170 | 734 |
contains simple examples of type-checking and type deduction. |
104 | 735 |
|
314 | 736 |
\item[CTT/ex/elim.ML] |
104 | 737 |
contains some examples from Martin-L\"of~\cite{martinlof84}, proved using |
738 |
{\tt pc_tac}. |
|
739 |
||
314 | 740 |
\item[CTT/ex/equal.ML] |
104 | 741 |
contains simple examples of rewriting. |
742 |
||
314 | 743 |
\item[CTT/ex/synth.ML] |
104 | 744 |
demonstrates the use of unknowns with some trivial examples of program |
745 |
synthesis. |
|
314 | 746 |
\end{ttdescription} |
104 | 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} |
|
5151 | 756 |
Goal "lam n. rec(n, 0, \%x y. x) : ?A"; |
104 | 757 |
{\out Level 0} |
284 | 758 |
{\out lam n. rec(n,0,\%x y. x) : ?A} |
759 |
{\out 1. lam n. rec(n,0,\%x y. x) : ?A} |
|
104 | 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 |
|
314 | 763 |
\tdx{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a |
104 | 764 |
product type of unknown domain and range. |
765 |
\begin{ttbox} |
|
766 |
by (resolve_tac [ProdI] 1); |
|
767 |
{\out Level 1} |
|
284 | 768 |
{\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)} |
104 | 769 |
{\out 1. ?A1 type} |
284 | 770 |
{\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)} |
104 | 771 |
\end{ttbox} |
284 | 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 |
|
314 | 775 |
with {\tt rec}, which can be found by $N$-elimination.% |
776 |
\index{*NE theorem} |
|
104 | 777 |
\begin{ttbox} |
778 |
by (eresolve_tac [NE] 2); |
|
779 |
{\out Level 2} |
|
284 | 780 |
{\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)} |
104 | 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} |
|
284 | 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. |
|
314 | 787 |
Subgoal~2 asks, what is the type of~0?\index{*NIO theorem} |
104 | 788 |
\begin{ttbox} |
789 |
by (resolve_tac [NI0] 2); |
|
790 |
{\out Level 3} |
|
284 | 791 |
{\out lam n. rec(n,0,\%x y. x) : N --> N} |
104 | 792 |
{\out 1. N type} |
793 |
{\out 2. !!n x y. [| x : N; y : N |] ==> x : N} |
|
794 |
\end{ttbox} |
|
284 | 795 |
The type~$\Var{A}$ is now fully determined. It is the product type |
314 | 796 |
$\prod@{x\in N}N$, which is shown as the function type $N\to N$ because |
284 | 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 |
|
314 | 799 |
assumption and the remaining subgoal falls by $N$-formation.% |
800 |
\index{*NF theorem} |
|
104 | 801 |
\begin{ttbox} |
802 |
by (assume_tac 2); |
|
803 |
{\out Level 4} |
|
284 | 804 |
{\out lam n. rec(n,0,\%x y. x) : N --> N} |
104 | 805 |
{\out 1. N type} |
284 | 806 |
\ttbreak |
104 | 807 |
by (resolve_tac [NF] 1); |
808 |
{\out Level 5} |
|
284 | 809 |
{\out lam n. rec(n,0,\%x y. x) : N --> N} |
104 | 810 |
{\out No subgoals!} |
811 |
\end{ttbox} |
|
812 |
Calling \ttindex{typechk_tac} can prove this theorem in one step. |
|
813 |
||
284 | 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} |
|
5151 | 818 |
Goal "lam n. rec(n, 0, \%x y. tt) : ?A"; |
284 | 819 |
\end{ttbox} |
820 |
||
821 |
||
104 | 822 |
|
823 |
\section{An example of logical reasoning} |
|
824 |
Logical reasoning in Type Theory involves proving a goal of the form |
|
314 | 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: |
|
104 | 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 |
\] |
|
314 | 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: |
|
104 | 836 |
\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \] |
837 |
Generalizing this from $\times$ to $\Sigma$, and making the typing |
|
314 | 838 |
conditions explicit, yields the rule we must derive: |
104 | 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 |
\] |
|
314 | 845 |
To begin, we bind the rule's premises --- returned by the~{\tt goal} |
846 |
command --- to the {\ML} variable~{\tt prems}. |
|
104 | 847 |
\begin{ttbox} |
5151 | 848 |
val prems = Goal |
104 | 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))} |
|
114 | 857 |
\ttbreak |
111 | 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} |
|
104 | 863 |
\end{ttbox} |
314 | 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} |
|
104 | 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} |
|
284 | 883 |
The subgoal has two new parameters, $x$ and~$y$. In the main goal, |
314 | 884 |
$\Var{a}$ has been instantiated with a \cdx{split} term. The |
284 | 885 |
assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and |
314 | 886 |
creating the parameter~$xa$. This inference also inserts~\cdx{when} |
887 |
into the main goal.\index{*PlusE theorem} |
|
104 | 888 |
\begin{ttbox} |
889 |
by (eresolve_tac [PlusE] 1); |
|
890 |
{\out Level 2} |
|
284 | 891 |
{\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))} |
104 | 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))} |
|
114 | 896 |
\ttbreak |
104 | 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 |
|
314 | 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} |
|
104 | 906 |
\begin{ttbox} |
907 |
by (resolve_tac [PlusI_inl] 1); |
|
908 |
{\out Level 3} |
|
284 | 909 |
{\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))} |
104 | 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} |
|
114 | 913 |
\ttbreak |
104 | 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} |
|
314 | 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} |
|
104 | 923 |
\begin{ttbox} |
924 |
by (resolve_tac [SumI] 1); |
|
925 |
{\out Level 4} |
|
284 | 926 |
{\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))} |
104 | 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} |
|
284 | 940 |
{\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))} |
104 | 941 |
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
284 | 942 |
\ttbreak |
104 | 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))} |
|
284 | 948 |
\ttbreak |
104 | 949 |
by (assume_tac 1); |
950 |
{\out Level 6} |
|
284 | 951 |
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))} |
104 | 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} |
|
314 | 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. |
|
104 | 961 |
\begin{ttbox} |
962 |
by (typechk_tac prems); |
|
963 |
{\out Level 7} |
|
284 | 964 |
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))} |
104 | 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} |
|
314 | 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. |
|
104 | 973 |
\begin{ttbox} |
974 |
by (pc_tac prems 1); |
|
975 |
{\out Level 8} |
|
284 | 976 |
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))} |
104 | 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)). \] |
|
314 | 987 |
Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$. |
284 | 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$. |
|
104 | 998 |
\begin{ttbox} |
5151 | 999 |
val prems = Goal |
284 | 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 |
|
104 | 1005 |
{\out Level 0} |
284 | 1006 |
{\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->} |
1007 |
{\out (PROD x:A. PROD y:B(x). C(<x,y>))} |
|
104 | 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>))} |
|
114 | 1010 |
\ttbreak |
111 | 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} |
|
104 | 1015 |
\end{ttbox} |
284 | 1016 |
This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic |
314 | 1017 |
repeatedly applies $\Pi$-introduction and proves the rather |
284 | 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. |
|
104 | 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>))} |
|
284 | 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>)} |
|
104 | 1033 |
\end{ttbox} |
284 | 1034 |
Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$. |
314 | 1035 |
\index{*ProdE theorem} |
104 | 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>))} |
|
284 | 1041 |
{\out 1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)} |
104 | 1042 |
\end{ttbox} |
314 | 1043 |
Finally, we verify that the argument's type is suitable for the function |
1044 |
application. This is straightforward using introduction rules. |
|
104 | 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 |
|
333 | 1068 |
Theory. The following definitions work: |
104 | 1069 |
\begin{eqnarray*} |
1070 |
f & \equiv & {\tt fst} \circ h \\ |
|
1071 |
g & \equiv & {\tt snd} \circ h |
|
1072 |
\end{eqnarray*} |
|
314 | 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 |
|
6170 | 1076 |
(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can |
314 | 1077 |
prove the theorem in nine steps. |
104 | 1078 |
\begin{ttbox} |
5151 | 1079 |
val prems = Goal |
284 | 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, f`x))"; |
|
104 | 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))} |
|
111 | 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} |
|
104 | 1095 |
\end{ttbox} |
1096 |
First, \ttindex{intr_tac} applies introduction rules and performs routine |
|
6170 | 1097 |
type-checking. This instantiates~$\Var{a}$ to a construction involving |
314 | 1098 |
a $\lambda$-abstraction and an ordered pair. The pair's components are |
1099 |
themselves $\lambda$-abstractions and there is a subgoal for each. |
|
104 | 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))} |
|
114 | 1106 |
\ttbreak |
284 | 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)} |
|
114 | 1110 |
\ttbreak |
284 | 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)} |
|
104 | 1114 |
\end{ttbox} |
1115 |
Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some |
|
284 | 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. |
|
314 | 1120 |
\index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS} |
104 | 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))} |
|
114 | 1127 |
\ttbreak |
284 | 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)} |
|
104 | 1132 |
\end{ttbox} |
314 | 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. |
|
104 | 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))} |
|
284 | 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)} |
|
104 | 1145 |
\end{ttbox} |
314 | 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 |
|
284 | 1148 |
by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$: |
104 | 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))} |
|
114 | 1155 |
\ttbreak |
284 | 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)} |
|
114 | 1159 |
\ttbreak |
284 | 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)} |
|
104 | 1163 |
\end{ttbox} |
314 | 1164 |
The derived rule \tdx{subst_eqtyparg} lets us simplify a type's |
104 | 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))} |
|
114 | 1172 |
\ttbreak |
284 | 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)} |
|
114 | 1176 |
\ttbreak |
284 | 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) |] ==>} |
|
104 | 1180 |
{\out C(x,z) type} |
114 | 1181 |
\ttbreak |
284 | 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))} |
|
104 | 1185 |
\end{ttbox} |
284 | 1186 |
Subgoal~1 requires simply $\beta$-contraction, which is the rule |
314 | 1187 |
\tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal |
284 | 1188 |
receives the contracted result. |
104 | 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))} |
|
114 | 1195 |
\ttbreak |
284 | 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)} |
|
114 | 1199 |
\ttbreak |
284 | 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)} |
|
114 | 1204 |
\ttbreak |
284 | 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) |] ==>} |
|
104 | 1208 |
{\out C(x,z) type} |
114 | 1209 |
\ttbreak |
284 | 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))} |
|
104 | 1213 |
\end{ttbox} |
6170 | 1214 |
Routine type-checking goals proliferate in Constructive Type Theory, but |
104 | 1215 |
\ttindex{typechk_tac} quickly solves them. Note the inclusion of |
314 | 1216 |
\tdx{SumE_fst} along with the premises. |
104 | 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))} |
|
284 | 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))} |
|
104 | 1227 |
\end{ttbox} |
314 | 1228 |
We are finally ready to compose {\tt snd} with~$h$. |
1229 |
\index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS} |
|
104 | 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))} |
|
284 | 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} |
|
104 | 1240 |
\end{ttbox} |
1241 |
The proof object has reached its final form. We call \ttindex{typechk_tac} |
|
6170 | 1242 |
to finish the type-checking. |
104 | 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} |
|
314 | 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|)} |