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