summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/CTT.tex

changeset 9695 | ec7d7f877712 |

parent 7159 | b009afd1ace5 |

child 12679 | 8ed660138f83 |

equal
deleted
inserted
replaced

9694:13f3aaf12be2 | 9695:ec7d7f877712 |
---|---|

38 \end{array} |
38 \end{array} |

39 \] |
39 \] |

40 Assumptions can use all the judgement forms, for instance to express that |
40 Assumptions can use all the judgement forms, for instance to express that |

41 $B$ is a family of types over~$A$: |
41 $B$ is a family of types over~$A$: |

42 \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \] |
42 \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \] |

43 To justify the {\CTT} formulation it is probably best to appeal directly |
43 To justify the CTT formulation it is probably best to appeal directly to the |

44 to the semantic explanations of the rules~\cite{martinlof84}, rather than |
44 semantic explanations of the rules~\cite{martinlof84}, rather than to the |

45 to the rules themselves. The order of assumptions no longer matters, |
45 rules themselves. The order of assumptions no longer matters, unlike in |

46 unlike in standard Type Theory. Contexts, which are typical of many modern |
46 standard Type Theory. Contexts, which are typical of many modern type |

47 type theories, are difficult to represent in Isabelle. In particular, it |
47 theories, are difficult to represent in Isabelle. In particular, it is |

48 is difficult to enforce that all the variables in a context are distinct. |
48 difficult to enforce that all the variables in a context are distinct. |

49 \index{assumptions!in {\CTT}} |
49 \index{assumptions!in CTT} |

50 |
50 |

51 The theory does not use polymorphism. Terms in {\CTT} have type~\tydx{i}, the |
51 The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the |

52 type of individuals. Types in {\CTT} have type~\tydx{t}. |
52 type of individuals. Types in CTT have type~\tydx{t}. |

53 |
53 |

54 \begin{figure} \tabcolsep=1em %wider spacing in tables |
54 \begin{figure} \tabcolsep=1em %wider spacing in tables |

55 \begin{center} |
55 \begin{center} |

56 \begin{tabular}{rrr} |
56 \begin{tabular}{rrr} |

57 \it name & \it meta-type & \it description \\ |
57 \it name & \it meta-type & \it description \\ |

79 \cdx{contr} & $i\to i$ & eliminator\\[2ex] |
79 \cdx{contr} & $i\to i$ & eliminator\\[2ex] |

80 \cdx{T} & $t$ & singleton type\\ |
80 \cdx{T} & $t$ & singleton type\\ |

81 \cdx{tt} & $i$ & constructor |
81 \cdx{tt} & $i$ & constructor |

82 \end{tabular} |
82 \end{tabular} |

83 \end{center} |
83 \end{center} |

84 \caption{The constants of {\CTT}} \label{ctt-constants} |
84 \caption{The constants of CTT} \label{ctt-constants} |

85 \end{figure} |
85 \end{figure} |

86 |
86 |

87 |
87 |

88 {\CTT} supports all of Type Theory apart from list types, well-ordering |
88 CTT supports all of Type Theory apart from list types, well-ordering types, |

