doc-src/Logics/CTT.tex
 changeset 6170 9a59cf8ae9b5 parent 6072 5583261db33d child 7159 b009afd1ace5
equal inserted replaced
6169:f3f2560fbed9 6170:9a59cf8ae9b5
   539
   539
   540 \item[\ttindexbold{equal_tac} $thms$]
   540 \item[\ttindexbold{equal_tac} $thms$]
   541 uses $thms$ with the long introduction and elimination rules to solve goals
   541 uses $thms$ with the long introduction and elimination rules to solve goals
   542 of the form $a=b\in A$, where $a$ is rigid.  It is intended for deriving
   542 of the form $a=b\in A$, where $a$ is rigid.  It is intended for deriving
   543 the long rules for defined constants such as the arithmetic operators.  The
   543 the long rules for defined constants such as the arithmetic operators.  The
   544 tactic can also perform type checking.
   544 tactic can also perform type-checking.
   545
   545
   546 \item[\ttindexbold{intr_tac} $thms$]
   546 \item[\ttindexbold{intr_tac} $thms$]
   547 uses $thms$ with the introduction rules to break down a type.  It is
   547 uses $thms$ with the introduction rules to break down a type.  It is
   548 designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
   548 designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
   549 rigid.  These typically arise when trying to prove a proposition~$A$,
   549 rigid.  These typically arise when trying to prove a proposition~$A$,
   605 step_tac     : thm list -> int -> tactic
   605 step_tac     : thm list -> int -> tactic
   606 pc_tac       : thm list -> int -> tactic
   606 pc_tac       : thm list -> int -> tactic
   607 \end{ttbox}
   607 \end{ttbox}
   608 These are loosely based on the intuitionistic proof procedures
   608 These are loosely based on the intuitionistic proof procedures
   609 of~\thydx{FOL}.  For the reasons discussed above, a rule that is safe for
   609 of~\thydx{FOL}.  For the reasons discussed above, a rule that is safe for
   610 propositional reasoning may be unsafe for type checking; thus, some of the
   610 propositional reasoning may be unsafe for type-checking; thus, some of the
   611 safe' tactics are misnamed.
   611 safe' tactics are misnamed.
   612 \begin{ttdescription}
   612 \begin{ttdescription}
   613 \item[\ttindexbold{mp_tac} $i$]
   613 \item[\ttindexbold{mp_tac} $i$]
   614 searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
   614 searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
   615 $a\in A$, where~$A$ may be found by unification.  It replaces
   615 $a\in A$, where~$A$ may be found by unification.  It replaces
   727
   727
   728 \section{The examples directory}
   728 \section{The examples directory}
   729 This directory contains examples and experimental proofs in {\CTT}.
   729 This directory contains examples and experimental proofs in {\CTT}.
   730 \begin{ttdescription}
   730 \begin{ttdescription}
   731 \item[CTT/ex/typechk.ML]
   731 \item[CTT/ex/typechk.ML]
   732 contains simple examples of type checking and type deduction.
   732 contains simple examples of type-checking and type deduction.
   733
   733
   734 \item[CTT/ex/elim.ML]
   734 \item[CTT/ex/elim.ML]
   735 contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
   735 contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
   736 {\tt pc_tac}.
   736 {\tt pc_tac}.
   737
   737
  1069     g & \equiv & {\tt snd} \circ h
  1069     g & \equiv & {\tt snd} \circ h
  1070 \end{eqnarray*}
  1070 \end{eqnarray*}
  1071 But a completely formal proof is hard to find.  The rules can be applied in
  1071 But a completely formal proof is hard to find.  The rules can be applied in
  1072 countless ways, yielding many higher-order unifiers.  The proof can get
  1072 countless ways, yielding many higher-order unifiers.  The proof can get
  1073 bogged down in the details.  But with a careful selection of derived rules
  1073 bogged down in the details.  But with a careful selection of derived rules
  1074 (recall Fig.\ts\ref{ctt-derived}) and the type checking tactics, we can
  1074 (recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
  1075 prove the theorem in nine steps.
  1075 prove the theorem in nine steps.
  1076 \begin{ttbox}
  1076 \begin{ttbox}
  1077 val prems = Goal
  1077 val prems = Goal
  1078     "[| A type;  !!x. x:A ==> B(x) type;                    \ttback
  1078     "[| A type;  !!x. x:A ==> B(x) type;                    \ttback
  1079 \ttback       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type            \ttback
  1079 \ttback       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type            \ttback
  1090 {\out              "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
  1090 {\out              "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
  1091 {\out               [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
  1091 {\out               [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
  1092 {\out             : thm list}
  1092 {\out             : thm list}
  1093 \end{ttbox}
  1093 \end{ttbox}
  1094 First, \ttindex{intr_tac} applies introduction rules and performs routine
  1094 First, \ttindex{intr_tac} applies introduction rules and performs routine
  1095 type checking.  This instantiates~$\Var{a}$ to a construction involving
  1095 type-checking.  This instantiates~$\Var{a}$ to a construction involving
  1096 a $\lambda$-abstraction and an ordered pair.  The pair's components are
  1096 a $\lambda$-abstraction and an ordered pair.  The pair's components are
  1097 themselves $\lambda$-abstractions and there is a subgoal for each.
  1097 themselves $\lambda$-abstractions and there is a subgoal for each.
  1098 \begin{ttbox}
  1098 \begin{ttbox}
  1099 by (intr_tac prems);
  1099 by (intr_tac prems);
  1100 {\out Level 1}
  1100 {\out Level 1}
  1207 \ttbreak
  1207 \ttbreak
  1208 {\out  4. !!h x.}
  1208 {\out  4. !!h x.}
  1209 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1209 {\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
  1210 {\out        ?b8(h,x) : C(x,fst(h  x))}
  1210 {\out        ?b8(h,x) : C(x,fst(h  x))}
  1211 \end{ttbox}
  1211 \end{ttbox}
  1212 Routine type checking goals proliferate in Constructive Type Theory, but
  1212 Routine type-checking goals proliferate in Constructive Type Theory, but
  1213 \ttindex{typechk_tac} quickly solves them.  Note the inclusion of
  1213 \ttindex{typechk_tac} quickly solves them.  Note the inclusion of
  1214 \tdx{SumE_fst} along with the premises.
  1214 \tdx{SumE_fst} along with the premises.
  1215 \begin{ttbox}
  1215 \begin{ttbox}
  1216 by (typechk_tac (SumE_fst::prems));
  1216 by (typechk_tac (SumE_fst::prems));
  1217 {\out Level 7}
  1217 {\out Level 7}
  1235 {\out  1. !!h x. x : A ==> x : A}
  1235 {\out  1. !!h x. x : A ==> x : A}
  1236 {\out  2. !!h x. x : A ==> B(x) type}
  1236 {\out  2. !!h x. x : A ==> B(x) type}
  1237 {\out  3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
  1237 {\out  3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
  1238 \end{ttbox}
  1238 \end{ttbox}
  1239 The proof object has reached its final form.  We call \ttindex{typechk_tac}
  1239 The proof object has reached its final form.  We call \ttindex{typechk_tac}
  1240 to finish the type checking.
  1240 to finish the type-checking.
  1241 \begin{ttbox}
  1241 \begin{ttbox}
  1242 by (typechk_tac prems);
  1242 by (typechk_tac prems);
  1243 {\out Level 9}
  1243 {\out Level 9}
  1244 {\out lam x. <lam xa. fst(x  xa),lam xa. snd(x  xa)>}
  1244 {\out lam x. <lam xa. fst(x  xa),lam xa. snd(x  xa)>}
  1245 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
  1245 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}