|
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 |] ==> p`a : B(a) |
|
269 \tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a) |
|
270 |
|
271 \tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x) |
|
272 |] ==> (lam x. b(x)) ` a = b(a) : B(a) |
|
273 |
|
274 \tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x) |
|
275 \end{ttbox} |
|
276 \caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod} |
|
277 \end{figure} |
|
278 |
|
279 |
|
280 \begin{figure} |
|
281 \begin{ttbox} |
|
282 \tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type |
|
283 \tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x) |
|
284 |] ==> SUM x:A. B(x) = SUM x:C. D(x) |
|
285 |
|
286 \tdx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x) |
|
287 \tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x) |
|
288 |
|
289 \tdx{SumE} [| p: SUM x:A. B(x); |
|
290 !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |
|
291 |] ==> split(p, \%x y. c(x,y)) : C(p) |
|
292 |
|
293 \tdx{SumEL} [| p=q : SUM x:A. B(x); |
|
294 !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>) |
|
295 |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p) |
|
296 |
|
297 \tdx{SumC} [| a: A; b: B(a); |
|
298 !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |
|
299 |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>) |
|
300 |
|
301 \tdx{fst_def} fst(a) == split(a, \%x y. x) |
|
302 \tdx{snd_def} snd(a) == split(a, \%x y. y) |
|
303 \end{ttbox} |
|
304 \caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum} |
|
305 \end{figure} |
|
306 |
|
307 |
|
308 \begin{figure} |
|
309 \begin{ttbox} |
|
310 \tdx{PlusF} [| A type; B type |] ==> A+B type |
|
311 \tdx{PlusFL} [| A = C; B = D |] ==> A+B = C+D |
|
312 |
|
313 \tdx{PlusI_inl} [| a : A; B type |] ==> inl(a) : A+B |
|
314 \tdx{PlusI_inlL} [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B |
|
315 |
|
316 \tdx{PlusI_inr} [| A type; b : B |] ==> inr(b) : A+B |
|
317 \tdx{PlusI_inrL} [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B |
|
318 |
|
319 \tdx{PlusE} [| p: A+B; |
|
320 !!x. x:A ==> c(x): C(inl(x)); |
|
321 !!y. y:B ==> d(y): C(inr(y)) |
|
322 |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p) |
|
323 |
|
324 \tdx{PlusEL} [| p = q : A+B; |
|
325 !!x. x: A ==> c(x) = e(x) : C(inl(x)); |
|
326 !!y. y: B ==> d(y) = f(y) : C(inr(y)) |
|
327 |] ==> when(p, \%x. c(x), \%y. d(y)) = |
|
328 when(q, \%x. e(x), \%y. f(y)) : C(p) |
|
329 |
|
330 \tdx{PlusC_inl} [| a: A; |
|
331 !!x. x:A ==> c(x): C(inl(x)); |
|
332 !!y. y:B ==> d(y): C(inr(y)) |
|
333 |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a)) |
|
334 |
|
335 \tdx{PlusC_inr} [| b: B; |
|
336 !!x. x:A ==> c(x): C(inl(x)); |
|
337 !!y. y:B ==> d(y): C(inr(y)) |
|
338 |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b)) |
|
339 \end{ttbox} |
|
340 \caption{Rules for the binary sum type $A+B$} \label{ctt-plus} |
|
341 \end{figure} |
|
342 |
|
343 |
|
344 \begin{figure} |
|
345 \begin{ttbox} |
|
346 \tdx{FF} F type |
|
347 \tdx{FE} [| p: F; C type |] ==> contr(p) : C |
|
348 \tdx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C |
|
349 |
|
350 \tdx{TF} T type |
|
351 \tdx{TI} tt : T |
|
352 \tdx{TE} [| p : T; c : C(tt) |] ==> c : C(p) |
|
353 \tdx{TEL} [| p = q : T; c = d : C(tt) |] ==> c = d : C(p) |
|
354 \tdx{TC} p : T ==> p = tt : T) |
|
355 \end{ttbox} |
|
356 |
|
357 \caption{Rules for types $F$ and $T$} \label{ctt-ft} |
|
358 \end{figure} |
|
359 |
|
360 |
|
361 \begin{figure} |
|
362 \begin{ttbox} |
|
363 \tdx{EqF} [| A type; a : A; b : A |] ==> Eq(A,a,b) type |
|
364 \tdx{EqFL} [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d) |
|
365 \tdx{EqI} a = b : A ==> eq : Eq(A,a,b) |
|
366 \tdx{EqE} p : Eq(A,a,b) ==> a = b : A |
|
367 \tdx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b) |
|
368 \end{ttbox} |
|
369 \caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq} |
|
370 \end{figure} |
|
371 |
|
372 |
|
373 \begin{figure} |
|
374 \begin{ttbox} |
|
375 \tdx{replace_type} [| B = A; a : A |] ==> a : B |
|
376 \tdx{subst_eqtyparg} [| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c) |
|
377 |
|
378 \tdx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) |
|
379 |] ==> c(p`a): C(p`a) |
|
380 |
|
381 \tdx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B) |
|
382 |
|
383 \tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A |
|
384 |
|
385 \tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type |
|
386 |] ==> snd(p) : B(fst(p)) |
|
387 \end{ttbox} |
|
388 |
|
389 \caption{Derived rules for CTT} \label{ctt-derived} |
|
390 \end{figure} |
|
391 |
|
392 |
|
393 \section{Rules of inference} |
|
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, f`x))"; |
|
1087 {\out Level 0} |
|
1088 {\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
|
1089 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
|
1090 {\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
|
1091 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
|
1092 \ttbreak |
|
1093 {\out val prems = ["A type [A type]",} |
|
1094 {\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} |
|
1095 {\out "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type} |
|
1096 {\out [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]} |
|
1097 {\out : thm list} |
|
1098 \end{ttbox} |
|
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|)} |