89 types, and universes. Universes could be introduced {\em\`a la Tarski}, |
89 and universes. Universes could be introduced {\em\`a la Tarski}, adding new |

90 adding new constants as names for types. The formulation {\em\`a la |
90 constants as names for types. The formulation {\em\`a la Russell}, where |

91 Russell}, where types denote themselves, is only possible if we identify |
91 types denote themselves, is only possible if we identify the meta-types~{\tt |

92 the meta-types~{\tt i} and~{\tt t}. Most published formulations of |
92 i} and~{\tt t}. Most published formulations of well-ordering types have |

93 well-ordering types have difficulties involving extensionality of |
93 difficulties involving extensionality of functions; I suggest that you use |

94 functions; I suggest that you use some other method for defining recursive |
94 some other method for defining recursive types. List types are easy to |

95 types. List types are easy to introduce by declaring new rules. |
95 introduce by declaring new rules. |

96 |
96 |

97 {\CTT} uses the 1982 version of Type Theory, with extensional equality. |
97 CTT uses the 1982 version of Type Theory, with extensional equality. The |

98 The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are |
98 computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable. |

99 interchangeable. Its rewriting tactics prove theorems of the form $a=b\in |
99 Its rewriting tactics prove theorems of the form $a=b\in A$. It could be |

100 A$. It could be modified to have intensional equality, but rewriting |
100 modified to have intensional equality, but rewriting tactics would have to |

101 tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the |
101 prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might |

102 computation rules might require a separate simplifier. |
102 require a separate simplifier. |

103 |
103 |

104 |
104 |

105 \begin{figure} \tabcolsep=1em %wider spacing in tables |
105 \begin{figure} \tabcolsep=1em %wider spacing in tables |

106 \index{lambda abs@$\lambda$-abstractions!in \CTT} |
106 \index{lambda abs@$\lambda$-abstractions!in CTT} |

107 \begin{center} |
107 \begin{center} |

108 \begin{tabular}{llrrr} |
108 \begin{tabular}{llrrr} |

109 \it symbol &\it name &\it meta-type & \it priority & \it description \\ |
109 \it symbol &\it name &\it meta-type & \it priority & \it description \\ |

110 \sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction |
110 \sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction |

111 \end{tabular} |
111 \end{tabular} |

112 \end{center} |
112 \end{center} |

113 \subcaption{Binders} |
113 \subcaption{Binders} |

114 |
114 |

115 \begin{center} |
115 \begin{center} |

116 \index{*"` symbol}\index{function applications!in \CTT} |
116 \index{*"` symbol}\index{function applications!in CTT} |

117 \index{*"+ symbol} |
117 \index{*"+ symbol} |

118 \begin{tabular}{rrrr} |
118 \begin{tabular}{rrrr} |

119 \it symbol & \it meta-type & \it priority & \it description \\ |
119 \it symbol & \it meta-type & \it priority & \it description \\ |

120 \tt ` & $[i,i]\to i$ & Left 55 & function application\\ |
120 \tt ` & $[i,i]\to i$ & Left 55 & function application\\ |

121 \tt + & $[t,t]\to t$ & Right 30 & sum of two types |
121 \tt + & $[t,t]\to t$ & Right 30 & sum of two types |

158 & | & "< " term " , " term " >" |
158 & | & "< " term " , " term " >" |

159 \end{array} |
159 \end{array} |

160 \] |
160 \] |

161 \end{center} |
161 \end{center} |

162 \subcaption{Grammar} |
162 \subcaption{Grammar} |

163 \caption{Syntax of {\CTT}} \label{ctt-syntax} |
163 \caption{Syntax of CTT} \label{ctt-syntax} |

164 \end{figure} |
164 \end{figure} |

165 |
165 |

166 %%%%\section{Generic Packages} typedsimp.ML???????????????? |
166 %%%%\section{Generic Packages} typedsimp.ML???????????????? |

167 |
167 |

168 |
168 |

169 \section{Syntax} |
169 \section{Syntax} |

170 The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include |
170 The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include |

171 the function application operator (sometimes called `apply'), and the |
171 the function application operator (sometimes called `apply'), and the 2-place |

172 2-place type operators. Note that meta-level abstraction and application, |
172 type operators. Note that meta-level abstraction and application, $\lambda |

173 $\lambda x.b$ and $f(a)$, differ from object-level abstraction and |
173 x.b$ and $f(a)$, differ from object-level abstraction and application, |

174 application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT} |
174 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an |

175 function~$f$ is simply an individual as far as Isabelle is concerned: its |
175 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say |

176 Isabelle type is~$i$, not say $i\To i$. |
176 $i\To i$. |

177 |
177 |

178 The notation for~{\CTT} (Fig.\ts\ref{ctt-syntax}) is based on that of |
178 The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om |

179 Nordstr\"om et al.~\cite{nordstrom90}. The empty type is called $F$ and |
179 et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element |

180 the one-element type is $T$; other finite types are built as $T+T+T$, etc. |
180 type is $T$; other finite types are built as $T+T+T$, etc. |

181 |
181 |

182 \index{*SUM symbol}\index{*PROD symbol} |
182 \index{*SUM symbol}\index{*PROD symbol} |

183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and |
183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and |

184 products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt |
184 products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt |

185 Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt |
185 Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt |

385 |
385 |

386 \tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type |
386 \tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type |

387 |] ==> snd(p) : B(fst(p)) |
387 |] ==> snd(p) : B(fst(p)) |

