diff options
| -rw-r--r-- | Makefile.doc | 42 | ||||
| -rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 49 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 51 | ||||
| -rwxr-xr-x | doc/tutorial/Tutorial.tex | 41 | ||||
| -rw-r--r-- | lib/pp_control.ml | 4 | ||||
| -rw-r--r-- | theories/Logic/Hurkens.v | 2 |
9 files changed, 131 insertions, 88 deletions
diff --git a/Makefile.doc b/Makefile.doc index 5afd12393..9382e1b6f 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -17,15 +17,15 @@ doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt doc-html:\ doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ - doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.v.html + doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html doc-pdf:\ doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \ - doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.v.pdf + doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf doc-ps:\ doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \ - doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps + doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps refman: \ doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf @@ -38,8 +38,8 @@ stdlib: \ faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf -rectutorial: doc/RecTutorial/RecTutorial.v.html \ - doc/RecTutorial/RecTutorial.v.ps doc/RecTutorial/RecTutorial.v.pdf +rectutorial: doc/RecTutorial/RecTutorial.html \ + doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf ###################################################################### ### Implicit rules @@ -216,32 +216,32 @@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li (cd doc/stdlib;\ $(LATEX) -interaction=batchmode Library;\ $(LATEX) -interaction=batchmode Library > /dev/null;\ - ../tools/show_latex_messages Library.log) + ../tools/show_latex_messages -no-overfull Library.log) doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi (cd doc/stdlib;\ $(PDFLATEX) -interaction=batchmode Library;\ - ../tools/show_latex_messages Library.log) + ../tools/show_latex_messages -no-overfull Library.log) ###################################################################### # Tutorial on inductive types ###################################################################### -doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex +doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex (cd doc/RecTutorial;\ - $(LATEX) -interaction=batchmode RecTutorial.v;\ - $(BIBTEX) -terse RecTutorial.v;\ - $(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\ - $(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\ - ../tools/show_latex_messages RecTutorial.v.log) + $(LATEX) -interaction=batchmode RecTutorial;\ + $(BIBTEX) -terse RecTutorial;\ + $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\ + $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\ + ../tools/show_latex_messages RecTutorial.log) -doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi +doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi (cd doc/RecTutorial;\ - $(PDFLATEX) -interaction=batchmode RecTutorial.v.tex;\ - ../tools/show_latex_messages RecTutorial.v.log) + $(PDFLATEX) -interaction=batchmode RecTutorial.tex;\ + ../tools/show_latex_messages RecTutorial.log) -doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex - (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v) +doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex + (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial) ###################################################################### # Index file for CoqIDE @@ -267,7 +267,7 @@ install-doc-html: $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq) $(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.html $(FULLDOCDIR)/html/RecTutorial.html + $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html $(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html @@ -278,8 +278,8 @@ install-doc-printable: $(INSTALLLIB) doc/refman/Reference-Manual.ps \ doc/stdlib/Library.ps $(FULLDOCDIR)/ps $(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf + $(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf $(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf $(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.ps $(FULLDOCDIR)/ps/RecTutorial.ps + $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex index 79b4f7f1a..372f13326 100644 --- a/doc/RecTutorial/RecTutorial.tex +++ b/doc/RecTutorial/RecTutorial.tex @@ -724,7 +724,7 @@ for \linebreak ``~\citecoq{ex (fun $x$:$A$ \funarrow{} $B$)}~''. \noindent The former quantifier inhabits the universe of propositions. As for the conjunction and disjunction connectives, there is also another version of existential quantification inhabiting the universes $\Type_i$, -which is noted \texttt{sig $P$}. The syntax +which is written \texttt{sig $P$}. The syntax ``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''. @@ -934,7 +934,7 @@ Definition predecessor : {\prodsym} n:nat, pred_spec n. Defined. \end{alltt} -If we print the term built by {\coq}, we can observe its dependent pattern-matching structure: +If we print the term built by {\coq}, its dependent pattern-matching structure can be observed: \begin{alltt} predecessor = fun n : nat {\funarrow} @@ -950,8 +950,9 @@ predecessor = fun n : nat {\funarrow} \end{alltt} -Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at the reference manual and/or the book: tactics -\texttt{destruct}, ``~\texttt{intro \emph{pattern}}~'', etc. +Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at for tactics +``~\texttt{destruct}~'', ``~\texttt{intro \emph{pattern}}~'', etc. in +the reference manual and/or the book. \noindent The command \texttt{Extraction} \refmancite{Section \ref{ExtractionIdent}} can be used to see the computational @@ -1240,7 +1241,7 @@ Let $n$ and $p$ be terms of type \citecoq{nat}, and $Q$ a predicate of type $\citecoq{nat}\arrow{}\Prop$. If $H$ is a proof of ``~\texttt{n {\coqle} p}~'', $H_0$ a proof of ``~\texttt{$Q$ n}~'' and -$H_S$ a proof of ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'', +$H_S$ a proof of the statement ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'', then the term \begin{alltt} match H in (_ {\coqle} q) return (Q q) with @@ -2604,8 +2605,8 @@ End Principle_of_Double_Induction. \end{alltt} Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$, -another combinator \texttt{nat\_double\_rect} for constructing -(certified) programs can be defined in exactly the same way. +another combinator for constructing +(certified) programs, \texttt{nat\_double\_rect}, can be defined in exactly the same way. This definition is left as an exercise.\label{natdoublerect} \iffalse @@ -2751,8 +2752,8 @@ has a universally quantified formula as conclusion, which confuses Therefore, -in this case the abstraction must be explicited using the tactic -\texttt{pattern}. Once the right abstraction is provided, the rest of +in this case the abstraction must be explicited using the +\texttt{pattern} tactic. Once the right abstraction is provided, the rest of the proof is immediate: \begin{alltt} @@ -2804,8 +2805,8 @@ Defined. \begin{exercise} \begin{enumerate} -\item Define a recursive function \emph{nat2itree} -mapping any natural number $n$ into an infinitely branching +\item Define a recursive function of name \emph{nat2itree} +that maps any natural number $n$ into an infinitely branching tree of height $n$. \item Provide an elimination combinator for these trees. \item Prove that the relation \citecoq{itree\_le} is a preorder @@ -2831,7 +2832,7 @@ for all n and p. (\citecoq{le'} is defined in section \ref{parameterstuff}). Structural induction is a strong elimination rule for inductive types. This method can be used to define any function whose termination is -based on the well-foundedness of certain order relation $R$ decreasing +a consequence of the well-foundedness of a certain order relation $R$ decreasing at each recursive call. What makes this principle so strong is the possibility of reasoning by structural induction on the proof that certain $R$ is well-founded. In order to illustrate this we have @@ -2867,8 +2868,8 @@ let rec div x y = \end{verbatim} -The equality test on natural numbers can be represented as the -function \textsl{eq\_nat\_dec} defined page \pageref{iseqpage}. Giving $x$ and +The equality test on natural numbers can be implemented using the +function \textsl{eq\_nat\_dec} that is defined page \pageref{iseqpage}. Giving $x$ and $y$, this function yields either the value $(\textsl{left}\;p)$ if there exists a proof $p:x=y$, or the value $(\textsl{right}\;q)$ if there exists $q:a\not = b$. The subtraction function is already @@ -3112,7 +3113,7 @@ The term "Vnil A" has type "vector A 0" while it is expected to have type "vector A n" \end{alltt} -In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill typed, +In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill-typed and this is because the type ``~\citecoq{vector A n}~'' is not \emph{convertible} with ``~\citecoq{vector A 0}~''. @@ -3264,11 +3265,11 @@ on vectors of same length: \begin{alltt} Definition vector_double_rect : - {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type), - P 0 Vnil Vnil {\arrow} - ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow} - P (S n) (Vcons a v1) (Vcons b v2)) {\arrow} - {\prodsym} n (v1 v2 : vector A n), P n v1 v2. + {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type), + P 0 Vnil Vnil {\arrow} + ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow} + P (S n) (Vcons a v1) (Vcons b v2)) {\arrow} + {\prodsym} n (v1 v2 : vector A n), P n v1 v2. induction n. intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2). auto. @@ -3361,7 +3362,7 @@ CoInductive LList (A: Type) : Type := It is also possible to define co-inductive types for the -trees with infinite branches (see Chapter 13 of~\cite{coqart}). +trees with infinitely-many branches (see Chapter 13 of~\cite{coqart}). Structural induction is the way of expressing that inductive types only contain well-founded objects. Hence, this elimination principle @@ -3555,7 +3556,7 @@ Qed. \end{alltt} \begin{exercise} -Define a co-inductive type $Nat$ containing non-standard +Define a co-inductive type of name $Nat$ that contains non-standard natural numbers --this is, verifying $$\exists m \in \mbox{\texttt{Nat}}, \forall\, n \in \mbox{\texttt{Nat}}, n<m$$. @@ -3591,8 +3592,8 @@ Proof. Qed. Lemma injection_demo : {\prodsym} (A:Type)(a b : A)(l l': LList A), - LCons a (LCons b l) = LCons b (LCons a l') {\arrow} - a = b {\coqand} l = l'. + LCons a (LCons b l) = LCons b (LCons a l') {\arrow} + a = b {\coqand} l = l'. Proof. intros A a b l l' e; injection e; auto. Qed. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 8b404f4ef..501f9b0b1 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -343,7 +343,7 @@ for all the arguments. For example, the preceding example can be written: Reset fst. \end{coq_eval} \begin{coq_example} -Definition fst (A B:Set) (p:A * B) := let 'pair x _ := p in x. +Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. \end{coq_example} This is useful to match deeper inside tuples and also to use notations @@ -351,10 +351,10 @@ for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary patterns to do the deconstruction. For example: \begin{coq_example} -Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A := +Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := let '((a,b), (c, d)) := x in (a,b,c,d). Notation " x 'with' p " := (exist _ x p) (at level 20). -Definition proj1_sig' (A :Set) (P : A -> Prop) (t:{ x : A | P x }) : A := +Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := let 'x with p := t in x. \end{coq_example} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 3a4d7f03e..48c18e265 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -226,7 +226,7 @@ Chapter \ref{Addoc-syntax}. \begin{figure}[htbp] \begin{centerframe} -\begin{tabular}{lcl@{\qquad}r} +\begin{tabular}{lcl@{\quad~}r} % warning: page width exceeded with \qquad {\term} & ::= & {\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\ & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\ @@ -266,10 +266,10 @@ Chapter \ref{Addoc-syntax}. {\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\ & $|$ & {\binder} \nelist{\binderlet}{} &\\ &&&\\ -{\binder} & ::= & {\name} & \ref{Binders} \\ +{\binder} & ::= & {\name} & (\ref{Binders}) \\ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ &&&\\ -{\binderlet} & ::= & {\binder} & \ref{Binders} \\ +{\binderlet} & ::= & {\binder} & (\ref{Binders}) \\ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ & & &\\ {\name} & ::= & {\ident} &\\ diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index d15859047..24eb3d112 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -267,11 +267,11 @@ Abort. \begin{coq_example*} End equality. Definition eq_ind_r : - forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. + forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y. Definition eq_rec_r : - forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. + forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y. Definition eq_rect_r : - forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y. + forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y. \end{coq_example*} \begin{coq_eval} Abort. @@ -290,8 +290,9 @@ arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3}, For instance {\tt f\_equal3} is defined the following way. \begin{coq_example*} Theorem f_equal3 : - forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) - (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. + forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) + (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), + x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. \end{coq_example*} \begin{coq_eval} Abort. @@ -478,7 +479,9 @@ in the \verb"Set" \verb"A+{B}". \ttindex{A+\{B\}} \begin{coq_example*} -Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B). +Inductive sumor (A:Set) (B:Prop) : Set := +| inleft (_:A) +| inright (_:B). \end{coq_example*} We may define variants of the axiom of choice, like in Martin-Löf's @@ -675,7 +678,8 @@ induction principle. \begin{coq_example*} Theorem nat_case : - forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. + forall (n:nat) (P:nat -> Prop), + P 0 -> (forall m:nat, P (S m)) -> P n. \end{coq_example*} \begin{coq_eval} Abort All. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index d5c6dbfdb..5b447f350 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -22,7 +22,7 @@ problems. \def\letclause{\textrm{\textsl{let\_clause}}} \def\matchrule{\textrm{\textsl{match\_rule}}} \def\contextrule{\textrm{\textsl{context\_rule}}} -\def\contexthyps{\textrm{\textsl{context\_hyps}}} +\def\contexthyp{\textrm{\textsl{context\_hyp}}} \def\tacarg{\nterm{tacarg}} \def\cpattern{\nterm{cpattern}} @@ -166,11 +166,12 @@ is understood as \letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\ \\ \contextrule & ::= & - \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\ + \nelist{\contexthyp}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\ & $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\ & $|$ & {\tt \_ =>} {\tacexpr}\\ \\ -\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\ +\contexthyp & ::= & {\name} {\tt :} {\cpattern}\\ + & $|$ & {\name} {\tt :=} {\cpattern} \zeroone{{\tt :} {\cpattern}}\\ \\ \matchrule & ::= & {\cpattern} {\tt =>} {\tacexpr}\\ @@ -268,31 +269,53 @@ A sequence is an expression of the following form: \begin{quote} {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$ \end{quote} -{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and -$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied -and $v_2$ is applied to every subgoal generated by the application of -$v_1$. Sequence is left-associative. +The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated +to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is +then applied and $v_2$ is applied to every subgoal generated by the +application of $v_1$. Sequence is left-associative. \subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}} %\tacindex{; [ | ]} %\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}} \index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}} -We can generalize the previous sequence operator as +A general sequence has the following form: \begin{quote} {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} \end{quote} -{\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is -applied and $v_i$ is applied to the $i$-th generated subgoal by the -application of $v_0$, for $=1,...,n$. It fails if the application of -$v_0$ does not generate exactly $n$ subgoals. +The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=0,...,n$ +and all have to be tactics. The tactic $v_0$ is applied and $v_i$ is +applied to the $i$-th generated subgoal by the application of $v_0$, +for $=1,...,n$. It fails if the application of $v_0$ does not generate +exactly $n$ subgoals. -\variant If no tactic is given for the $i$-th generated subgoal, it +\begin{Variants} + \item If no tactic is given for the $i$-th generated subgoal, it behaves as if the tactic {\tt idtac} were given. For instance, {\tt split ; [ | auto ]} is a shortcut for {\tt split ; [ idtac | auto ]}. + \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} + {\tacexpr}$_i$ {\tt |} {\tt ..} {\tt |} {\tacexpr}$_{i+1+j}$ {\tt |} + $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} + + In this variant, {\tt idtac} is used for the subgoals numbered from + $i+1$ to $i+j$ (assuming $n$ is the number of subgoals). + + Note that {\tt ..} is part of the syntax, while $...$ is the meta-symbol used + to describe a list of {\tacexpr} of arbitrary length. + + \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} + {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |} + {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} + + In this variant, {\tacexpr} is used instead of {\tt idtac} for the + subgoals numbered from $i+1$ to $i+j$. + +\end{Variants} + + \subsubsection[For loop]{For loop\tacindex{do} \index{Tacticals!do@{\tt do}}} @@ -591,7 +614,7 @@ We can make pattern matching on goals using the following expression: \end{quote} If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$ -is matched (non-linear first order unification) by an hypothesis of +is matched (non-linear first-order unification) by an hypothesis of the goal and if {\cpattern}$_1$ is matched by the conclusion of the goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the pattern matching to the metavariables and the real hypothesis names diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 8944ec979..219706e35 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -108,6 +108,10 @@ $e:\tau(E)$ for the judgment that $e$ is of type $E$. You may request \Coq~ to return to you the type of a valid expression by using the command \verb:Check:: +\begin{coq_eval} +Set Printing Width 60. +\end{coq_eval} + \begin{coq_example} Check O. \end{coq_example} @@ -169,9 +173,9 @@ arrow function constructor, in order to get a functional type \begin{coq_example} Check (nat -> Prop). \end{coq_example} -which may be composed again with \verb:nat: in order to obtain the +which may be composed one more times with \verb:nat: in order to obtain the type \verb:nat->nat->Prop: of binary relations over natural numbers. -Actually \verb:nat->nat->Prop: is an abbreviation for +Actually the type \verb:nat->nat->Prop: is an abbreviation for \verb:nat->(nat->Prop):. Functional notions may be composed in the usual way. An expression $f$ @@ -213,7 +217,7 @@ argument \verb:m: of type \verb:nat: in order to build its result as \begin{coq_example} Definition double (m:nat) := plus m m. \end{coq_example} -This definition introduces the constant \texttt{double} defined as the +This introduces the constant \texttt{double} defined as the expression \texttt{fun m:nat => plus m m}. The abstraction introduced by \texttt{fun} is explained as follows. The expression \verb+fun x:A => e+ is well formed of type \verb+A->B+ in a context @@ -445,7 +449,6 @@ conjunctive goal into the two subgoals: \begin{coq_example} split. \end{coq_example} - and the proof is now trivial. Indeed, the whole proof is obtainable as follows: \begin{coq_example} Restart. @@ -540,7 +543,7 @@ explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+, corresponds to \verb:intro H:, whereas a subterm such as \verb:(or_intror: \verb:B H0): -corresponds to the sequence \verb:apply or_intror; exact H0:. +corresponds to the sequence of tactics \verb:apply or_intror; exact H0:. The generic combinator \verb:or_intror: needs to be instantiated by the two properties \verb:B: and \verb:A:. Because \verb:A: can be deduced from the type of \verb:H0:, only \verb:B: is printed. @@ -559,7 +562,7 @@ Qed. \subsection{Classical reasoning} -\verb:tauto: always comes back with an answer. Here is an example where it +The tactic \verb:tauto: always comes back with an answer. Here is an example where it fails: \begin{coq_example} Lemma Peirce : ((A -> B) -> A) -> A. @@ -661,6 +664,9 @@ remove a section, or we may return to the initial state using~: \begin{coq_example} Reset Initial. \end{coq_example} +\begin{coq_eval} +Set Printing Width 60. +\end{coq_eval} We shall now declare a new \verb:Section:, which will allow us to define notions local to a well-delimited scope. We start by assuming a domain of @@ -705,7 +711,7 @@ predicate as argument: Check ex. \end{coq_example} and the notation \verb+(exists x:D, P x)+ is just concrete syntax for -\verb+(ex D (fun x:D => P x))+. +the expression \verb+(ex D (fun x:D => P x))+. Existential quantification is handled in \Coq~ in a similar fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by the proof combinator \verb:ex_intro:, which is invoked by the specific @@ -842,7 +848,8 @@ elim (EM (exists x, ~ P x)). We first look at the first case. Let Tom be the non-drinker: \begin{coq_example} -intro Non_drinker; elim Non_drinker; intros Tom Tom_does_not_drink. +intro Non_drinker; elim Non_drinker; + intros Tom Tom_does_not_drink. \end{coq_example} We conclude in that case by considering Tom, since his drinking leads to @@ -1026,7 +1033,8 @@ predicates over some universe \verb:U:. For instance: Variable U : Type. Definition set := U -> Prop. Definition element (x:U) (S:set) := S x. -Definition subset (A B:set) := forall x:U, element x A -> element x B. +Definition subset (A B:set) := + forall x:U, element x A -> element x B. \end{coq_example} Now, assume that we have loaded a module of general properties about @@ -1151,7 +1159,7 @@ right; trivial. \end{coq_example} Indeed, the whole proof can be done with the combination of the -\verb:simple induction: tactic, which combines \verb:intro: and \verb:elim:, + \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:, with good old \verb:auto:: \begin{coq_example} Restart. @@ -1197,13 +1205,15 @@ an expression to its {\sl normal form}: \begin{coq_example} Eval cbv beta in ((fun _:nat => nat) O -> - (forall y:nat, (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) -> + (forall y:nat, + (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) -> forall n:nat, (fun _:nat => nat) n). \end{coq_example} Let us now show how to program addition with primitive recursion: \begin{coq_example} -Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n. +Definition addition (n m:nat) := + prim_rec m (fun p rec:nat => S rec) n. \end{coq_example} That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n: @@ -1242,6 +1252,9 @@ Reset bool. \begin{coq_eval} Reset Initial. \end{coq_eval} +\begin{coq_eval} +Set Printing Width 60. +\end{coq_eval} Let us now show how to do proofs by structural induction. We start with easy properties of the \verb:plus: function we just defined. Let us first @@ -1508,13 +1521,13 @@ development is not type-checked again. \section{Creating your own modules} -You may create your own modules, by writing \Coq~ commands in a file, +You may create your own module files, by writing {\Coq} commands in a file, say \verb:my_module.v:. Such a module may be simply loaded in the current context, with command \verb:Load my_module:. It may also be compiled, in ``batch'' mode, using the UNIX command \verb:coqc:. Compiling the module \verb:my_module.v: creates a file \verb:my_module.vo:{} that can be reloaded with command -\verb:Require Import my_module:. +\verb:Require: \verb:Import: \verb:my_module:. If a required module depends on other modules then the latters are automatically required beforehand. However their contents is not diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 67ae4a20a..7617d5ca4 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -105,5 +105,7 @@ let set_depth_boxes v = let get_margin () = Some (Format.pp_get_margin !std_ft ()) let set_margin v = - Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v) + let v = match v with None -> default_margin | Some v -> v in + Format.pp_set_margin !std_ft v; + Format.pp_set_margin !deep_ft v diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 46a574322..71c9af50b 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -19,7 +19,7 @@ and Applications (TLCA'95), 1995. - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001 - (see www.cs.kun.nl/~herman/note.ps.gz). + (see http://www.cs.kun.nl/~herman/note.ps.gz). *) Section Paradox. |