diff -r 30bd42401ab2 -r d8205bb279a7 doc-src/Logics/CTT.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Logics/CTT.tex Wed Nov 10 05:00:57 1993 +0100 @@ -0,0 +1,1110 @@ +%% $Id$ +\chapter{Constructive Type Theory} +Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can +be viewed at many different levels. It is a formal system that embodies +the principles of intuitionistic mathematics; it embodies the +interpretation of propositions as types; it is a vehicle for deriving +programs from proofs. The logic is complex and many authors have attempted +to simplify it. Thompson~\cite{thompson91} is a readable and thorough +account of the theory. + +Isabelle's original formulation of Type Theory was a kind of sequent +calculus, following Martin-L\"of~\cite{martinlof84}. It included rules for +building the context, namely variable bindings with their types. A typical +judgement was +\[ a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \; + [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ] +\] +This sequent calculus was not satisfactory because assumptions like +`suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$' +could not be formalized. + +The directory~\ttindexbold{CTT} implements Constructive Type Theory, using +natural deduction. The judgement above is expressed using $\Forall$ and +$\Imp$: +\[ \begin{array}{r@{}l} + \Forall x@1\ldots x@n. & + \List{x@1\in A@1; + x@2\in A@2(x@1); \cdots \; + x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\ + & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) + \end{array} +\] +Assumptions can use all the judgement forms, for instance to express that +$B$ is a family of types over~$A$: +\[ \Forall x . x\in A \Imp B(x)\;{\rm type} \] +To justify the {\CTT} formulation it is probably best to appeal directly +to the semantic explanations of the rules~\cite{martinlof84}, rather than +to the rules themselves. The order of assumptions no longer matters, +unlike in standard Type Theory. Contexts, which are typical of many modern +type theories, are difficult to represent in Isabelle. In particular, it +is difficult to enforce that all the variables in a context are distinct. + +The theory has the {\ML} identifier \ttindexbold{CTT.thy}. It does not +use polymorphism. Terms in {\CTT} have type~$i$, the type of individuals. +Types in {\CTT} have type~$t$. + +{\CTT} supports all of Type Theory apart from list types, well ordering +types, and universes. Universes could be introduced {\em\`a la Tarski}, +adding new constants as names for types. The formulation {\em\`a la +Russell}, where types denote themselves, is only possible if we identify +the meta-types~$i$ and~$o$. Most published formulations of well ordering +types have difficulties involving extensionality of functions; I suggest +that you use some other method for defining recursive types. List types +are easy to introduce by declaring new rules. + +{\CTT} uses the 1982 version of Type Theory, with extensional equality. +The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are +interchangeable. Its rewriting tactics prove theorems of the form $a=b\in +A$. It could be modified to have intensional equality, but rewriting +tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the +computation rules might require a second simplifier. + + +\begin{figure} \tabcolsep=1em %wider spacing in tables +\begin{center} +\begin{tabular}{rrr} + \it symbol & \it meta-type & \it description \\ + \idx{Type} & $t \to prop$ & judgement form \\ + \idx{Eqtype} & $[t,t]\to prop$ & judgement form\\ + \idx{Elem} & $[i, t]\to prop$ & judgement form\\ + \idx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\ + \idx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex] + + \idx{N} & $t$ & natural numbers type\\ + \idx{0} & $i$ & constructor\\ + \idx{succ} & $i\to i$ & constructor\\ + \idx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex] + \idx{Prod} & $[t,i\to t]\to t$ & general product type\\ + \idx{lambda} & $(i\to i)\to i$ & constructor\\[2ex] + \idx{Sum} & $[t, i\to t]\to t$ & general sum type\\ + \idx{pair} & $[i,i]\to i$ & constructor\\ + \idx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\ + \idx{fst} snd & $i\to i$ & projections\\[2ex] + \idx{inl} inr & $i\to i$ & constructors for $+$\\ + \idx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex] + \idx{Eq} & $[t,i,i]\to t$ & equality type\\ + \idx{eq} & $i$ & constructor\\[2ex] + \idx{F} & $t$ & empty type\\ + \idx{contr} & $i\to i$ & eliminator\\[2ex] + \idx{T} & $t$ & singleton type\\ + \idx{tt} & $i$ & constructor +\end{tabular} +\end{center} +\caption{The constants of {\CTT}} \label{ctt-constants} +\end{figure} + + +\begin{figure} \tabcolsep=1em %wider spacing in tables +\begin{center} +\begin{tabular}{llrrr} + \it symbol &\it name &\it meta-type & \it precedence & \it description \\ + \idx{lam} & \idx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction +\end{tabular} +\end{center} +\subcaption{Binders} + +\begin{center} +\indexbold{*"`} +\indexbold{*"+} +\begin{tabular}{rrrr} + \it symbol & \it meta-type & \it precedence & \it description \\ + \tt ` & $[i,i]\to i$ & Left 55 & function application\\ + \tt + & $[t,t]\to t$ & Right 30 & sum of two types +\end{tabular} +\end{center} +\subcaption{Infixes} + +\indexbold{*"*} +\indexbold{*"-"-">} +\begin{center} \tt\frenchspacing +\begin{tabular}{rrr} + \it external & \it internal & \it standard notation \\ + \idx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) & + \rm product $\prod@{x\in A}B[x]$ \\ + \idx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) & + \rm sum $\sum@{x\in A}B[x]$ \\ + $A$ --> $B$ & Prod($A$, $\lambda x.B$) & + \rm function space $A\to B$ \\ + $A$ * $B$ & Sum($A$, $\lambda x.B$) & + \rm binary product $A\times B$ +\end{tabular} +\end{center} +\subcaption{Translations} + +\indexbold{*"=} +\begin{center} +\dquotes +\[ \begin{array}{rcl} +prop & = & type " type" \\ + & | & type " = " type \\ + & | & term " : " type \\ + & | & term " = " term " : " type +\\[2ex] +type & = & \hbox{expression of type~$t$} \\ + & | & "PROD~" id " : " type " . " type \\ + & | & "SUM~~" id " : " type " . " type +\\[2ex] +term & = & \hbox{expression of type~$i$} \\ + & | & "lam " id~id^* " . " term \\ + & | & "< " term " , " term " >" +\end{array} +\] +\end{center} +\subcaption{Grammar} +\caption{Syntax of {\CTT}} \label{ctt-syntax} +\end{figure} + +%%%%\section{Generic Packages} typedsimp.ML???????????????? + + +\section{Syntax} +The constants are shown in Figure~\ref{ctt-constants}. The infixes include +the function application operator (sometimes called `apply'), and the +2-place type operators. Note that meta-level abstraction and application, +$\lambda x.b$ and $f(a)$, differ from object-level abstraction and +application, \hbox{\tt lam $x$.$b$} and $b{\tt`}a$. A {\CTT} +function~$f$ is simply an individual as far as Isabelle is concerned: its +Isabelle type is~$i$, not say $i\To i$. + +\indexbold{*F}\indexbold{*T}\indexbold{*SUM}\indexbold{*PROD} +The empty type is called $F$ and the one-element type is $T$; other finite +sets are built as $T+T+T$, etc. The notation for~{\CTT} +(Figure~\ref{ctt-syntax}) is based on that of Nordstr\"om et +al.~\cite{nordstrom90}. We can write +\begin{ttbox} +SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, %y. Prod(A, %x. C(x,y))) +\end{ttbox} +The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate +general sums and products over a constant family.\footnote{Unlike normal +infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are +no constants~{\tt op~*} and~\hbox{\tt op~-->}.} Isabelle accepts these +abbreviations in parsing and uses them whenever possible for printing. + + +\begin{figure} +\begin{ttbox} +\idx{refl_type} A type ==> A = A +\idx{refl_elem} a : A ==> a = a : A + +\idx{sym_type} A = B ==> B = A +\idx{sym_elem} a = b : A ==> b = a : A + +\idx{trans_type} [| A = B; B = C |] ==> A = C +\idx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A + +\idx{equal_types} [| a : A; A = B |] ==> a : B +\idx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B + +\idx{subst_type} [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type +\idx{subst_typeL} [| a = c : A; !!z. z:A ==> B(z) = D(z) + |] ==> B(a) = D(c) + +\idx{subst_elem} [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a) +\idx{subst_elemL} [| a = c : A; !!z. z:A ==> b(z) = d(z) : B(z) + |] ==> b(a) = d(c) : B(a) + +\idx{refl_red} Reduce(a,a) +\idx{red_if_equal} a = b : A ==> Reduce(a,b) +\idx{trans_red} [| a = b : A; Reduce(b,c) |] ==> a = c : A +\end{ttbox} +\caption{General equality rules} \label{ctt-equality} +\end{figure} + + +\begin{figure} +\begin{ttbox} +\idx{NF} N type + +\idx{NI0} 0 : N +\idx{NI_succ} a : N ==> succ(a) : N +\idx{NI_succL} a = b : N ==> succ(a) = succ(b) : N + +\idx{NE} [| p: N; a: C(0); + !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) + |] ==> rec(p, a, %u v.b(u,v)) : C(p) + +\idx{NEL} [| p = q : N; a = c : C(0); + !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u)) + |] ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p) + +\idx{NC0} [| a: C(0); + !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) + |] ==> rec(0, a, %u v.b(u,v)) = a : C(0) + +\idx{NC_succ} [| p: N; a: C(0); + !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) + |] ==> rec(succ(p), a, %u v.b(u,v)) = + b(p, rec(p, a, %u v.b(u,v))) : C(succ(p)) + +\idx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F +\end{ttbox} +\caption{Rules for type~$N$} \label{ctt-N} +\end{figure} + + +\begin{figure} +\begin{ttbox} +\idx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type +\idx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==> + PROD x:A.B(x) = PROD x:C.D(x) + +\idx{ProdI} [| A type; !!x. x:A ==> b(x):B(x) + |] ==> lam x.b(x) : PROD x:A.B(x) +\idx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x) + |] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x) + +\idx{ProdE} [| p : PROD x:A.B(x); a : A |] ==> p`a : B(a) +\idx{ProdEL} [| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a) + +\idx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x) + |] ==> (lam x.b(x)) ` a = b(a) : B(a) + +\idx{ProdC2} p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x) +\end{ttbox} +\caption{Rules for the product type $\prod@{x\in A}B[x]$} \label{ctt-prod} +\end{figure} + + +\begin{figure} +\begin{ttbox} +\idx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type +\idx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x) + |] ==> SUM x:A.B(x) = SUM x:C.D(x) + +\idx{SumI} [| a : A; b : B(a) |] ==> : SUM x:A.B(x) +\idx{SumIL} [| a=c:A; b=d:B(a) |] ==> = : SUM x:A.B(x) + +\idx{SumE} [| p: SUM x:A.B(x); + !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() + |] ==> split(p, %x y.c(x,y)) : C(p) + +\idx{SumEL} [| p=q : SUM x:A.B(x); + !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C() + |] ==> split(p, %x y.c(x,y)) = split(q, %x y.d(x,y)) : C(p) + +\idx{SumC} [| a: A; b: B(a); + !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() + |] ==> split(, %x y.c(x,y)) = c(a,b) : C() + +\idx{fst_def} fst(a) == split(a, %x y.x) +\idx{snd_def} snd(a) == split(a, %x y.y) +\end{ttbox} +\caption{Rules for the sum type $\sum@{x\in A}B[x]$} \label{ctt-sum} +\end{figure} + + +\begin{figure} +\begin{ttbox} +\idx{PlusF} [| A type; B type |] ==> A+B type +\idx{PlusFL} [| A = C; B = D |] ==> A+B = C+D + +\idx{PlusI_inl} [| a : A; B type |] ==> inl(a) : A+B +\idx{PlusI_inlL} [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B + +\idx{PlusI_inr} [| A type; b : B |] ==> inr(b) : A+B +\idx{PlusI_inrL} [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B + +\idx{PlusE} [| p: A+B; + !!x. x:A ==> c(x): C(inl(x)); + !!y. y:B ==> d(y): C(inr(y)) + |] ==> when(p, %x.c(x), %y.d(y)) : C(p) + +\idx{PlusEL} [| p = q : A+B; + !!x. x: A ==> c(x) = e(x) : C(inl(x)); + !!y. y: B ==> d(y) = f(y) : C(inr(y)) + |] ==> when(p, %x.c(x), %y.d(y)) = + when(q, %x.e(x), %y.f(y)) : C(p) + +\idx{PlusC_inl} [| a: A; + !!x. x:A ==> c(x): C(inl(x)); + !!y. y:B ==> d(y): C(inr(y)) + |] ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a)) + +\idx{PlusC_inr} [| b: B; + !!x. x:A ==> c(x): C(inl(x)); + !!y. y:B ==> d(y): C(inr(y)) + |] ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b)) +\end{ttbox} +\caption{Rules for the binary sum type $A+B$} \label{ctt-plus} +\end{figure} + + +\begin{figure} +\begin{ttbox} +\idx{EqF} [| A type; a : A; b : A |] ==> Eq(A,a,b) type +\idx{EqFL} [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d) +\idx{EqI} a = b : A ==> eq : Eq(A,a,b) +\idx{EqE} p : Eq(A,a,b) ==> a = b : A +\idx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b) +\end{ttbox} +\subcaption{The equality type $Eq(A,a,b)$} + +\begin{ttbox} +\idx{FF} F type +\idx{FE} [| p: F; C type |] ==> contr(p) : C +\idx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C +\end{ttbox} +\subcaption{The empty type $F$} + +\begin{ttbox} +\idx{TF} T type +\idx{TI} tt : T +\idx{TE} [| p : T; c : C(tt) |] ==> c : C(p) +\idx{TEL} [| p = q : T; c = d : C(tt) |] ==> c = d : C(p) +\idx{TC} p : T ==> p = tt : T) +\end{ttbox} +\subcaption{The unit type $T$} + +\caption{Rules for other {\CTT} types} \label{ctt-others} +\end{figure} + + + +\begin{figure} +\begin{ttbox} +\idx{replace_type} [| B = A; a : A |] ==> a : B +\idx{subst_eqtyparg} [| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c) + +\idx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) + |] ==> c(p`a): C(p`a) + +\idx{SumIL2} [| c=a : A; d=b : B(a) |] ==> = : Sum(A,B) + +\idx{SumE_fst} p : Sum(A,B) ==> fst(p) : A + +\idx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type + |] ==> snd(p) : B(fst(p)) +\end{ttbox} + +\caption{Derived rules for {\CTT}} \label{ctt-derived} +\end{figure} + + +\section{Rules of inference} +The rules obey the following naming conventions. Type formation rules have +the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@. +Elimination rules have the suffix~{\tt E}\@. Computation rules, which +describe the reduction of eliminators, have the suffix~{\tt C}\@. The +equality versions of the rules (which permit reductions on subterms) are +called {\em long} rules; their names have the suffix~{\tt L}\@. +Introduction and computation rules often are further suffixed with +constructor names. + +Figures~\ref{ctt-equality}--\ref{ctt-others} shows the rules. Those +for~$N$ include \ttindex{zero_ne_succ}, $0\not=n+1$: the fourth Peano axiom +cannot be derived without universes \cite[page 91]{martinlof84}. +Figure~\ref{ctt-sum} shows the rules for general sums, which include binary +products as a special case, with the projections \ttindex{fst} +and~\ttindex{snd}. + +The extra judgement \ttindex{Reduce} is used to implement rewriting. The +judgement ${\tt Reduce}(a,b)$ holds when $a=b:A$ holds. It also holds +when $a$ and $b$ are syntactically identical, even if they are ill-typed, +because rule \ttindex{refl_red} does not verify that $a$ belongs to $A$. These +rules do not give rise to new theorems about the standard judgements --- +note that the only rule that makes use of {\tt Reduce} is \ttindex{trans_red}, +whose first premise ensures that $a$ and $b$ (and thus $c$) are well-typed. + +Derived rules are shown in Figure~\ref{ctt-derived}. The rule +\ttindex{subst_prodE} is derived from \ttindex{prodE}, and is easier to +use in backwards proof. The rules \ttindex{SumE_fst} and +\ttindex{SumE_snd} express the typing of~\ttindex{fst} and~\ttindex{snd}; +together, they are roughly equivalent to~\ttindex{SumE} with the advantage +of creating no parameters. These rules are demonstrated in a proof of the +Axiom of Choice~(\S\ref{ctt-choice}). + +All the rules are given in $\eta$-expanded form. For instance, every +occurrence of $\lambda u\,v.b(u,v)$ could be abbreviated to~$b$ in the +rules for~$N$. This permits Isabelle to preserve bound variable names +during backward proof. Names of bound variables in the conclusion (here, +$u$ and~$v$) are matched with corresponding bound variables in the premises. + + +\section{Rule lists} +The Type Theory tactics provide rewriting, type inference, and logical +reasoning. Many proof procedures work by repeatedly resolving certain Type +Theory rules against a proof state. {\CTT} defines lists --- each with +type +\hbox{\tt thm list} --- of related rules. +\begin{description} +\item[\ttindexbold{form_rls}] +contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$, +$F$, and $T$. + +\item[\ttindexbold{formL_rls}] +contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$. (For +other types use \ttindex{refl_type}.) + +\item[\ttindexbold{intr_rls}] +contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and +$T$. + +\item[\ttindexbold{intrL_rls}] +contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$. (For +$T$ use \ttindex{refl_elem}.) + +\item[\ttindexbold{elim_rls}] +contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and +$F$. The rules for $Eq$ and $T$ are omitted because they involve no +eliminator. + +\item[\ttindexbold{elimL_rls}] +contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$. + +\item[\ttindexbold{comp_rls}] +contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$. +Those for $Eq$ and $T$ involve no eliminator. + +\item[\ttindexbold{basic_defs}] +contains the definitions of \ttindex{fst} and \ttindex{snd}. +\end{description} + + +\section{Tactics for subgoal reordering} +\begin{ttbox} +test_assume_tac : int -> tactic +typechk_tac : thm list -> tactic +equal_tac : thm list -> tactic +intr_tac : thm list -> tactic +\end{ttbox} +Blind application of {\CTT} rules seldom leads to a proof. The elimination +rules, especially, create subgoals containing new unknowns. These subgoals +unify with anything, causing an undirectional search. The standard tactic +\ttindex{filt_resolve_tac} (see the {\em Reference Manual}) can reject +overly flexible goals; so does the {\CTT} tactic {\tt test_assume_tac}. +Used with the tactical \ttindex{REPEAT_FIRST} they achieve a simple kind of +subgoal reordering: the less flexible subgoals are attempted first. Do +some single step proofs, or study the examples below, to see why this is +necessary. +\begin{description} +\item[\ttindexbold{test_assume_tac} $i$] +uses \ttindex{assume_tac} to solve the subgoal by assumption, but only if +subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown. +Otherwise, it fails. + +\item[\ttindexbold{typechk_tac} $thms$] +uses $thms$ with formation, introduction, and elimination rules to check +the typing of constructions. It is designed to solve goals of the form +$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible. Thus it +performs Hindley-Milner type inference. The tactic can also solve goals of +the form $A\;\rm type$. + +\item[\ttindexbold{equal_tac} $thms$] +uses $thms$ with the long introduction and elimination rules to solve goals +of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving +the long rules for defined constants such as the arithmetic operators. The +tactic can also perform type checking. + +\item[\ttindexbold{intr_tac} $thms$] +uses $thms$ with the introduction rules to break down a type. It is +designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$ +rigid. These typically arise when trying to prove a proposition~$A$, +expressed as a type. +\end{description} + + + +\section{Rewriting tactics} +\begin{ttbox} +rew_tac : thm list -> tactic +hyp_rew_tac : thm list -> tactic +\end{ttbox} +Object-level simplification is accomplished through proof, using the {\tt +CTT} equality rules and the built-in rewriting functor +\ttindex{TSimpFun}.\footnote{This should not be confused with {\tt +SimpFun}, which is the main rewriting functor; {\tt TSimpFun} is only +useful for {\CTT} and similar logics with type inference rules.} +The rewrites include the computation rules and other equations. The +long versions of the other rules permit rewriting of subterms and subtypes. +Also used are transitivity and the extra judgement form \ttindex{Reduce}. +Meta-level simplification handles only definitional equality. +\begin{description} +\item[\ttindexbold{rew_tac} $thms$] +applies $thms$ and the computation rules as left-to-right rewrites. It +solves the goal $a=b\in A$ by rewriting $a$ to $b$. If $b$ is an unknown +then it is assigned the rewritten form of~$a$. All subgoals are rewritten. + +\item[\ttindexbold{hyp_rew_tac} $thms$] +is like {\tt rew_tac}, but includes as rewrites any equations present in +the assumptions. +\end{description} + + +\section{Tactics for logical reasoning} +Interpreting propositions as types lets {\CTT} express statements of +intuitionistic logic. However, Constructive Type Theory is not just +another syntax for first-order logic. A key question: can assumptions be +deleted after use? Not every occurrence of a type represents a +proposition, and Type Theory assumptions declare variables. + +In first-order logic, $\disj$-elimination with the assumption $P\disj Q$ +creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$ +can be deleted. In Type Theory, $+$-elimination with the assumption $z\in +A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in B$ +(for arbitrary $x$ and $y$). Deleting $z\in A+B$ may render the subgoals +unprovable if other assumptions refer to $z$. Some people might argue that +such subgoals are not even meaningful. +\begin{ttbox} +mp_tac : int -> tactic +add_mp_tac : int -> tactic +safestep_tac : thm list -> int -> tactic +safe_tac : thm list -> int -> tactic +step_tac : thm list -> int -> tactic +pc_tac : thm list -> int -> tactic +\end{ttbox} +These are loosely based on the intuitionistic proof procedures +of~\ttindex{FOL}. For the reasons discussed above, a rule that is safe for +propositional reasoning may be unsafe for type checking; thus, some of the +``safe'' tactics are misnamed. +\begin{description} +\item[\ttindexbold{mp_tac} $i$] +searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and +$a\in A$, where~$A$ may be found by unification. It replaces +$f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter. The tactic +can produce multiple outcomes for each suitable pair of assumptions. In +short, {\tt mp_tac} performs Modus Ponens among the assumptions. + +\item[\ttindexbold{add_mp_tac} $i$] +is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. + +\item[\ttindexbold{safestep_tac} $thms$ $i$] +attacks subgoal~$i$ using formation rules and certain other `safe' rules +(\ttindex{FE}, \ttindex{ProdI}, \ttindex{SumE}, \ttindex{PlusE}), calling +{\tt mp_tac} when appropriate. It also uses~$thms$, +which are typically premises of the rule being derived. + +\item[\ttindexbold{safe_tac} $thms$ $i$] +tries to solve subgoal~$i$ by backtracking, using {\tt safestep_tac}. + +\item[\ttindexbold{step_tac} $thms$ $i$] +tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe +rules. It may produce multiple outcomes. + +\item[\ttindexbold{pc_tac} $thms$ $i$] +tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}. +\end{description} + + + +\begin{figure} +\begin{ttbox} +\idx{add_def} a#+b == rec(a, b, %u v.succ(v)) +\idx{diff_def} a-b == rec(b, a, %u v.rec(v, 0, %x y.x)) +\idx{absdiff_def} a|-|b == (a-b) #+ (b-a) +\idx{mult_def} a#*b == rec(a, 0, %u v. b #+ v) + +\idx{mod_def} a//b == rec(a, 0, + %u v. rec(succ(v) |-| b, 0, %x y.succ(v))) + +\idx{quo_def} a/b == rec(a, 0, + %u v. rec(succ(u) // b, succ(v), %x y.v)) +\end{ttbox} +\subcaption{Definitions of the operators} + +\begin{ttbox} +\idx{add_typing} [| a:N; b:N |] ==> a #+ b : N +\idx{addC0} b:N ==> 0 #+ b = b : N +\idx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N + +\idx{add_assoc} [| a:N; b:N; c:N |] ==> + (a #+ b) #+ c = a #+ (b #+ c) : N + +\idx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N + +\idx{mult_typing} [| a:N; b:N |] ==> a #* b : N +\idx{multC0} b:N ==> 0 #* b = 0 : N +\idx{multC_succ} [| a:N; b:N |] ==> succ(a) #* b = b #+ (a#*b) : N +\idx{mult_commute} [| a:N; b:N |] ==> a #* b = b #* a : N + +\idx{add_mult_dist} [| a:N; b:N; c:N |] ==> + (a #+ b) #* c = (a #* c) #+ (b #* c) : N + +\idx{mult_assoc} [| a:N; b:N; c:N |] ==> + (a #* b) #* c = a #* (b #* c) : N + +\idx{diff_typing} [| a:N; b:N |] ==> a - b : N +\idx{diffC0} a:N ==> a - 0 = a : N +\idx{diff_0_eq_0} b:N ==> 0 - b = 0 : N +\idx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N +\idx{diff_self_eq_0} a:N ==> a - a = 0 : N +\idx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N +\end{ttbox} +\subcaption{Some theorems of arithmetic} +\caption{The theory of arithmetic} \label{ctt-arith} +\end{figure} + + +\section{A theory of arithmetic} +{\CTT} contains a theory of elementary arithmetic. It proves the +properties of addition, multiplication, subtraction, division, and +remainder, culminating in the theorem +\[ a \bmod b + (a/b)\times b = a. \] +Figure~\ref{ctt-arith} presents the definitions and some of the key +theorems, including commutative, distributive, and associative laws. The +theory has the {\ML} identifier \ttindexbold{arith.thy}. All proofs are on +the file \ttindexbold{CTT/arith.ML}. + +The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'//' +and~\verb'/' stand for sum, difference, absolute difference, product, +remainder and quotient, respectively. Since Type Theory has only primitive +recursion, some of their definitions may be obscure. + +The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where +the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$. + +The remainder $a//b$ counts up to~$a$ in a cyclic fashion, using 0 as the +successor of~$b-1$. Absolute difference is used to test the equality +$succ(v)=b$. + +The quotient $a//b$ is computed by adding one for every number $x$ such +that $0\leq x \leq a$ and $x//b = 0$. + + + +\section{The examples directory} +This directory contains examples and experimental proofs in {\CTT}. +\begin{description} +\item[\ttindexbold{CTT/ex/typechk.ML}] +contains simple examples of type checking and type deduction. + +\item[\ttindexbold{CTT/ex/elim.ML}] +contains some examples from Martin-L\"of~\cite{martinlof84}, proved using +{\tt pc_tac}. + +\item[\ttindexbold{CTT/ex/equal.ML}] +contains simple examples of rewriting. + +\item[\ttindexbold{CTT/ex/synth.ML}] +demonstrates the use of unknowns with some trivial examples of program +synthesis. +\end{description} + + +\section{Example: type inference} +Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$ +is a term and $\Var{A}$ is an unknown standing for its type. The type, +initially +unknown, takes shape in the course of the proof. Our example is the +predecessor function on the natural numbers. +\begin{ttbox} +goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A"; +{\out Level 0} +{\out lam n. rec(n,0,%x y. x) : ?A} +{\out 1. lam n. rec(n,0,%x y. x) : ?A} +\end{ttbox} +Since the term is a Constructive Type Theory $\lambda$-abstraction (not to +be confused with a meta-level abstraction), we apply the rule +\ttindex{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a +product type of unknown domain and range. +\begin{ttbox} +by (resolve_tac [ProdI] 1); +{\out Level 1} +{\out lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)} +{\out 1. ?A1 type} +{\out 2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)} +\end{ttbox} +Subgoal~1 can be solved by instantiating~$\Var{A@1}$ to any type, but this +could invalidate subgoal~2. We therefore tackle the latter subgoal. It +asks the type of a term beginning with {\tt rec}, which can be found by +$N$-elimination.\index{*NE} +\begin{ttbox} +by (eresolve_tac [NE] 2); +{\out Level 2} +{\out lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)} +{\out 1. N type} +{\out 2. !!n. 0 : ?C2(n,0)} +{\out 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))} +\end{ttbox} +We now know~$\Var{A@1}$ is the type of natural numbers. However, let us +continue with subgoal~2. What is the type of~0?\index{*NIO} +\begin{ttbox} +by (resolve_tac [NI0] 2); +{\out Level 3} +{\out lam n. rec(n,0,%x y. x) : N --> N} +{\out 1. N type} +{\out 2. !!n x y. [| x : N; y : N |] ==> x : N} +\end{ttbox} +The type~$\Var{A}$ is now determined. It is $\prod@{n\in N}N$, which is +equivalent to $N\to N$. But we must prove all the subgoals to show that +the original term is validly typed. Subgoal~2 is provable by assumption +and the remaining subgoal falls by $N$-formation.\index{*NF} +\begin{ttbox} +by (assume_tac 2); +{\out Level 4} +{\out lam n. rec(n,0,%x y. x) : N --> N} +{\out 1. N type} +by (resolve_tac [NF] 1); +{\out Level 5} +{\out lam n. rec(n,0,%x y. x) : N --> N} +{\out No subgoals!} +\end{ttbox} +Calling \ttindex{typechk_tac} can prove this theorem in one step. + + +\section{An example of logical reasoning} +Logical reasoning in Type Theory involves proving a goal of the form +$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ is an +unknown standing +for its proof term: a value of type $A$. This term is initially unknown, as +with type inference, and takes shape during the proof. Our example +expresses, by propositions-as-types, a theorem about quantifiers in a +sorted logic: +\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))} + {\ex{x\in A}P(x)\disj Q(x)} +\] +It it related to a distributive law of Type Theory: +\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \] +Generalizing this from $\times$ to $\Sigma$, and making the typing +conditions explicit, yields +\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))} + {\hbox{$A$ type} & + \infer*{\hbox{$B(x)$ type}}{[x\in A]} & + \infer*{\hbox{$C(x)$ type}}{[x\in A]} & + p\in \sum@{x\in A} B(x)+C(x)} +\] +To derive this rule, we bind its premises --- returned by~\ttindex{goal} +--- to the {\ML} variable~{\tt prems}. +\begin{ttbox} +val prems = goal CTT.thy + "[| A type; \ttback +\ttback !!x. x:A ==> B(x) type; \ttback +\ttback !!x. x:A ==> C(x) type; \ttback +\ttback p: SUM x:A. B(x) + C(x) \ttback +\ttback |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))"; +{\out Level 0} +{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +One of the premises involves summation ($\Sigma$). Since it is a premise +rather than the assumption of a goal, it cannot be found by +\ttindex{eresolve_tac}. We could insert it by calling +\hbox{\tt \ttindex{cut_facts_tac} prems 1}. Instead, let us resolve the +$\Sigma$-elimination rule with the premises; this yields one result, which +we supply to \ttindex{resolve_tac}.\index{*SumE}\index{*RL} +\begin{ttbox} +by (resolve_tac (prems RL [SumE]) 1); +{\out Level 1} +{\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y.} +{\out [| x : A; y : B(x) + C(x) |] ==>} +{\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +The subgoal has two new parameters. In the main goal, $\Var{a}$ has been +instantiated with a \ttindex{split} term. The assumption $y\in B(x) + C(x)$ is +eliminated next, causing a case split and a new parameter. The main goal +now contains~\ttindex{when}. +\index{*PlusE} +\begin{ttbox} +by (eresolve_tac [PlusE] 1); +{\out Level 2} +{\out split(p,%x y. when(y,?c2(x,y),?d2(x,y)))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y xa.} +{\out [| x : A; xa : B(x) |] ==>} +{\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 2. !!x y ya.} +{\out [| x : A; ya : C(x) |] ==>} +{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +To complete the proof object for the main goal, we need to instantiate the +terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$. We attack subgoal~1 by +introduction of~$+$; since it assumes $xa\in B(x)$, we take the left +injection~(\ttindex{inl}). +\index{*PlusI_inl} +\begin{ttbox} +by (resolve_tac [PlusI_inl] 1); +{\out Level 3} +{\out split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y)))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)} +{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type} +{\out 3. !!x y ya.} +{\out [| x : A; ya : C(x) |] ==>} +{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +A new subgoal has appeared, to verify that $\sum@{x\in A}C(x)$ is a type. +Continuing with subgoal~1, we apply $\Sigma$-introduction. The main goal +now contains an ordered pair. +\index{*SumI} +\begin{ttbox} +by (resolve_tac [SumI] 1); +{\out Level 4} +{\out split(p,%x y. when(y,%xa. inl(),?d2(x,y)))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A} +{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))} +{\out 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type} +{\out 4. !!x y ya.} +{\out [| x : A; ya : C(x) |] ==>} +{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +The two new subgoals both hold by assumption. Observe how the unknowns +$\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state. +\begin{ttbox} +by (assume_tac 1); +{\out Level 5} +{\out split(p,%x y. when(y,%xa. inl(),?d2(x,y)))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)} +{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type} +{\out 3. !!x y ya.} +{\out [| x : A; ya : C(x) |] ==>} +{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +by (assume_tac 1); +{\out Level 6} +{\out split(p,%x y. when(y,%xa. inl(),?d2(x,y)))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type} +{\out 2. !!x y ya.} +{\out [| x : A; ya : C(x) |] ==>} +{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +Subgoal~1 is just type checking. It yields to \ttindex{typechk_tac}, +supplied with the current list of premises. +\begin{ttbox} +by (typechk_tac prems); +{\out Level 7} +{\out split(p,%x y. when(y,%xa. inl(),?d2(x,y)))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out 1. !!x y ya.} +{\out [| x : A; ya : C(x) |] ==>} +{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} +\end{ttbox} +The other case is similar. Let us prove it by \ttindex{pc_tac}, and note +the final proof object. +\begin{ttbox} +by (pc_tac prems 1); +{\out Level 8} +{\out split(p,%x y. when(y,%xa. inl(),%y. inr()))} +{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} +{\out No subgoals!} +\end{ttbox} +Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also +proves this theorem. + + +\section{Example: deriving a currying functional} +In simply-typed languages such as {\ML}, a currying functional has the type +\[ (A\times B \to C) \to (A\to (B\to C)). \] +Let us generalize this to~$\Sigma$ and~$\Pi$. The argument of the +functional is a function that maps $z:\Sigma(A,B)$ to~$C(z)$; the resulting +function maps $x\in A$ and $y\in B(x)$ to $C(\langle x,y\rangle)$. Here +$B$ is a family over~$A$, while $C$ is a family over $\Sigma(A,B)$. +\begin{ttbox} +val prems = goal CTT.thy + "[| A type; !!x. x:A ==> B(x) type; \ttback +\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \ttback +\ttback ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ttback +\ttback --> (PROD x:A . PROD y:B(x) . C())"; +{\out Level 0} +{\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C())} +{\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->} +{\out (PROD x:A. PROD y:B(x). C())} +\end{ttbox} +This is an opportunity to demonstrate \ttindex{intr_tac}. Here, the tactic +repeatedly applies $\Pi$-introduction, automatically proving the rather +tiresome typing conditions. Note that $\Var{a}$ becomes instantiated to +three nested $\lambda$-abstractions. +\begin{ttbox} +by (intr_tac prems); +{\out Level 1} +{\out lam x xa xb. ?b7(x,xa,xb)} +{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C())} +{\out 1. !!uu x y.} +{\out [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>} +{\out ?b7(uu,x,y) : C()} +\end{ttbox} +Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$uu$. +\index{*ProdE} +\begin{ttbox} +by (eresolve_tac [ProdE] 1); +{\out Level 2} +{\out lam x xa xb. x ` } +{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C())} +{\out 1. !!uu x y. [| x : A; y : B(x) |] ==> : SUM x:A. B(x)} +\end{ttbox} +Finally, we exhibit a suitable argument for the function application. This +is straightforward using introduction rules. +\index{*intr_tac} +\begin{ttbox} +by (intr_tac prems); +{\out Level 3} +{\out lam x xa xb. x ` } +{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C())} +{\out No subgoals!} +\end{ttbox} +Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can +also prove an example by Martin-L\"of, related to $\disj$-elimination +\cite[page~58]{martinlof84}. + + +\section{Example: proving the Axiom of Choice} \label{ctt-choice} +Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$, +which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$. +Interpreting propositions as types, this asserts that for all $x\in A$ +there exists $y\in B(x)$ such that $C(x,y)$. The Axiom of Choice asserts +that we can construct a function $f\in \prod@{x\in A}B(x)$ such that +$C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a +function $g\in \prod@{x\in A}C(x,f{\tt`}x)$. + +In principle, the Axiom of Choice is simple to derive in Constructive Type +Theory \cite[page~50]{martinlof84}. The following definitions work: +\begin{eqnarray*} + f & \equiv & {\tt fst} \circ h \\ + g & \equiv & {\tt snd} \circ h +\end{eqnarray*} +But a completely formal proof is hard to find. Many of the rules can be +applied in a multiplicity of ways, yielding a large number of higher-order +unifiers. The proof can get bogged down in the details. But with a +careful selection of derived rules (recall Figure~\ref{ctt-derived}) and +the type checking tactics, we can prove the theorem in nine steps. +\begin{ttbox} +val prems = goal CTT.thy + "[| A type; !!x. x:A ==> B(x) type; \ttback +\ttback !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ttback +\ttback |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ttback +\ttback --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; +{\out Level 0} +{\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +\end{ttbox} +First, \ttindex{intr_tac} applies introduction rules and performs routine +type checking. This instantiates~$\Var{a}$ to a construction involving +three $\lambda$-abstractions and an ordered pair. +\begin{ttbox} +by (intr_tac prems); +{\out Level 1} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b7(uu,x) : B(x)} +{\out 2. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)} +\end{ttbox} +Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some +$\Var{b@7}(uu,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof +object $\Var{b@8}(uu,x)$ to witness that the choice function's argument +and result lie in the relation~$C$. +\index{*ProdE}\index{*SumE_fst}\index{*RS} +\begin{ttbox} +by (eresolve_tac [ProdE RS SumE_fst] 1); +{\out Level 2} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x. x : A ==> x : A} +{\out 2. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)} +\end{ttbox} +Above, we have composed \ttindex{fst} with the function~$h$ (named~$uu$ in +the assumptions). Unification has deduced that the function must be +applied to $x\in A$. +\begin{ttbox} +by (assume_tac 1); +{\out Level 3} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)} +\end{ttbox} +Before we can compose \ttindex{snd} with~$h$, the arguments of $C$ must be +simplified. The derived rule \ttindex{replace_type} lets us replace a type +by any equivalent type: +\begin{ttbox} +by (resolve_tac [replace_type] 1); +{\out Level 4} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)} +{\out 2. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : ?A13(uu,x)} +\end{ttbox} +The derived rule \ttindex{subst_eqtyparg} lets us simplify a type's +argument (by currying, $C(x)$ is a unary type operator): +\begin{ttbox} +by (resolve_tac [subst_eqtyparg] 1); +{\out Level 5} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)} +{\out 2. !!uu x z.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;} +{\out z : ?A14(uu,x) |] ==>} +{\out C(x,z) type} +{\out 3. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : C(x,?c14(uu,x))} +\end{ttbox} +The rule \ttindex{ProdC} is simply $\beta$-reduction. The term +$\Var{c@{14}}(uu,x)$ receives the simplified form, $f{\tt`}x$. +\begin{ttbox} +by (resolve_tac [ProdC] 1); +{\out Level 6} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)} +{\out 2. !!uu x xa.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;} +{\out xa : ?A15(uu,x) |] ==>} +{\out fst(uu ` xa) : ?B15(uu,x,xa)} +{\out 3. !!uu x z.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;} +{\out z : ?B15(uu,x,x) |] ==>} +{\out C(x,z) type} +{\out 4. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : C(x,fst(uu ` x))} +\end{ttbox} +Routine type checking goals proliferate in Constructive Type Theory, but +\ttindex{typechk_tac} quickly solves them. Note the inclusion of +\ttindex{SumE_fst}. +\begin{ttbox} +by (typechk_tac (SumE_fst::prems)); +{\out Level 7} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x.} +{\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} +{\out ?b8(uu,x) : C(x,fst(uu ` x))} +\end{ttbox} +We are finally ready to compose \ttindex{snd} with~$h$. +\index{*ProdE}\index{*SumE_snd}\index{*RS} +\begin{ttbox} +by (eresolve_tac [ProdE RS SumE_snd] 1); +{\out Level 8} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out 1. !!uu x. x : A ==> x : A} +{\out 2. !!uu x. x : A ==> B(x) type} +{\out 3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type} +\end{ttbox} +The proof object has reached its final form. We call \ttindex{typechk_tac} +to finish the type checking. +\begin{ttbox} +by (typechk_tac prems); +{\out Level 9} +{\out lam x. } +{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} +{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} +{\out No subgoals!} +\end{ttbox}