388 \end{ttbox} |
388 \end{ttbox} |

389 |
389 |

390 \caption{Derived rules for {\CTT}} \label{ctt-derived} |
390 \caption{Derived rules for CTT} \label{ctt-derived} |

391 \end{figure} |
391 \end{figure} |

392 |
392 |

393 |
393 |

394 \section{Rules of inference} |
394 \section{Rules of inference} |

395 The rules obey the following naming conventions. Type formation rules have |
395 The rules obey the following naming conventions. Type formation rules have |

468 |
468 |

469 |
469 |

470 \section{Rule lists} |
470 \section{Rule lists} |

471 The Type Theory tactics provide rewriting, type inference, and logical |
471 The Type Theory tactics provide rewriting, type inference, and logical |

472 reasoning. Many proof procedures work by repeatedly resolving certain Type |
472 reasoning. Many proof procedures work by repeatedly resolving certain Type |

473 Theory rules against a proof state. {\CTT} defines lists --- each with |
473 Theory rules against a proof state. CTT defines lists --- each with |

474 type |
474 type |

475 \hbox{\tt thm list} --- of related rules. |
475 \hbox{\tt thm list} --- of related rules. |

476 \begin{ttdescription} |
476 \begin{ttdescription} |

477 \item[\ttindexbold{form_rls}] |
477 \item[\ttindexbold{form_rls}] |

478 contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$, |
478 contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$, |

512 test_assume_tac : int -> tactic |
512 test_assume_tac : int -> tactic |

513 typechk_tac : thm list -> tactic |
513 typechk_tac : thm list -> tactic |

514 equal_tac : thm list -> tactic |
514 equal_tac : thm list -> tactic |

515 intr_tac : thm list -> tactic |
515 intr_tac : thm list -> tactic |

516 \end{ttbox} |
516 \end{ttbox} |

517 Blind application of {\CTT} rules seldom leads to a proof. The elimination |
517 Blind application of CTT rules seldom leads to a proof. The elimination |

518 rules, especially, create subgoals containing new unknowns. These subgoals |
518 rules, especially, create subgoals containing new unknowns. These subgoals |

519 unify with anything, creating a huge search space. The standard tactic |
519 unify with anything, creating a huge search space. The standard tactic |

520 \ttindex{filt_resolve_tac} |
520 \ttindex{filt_resolve_tac} |

521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% |
521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% |

522 {\S\ref{filt_resolve_tac}}) |
522 {\S\ref{filt_resolve_tac}}) |

523 % |
523 % |

524 fails for goals that are too flexible; so does the {\CTT} tactic {\tt |
524 fails for goals that are too flexible; so does the CTT tactic {\tt |

525 test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they |
525 test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they |

526 achieve a simple kind of subgoal reordering: the less flexible subgoals are |
526 achieve a simple kind of subgoal reordering: the less flexible subgoals are |

527 attempted first. Do some single step proofs, or study the examples below, |
527 attempted first. Do some single step proofs, or study the examples below, |

528 to see why this is necessary. |
528 to see why this is necessary. |

529 \begin{ttdescription} |
529 \begin{ttdescription} |

561 \end{ttbox} |
561 \end{ttbox} |

562 Object-level simplification is accomplished through proof, using the {\tt |
562 Object-level simplification is accomplished through proof, using the {\tt |

563 CTT} equality rules and the built-in rewriting functor |
563 CTT} equality rules and the built-in rewriting functor |

564 {\tt TSimpFun}.% |
564 {\tt TSimpFun}.% |

565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt |
565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt |

566 TSimpFun} is only useful for {\CTT} and similar logics with type |
566 TSimpFun} is only useful for CTT and similar logics with type inference |

