393 The rules obey the following naming conventions. Type formation rules have |
393 The rules obey the following naming conventions. Type formation rules have |
394 the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@. |
394 the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@. |
395 Elimination rules have the suffix~{\tt E}\@. Computation rules, which |
395 Elimination rules have the suffix~{\tt E}\@. Computation rules, which |
396 describe the reduction of eliminators, have the suffix~{\tt C}\@. The |
396 describe the reduction of eliminators, have the suffix~{\tt C}\@. The |
397 equality versions of the rules (which permit reductions on subterms) are |
397 equality versions of the rules (which permit reductions on subterms) are |
398 called {\em long} rules; their names have the suffix~{\tt L}\@. |
398 called {\bf long} rules; their names have the suffix~{\tt L}\@. |
399 Introduction and computation rules often are further suffixed with |
399 Introduction and computation rules are often further suffixed with |
400 constructor names. |
400 constructor names. |
401 |
401 |
402 Figure~\ref{ctt-equality} presents the equality rules. Most of them are |
402 Figure~\ref{ctt-equality} presents the equality rules. Most of them are |
403 straightforward: reflexivity, symmetry, transitivity and substitution. The |
403 straightforward: reflexivity, symmetry, transitivity and substitution. The |
404 judgement \cdx{Reduce} does not belong to Type Theory proper; it has |
404 judgement \cdx{Reduce} does not belong to Type Theory proper; it has |
512 equal_tac : thm list -> tactic |
512 equal_tac : thm list -> tactic |
513 intr_tac : thm list -> tactic |
513 intr_tac : thm list -> tactic |
514 \end{ttbox} |
514 \end{ttbox} |
515 Blind application of {\CTT} rules seldom leads to a proof. The elimination |
515 Blind application of {\CTT} rules seldom leads to a proof. The elimination |
516 rules, especially, create subgoals containing new unknowns. These subgoals |
516 rules, especially, create subgoals containing new unknowns. These subgoals |
517 unify with anything, causing an undirectional search. The standard tactic |
517 unify with anything, creating a huge search space. The standard tactic |
518 \ttindex{filt_resolve_tac} |
518 \ttindex{filt_resolve_tac} |
519 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% |
519 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% |
520 {\S\ref{filt_resolve_tac}}) |
520 {\S\ref{filt_resolve_tac}}) |
521 % |
521 % |
522 can reject overly flexible goals; so does the {\CTT} tactic {\tt |
522 fails for goals that are too flexible; so does the {\CTT} tactic {\tt |
523 test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they |
523 test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they |
524 achieve a simple kind of subgoal reordering: the less flexible subgoals are |
524 achieve a simple kind of subgoal reordering: the less flexible subgoals are |
525 attempted first. Do some single step proofs, or study the examples below, |
525 attempted first. Do some single step proofs, or study the examples below, |
526 to see why this is necessary. |
526 to see why this is necessary. |
527 \begin{ttdescription} |
527 \begin{ttdescription} |
621 is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. It |
621 is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. It |
622 avoids information loss but obviously loops if repeated. |
622 avoids information loss but obviously loops if repeated. |
623 |
623 |
624 \item[\ttindexbold{safestep_tac} $thms$ $i$] |
624 \item[\ttindexbold{safestep_tac} $thms$ $i$] |
625 attacks subgoal~$i$ using formation rules and certain other `safe' rules |
625 attacks subgoal~$i$ using formation rules and certain other `safe' rules |
626 (tdx{FE}, tdx{ProdI}, tdx{SumE}, tdx{PlusE}), calling |
626 (\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling |
627 {\tt mp_tac} when appropriate. It also uses~$thms$, |
627 {\tt mp_tac} when appropriate. It also uses~$thms$, |
628 which are typically premises of the rule being derived. |
628 which are typically premises of the rule being derived. |
629 |
629 |
630 \item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by |
630 \item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by |
631 means of backtracking, using {\tt safestep_tac}. |
631 means of backtracking, using {\tt safestep_tac}. |
706 properties of addition, multiplication, subtraction, division, and |
706 properties of addition, multiplication, subtraction, division, and |
707 remainder, culminating in the theorem |
707 remainder, culminating in the theorem |
708 \[ a \bmod b + (a/b)\times b = a. \] |
708 \[ a \bmod b + (a/b)\times b = a. \] |
709 Figure~\ref{ctt-arith} presents the definitions and some of the key |
709 Figure~\ref{ctt-arith} presents the definitions and some of the key |
710 theorems, including commutative, distributive, and associative laws. |
710 theorems, including commutative, distributive, and associative laws. |
711 All proofs are on the file {\tt CTT/arith.ML}. |
|
712 |
711 |
713 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod' |
712 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod' |
714 and~\verb'div' stand for sum, difference, absolute difference, product, |
713 and~\verb'div' stand for sum, difference, absolute difference, product, |
715 remainder and quotient, respectively. Since Type Theory has only primitive |
714 remainder and quotient, respectively. Since Type Theory has only primitive |
716 recursion, some of their definitions may be obscure. |
715 recursion, some of their definitions may be obscure. |
1063 that we can construct a function $f\in \prod@{x\in A}B(x)$ such that |
1062 that we can construct a function $f\in \prod@{x\in A}B(x)$ such that |
1064 $C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a |
1063 $C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a |
1065 function $g\in \prod@{x\in A}C(x,f{\tt`}x)$. |
1064 function $g\in \prod@{x\in A}C(x,f{\tt`}x)$. |
1066 |
1065 |
1067 In principle, the Axiom of Choice is simple to derive in Constructive Type |
1066 In principle, the Axiom of Choice is simple to derive in Constructive Type |
1068 Theory \cite[page~50]{martinlof84}. The following definitions work: |
1067 Theory. The following definitions work: |
1069 \begin{eqnarray*} |
1068 \begin{eqnarray*} |
1070 f & \equiv & {\tt fst} \circ h \\ |
1069 f & \equiv & {\tt fst} \circ h \\ |
1071 g & \equiv & {\tt snd} \circ h |
1070 g & \equiv & {\tt snd} \circ h |
1072 \end{eqnarray*} |
1071 \end{eqnarray*} |
1073 But a completely formal proof is hard to find. The rules can be applied in |
1072 But a completely formal proof is hard to find. The rules can be applied in |