157 |
157 |
158 %%%%\section{Generic Packages} typedsimp.ML???????????????? |
158 %%%%\section{Generic Packages} typedsimp.ML???????????????? |
159 |
159 |
160 |
160 |
161 \section{Syntax} |
161 \section{Syntax} |
162 The constants are shown in Figure~\ref{ctt-constants}. The infixes include |
162 The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include |
163 the function application operator (sometimes called `apply'), and the |
163 the function application operator (sometimes called `apply'), and the |
164 2-place type operators. Note that meta-level abstraction and application, |
164 2-place type operators. Note that meta-level abstraction and application, |
165 $\lambda x.b$ and $f(a)$, differ from object-level abstraction and |
165 $\lambda x.b$ and $f(a)$, differ from object-level abstraction and |
166 application, \hbox{\tt lam $x$.$b$} and $b{\tt`}a$. A {\CTT} |
166 application, \hbox{\tt lam $x$.$b$} and $b{\tt`}a$. A {\CTT} |
167 function~$f$ is simply an individual as far as Isabelle is concerned: its |
167 function~$f$ is simply an individual as far as Isabelle is concerned: its |
168 Isabelle type is~$i$, not say $i\To i$. |
168 Isabelle type is~$i$, not say $i\To i$. |
169 |
169 |
170 \indexbold{*F}\indexbold{*T}\indexbold{*SUM}\indexbold{*PROD} |
170 \indexbold{*F}\indexbold{*T}\indexbold{*SUM}\indexbold{*PROD} |
171 The empty type is called $F$ and the one-element type is $T$; other finite |
171 The empty type is called $F$ and the one-element type is $T$; other finite |
172 sets are built as $T+T+T$, etc. The notation for~{\CTT} |
172 sets are built as $T+T+T$, etc. The notation for~{\CTT} |
173 (Figure~\ref{ctt-syntax}) is based on that of Nordstr\"om et |
173 (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om et |
174 al.~\cite{nordstrom90}. We can write |
174 al.~\cite{nordstrom90}. We can write |
175 \begin{ttbox} |
175 \begin{ttbox} |
176 SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, %y. Prod(A, %x. C(x,y))) |
176 SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y))) |
177 \end{ttbox} |
177 \end{ttbox} |
178 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate |
178 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate |
179 general sums and products over a constant family.\footnote{Unlike normal |
179 general sums and products over a constant family.\footnote{Unlike normal |
180 infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are |
180 infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are |
181 no constants~{\tt op~*} and~\hbox{\tt op~-->}.} Isabelle accepts these |
181 no constants~{\tt op~*} and~\hbox{\tt op~-->}.} Isabelle accepts these |
220 \idx{NI_succ} a : N ==> succ(a) : N |
220 \idx{NI_succ} a : N ==> succ(a) : N |
221 \idx{NI_succL} a = b : N ==> succ(a) = succ(b) : N |
221 \idx{NI_succL} a = b : N ==> succ(a) = succ(b) : N |
222 |
222 |
223 \idx{NE} [| p: N; a: C(0); |
223 \idx{NE} [| p: N; a: C(0); |
224 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
224 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
225 |] ==> rec(p, a, %u v.b(u,v)) : C(p) |
225 |] ==> rec(p, a, \%u v.b(u,v)) : C(p) |
226 |
226 |
227 \idx{NEL} [| p = q : N; a = c : C(0); |
227 \idx{NEL} [| p = q : N; a = c : C(0); |
228 !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u)) |
228 !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u)) |
229 |] ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p) |
229 |] ==> rec(p, a, \%u v.b(u,v)) = rec(q,c,d) : C(p) |
230 |
230 |
231 \idx{NC0} [| a: C(0); |
231 \idx{NC0} [| a: C(0); |
232 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
232 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
233 |] ==> rec(0, a, %u v.b(u,v)) = a : C(0) |
233 |] ==> rec(0, a, \%u v.b(u,v)) = a : C(0) |
234 |
234 |
235 \idx{NC_succ} [| p: N; a: C(0); |
235 \idx{NC_succ} [| p: N; a: C(0); |
236 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
236 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |
237 |] ==> rec(succ(p), a, %u v.b(u,v)) = |
237 |] ==> rec(succ(p), a, \%u v.b(u,v)) = |
238 b(p, rec(p, a, %u v.b(u,v))) : C(succ(p)) |
238 b(p, rec(p, a, \%u v.b(u,v))) : C(succ(p)) |
239 |
239 |
240 \idx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F |
240 \idx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F |
241 \end{ttbox} |
241 \end{ttbox} |
242 \caption{Rules for type~$N$} \label{ctt-N} |
242 \caption{Rules for type~$N$} \label{ctt-N} |
243 \end{figure} |
243 \end{figure} |
686 is a term and $\Var{A}$ is an unknown standing for its type. The type, |
686 is a term and $\Var{A}$ is an unknown standing for its type. The type, |
687 initially |
687 initially |
688 unknown, takes shape in the course of the proof. Our example is the |
688 unknown, takes shape in the course of the proof. Our example is the |
689 predecessor function on the natural numbers. |
689 predecessor function on the natural numbers. |
690 \begin{ttbox} |
690 \begin{ttbox} |
691 goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A"; |
691 goal CTT.thy "lam n. rec(n, 0, \%x y.x) : ?A"; |
692 {\out Level 0} |
692 {\out Level 0} |
693 {\out lam n. rec(n,0,%x y. x) : ?A} |
693 {\out lam n. rec(n,0,\%x y. x) : ?A} |
694 {\out 1. lam n. rec(n,0,%x y. x) : ?A} |
694 {\out 1. lam n. rec(n,0,\%x y. x) : ?A} |
695 \end{ttbox} |
695 \end{ttbox} |
696 Since the term is a Constructive Type Theory $\lambda$-abstraction (not to |
696 Since the term is a Constructive Type Theory $\lambda$-abstraction (not to |
697 be confused with a meta-level abstraction), we apply the rule |
697 be confused with a meta-level abstraction), we apply the rule |
698 \ttindex{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a |
698 \ttindex{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a |
699 product type of unknown domain and range. |
699 product type of unknown domain and range. |
700 \begin{ttbox} |
700 \begin{ttbox} |
701 by (resolve_tac [ProdI] 1); |
701 by (resolve_tac [ProdI] 1); |
702 {\out Level 1} |
702 {\out Level 1} |
703 {\out lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)} |
703 {\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)} |
704 {\out 1. ?A1 type} |
704 {\out 1. ?A1 type} |
705 {\out 2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)} |
705 {\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)} |
706 \end{ttbox} |
706 \end{ttbox} |
707 Subgoal~1 can be solved by instantiating~$\Var{A@1}$ to any type, but this |
707 Subgoal~1 is too flexible. It can be solved by instantiating~$\Var{A@1}$ |
708 could invalidate subgoal~2. We therefore tackle the latter subgoal. It |
708 to any type, but most instantiations will invalidate subgoal~2. We |
709 asks the type of a term beginning with {\tt rec}, which can be found by |
709 therefore tackle the latter subgoal. It asks the type of a term beginning |
710 $N$-elimination.\index{*NE} |
710 with {\tt rec}, which can be found by $N$-elimination.\index{*NE} |
711 \begin{ttbox} |
711 \begin{ttbox} |
712 by (eresolve_tac [NE] 2); |
712 by (eresolve_tac [NE] 2); |
713 {\out Level 2} |
713 {\out Level 2} |
714 {\out lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)} |
714 {\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)} |
715 {\out 1. N type} |
715 {\out 1. N type} |
716 {\out 2. !!n. 0 : ?C2(n,0)} |
716 {\out 2. !!n. 0 : ?C2(n,0)} |
717 {\out 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))} |
717 {\out 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))} |
718 \end{ttbox} |
718 \end{ttbox} |
719 We now know~$\Var{A@1}$ is the type of natural numbers. However, let us |
719 Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of |
720 continue with subgoal~2. What is the type of~0?\index{*NIO} |
720 natural numbers. However, let us continue proving nontrivial subgoals. |
|
721 Subgoal~2 asks, what is the type of~0?\index{*NIO} |
721 \begin{ttbox} |
722 \begin{ttbox} |
722 by (resolve_tac [NI0] 2); |
723 by (resolve_tac [NI0] 2); |
723 {\out Level 3} |
724 {\out Level 3} |
724 {\out lam n. rec(n,0,%x y. x) : N --> N} |
725 {\out lam n. rec(n,0,\%x y. x) : N --> N} |
725 {\out 1. N type} |
726 {\out 1. N type} |
726 {\out 2. !!n x y. [| x : N; y : N |] ==> x : N} |
727 {\out 2. !!n x y. [| x : N; y : N |] ==> x : N} |
727 \end{ttbox} |
728 \end{ttbox} |
728 The type~$\Var{A}$ is now determined. It is $\prod@{n\in N}N$, which is |
729 The type~$\Var{A}$ is now fully determined. It is the product type |
729 equivalent to $N\to N$. But we must prove all the subgoals to show that |
730 $\prod@{x\in N}N$, which is equivalent to function type $N\to N$ because |
730 the original term is validly typed. Subgoal~2 is provable by assumption |
731 there is no dependence on~$x$. But we must prove all the subgoals to show |
731 and the remaining subgoal falls by $N$-formation.\index{*NF} |
732 that the original term is validly typed. Subgoal~2 is provable by |
|
733 assumption and the remaining subgoal falls by $N$-formation.\index{*NF} |
732 \begin{ttbox} |
734 \begin{ttbox} |
733 by (assume_tac 2); |
735 by (assume_tac 2); |
734 {\out Level 4} |
736 {\out Level 4} |
735 {\out lam n. rec(n,0,%x y. x) : N --> N} |
737 {\out lam n. rec(n,0,\%x y. x) : N --> N} |
736 {\out 1. N type} |
738 {\out 1. N type} |
|
739 \ttbreak |
737 by (resolve_tac [NF] 1); |
740 by (resolve_tac [NF] 1); |
738 {\out Level 5} |
741 {\out Level 5} |
739 {\out lam n. rec(n,0,%x y. x) : N --> N} |
742 {\out lam n. rec(n,0,\%x y. x) : N --> N} |
740 {\out No subgoals!} |
743 {\out No subgoals!} |
741 \end{ttbox} |
744 \end{ttbox} |
742 Calling \ttindex{typechk_tac} can prove this theorem in one step. |
745 Calling \ttindex{typechk_tac} can prove this theorem in one step. |
|
746 |
|
747 Even if the original term is ill-typed, one can infer a type for it, but |
|
748 unprovable subgoals will be left. As an exercise, try to prove the |
|
749 following invalid goal: |
|
750 \begin{ttbox} |
|
751 goal CTT.thy "lam n. rec(n, 0, \%x y.tt) : ?A"; |
|
752 \end{ttbox} |
|
753 |
743 |
754 |
744 |
755 |
745 \section{An example of logical reasoning} |
756 \section{An example of logical reasoning} |
746 Logical reasoning in Type Theory involves proving a goal of the form |
757 Logical reasoning in Type Theory involves proving a goal of the form |
747 $\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ is an |
758 $\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ is an |
784 \end{ttbox} |
795 \end{ttbox} |
785 One of the premises involves summation ($\Sigma$). Since it is a premise |
796 One of the premises involves summation ($\Sigma$). Since it is a premise |
786 rather than the assumption of a goal, it cannot be found by |
797 rather than the assumption of a goal, it cannot be found by |
787 \ttindex{eresolve_tac}. We could insert it by calling |
798 \ttindex{eresolve_tac}. We could insert it by calling |
788 \hbox{\tt \ttindex{cut_facts_tac} prems 1}. Instead, let us resolve the |
799 \hbox{\tt \ttindex{cut_facts_tac} prems 1}. Instead, let us resolve the |
789 $\Sigma$-elimination rule with the premises; this yields one result, which |
800 $\Sigma$-elimination rule with the premises using~{\tt RL}; this forward |
790 we supply to \ttindex{resolve_tac}.\index{*SumE}\index{*RL} |
801 inference yields one result, which we supply to |
|
802 \ttindex{resolve_tac}.\index{*SumE}\index{*RL} |
791 \begin{ttbox} |
803 \begin{ttbox} |
792 by (resolve_tac (prems RL [SumE]) 1); |
804 by (resolve_tac (prems RL [SumE]) 1); |
793 {\out Level 1} |
805 {\out Level 1} |
794 {\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
806 {\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
795 {\out 1. !!x y.} |
807 {\out 1. !!x y.} |
796 {\out [| x : A; y : B(x) + C(x) |] ==>} |
808 {\out [| x : A; y : B(x) + C(x) |] ==>} |
797 {\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
809 {\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
798 \end{ttbox} |
810 \end{ttbox} |
799 The subgoal has two new parameters. In the main goal, $\Var{a}$ has been |
811 The subgoal has two new parameters, $x$ and~$y$. In the main goal, |
800 instantiated with a \ttindex{split} term. The assumption $y\in B(x) + C(x)$ is |
812 $\Var{a}$ has been instantiated with a \ttindex{split} term. The |
801 eliminated next, causing a case split and a new parameter. The main goal |
813 assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and |
802 now contains~\ttindex{when}. |
814 a further parameter,~$xa$. It also inserts~\ttindex{when} into the main goal. |
803 \index{*PlusE} |
815 \index{*PlusE} |
804 \begin{ttbox} |
816 \begin{ttbox} |
805 by (eresolve_tac [PlusE] 1); |
817 by (eresolve_tac [PlusE] 1); |
806 {\out Level 2} |
818 {\out Level 2} |
807 {\out split(p,%x y. when(y,?c2(x,y),?d2(x,y)))} |
819 {\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))} |
808 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
820 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
809 {\out 1. !!x y xa.} |
821 {\out 1. !!x y xa.} |
810 {\out [| x : A; xa : B(x) |] ==>} |
822 {\out [| x : A; xa : B(x) |] ==>} |
811 {\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
823 {\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
812 \ttbreak |
824 \ttbreak |
871 Subgoal~1 is just type checking. It yields to \ttindex{typechk_tac}, |
885 Subgoal~1 is just type checking. It yields to \ttindex{typechk_tac}, |
872 supplied with the current list of premises. |
886 supplied with the current list of premises. |
873 \begin{ttbox} |
887 \begin{ttbox} |
874 by (typechk_tac prems); |
888 by (typechk_tac prems); |
875 {\out Level 7} |
889 {\out Level 7} |
876 {\out split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))} |
890 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))} |
877 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
891 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
878 {\out 1. !!x y ya.} |
892 {\out 1. !!x y ya.} |
879 {\out [| x : A; ya : C(x) |] ==>} |
893 {\out [| x : A; ya : C(x) |] ==>} |
880 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
894 {\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
881 \end{ttbox} |
895 \end{ttbox} |
882 The other case is similar. Let us prove it by \ttindex{pc_tac}, and note |
896 The other case is similar. Let us prove it by \ttindex{pc_tac}, and note |
883 the final proof object. |
897 the final proof object. |
884 \begin{ttbox} |
898 \begin{ttbox} |
885 by (pc_tac prems 1); |
899 by (pc_tac prems 1); |
886 {\out Level 8} |
900 {\out Level 8} |
887 {\out split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))} |
901 {\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))} |
888 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
902 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))} |
889 {\out No subgoals!} |
903 {\out No subgoals!} |
890 \end{ttbox} |
904 \end{ttbox} |
891 Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also |
905 Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also |
892 proves this theorem. |
906 proves this theorem. |
893 |
907 |
894 |
908 |
895 \section{Example: deriving a currying functional} |
909 \section{Example: deriving a currying functional} |
896 In simply-typed languages such as {\ML}, a currying functional has the type |
910 In simply-typed languages such as {\ML}, a currying functional has the type |
897 \[ (A\times B \to C) \to (A\to (B\to C)). \] |
911 \[ (A\times B \to C) \to (A\to (B\to C)). \] |
898 Let us generalize this to~$\Sigma$ and~$\Pi$. The argument of the |
912 Let us generalize this to~$\Sigma$ and~$\Pi$. |
899 functional is a function that maps $z:\Sigma(A,B)$ to~$C(z)$; the resulting |
913 The functional takes a function~$f$ that maps $z:\Sigma(A,B)$ |
900 function maps $x\in A$ and $y\in B(x)$ to $C(\langle x,y\rangle)$. Here |
914 to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to |
901 $B$ is a family over~$A$, while $C$ is a family over $\Sigma(A,B)$. |
915 $C(\langle x,y\rangle)$. |
|
916 |
|
917 Formally, there are three typing premises. $A$ is a type; $B$ is an |
|
918 $A$-indexed family of types; $C$ is a family of types indexed by |
|
919 $\Sigma(A,B)$. The goal is expressed using \hbox{\tt PROD f} to ensure |
|
920 that the parameter corresponding to the functional's argument is really |
|
921 called~$f$; Isabelle echoes the type using \verb|-->| because there is no |
|
922 explicit dependence upon~$f$. |
902 \begin{ttbox} |
923 \begin{ttbox} |
903 val prems = goal CTT.thy |
924 val prems = goal CTT.thy |
904 "[| A type; !!x. x:A ==> B(x) type; \ttback |
925 "[| A type; !!x. x:A ==> B(x) type; \ttback |
905 \ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \ttback |
926 \ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback |
906 \ttback ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ttback |
927 \ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback |
907 \ttback --> (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
928 \ttback (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
|
929 \ttbreak |
908 {\out Level 0} |
930 {\out Level 0} |
909 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))} |
931 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->} |
|
932 {\out (PROD x:A. PROD y:B(x). C(<x,y>))} |
910 {\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->} |
933 {\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->} |
911 {\out (PROD x:A. PROD y:B(x). C(<x,y>))} |
934 {\out (PROD x:A. PROD y:B(x). C(<x,y>))} |
912 \ttbreak |
935 \ttbreak |
913 {\out val prems = ["A type [A type]",} |
936 {\out val prems = ["A type [A type]",} |
914 {\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} |
937 {\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",} |
915 {\out "?z : SUM x:A. B(x) ==> C(?z) type} |
938 {\out "?z : SUM x:A. B(x) ==> C(?z) type} |
916 {\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list} |
939 {\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list} |
917 \end{ttbox} |
940 \end{ttbox} |
918 This is an opportunity to demonstrate \ttindex{intr_tac}. Here, the tactic |
941 This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic |
919 repeatedly applies $\Pi$-introduction, automatically proving the rather |
942 repeatedly applies $\Pi$-introduction, proving the rather |
920 tiresome typing conditions. Note that $\Var{a}$ becomes instantiated to |
943 tiresome typing conditions. |
921 three nested $\lambda$-abstractions. |
944 |
|
945 Note that $\Var{a}$ becomes instantiated to three nested |
|
946 $\lambda$-abstractions. It would be easier to read if the bound variable |
|
947 names agreed with the parameters in the subgoal. Isabelle attempts to give |
|
948 parameters the same names as corresponding bound variables in the goal, but |
|
949 this does not always work. In any event, the goal is logically correct. |
922 \begin{ttbox} |
950 \begin{ttbox} |
923 by (intr_tac prems); |
951 by (intr_tac prems); |
924 {\out Level 1} |
952 {\out Level 1} |
925 {\out lam x xa xb. ?b7(x,xa,xb)} |
953 {\out lam x xa xb. ?b7(x,xa,xb)} |
926 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))} |
954 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))} |
927 {\out 1. !!uu x y.} |
955 {\out 1. !!f x y.} |
928 {\out [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>} |
956 {\out [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>} |
929 {\out ?b7(uu,x,y) : C(<x,y>)} |
957 {\out ?b7(f,x,y) : C(<x,y>)} |
930 \end{ttbox} |
958 \end{ttbox} |
931 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$uu$. |
959 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$. |
932 \index{*ProdE} |
960 \index{*ProdE} |
933 \begin{ttbox} |
961 \begin{ttbox} |
934 by (eresolve_tac [ProdE] 1); |
962 by (eresolve_tac [ProdE] 1); |
935 {\out Level 2} |
963 {\out Level 2} |
936 {\out lam x xa xb. x ` <xa,xb>} |
964 {\out lam x xa xb. x ` <xa,xb>} |
937 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))} |
965 {\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))} |
938 {\out 1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)} |
966 {\out 1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)} |
939 \end{ttbox} |
967 \end{ttbox} |
940 Finally, we exhibit a suitable argument for the function application. This |
968 Finally, we exhibit a suitable argument for the function application. This |
941 is straightforward using introduction rules. |
969 is straightforward using introduction rules. |
942 \index{*intr_tac} |
970 \index{*intr_tac} |
943 \begin{ttbox} |
971 \begin{ttbox} |
998 {\out Level 1} |
1026 {\out Level 1} |
999 {\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>} |
1027 {\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>} |
1000 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1028 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1001 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1029 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1002 \ttbreak |
1030 \ttbreak |
1003 {\out 1. !!uu x.} |
1031 {\out 1. !!h x.} |
1004 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1032 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1005 {\out ?b7(uu,x) : B(x)} |
1033 {\out ?b7(h,x) : B(x)} |
1006 \ttbreak |
1034 \ttbreak |
1007 {\out 2. !!uu x.} |
1035 {\out 2. !!h x.} |
1008 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1036 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1009 {\out ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)} |
1037 {\out ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)} |
1010 \end{ttbox} |
1038 \end{ttbox} |
1011 Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some |
1039 Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some |
1012 $\Var{b@7}(uu,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof |
1040 $\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof |
1013 object $\Var{b@8}(uu,x)$ to witness that the choice function's argument |
1041 object $\Var{b@8}(h,x)$ to witness that the choice function's argument and |
1014 and result lie in the relation~$C$. |
1042 result lie in the relation~$C$. This latter task will take up most of the |
|
1043 proof. |
1015 \index{*ProdE}\index{*SumE_fst}\index{*RS} |
1044 \index{*ProdE}\index{*SumE_fst}\index{*RS} |
1016 \begin{ttbox} |
1045 \begin{ttbox} |
1017 by (eresolve_tac [ProdE RS SumE_fst] 1); |
1046 by (eresolve_tac [ProdE RS SumE_fst] 1); |
1018 {\out Level 2} |
1047 {\out Level 2} |
1019 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1048 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1020 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1049 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1021 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1050 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1022 \ttbreak |
1051 \ttbreak |
1023 {\out 1. !!uu x. x : A ==> x : A} |
1052 {\out 1. !!h x. x : A ==> x : A} |
1024 {\out 2. !!uu x.} |
1053 {\out 2. !!h x.} |
1025 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1054 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1026 {\out ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)} |
1055 {\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)} |
1027 \end{ttbox} |
1056 \end{ttbox} |
1028 Above, we have composed \ttindex{fst} with the function~$h$ (named~$uu$ in |
1057 Above, we have composed \ttindex{fst} with the function~$h$. Unification |
1029 the assumptions). Unification has deduced that the function must be |
1058 has deduced that the function must be applied to $x\in A$. |
1030 applied to $x\in A$. |
|
1031 \begin{ttbox} |
1059 \begin{ttbox} |
1032 by (assume_tac 1); |
1060 by (assume_tac 1); |
1033 {\out Level 3} |
1061 {\out Level 3} |
1034 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1062 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1035 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1063 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1036 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1064 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1037 {\out 1. !!uu x.} |
1065 {\out 1. !!h x.} |
1038 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1066 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1039 {\out ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)} |
1067 {\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)} |
1040 \end{ttbox} |
1068 \end{ttbox} |
1041 Before we can compose \ttindex{snd} with~$h$, the arguments of $C$ must be |
1069 Before we can compose \ttindex{snd} with~$h$, the arguments of $C$ must be |
1042 simplified. The derived rule \ttindex{replace_type} lets us replace a type |
1070 simplified. The derived rule \ttindex{replace_type} lets us replace a type |
1043 by any equivalent type: |
1071 by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$: |
1044 \begin{ttbox} |
1072 \begin{ttbox} |
1045 by (resolve_tac [replace_type] 1); |
1073 by (resolve_tac [replace_type] 1); |
1046 {\out Level 4} |
1074 {\out Level 4} |
1047 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1075 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1048 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1076 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1049 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1077 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1050 \ttbreak |
1078 \ttbreak |
1051 {\out 1. !!uu x.} |
1079 {\out 1. !!h x.} |
1052 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1080 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1053 {\out C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)} |
1081 {\out C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)} |
1054 \ttbreak |
1082 \ttbreak |
1055 {\out 2. !!uu x.} |
1083 {\out 2. !!h x.} |
1056 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1084 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1057 {\out ?b8(uu,x) : ?A13(uu,x)} |
1085 {\out ?b8(h,x) : ?A13(h,x)} |
1058 \end{ttbox} |
1086 \end{ttbox} |
1059 The derived rule \ttindex{subst_eqtyparg} lets us simplify a type's |
1087 The derived rule \ttindex{subst_eqtyparg} lets us simplify a type's |
1060 argument (by currying, $C(x)$ is a unary type operator): |
1088 argument (by currying, $C(x)$ is a unary type operator): |
1061 \begin{ttbox} |
1089 \begin{ttbox} |
1062 by (resolve_tac [subst_eqtyparg] 1); |
1090 by (resolve_tac [subst_eqtyparg] 1); |
1063 {\out Level 5} |
1091 {\out Level 5} |
1064 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1092 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1065 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1093 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1066 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1094 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1067 \ttbreak |
1095 \ttbreak |
1068 {\out 1. !!uu x.} |
1096 {\out 1. !!h x.} |
1069 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1097 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1070 {\out (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)} |
1098 {\out (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)} |
1071 \ttbreak |
1099 \ttbreak |
1072 {\out 2. !!uu x z.} |
1100 {\out 2. !!h x z.} |
1073 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;} |
1101 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;} |
1074 {\out z : ?A14(uu,x) |] ==>} |
1102 {\out z : ?A14(h,x) |] ==>} |
1075 {\out C(x,z) type} |
1103 {\out C(x,z) type} |
1076 \ttbreak |
1104 \ttbreak |
1077 {\out 3. !!uu x.} |
1105 {\out 3. !!h x.} |
1078 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1106 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1079 {\out ?b8(uu,x) : C(x,?c14(uu,x))} |
1107 {\out ?b8(h,x) : C(x,?c14(h,x))} |
1080 \end{ttbox} |
1108 \end{ttbox} |
1081 The rule \ttindex{ProdC} is simply $\beta$-reduction. The term |
1109 Subgoal~1 requires simply $\beta$-contraction, which is the rule |
1082 $\Var{c@{14}}(uu,x)$ receives the simplified form, $f{\tt`}x$. |
1110 \ttindex{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal |
|
1111 receives the contracted result. |
1083 \begin{ttbox} |
1112 \begin{ttbox} |
1084 by (resolve_tac [ProdC] 1); |
1113 by (resolve_tac [ProdC] 1); |
1085 {\out Level 6} |
1114 {\out Level 6} |
1086 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1115 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1087 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1116 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1088 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1117 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1089 \ttbreak |
1118 \ttbreak |
1090 {\out 1. !!uu x.} |
1119 {\out 1. !!h x.} |
1091 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)} |
1120 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1092 \ttbreak |
1121 {\out x : ?A15(h,x)} |
1093 {\out 2. !!uu x xa.} |
1122 \ttbreak |
1094 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;} |
1123 {\out 2. !!h x xa.} |
1095 {\out xa : ?A15(uu,x) |] ==>} |
1124 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;} |
1096 {\out fst(uu ` xa) : ?B15(uu,x,xa)} |
1125 {\out xa : ?A15(h,x) |] ==>} |
1097 \ttbreak |
1126 {\out fst(h ` xa) : ?B15(h,x,xa)} |
1098 {\out 3. !!uu x z.} |
1127 \ttbreak |
1099 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;} |
1128 {\out 3. !!h x z.} |
1100 {\out z : ?B15(uu,x,x) |] ==>} |
1129 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;} |
|
1130 {\out z : ?B15(h,x,x) |] ==>} |
1101 {\out C(x,z) type} |
1131 {\out C(x,z) type} |
1102 \ttbreak |
1132 \ttbreak |
1103 {\out 4. !!uu x.} |
1133 {\out 4. !!h x.} |
1104 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1134 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1105 {\out ?b8(uu,x) : C(x,fst(uu ` x))} |
1135 {\out ?b8(h,x) : C(x,fst(h ` x))} |
1106 \end{ttbox} |
1136 \end{ttbox} |
1107 Routine type checking goals proliferate in Constructive Type Theory, but |
1137 Routine type checking goals proliferate in Constructive Type Theory, but |
1108 \ttindex{typechk_tac} quickly solves them. Note the inclusion of |
1138 \ttindex{typechk_tac} quickly solves them. Note the inclusion of |
1109 \ttindex{SumE_fst}. |
1139 \ttindex{SumE_fst} along with the premises. |
1110 \begin{ttbox} |
1140 \begin{ttbox} |
1111 by (typechk_tac (SumE_fst::prems)); |
1141 by (typechk_tac (SumE_fst::prems)); |
1112 {\out Level 7} |
1142 {\out Level 7} |
1113 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1143 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>} |
1114 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1144 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1115 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1145 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1116 {\out 1. !!uu x.} |
1146 \ttbreak |
1117 {\out [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
1147 {\out 1. !!h x.} |
1118 {\out ?b8(uu,x) : C(x,fst(uu ` x))} |
1148 {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} |
|
1149 {\out ?b8(h,x) : C(x,fst(h ` x))} |
1119 \end{ttbox} |
1150 \end{ttbox} |
1120 We are finally ready to compose \ttindex{snd} with~$h$. |
1151 We are finally ready to compose \ttindex{snd} with~$h$. |
1121 \index{*ProdE}\index{*SumE_snd}\index{*RS} |
1152 \index{*ProdE}\index{*SumE_snd}\index{*RS} |
1122 \begin{ttbox} |
1153 \begin{ttbox} |
1123 by (eresolve_tac [ProdE RS SumE_snd] 1); |
1154 by (eresolve_tac [ProdE RS SumE_snd] 1); |
1124 {\out Level 8} |
1155 {\out Level 8} |
1125 {\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>} |
1156 {\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>} |
1126 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1157 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->} |
1127 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1158 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))} |
1128 {\out 1. !!uu x. x : A ==> x : A} |
1159 \ttbreak |
1129 {\out 2. !!uu x. x : A ==> B(x) type} |
1160 {\out 1. !!h x. x : A ==> x : A} |
1130 {\out 3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type} |
1161 {\out 2. !!h x. x : A ==> B(x) type} |
|
1162 {\out 3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type} |
1131 \end{ttbox} |
1163 \end{ttbox} |
1132 The proof object has reached its final form. We call \ttindex{typechk_tac} |
1164 The proof object has reached its final form. We call \ttindex{typechk_tac} |
1133 to finish the type checking. |
1165 to finish the type checking. |
1134 \begin{ttbox} |
1166 \begin{ttbox} |
1135 by (typechk_tac prems); |
1167 by (typechk_tac prems); |