567 inference rules. At present it is undocumented.} |
567 rules. At present it is undocumented.} |

568 % |
568 % |

569 The rewrites include the computation rules and other equations. The long |
569 The rewrites include the computation rules and other equations. The long |

570 versions of the other rules permit rewriting of subterms and subtypes. |
570 versions of the other rules permit rewriting of subterms and subtypes. |

571 Also used are transitivity and the extra judgement form \cdx{Reduce}. |
571 Also used are transitivity and the extra judgement form \cdx{Reduce}. |

572 Meta-level simplification handles only definitional equality. |
572 Meta-level simplification handles only definitional equality. |

581 the assumptions. |
581 the assumptions. |

582 \end{ttdescription} |
582 \end{ttdescription} |

583 |
583 |

584 |
584 |

585 \section{Tactics for logical reasoning} |
585 \section{Tactics for logical reasoning} |

586 Interpreting propositions as types lets {\CTT} express statements of |
586 Interpreting propositions as types lets CTT express statements of |

587 intuitionistic logic. However, Constructive Type Theory is not just |
587 intuitionistic logic. However, Constructive Type Theory is not just another |

588 another syntax for first-order logic. There are fundamental differences. |
588 syntax for first-order logic. There are fundamental differences. |

589 |
589 |

590 \index{assumptions!in {\CTT}} |
590 \index{assumptions!in CTT} |

591 Can assumptions be deleted after use? Not every occurrence of a type |
591 Can assumptions be deleted after use? Not every occurrence of a type |

592 represents a proposition, and Type Theory assumptions declare variables. |
592 represents a proposition, and Type Theory assumptions declare variables. |

593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$ |
593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$ |

594 creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$ |
594 creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$ |

595 can be deleted safely. In Type Theory, $+$-elimination with the assumption |
595 can be deleted safely. In Type Theory, $+$-elimination with the assumption |

596 $z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in |
596 $z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in |

597 B$ (for arbitrary $x$ and $y$). Deleting $z\in A+B$ when other assumptions |
597 B$ (for arbitrary $x$ and $y$). Deleting $z\in A+B$ when other assumptions |

598 refer to $z$ may render the subgoal unprovable: arguably, |
598 refer to $z$ may render the subgoal unprovable: arguably, |

599 meaningless. |
599 meaningless. |

600 |
600 |

601 Isabelle provides several tactics for predicate calculus reasoning in \CTT: |
601 Isabelle provides several tactics for predicate calculus reasoning in CTT: |

602 \begin{ttbox} |
602 \begin{ttbox} |

603 mp_tac : int -> tactic |
603 mp_tac : int -> tactic |

604 add_mp_tac : int -> tactic |
604 add_mp_tac : int -> tactic |

605 safestep_tac : thm list -> int -> tactic |
605 safestep_tac : thm list -> int -> tactic |

606 safe_tac : thm list -> int -> tactic |
606 safe_tac : thm list -> int -> tactic |

726 such that $0\leq x \leq a$ and $x\bmod b = 0$. |
726 such that $0\leq x \leq a$ and $x\bmod b = 0$. |

727 |
727 |

728 |
728 |

729 |
729 |

730 \section{The examples directory} |
730 \section{The examples directory} |

731 This directory contains examples and experimental proofs in {\CTT}. |
731 This directory contains examples and experimental proofs in CTT. |

732 \begin{ttdescription} |
732 \begin{ttdescription} |

733 \item[CTT/ex/typechk.ML] |
733 \item[CTT/ex/typechk.ML] |

734 contains simple examples of type-checking and type deduction. |
734 contains simple examples of type-checking and type deduction. |

735 |
735 |

736 \item[CTT/ex/elim.ML] |
736 \item[CTT/ex/elim.ML] |