From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- doc/faq/FAQ.tex | 11 +++++++++++ doc/refman/Classes.tex | 25 ++++++++++++++++++------- doc/refman/RefMan-ext.tex | 4 ++-- doc/refman/RefMan-ide.tex | 36 +++++++++++++++++++++--------------- doc/refman/RefMan-tac.tex | 34 ++++++++++++++++++++++++++++++++-- doc/tutorial/Tutorial.tex | 2 +- 6 files changed, 85 insertions(+), 27 deletions(-) (limited to 'doc') diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index de1d84be..bd6f7dbf 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -97,6 +97,7 @@ \def\symmetryin{{\tt symmetryin}} \def\instantiate{{\tt instantiate}} \def\inversion{{\tt inversion}} +\def\specialize{{\tt specialize}} \def\Defined{{\tt Defined}} \def\Qed{{\tt Qed}} \def\pattern{{\tt pattern}} @@ -868,6 +869,16 @@ provide names for these variables: {\Coq} will do it anyway, but such automatic naming decreases legibility and robustness. +\Question{My goal contains an universally quantified statement, how can I use it?} + +If the universally quantified assumption matches the goal you can +use the {\apply} tactic. If it is an equation you can use the +{\rewrite} tactic. Otherwise you can use the {\specialize} tactic +to instantiate the quantified variables with terms. The variant +{\tt assert(Ht := H t)} makes a copy of assumption {\tt H} before +instantiating it. + + \Question{My goal is an existential, how can I prove it?} Use some theorem or assumption or exhibit the witness using the {\existstac} tactic. diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 7bd4f352..f427609f 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -10,7 +10,7 @@ \label{typeclasses} \begin{flushleft} - \em The status of Type Classes is (extremely) experimental. + \em The status of Type Classes is experimental. \end{flushleft} This chapter presents a quick reference of the commands related to type @@ -128,9 +128,7 @@ particular support for type classes: methods. In the example above, \texttt{A} and \texttt{eqa} should be set maximally implicit. \item They support implicit quantification on partialy applied type - classes (\S \ref{implicit-generalization}). - Any argument not given as part of a type class binder will be - automatically generalized. + classes. \item They also support implicit quantification on superclasses (\S \ref{classes:superclasses}) \end{itemize} @@ -143,6 +141,19 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). Here \texttt{A} is implicitly generalized, and the resulting function is equivalent to the one above. +The parsing of generalized type-class binders is different from regular +binders: +\begin{itemize} +\item Implicit arguments of the class type are ignored. +\item Superclasses arguments are automatically generalized. +\item Any remaining arguments not given as part of a type class binder + will be automatically generalized. In other words, the rightmost + parameters are automatically generalized if not mentionned. +\end{itemize} + +One can switch off this special treatment using the $!$ mark in front of +the class name (see example below). + \asection{Parameterized Instances} One can declare parameterized instances as in \Haskell simply by giving @@ -231,9 +242,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). \end{coq_example*} In some cases, to be able to specify sharing of structures, one may want to give -explicitly the superclasses. It is is possible to do it directly in regular -binders, and using the \texttt{!} modifier in class binders. For -example: +explicitly the superclasses. It is possible to do it directly in regular +generalized binders, and using the \texttt{!} modifier in class +binders. For example: \begin{coq_example*} Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 9efa7048..b8a893d5 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1622,7 +1622,7 @@ the generalized variables. Inside implicit generalization delimiters, free variables in the current context are automatically quantified using a product or a lambda abstraction to generate a closed term. In the following statement for example, the variables \texttt{n} -and \texttt{m} are autamatically generalized and become explicit +and \texttt{m} are automatically generalized and become explicit arguments of the lemma as we are using \verb|`( )|: \begin{coq_example} @@ -1638,7 +1638,7 @@ generalizations when mistyping identifiers. There are three variants of the command: \begin{quote} -{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} +{\tt (Global)? Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} \end{quote} \begin{Variants} diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 04830531..5d9c8c16 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -261,26 +261,32 @@ CONTROL and the SHIFT keys, and type the hexadecimal code of the symbol required, for example \verb|2200| for the $\forall$ symbol. A list of symbol codes is available at \url{http://www.unicode.org}. -This method obviously doesn't scale, that's why the preferred alternative is to -use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and -MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style -input method. - -To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user. -In the "Global Settings" group set the default Input Method to "ELatin" (don't -forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the -layout to "TeX", and remember the content of the "[ELatin] on" field (by default -"\"). You can now execute CoqIDE with the following commands (assuming -you use a Bourne-style shell): +This method obviously doesn't scale, that's why the preferred +alternative is to use an Input Method Editor. On POSIX systems (Linux +distributions, BSD variants and MacOS X), you can use \texttt{uim} to +support \LaTeX{}-style edition and, if using X Windows, you can also use +the XCompose method (XIM). How to use \texttt{uim} is documented below. + +If you have \texttt{uim} 1.5.x, first manually copy the files located +in directory {\tt ide/uim} of the Coq source distribution to the +{\tt uim} directory of input methods which typically is {\tt + /usr/share/uim}. Execute {\tt uim-module-manager -{-}register + coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set +the default Input Method to "CoqIDE" in the "Global Settings" group +(don't forget to tick the checkbox "Specify default IM"; you may also +have to first edit the set of "Enabled input method" to add CoqIDE to +the set). You can now execute CoqIDE with the following commands +(assuming you use a Bourne-style shell): \begin{verbatim} $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -Activate the ELatin Input Method with Ctrl-\textbackslash, then type the -sequence "\verb=\Gamma=". You will see the sequence being -replaced by $\Gamma$ as soon as you type the second "a". +If you then type the sequence "\verb=\Gamma=", you will see the sequence being +replaced by $\Gamma$ as soon as you type the second "a". + +If you have \texttt{uim} 1.6.x, the \LaTeX{} input method is built-in. You just have to execute \texttt{uim-pref-gtk} and choose "ELatin" as default Input Method in the "Global Settings". Then, in the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default "$\backslash$"). Proceed then as above. \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}} @@ -314,7 +320,7 @@ or -% $Id: RefMan-ide.tex 13477 2010-09-30 16:50:00Z vgross $ +% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b82cdc2d..450d3b2d 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -989,6 +989,36 @@ Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals have names of the form {\ident}\texttt{\_admitted} possibly followed by a number. +\subsection{\tt constr\_eq \term$_1$ \term$_2$ +\tacindex{constr\_eq} +\label{constreq}} + +This tactic applies to any goal. It checks whether its arguments are +equal modulo alpha conversion and casts. + +\ErrMsg \errindex{Not equal} + +\subsection{\tt is\_evar \term +\tacindex{is\_evar} +\label{isevar}} + +This tactic applies to any goal. It checks whether its argument is an +existential variable. Existential variables are uninstantiated +variables generated by e.g. {\tt eapply} (see Section~\ref{apply}). + +\ErrMsg \errindex{Not an evar} + +\subsection{\tt has\_evar \term +\tacindex{has\_evar} +\label{hasevar}} + +This tactic applies to any goal. It checks whether its argument has an +existential variable as a subterm. Unlike {\tt context} patterns +combined with {\tt is\_evar}, this tactic scans all subterms, +including those under binders. + +\ErrMsg \errindex{No evars} + \subsection{Bindings list \index{Binding list} \label{Binding-list}} @@ -3917,7 +3947,7 @@ where {\sl hint\_definition} is one of the following expressions: \begin{quotation} \begin{verbatim} -Hint Extern 4 ~(?=?) => discriminate. +Hint Extern 4 (~(_ = _)) => discriminate. \end{verbatim} \end{quotation} @@ -4294,7 +4324,7 @@ Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 13344 2010-07-28 15:04:36Z msozeau $ +% $Id: RefMan-tac.tex 13659 2010-11-29 11:09:07Z glondu $ %%% Local Variables: %%% mode: latex diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 63c35548..723295bf 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -1574,4 +1574,4 @@ with \Coq, in order to acquaint yourself with various proof techniques. \end{document} -% $Id: Tutorial.tex 13548 2010-10-14 12:35:43Z notin $ +% $Id: Tutorial.tex 13547 2010-10-14 12:35:00Z notin $ -- cgit v1.2.3