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