diff options
| -rw-r--r-- | Makefile.build | 14 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ind.tex | 510 | ||||
| -rw-r--r-- | doc/tutorial/Tutorial.tex | 445 | ||||
| -rw-r--r-- | engine/proofview.ml | 9 | ||||
| -rw-r--r-- | engine/proofview.mli | 2 | ||||
| -rw-r--r-- | lib/hashset.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 17 | ||||
| -rw-r--r-- | test-suite/output/Warnings.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Warnings.v | 5 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
14 files changed, 252 insertions, 768 deletions
diff --git a/Makefile.build b/Makefile.build index 0dafde997..05d751f54 100644 --- a/Makefile.build +++ b/Makefile.build @@ -101,7 +101,7 @@ DEPENDENCIES := \ ########################################################################### # Default timing command -STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" +STDTIME=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) @@ -275,7 +275,7 @@ grammar/grammar.cma : $(GRAMCMO) @touch grammar/test.mlp $(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test @rm -f grammar/test.* grammar/test - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ ## Support of Camlp5 and Camlp5 @@ -307,7 +307,7 @@ coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -317,7 +317,7 @@ $(COQTOPEXE): $(COQTOPBYTE) endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ # coqmktop @@ -667,7 +667,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; %: @echo "Error: no rule to make target $@ (or missing .PHONY)" && false -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: @@ -1,6 +1,6 @@ # Coq -[](https://travis-ci.org/coq/coq/builds) [](https://gitter.im/coq/coq) +[](https://travis-ci.org/coq/coq/builds) [](https://gitter.im/coq/coq) Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an diff --git a/configure.ml b/configure.ml index c75c3d7e1..9976c19d4 100644 --- a/configure.ml +++ b/configure.ml @@ -11,7 +11,7 @@ #load "str.cma" open Printf -let coq_version = "trunk" +let coq_version = "8.7.0~alpha" let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8691 diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 99ec43e41..91337b901 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -91,8 +91,8 @@ ######################################################################## # fiat_crypto ######################################################################## -: ${fiat_crypto_CI_BRANCH:=less_init_plugins} -: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git} +: ${fiat_crypto_CI_BRANCH:=master} +: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} ######################################################################## # formal-topology diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 0dd904648..4cfe0911b 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -9,4 +9,5 @@ opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} # Patch to avoid the upper version limit -( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make ) +( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make ) + diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex deleted file mode 100644 index 43bd2419f..000000000 --- a/doc/refman/RefMan-ind.tex +++ /dev/null @@ -1,510 +0,0 @@ - -%\documentstyle[11pt]{article} -%\input{title} - -%\include{macros} -%\makeindex - -%\begin{document} -%\coverpage{The module {\tt Equality}}{Cristina CORNES} - -%\tableofcontents - -\chapter[Tactics for inductive types and families]{Tactics for inductive types and families\label{Addoc-equality}} - -This chapter details a few special tactics useful for inferring facts -from inductive hypotheses. They can be considered as tools that -macro-generate complicated uses of the basic elimination tactics for -inductive types. - -Sections \ref{inversion_introduction} to \ref{inversion_using} present -inversion tactics and Section~\ref{scheme} describes -a command {\tt Scheme} for automatic generation of induction schemes -for mutual inductive types. - -%\end{document} -%\documentstyle[11pt]{article} -%\input{title} - -%\begin{document} -%\coverpage{Module Inv: Inversion Tactics}{Cristina CORNES} - -\section[Generalities about inversion]{Generalities about inversion\label{inversion_introduction}} -When working with (co)inductive predicates, we are very often faced to -some of these situations: -\begin{itemize} -\item we have an inconsistent instance of an inductive predicate in the - local context of hypotheses. Thus, the current goal can be trivially - proved by absurdity. - -\item we have a hypothesis that is an instance of an inductive - predicate, and the instance has some variables whose constraints we - would like to derive. -\end{itemize} - -The inversion tactics are very useful to simplify the work in these -cases. Inversion tools can be classified in three groups: -\begin{enumerate} -\item tactics for inverting an instance without stocking the inversion - lemma in the context: - (\texttt{Dependent}) \texttt{Inversion} and - (\texttt{Dependent}) \texttt{Inversion\_clear}. -\item commands for generating and stocking in the context the inversion - lemma corresponding to an instance: \texttt{Derive} - (\texttt{Dependent}) \texttt{Inversion}, \texttt{Derive} - (\texttt{Dependent}) \texttt{Inversion\_clear}. -\item tactics for inverting an instance using an already defined - inversion lemma: \texttt{Inversion \ldots using}. -\end{enumerate} - -These tactics work for inductive types of arity $(\vec{x}:\vec{T})s$ -where $s \in \{Prop,Set,Type\}$. Sections \ref{inversion_primitive}, -\ref{inversion_derivation} and \ref{inversion_using} -describe respectively each group of tools. - -As inversion proofs may be large in size, we recommend the user to -stock the lemmas whenever the same instance needs to be inverted -several times.\\ - -Let's consider the relation \texttt{Le} over natural numbers and the -following variables: - -\begin{coq_eval} -Restore State "Initial". -\end{coq_eval} - -\begin{coq_example*} -Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0%N n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). -Variable P : nat -> nat -> Prop. -Variable Q : forall n m:nat, Le n m -> Prop. -\end{coq_example*} - -For example purposes we defined \verb+Le: nat->nat->Set+ - but we may have defined -it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+. - - -\section[Inverting an instance]{Inverting an instance\label{inversion_primitive}} -\subsection{The non dependent case} -\begin{itemize} - -\item \texttt{Inversion\_clear} \ident~\\ -\index{Inversion-clear@{\tt Inversion\_clear}} - Let the type of \ident~ in the local context be $(I~\vec{t})$, - where $I$ is a (co)inductive predicate. Then, - \texttt{Inversion} applied to \ident~ derives for each possible - constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary - conditions that should hold for the instance $(I~\vec{t})$ to be - proved by $c_i$. Finally it erases \ident~ from the context. - - - -For example, consider the goal: -\begin{coq_eval} -Lemma ex : forall n m:nat, Le (S n) m -> P n m. -intros. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} - -To prove the goal we may need to reason by cases on \texttt{H} and to - derive that \texttt{m} is necessarily of -the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$. -Deriving these conditions corresponds to prove that the -only possible constructor of \texttt{(Le (S n) m)} is -\texttt{LeS} and that we can invert the -\texttt{->} in the type of \texttt{LeS}. -This inversion is possible because \texttt{Le} is the smallest set closed by -the constructors \texttt{LeO} and \texttt{LeS}. - - -\begin{coq_example} -inversion_clear H. -\end{coq_example} - -Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)} -and that the hypothesis \texttt{(Le n m0)} has been added to the -context. - -\item \texttt{Inversion} \ident~\\ -\index{Inversion@{\tt Inversion}} - This tactic differs from {\tt Inversion\_clear} in the fact that - it adds the equality constraints in the context and - it does not erase the hypothesis \ident. - - -In the previous example, {\tt Inversion\_clear} -has substituted \texttt{m} by \texttt{(S m0)}. Sometimes it is -interesting to have the equality \texttt{m=(S m0)} in the -context to use it after. In that case we can use \texttt{Inversion} that -does not clear the equalities: - -\begin{coq_example*} -Undo. -\end{coq_example*} -\begin{coq_example} -inversion H. -\end{coq_example} - -\begin{coq_eval} -Undo. -\end{coq_eval} - -Note that the hypothesis \texttt{(S m0)=m} has been deduced and -\texttt{H} has not been cleared from the context. - -\end{itemize} - -\begin{Variants} - -\item \texttt{Inversion\_clear } \ident~ \texttt{in} \ident$_1$ \ldots - \ident$_n$\\ -\index{Inversion_clear...in@{\tt Inversion\_clear...in}} - Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This - tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing - {\tt Inversion\_clear}. - -\item \texttt{Inversion } \ident~ \texttt{in} \ident$_1$ \ldots \ident$_n$\\ -\index{Inversion ... in@{\tt Inversion ... in}} - Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This - tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing - \texttt{Inversion}. - - -\item \texttt{Simple Inversion} \ident~ \\ -\index{Simple Inversion@{\tt Simple Inversion}} - It is a very primitive inversion tactic that derives all the necessary - equalities but it does not simplify - the constraints as \texttt{Inversion} and - {\tt Inversion\_clear} do. - -\end{Variants} - - -\subsection{The dependent case} -\begin{itemize} -\item \texttt{Dependent Inversion\_clear} \ident~\\ -\index{Dependent Inversion-clear@{\tt Dependent Inversion\_clear}} - Let the type of \ident~ in the local context be $(I~\vec{t})$, - where $I$ is a (co)inductive predicate, and let the goal depend both on - $\vec{t}$ and \ident. Then, - \texttt{Dependent Inversion\_clear} applied to \ident~ derives - for each possible constructor $c_i$ of $(I~\vec{t})$, {\bf all} the - necessary conditions that should hold for the instance $(I~\vec{t})$ to be - proved by $c_i$. It also substitutes \ident~ for the corresponding - term in the goal and it erases \ident~ from the context. - - -For example, consider the goal: -\begin{coq_eval} -Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H. -intros. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} - -As \texttt{H} occurs in the goal, we may want to reason by cases on its -structure and so, we would like inversion tactics to -substitute \texttt{H} by the corresponding term in constructor form. -Neither \texttt{Inversion} nor {\tt Inversion\_clear} make such a -substitution. To have such a behavior we use the dependent inversion tactics: - -\begin{coq_example} -dependent inversion_clear H. -\end{coq_example} - -Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and -\texttt{m} by \texttt{(S m0)}. - - -\end{itemize} - -\begin{Variants} - -\item \texttt{Dependent Inversion\_clear } \ident~ \texttt{ with } \term\\ -\index{Dependent Inversion_clear...with@{\tt Dependent Inversion\_clear...with}} - \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows giving - explicitly the good generalization of the goal. It is useful when - the system fails to generalize the goal automatically. If - \ident~ has type $(I~\vec{t})$ and $I$ has type - $(\vec{x}:\vec{T})s$, then \term~ must be of type - $I:(\vec{x}:\vec{T})(I~\vec{x})\rightarrow s'$ where $s'$ is the - type of the goal. - - - -\item \texttt{Dependent Inversion} \ident~\\ -\index{Dependent Inversion@{\tt Dependent Inversion}} - This tactic differs from \texttt{Dependent Inversion\_clear} in the fact that - it also adds the equality constraints in the context and - it does not erase the hypothesis \ident~. - -\item \texttt{Dependent Inversion } \ident~ \texttt{ with } \term \\ -\index{Dependent Inversion...with@{\tt Dependent Inversion...with}} - Analogous to \texttt{Dependent Inversion\_clear .. with..} above. -\end{Variants} - - - -\section[Deriving the inversion lemmas]{Deriving the inversion lemmas\label{inversion_derivation}} -\subsection{The non dependent case} - -The tactics (\texttt{Dependent}) \texttt{Inversion} and (\texttt{Dependent}) -{\tt Inversion\_clear} work on a -certain instance $(I~\vec{t})$ of an inductive predicate. At each -application, they inspect the given instance and derive the -corresponding inversion lemma. If we have to invert the same -instance several times it is recommended to stock the lemma in the -context and to reuse it whenever we need it. - -The families of commands \texttt{Derive Inversion}, \texttt{Derive -Dependent Inversion}, \texttt{Derive} \\ {\tt Inversion\_clear} and \texttt{Derive Dependent Inversion\_clear} -allow to generate inversion lemmas for given instances and sorts. Next -section describes the tactic \texttt{Inversion}$\ldots$\texttt{using} that refines the -goal with a specified inversion lemma. - -\begin{itemize} - -\item \texttt{Derive Inversion\_clear} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ -\index{Derive Inversion_clear...with@{\tt Derive Inversion\_clear...with}} - Let $I$ be an inductive predicate and $\vec{x}$ the variables - occurring in $\vec{t}$. This command generates and stocks - the inversion lemma for the sort \sort~ corresponding to the instance - $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf - global} environment. When applied it is equivalent to have - inverted the instance with the tactic {\tt Inversion\_clear}. - - - For example, to generate the inversion lemma for the instance - \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do: -\begin{coq_example} -Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort - Prop. -\end{coq_example} - -Let us inspect the type of the generated lemma: -\begin{coq_example} -Check leminv. -\end{coq_example} - - - -\end{itemize} - -%\variants -%\begin{enumerate} -%\item \verb+Derive Inversion_clear+ \ident$_1$ \ident$_2$ \\ -%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}} -% Let \ident$_1$ have type $(I~\vec{t})$ in the local context ($I$ -% an inductive predicate). Then, this command has the same semantics -% as \verb+Derive Inversion_clear+ \ident$_2$~ \verb+with+ -% $(\vec{x}:\vec{T})(I~\vec{t})$ \verb+Sort Prop+ where $\vec{x}$ are the free -% variables of $(I~\vec{t})$ declared in the local context (variables -% of the global context are considered as constants). -%\item \verb+Derive Inversion+ \ident$_1$~ \ident$_2$~\\ -%\index{Derive Inversion@{\tt Derive Inversion}} -% Analogous to the previous command. -%\item \verb+Derive Inversion+ $num$ \ident~ \ident~ \\ -%\index{Derive Inversion@{\tt Derive Inversion}} -% This command behaves as \verb+Derive Inversion+ \ident~ {\it -% namehyp} performed on the goal number $num$. -% -%\item \verb+Derive Inversion_clear+ $num$ \ident~ \ident~ \\ -%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}} -% This command behaves as \verb+Derive Inversion_clear+ \ident~ -% \ident~ performed on the goal number $num$. -%\end{enumerate} - - - -A derived inversion lemma is adequate for inverting the instance -with which it was generated, \texttt{Derive} applied to -different instances yields different lemmas. In general, if we generate -the inversion lemma with -an instance $(\vec{x}:\vec{T})(I~\vec{t})$ and a sort $s$, the inversion lemma will -expect a predicate of type $(\vec{x}:\vec{T})s$ as first argument. \\ - -\begin{Variant} -\item \texttt{Derive Inversion} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort\\ -\index{Derive Inversion...with@{\tt Derive Inversion...with}} - Analogous of \texttt{Derive Inversion\_clear .. with ..} but - when applied it is equivalent to having - inverted the instance with the tactic \texttt{Inversion}. -\end{Variant} - -\subsection{The dependent case} -\begin{itemize} -\item \texttt{Derive Dependent Inversion\_clear} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ -\index{Derive Dependent Inversion\_clear...with@{\tt Derive Dependent Inversion\_clear...with}} - Let $I$ be an inductive predicate. This command generates and stocks - the dependent inversion lemma for the sort \sort~ corresponding to the instance - $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf - global} environment. When applied it is equivalent to having - inverted the instance with the tactic \texttt{Dependent Inversion\_clear}. -\end{itemize} - -\begin{coq_example} -Derive Dependent Inversion_clear leminv_dep with - (forall n m:nat, Le (S n) m) Sort Prop. -\end{coq_example} - -\begin{coq_example} -Check leminv_dep. -\end{coq_example} - -\begin{Variants} -\item \texttt{Derive Dependent Inversion} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ -\index{Derive Dependent Inversion...with@{\tt Derive Dependent Inversion...with}} - Analogous to \texttt{Derive Dependent Inversion\_clear}, but when - applied it is equivalent to having - inverted the instance with the tactic \texttt{Dependent Inversion}. - -\end{Variants} - -\section[Using already defined inversion lemmas]{Using already defined inversion lemmas\label{inversion_using}} -\begin{itemize} -\item \texttt{Inversion} \ident \texttt{ using} \ident$'$ \\ -\index{Inversion...using@{\tt Inversion...using}} - Let \ident~ have type $(I~\vec{t})$ ($I$ an inductive - predicate) in the local context, and \ident$'$ be a (dependent) inversion - lemma. Then, this tactic refines the current goal with the specified - lemma. - - -\begin{coq_eval} -Abort. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} -\begin{coq_example} -inversion H using leminv. -\end{coq_example} - - -\end{itemize} -\variant -\begin{enumerate} -\item \texttt{Inversion} \ident~ \texttt{using} \ident$'$ \texttt{in} \ident$_1$\ldots \ident$_n$\\ -\index{Inversion...using...in@{\tt Inversion...using...in}} -This tactic behaves as generalizing \ident$_1$\ldots \ident$_n$, -then doing \texttt{Use Inversion} \ident~\ident$'$. -\end{enumerate} - -\section[\tt Scheme ...]{\tt Scheme ...\index{Scheme@{\tt Scheme}}\label{Scheme} -\label{scheme}} -The {\tt Scheme} command is a high-level tool for generating -automatically (possibly mutual) induction principles for given types -and sorts. Its syntax follows the schema : - -\noindent -{\tt Scheme {\ident$_1$} := Induction for \term$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} .. \\ - with {\ident$_m$} := Induction for {\term$_m$} Sort - {\sort$_m$}}\\ -\term$_1$ \ldots \term$_m$ are different inductive types belonging to -the same package of mutual inductive definitions. This command -generates {\ident$_1$}\ldots{\ident$_m$} to be mutually recursive -definitions. Each term {\ident$_i$} proves a general principle -of mutual induction for objects in type {\term$_i$}. - -\Example -The definition of principle of mutual induction for {\tt tree} and -{\tt forest} over the sort {\tt Set} is defined by the command: -\begin{coq_eval} -Restore State "Initial". -Variables A B : Set. -Inductive tree : Set := - node : A -> forest -> tree -with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. -\end{coq_eval} -\begin{coq_example*} -Scheme tree_forest_rec := Induction for tree - Sort Set - with forest_tree_rec := Induction for forest Sort Set. -\end{coq_example*} -You may now look at the type of {\tt tree\_forest\_rec} : -\begin{coq_example} -Check tree_forest_rec. -\end{coq_example} -This principle involves two different predicates for {\tt trees} and -{\tt forests}; it also has three premises each one corresponding to a -constructor of one of the inductive definitions. - -The principle {\tt tree\_forest\_rec} shares exactly the same -premises, only the conclusion now refers to the property of forests. -\begin{coq_example} -Check forest_tree_rec. -\end{coq_example} - -\begin{Variant} -\item {\tt Scheme {\ident$_1$} := Minimality for \term$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} .. \\ - with {\ident$_m$} := Minimality for {\term$_m$} Sort - {\sort$_m$}}\\ -Same as before but defines a non-dependent elimination principle more -natural in case of inductively defined relations. -\end{Variant} - -\Example -With the predicates {\tt odd} and {\tt even} inductively defined as: -% \begin{coq_eval} -% Restore State "Initial". -% \end{coq_eval} -\begin{coq_example*} -Inductive odd : nat -> Prop := - oddS : forall n:nat, even n -> odd (S n) -with even : nat -> Prop := - | evenO : even 0%N - | evenS : forall n:nat, odd n -> even (S n). -\end{coq_example*} -The following command generates a powerful elimination -principle: -\begin{coq_example*} -Scheme odd_even := Minimality for odd Sort Prop - with even_odd := Minimality for even Sort Prop. -\end{coq_example*} -The type of {\tt odd\_even} for instance will be: -\begin{coq_example} -Check odd_even. -\end{coq_example} -The type of {\tt even\_odd} shares the same premises but the -conclusion is {\tt (n:nat)(even n)->(Q n)}. - -\subsection[\tt Combined Scheme ...]{\tt Combined Scheme ...\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme} -\label{combinedscheme}} -The {\tt Combined Scheme} command is a tool for combining -induction principles generated by the {\tt Scheme} command. -Its syntax follows the schema : - -\noindent -{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\ -\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to -the same package of mutual inductive principle definitions. This command -generates {\ident$_0$} to be the conjunction of the principles: it is -build from the common premises of the principles and concluded by the -conjunction of their conclusions. For exemple, we can combine the -induction principles for trees and forests: - -\begin{coq_example*} -Combined Scheme tree_forest_mutind from tree_ind, forest_ind. -Check tree_forest_mutind. -\end{coq_example*} - -%\end{document} - diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 30b6304c1..8337b1c48 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -23,7 +23,7 @@ of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. It runs as a computer program on many architectures. -%, and mainly on Unix machines. + It is available with a variety of user interfaces. The present document does not attempt to present a comprehensive view of all the possibilities of \Coq, but rather to present in the most elementary @@ -33,63 +33,34 @@ proof tools. For more advanced information, the reader could refer to the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y. Bertot and P. Castéran on practical uses of the \Coq{} system. -Coq can be used from a standard teletype-like shell window but -preferably through the graphical user interface -CoqIde\footnote{Alternative graphical interfaces exist: Proof General -and Pcoq.}. - Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of \Coq, -which may be obtained from \Coq{} web site \url{https://coq.inria.fr/}. - -In the following, we assume that \Coq{} is called from a standard -teletype-like shell window. All examples preceded by the prompting -sequence \verb:Coq < : represent user input, terminated by a -period. - -The following lines usually show \Coq's answer as it appears on the -users screen. When used from a graphical user interface such as -CoqIde, the prompt is not displayed: user input is given in one window +which may be obtained from \Coq{} web site +\url{https://coq.inria.fr/}\footnote{You can report any bug you find +while using \Coq{} at \url{https://coq.inria.fr/bugs}. Make sure to +always provide a way to reproduce it and to specify the exact version +you used. You can get this information by running \texttt{coqc -v}}. +\Coq{} is distributed together with a graphical user interface called +CoqIDE. Alternative interfaces exist such as +Proof General\footnote{See \url{https://proofgeneral.github.io/}.}. + +In the following examples, lines preceded by the prompt \verb:Coq < : +represent user input, terminated by a period. +The following lines usually show \Coq's answer. +When used from a graphical user interface such as +CoqIDE, the prompt is not displayed: user input is given in one window and \Coq's answers are displayed in a different window. -The sequence of such examples is a valid \Coq{} -session, unless otherwise specified. This version of the tutorial has -been prepared on a PC workstation running Linux. The standard -invocation of \Coq{} delivers a message such as: - -\begin{small} -\begin{flushleft} -\begin{verbatim} -unix:~> coqtop -Welcome to Coq 8.2 (January 2009) - -Coq < -\end{verbatim} -\end{flushleft} -\end{small} - -The first line gives a banner stating the precise version of \Coq{} -used. You should always return this banner when you report an anomaly -to our bug-tracking system -\url{https://coq.inria.fr/bugs/}. - \chapter{Basic Predicate Calculus} \section{An overview of the specification language Gallina} A formal development in Gallina consists in a sequence of {\sl declarations} -and {\sl definitions}. You may also send \Coq{} {\sl commands} which are -not really part of the formal development, but correspond to information -requests, or service routine invocations. For instance, the command: -\begin{verbatim} -Coq < Quit. -\end{verbatim} -terminates the current session. +and {\sl definitions}. \subsection{Declarations} -A declaration associates a {\sl name} with -a {\sl specification}. +A declaration associates a {\sl name} with a {\sl specification}. A name corresponds roughly to an identifier in a programming language, i.e. to a string of letters, digits, and a few ASCII symbols like underscore (\verb"_") and prime (\verb"'"), starting with a letter. @@ -165,25 +136,25 @@ in the current context: Check gt. \end{coq_example} -which tells us that \verb:gt: is a function expecting two arguments of -type \verb:nat: in order to build a logical proposition. +which tells us that \texttt{gt} is a function expecting two arguments of +type \texttt{nat} in order to build a logical proposition. What happens here is similar to what we are used to in a functional -programming language: we may compose the (specification) type \verb:nat: -with the (abstract) type \verb:Prop: of logical propositions through the +programming language: we may compose the (specification) type \texttt{nat} +with the (abstract) type \texttt{Prop} of logical propositions through the arrow function constructor, in order to get a functional type -\verb:nat->Prop:: +\texttt{nat -> Prop}: \begin{coq_example} Check (nat -> Prop). \end{coq_example} -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 the type \verb:nat->nat->Prop: is an abbreviation for -\verb:nat->(nat->Prop):. +which may be composed once more with \verb:nat: in order to obtain the +type \texttt{nat -> nat -> Prop} of binary relations over natural numbers. +Actually the type \texttt{nat -> nat -> Prop} is an abbreviation for +\texttt{nat -> (nat -> Prop)}. Functional notions may be composed in the usual way. An expression $f$ of type $A\ra B$ may be applied to an expression $e$ of type $A$ in order to form the expression $(f~e)$ of type $B$. Here we get that -the expression \verb:(gt n): is well-formed of type \verb:nat->Prop:, +the expression \verb:(gt n): is well-formed of type \texttt{nat -> Prop}, and thus that the expression \verb:(gt n O):, which abbreviates \verb:((gt n) O):, is a well-formed proposition. \begin{coq_example} @@ -193,11 +164,12 @@ Check gt n O. \subsection{Definitions} The initial prelude contains a few arithmetic definitions: -\verb:nat: is defined as a mathematical collection (type \verb:Set:), constants -\verb:O:, \verb:S:, \verb:plus:, are defined as objects of types -respectively \verb:nat:, \verb:nat->nat:, and \verb:nat->nat->nat:. +\texttt{nat} is defined as a mathematical collection (type \texttt{Set}), +constants \texttt{O}, \texttt{S}, \texttt{plus}, are defined as objects of +types respectively \texttt{nat}, \texttt{nat -> nat}, and \texttt{nat -> +nat -> nat}. You may introduce new definitions, which link a name to a well-typed value. -For instance, we may introduce the constant \verb:one: as being defined +For instance, we may introduce the constant \texttt{one} as being defined to be equal to the successor of zero: \begin{coq_example} Definition one := (S O). @@ -217,17 +189,18 @@ argument \verb:m: of type \verb:nat: in order to build its result as \verb:(plus m m):: \begin{coq_example} -Definition double (m:nat) := plus m m. +Definition double (m : nat) := plus m m. \end{coq_example} 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 -whenever the expression \verb+e+ is well-formed of type \verb+B+ in -the given context to which we add the declaration that \verb+x+ -is of type \verb+A+. Here \verb+x+ is a bound, or dummy variable in -the expression \verb+fun x:A => e+. For instance we could as well have -defined \verb:double: as \verb+fun n:nat => (plus n n)+. +expression \texttt{fun m : nat => plus m m}. +The abstraction introduced by \texttt{fun} is explained as follows. +The expression \texttt{fun x : A => e} is well formed of type +\texttt{A -> B} in a context whenever the expression \texttt{e} is +well-formed of type \texttt{B} in the given context to which we add the +declaration that \texttt{x} is of type \texttt{A}. Here \texttt{x} is a +bound, or dummy variable in the expression \texttt{fun x : A => e}. +For instance we could as well have defined \texttt{double} as +\texttt{fun n : nat => (plus n n)}. Bound (local) variables and free (global) variables may be mixed. For instance, we may define the function which adds the constant \verb:n: @@ -243,19 +216,17 @@ Binding operations are well known for instance in logic, where they are called quantifiers. Thus we may universally quantify a proposition such as $m>0$ in order to get a universal proposition $\forall m\cdot m>0$. Indeed this operator is available in \Coq, with -the following syntax: \verb+forall m:nat, gt m O+. Similarly to the +the following syntax: \texttt{forall m : nat, gt m O}. Similarly to the case of the functional abstraction binding, we are obliged to declare explicitly the type of the quantified variable. We check: \begin{coq_example} -Check (forall m:nat, gt m 0). -\end{coq_example} -We may revert to the clean state of -our initial session using the \Coq{} \verb:Reset: command: -\begin{coq_example} -Reset Initial. +Check (forall m : nat, gt m 0). \end{coq_example} + \begin{coq_eval} +Reset Initial. Set Printing Width 60. +Set Printing Compact Contexts. \end{coq_eval} \section{Introduction to the proof engine: Minimal Logic} @@ -340,17 +311,12 @@ the current goal is solvable from the current local assumptions: assumption. \end{coq_example} -The proof is now finished. We may either discard it, by using the -command \verb:Abort: which returns to the standard \Coq{} toplevel loop -without further ado, or else save it as a lemma in the current context, -under name say \verb:trivial_lemma:: +The proof is now finished. We are now going to ask \Coq{}'s kernel +to check and save the proof. \begin{coq_example} -Save trivial_lemma. +Qed. \end{coq_example} -As a comment, the system shows the proof script listing all tactic -commands used in the proof. - Let us redo the same proof with a few variations. First of all we may name the initial goal as a conjectured lemma: \begin{coq_example} @@ -383,46 +349,30 @@ We may thus complete the proof of \verb:distr_impl: with one composite tactic: apply H; [ assumption | apply H0; assumption ]. \end{coq_example} -Let us now save lemma \verb:distr_impl:: -\begin{coq_example} -Qed. -\end{coq_example} - -Here \verb:Qed: needs no argument, since we gave the name \verb:distr_impl: -in advance. +You should be aware however that relying on automatically generated names is +not robust to slight updates to this proof script. Consequently, it is +discouraged in finished proof scripts. As for the composition of tactics with +\texttt{:} it may hinder the readability of the proof script and it is also +harder to see what's going on when replaying the proof because composed +tactics are evaluated in one go. Actually, such an easy combination of tactics \verb:intro:, \verb:apply: and \verb:assumption: may be found completely automatically by an automatic tactic, called \verb:auto:, without user guidance: -\begin{coq_example} -Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C. -auto. -\end{coq_example} - -This time, we do not save the proof, we just discard it with the \verb:Abort: -command: -\begin{coq_example} +\begin{coq_eval} Abort. +\end{coq_eval} +\begin{coq_example} +Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C. +auto. \end{coq_example} -At any point during a proof, we may use \verb:Abort: to exit the proof mode -and go back to Coq's main loop. We may also use \verb:Restart: to restart -from scratch the proof of the same lemma. We may also use \verb:Undo: to -backtrack one step, and more generally \verb:Undo n: to -backtrack n steps. - -We end this section by showing a useful command, \verb:Inspect n.:, -which inspects the global \Coq{} environment, showing the last \verb:n: declared -notions: +Let us now save lemma \verb:distr_impl:: \begin{coq_example} -Inspect 3. +Qed. \end{coq_example} -The declarations, whether global parameters or axioms, are shown preceded by -\verb:***:; definitions and lemmas are stated with their specification, but -their value (or proof-term) is omitted. - \section{Propositional Calculus} \subsection{Conjunction} @@ -438,7 +388,7 @@ connective. Let us show how to use these ideas for the propositional connectives \begin{coq_example} Lemma and_commutative : A /\ B -> B /\ A. -intro. +intro H. \end{coq_example} We make use of the conjunctive hypothesis \verb:H: with the \verb:elim: tactic, @@ -453,8 +403,11 @@ conjunctive goal into the two subgoals: split. \end{coq_example} and the proof is now trivial. Indeed, the whole proof is obtainable as follows: +\begin{coq_eval} +Abort. +\end{coq_eval} \begin{coq_example} -Restart. +Lemma and_commutative : A /\ B -> B /\ A. intro H; elim H; auto. Qed. \end{coq_example} @@ -465,7 +418,7 @@ conjunction introduction operator \verb+conj+ Check conj. \end{coq_example} -Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+ +Actually, the tactic \verb+split+ is just an abbreviation for \verb+apply conj.+ What we have just seen is that the \verb:auto: tactic is more powerful than just a simple application of local hypotheses; it tries to apply as well @@ -498,6 +451,17 @@ clear away unnecessary hypotheses which may clutter your screen. clear H. \end{coq_example} +The tactic \verb:destruct: combines the effects of \verb:elim:, \verb:intros:, +and \verb:clear:: + +\begin{coq_eval} +Abort. +\end{coq_eval} +\begin{coq_example} +Lemma or_commutative : A \/ B -> B \/ A. +intros H; destruct H. +\end{coq_example} + The disjunction connective has two introduction rules, since \verb:P\/Q: may be obtained from \verb:P: or from \verb:Q:; the two corresponding proof constructors are called respectively \verb:or_introl: and @@ -528,8 +492,11 @@ such a simple tautology. The reason is that we want to keep A complete tactic for propositional tautologies is indeed available in \Coq{} as the \verb:tauto: tactic. +\begin{coq_eval} +Abort. +\end{coq_eval} \begin{coq_example} -Restart. +Lemma or_commutative : A \/ B -> B \/ A. tauto. Qed. \end{coq_example} @@ -541,8 +508,8 @@ currently defined in the context: Print or_commutative. \end{coq_example} -It is not easy to understand the notation for proof terms without a few -explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+, +It is not easy to understand the notation for proof terms without some +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): @@ -572,15 +539,17 @@ Lemma Peirce : ((A -> B) -> A) -> A. try tauto. \end{coq_example} -Note the use of the \verb:Try: tactical, which does nothing if its tactic +Note the use of the \verb:try: tactical, which does nothing if its tactic argument fails. This may come as a surprise to someone familiar with classical reasoning. Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation of Peirce's law may be proved in \Coq{} using \verb:tauto:: -\begin{coq_example} +\begin{coq_eval} Abort. +\end{coq_eval} +\begin{coq_example} Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A). tauto. Qed. @@ -651,26 +620,20 @@ function and predicate symbols. \subsection{Sections and signatures} Usually one works in some domain of discourse, over which range the individual -variables and function symbols. In \Coq{} we speak in a language with a rich -variety of types, so me may mix several domains of discourse, in our +variables and function symbols. In \Coq{}, we speak in a language with a rich +variety of types, so we may mix several domains of discourse, in our multi-sorted language. For the moment, we just do a few exercises, over a domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two predicate symbols \verb:P: and \verb:R: over \verb:D:, of arities -respectively 1 and 2. Such abstract entities may be entered in the context -as global variables. But we must be careful about the pollution of our -global environment by such declarations. For instance, we have already -polluted our \Coq{} session by declaring the variables -\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. +1 and 2, respectively. -\begin{coq_example} -Reset Initial. -\end{coq_example} \begin{coq_eval} +Reset Initial. Set Printing Width 60. +Set Printing Compact Contexts. \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 +We start by assuming a domain of discourse \verb:D:, and a binary relation \verb:R: over \verb:D:: \begin{coq_example} Section Predicate_calculus. @@ -686,18 +649,19 @@ a theory, but rather local hypotheses to a theorem, we open a specific section to this effect. \begin{coq_example} Section R_sym_trans. -Hypothesis R_symmetric : forall x y:D, R x y -> R y x. -Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z. +Hypothesis R_symmetric : forall x y : D, R x y -> R y x. +Hypothesis R_transitive : + forall x y z : D, R x y -> R y z -> R x z. \end{coq_example} -Remark the syntax \verb+forall x:D,+ which stands for universal quantification +Remark the syntax \verb+forall x : D,+ which stands for universal quantification $\forall x : D$. \subsection{Existential quantification} We now state our lemma, and enter proof mode. \begin{coq_example} -Lemma refl_if : forall x:D, (exists y, R x y) -> R x x. +Lemma refl_if : forall x : D, (exists y, R x y) -> R x x. \end{coq_example} Remark that the hypotheses which are local to the currently opened sections @@ -711,13 +675,13 @@ predicate as argument: \begin{coq_example} Check ex. \end{coq_example} -and the notation \verb+(exists x:D, P x)+ is just concrete syntax for -the expression \verb+(ex D (fun x:D => P x))+. +and the notation \verb+(exists x : D, P x)+ is just concrete syntax for +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 +fashion to the connectives \verb:/\: and \verb:\/:: it is introduced by the proof combinator \verb:ex_intro:, which is invoked by the specific -tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to -\verb:P:, together with an assumption \verb+h:(P a)+ that indeed \verb+a+ +tactic \verb:exists:, and its elimination provides a witness \verb+a : D+ to +\verb:P:, together with an assumption \verb+h : (P a)+ that indeed \verb+a+ verifies \verb:P:. Let us see how this works on this simple example. \begin{coq_example} intros x x_Rlinked. @@ -773,8 +737,8 @@ End R_sym_trans. All the local hypotheses have been discharged in the statement of \verb:refl_if:, which now becomes a general theorem in the first-order language declared in section -\verb:Predicate_calculus:. In this particular example, the use of section -\verb:R_sym_trans: has not been really significant, since we could have +\verb:Predicate_calculus:. In this particular example, section +\verb:R_sym_trans: has not been really useful, since we could have instead stated theorem \verb:refl_if: in its general form, and done basically the same proof, obtaining \verb:R_symmetric: and \verb:R_transitive: as local hypotheses by initial \verb:intros: rather @@ -802,7 +766,7 @@ Lemma weird : (forall x:D, P x) -> exists a, P a. \end{coq_example} First of all, notice the pair of parentheses around -\verb+forall x:D, P x+ in +\verb+forall x : D, P x+ in the statement of lemma \verb:weird:. If we had omitted them, \Coq's parser would have interpreted the statement as a truly trivial fact, since we would @@ -820,7 +784,7 @@ systematically inhabited, lemma \verb:weird: only holds in signatures which allow the explicit construction of an element in the domain of the predicate. -Let us conclude the proof, in order to show the use of the \verb:Exists: +Let us conclude the proof, in order to show the use of the \verb:exists: tactic: \begin{coq_example} exists d; trivial. @@ -836,8 +800,8 @@ We shall need classical reasoning. Instead of loading the \verb:Classical: module as we did above, we just state the law of excluded middle as a local hypothesis schema at this point: \begin{coq_example} -Hypothesis EM : forall A:Prop, A \/ ~ A. -Lemma drinker : exists x:D, P x -> forall x:D, P x. +Hypothesis EM : forall A : Prop, A \/ ~ A. +Lemma drinker : exists x : D, P x -> forall x : D, P x. \end{coq_example} The proof goes by cases on whether or not there is someone who does not drink. Such reasoning by cases proceeds @@ -847,10 +811,11 @@ proper instance of \verb:EM:: elim (EM (exists x, ~ P x)). \end{coq_example} -We first look at the first case. Let Tom be the non-drinker: +We first look at the first case. Let Tom be the non-drinker. +The following combines at once the effect of \verb:intros: and +\verb:destruct:: \begin{coq_example} -intro Non_drinker; elim Non_drinker; - intros Tom Tom_does_not_drink. +intros (Tom, Tom_does_not_drink). \end{coq_example} We conclude in that case by considering Tom, since his drinking leads to @@ -860,9 +825,10 @@ exists Tom; intro Tom_drinks. \end{coq_example} There are several ways in which we may eliminate a contradictory case; -a simple one is to use the \verb:absurd: tactic as follows: +in this case, we use \verb:contradiction: to let \Coq{} find out the +two contradictory hypotheses: \begin{coq_example} -absurd (P Tom); trivial. +contradiction. \end{coq_example} We now proceed with the second case, in which actually any person will do; @@ -904,9 +870,10 @@ Finally, the excluded middle hypothesis is discharged only in Note that the name \verb:d: has vanished as well from the statements of \verb:weird: and \verb:drinker:, since \Coq's pretty-printer replaces -systematically a quantification such as \verb+forall d:D, E+, where \verb:d: -does not occur in \verb:E:, by the functional notation \verb:D->E:. -Similarly the name \verb:EM: does not appear in \verb:drinker:. +systematically a quantification such as \texttt{forall d : D, E}, +where \texttt{d} does not occur in \texttt{E}, +by the functional notation \texttt{D -> E}. +Similarly the name \texttt{EM} does not appear in \texttt{drinker}. Actually, universal quantification, implication, as well as function formation, are @@ -935,12 +902,12 @@ intros. generalize H0. \end{coq_example} -Sometimes it may be convenient to use a lemma, although we do not have -a direct way to appeal to such an already proven fact. The tactic \verb:cut: -permits to use the lemma at this point, keeping the corresponding proof -obligation as a new subgoal: +Sometimes it may be convenient to state an intermediate fact. +The tactic \verb:assert: does this and introduces a new subgoal +for this fact to be proved first. The tactic \verb:enough: does +the same while keeping this goal for later. \begin{coq_example} -cut (R x x); trivial. +enough (R x x) by auto. \end{coq_example} We clean the goal by doing an \verb:Abort: command. \begin{coq_example*} @@ -951,10 +918,10 @@ Abort. \subsection{Equality} The basic equality provided in \Coq{} is Leibniz equality, noted infix like -\verb+x=y+, when \verb:x: and \verb:y: are two expressions of -type the same Set. The replacement of \verb:x: by \verb:y: in any -term is effected by a variety of tactics, such as \verb:rewrite: -and \verb:replace:. +\texttt{x = y}, when \texttt{x} and \texttt{y} are two expressions of +type the same Set. The replacement of \texttt{x} by \texttt{y} in any +term is effected by a variety of tactics, such as \texttt{rewrite} +and \texttt{replace}. Let us give a few examples of equality replacement. Let us assume that some arithmetic function \verb:f: is null in zero: @@ -1009,10 +976,14 @@ In case the equality $t=u$ generated by \verb:replace: $u$ \verb:with: $t$ is an assumption (possibly modulo symmetry), it will be automatically proved and the corresponding goal will not appear. For instance: -\begin{coq_example} + +\begin{coq_eval} Restart. -replace (f 0) with 0. -rewrite f10; rewrite foo; trivial. +\end{coq_eval} +\begin{coq_example} +Lemma L2 : f (f 1) = 0. +replace (f 1) with (f 0). +replace (f 0) with 0; trivial. Qed. \end{coq_example} @@ -1033,20 +1004,20 @@ predicates over some universe \verb:U:. For instance: \begin{coq_example} 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 element (x : U) (S : set) := S x. +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 relations over some abstract type \verb:T:, such as transitivity: \begin{coq_example} -Definition transitive (T:Type) (R:T -> T -> Prop) := - forall x y z:T, R x y -> R y z -> R x z. +Definition transitive (T : Type) (R : T -> T -> Prop) := + forall x y z : T, R x y -> R y z -> R x z. \end{coq_example} -Now, assume that we want to prove that \verb:subset: is a \verb:transitive: +We want to prove that \verb:subset: is a \verb:transitive: relation. \begin{coq_example} Lemma subset_transitive : transitive set subset. @@ -1071,9 +1042,12 @@ auto. \end{coq_example} Many variations on \verb:unfold: are provided in \Coq. For instance, -we may selectively unfold one designated occurrence: -\begin{coq_example} +instead of unfolding all occurrences of \verb:subset:, we may want to +unfold only one designated occurrence: +\begin{coq_eval} Undo 2. +\end{coq_eval} +\begin{coq_example} unfold subset at 2. \end{coq_example} @@ -1111,6 +1085,7 @@ are {\sl transparent}. \begin{coq_eval} Reset Initial. Set Printing Width 60. +Set Printing Compact Contexts. \end{coq_eval} \section{Data Types as Inductively Defined Mathematical Collections} @@ -1166,11 +1141,14 @@ right; trivial. \end{coq_example} Indeed, the whole proof can be done with the combination of the - \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:, + \verb:destruct:, which combines \verb:intro: and \verb:elim:, with good old \verb:auto:: +\begin{coq_eval} +Abort. +\end{coq_eval} \begin{coq_example} -Restart. -simple induction b; auto. +Lemma duality : forall b:bool, b = true \/ b = false. +destruct b; auto. Qed. \end{coq_example} @@ -1194,7 +1172,7 @@ Check nat_rec. Let us start by showing how to program the standard primitive recursion operator \verb:prim_rec: from the more general \verb:nat_rec:: \begin{coq_example} -Definition prim_rec := nat_rec (fun i:nat => nat). +Definition prim_rec := nat_rec (fun i : nat => nat). \end{coq_example} That is, instead of computing for natural \verb:i: an element of the indexed @@ -1205,22 +1183,27 @@ About prim_rec. \end{coq_example} Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we -get an apparently more complicated expression. Indeed the type of -\verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may -be checked in \Coq{} by command \verb:Eval Cbv Beta:, which $\beta$-reduces -an expression to its {\sl normal form}: +get an apparently more complicated expression. +In fact, the two types are convertible and one way of having the proper +type would be to do some computation before actually defining \verb:prim_rec: +as such: + +\begin{coq_eval} +Reset Initial. +Set Printing Width 60. +Set Printing Compact Contexts. +\end{coq_eval} + \begin{coq_example} -Eval cbv beta in - ((fun _:nat => nat) O -> - (forall y:nat, - (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) -> - forall n:nat, (fun _:nat => nat) n). +Definition prim_rec := + Eval compute in nat_rec (fun i : nat => nat). +About prim_rec. \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. + 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: @@ -1244,15 +1227,11 @@ Fixpoint plus (n m:nat) {struct n} : nat := end. \end{coq_example} -For the rest of the session, we shall clean up what we did so far with -types \verb:bool: and \verb:nat:, in order to use the initial definitions -given in \Coq's \verb:Prelude: module, and not to get confusing error -messages due to our redefinitions. We thus revert to the initial state: +\begin{coq_eval} \begin{coq_example} Reset Initial. -\end{coq_example} -\begin{coq_eval} Set Printing Width 60. +Set Printing Compact Contexts. \end{coq_eval} \subsection{Simple proofs by induction} @@ -1261,20 +1240,21 @@ 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 show that $n=n+0$. \begin{coq_example} -Lemma plus_n_O : forall n:nat, n = n + 0. +Lemma plus_n_O : forall n : nat, n = n + 0. intro n; elim n. \end{coq_example} -What happened was that \verb:elim n:, in order to construct a \verb:Prop: -(the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the -corresponding induction principle \verb:nat_ind: which we saw was indeed +What happened was that \texttt{elim n}, in order to construct a \texttt{Prop} +(the initial goal) from a \texttt{nat} (i.e. \texttt{n}), appealed to the +corresponding induction principle \texttt{nat\_ind} which we saw was indeed exactly Peano's induction scheme. Pattern-matching instantiated the -corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get -as subgoals the corresponding instantiations of the base case \verb:(P O): , -and of the inductive step \verb+forall y:nat, P y -> P (S y)+. -In each case we get an instance of function \verb:plus: in which its second +corresponding predicate \texttt{P} to \texttt{fun n : nat => n = n + 0}, +and we get as subgoals the corresponding instantiations of the base case +\texttt{(P O)}, and of the inductive step +\texttt{forall y : nat, P y -> P (S y)}. +In each case we get an instance of function \texttt{plus} in which its second argument starts with a constructor, and is thus amenable to simplification -by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for +by primitive recursion. The \Coq{} tactic \texttt{simpl} can be used for this purpose: \begin{coq_example} simpl. @@ -1305,12 +1285,12 @@ We now proceed to the similar property concerning the other constructor Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m. \end{coq_example} -We now go faster, remembering that tactic \verb:simple induction: does the +We now go faster, using the tactic \verb:induction:, which does the necessary \verb:intros: before applying \verb:elim:. Factoring simplification and automation in both cases thanks to tactic composition, we prove this lemma in one line: \begin{coq_example} -simple induction n; simpl; auto. +induction n; simpl; auto. Qed. Hint Resolve plus_n_S . \end{coq_example} @@ -1324,7 +1304,7 @@ Lemma plus_com : forall n m:nat, n + m = m + n. Here we have a choice on doing an induction on \verb:n: or on \verb:m:, the situation being symmetric. For instance: \begin{coq_example} -simple induction m; simpl; auto. +induction m as [ | m IHm ]; simpl; auto. \end{coq_example} Here \verb:auto: succeeded on the base case, thanks to our hint @@ -1332,7 +1312,7 @@ Here \verb:auto: succeeded on the base case, thanks to our hint \verb:auto: does not handle: \begin{coq_example} -intros m' E; rewrite <- E; auto. +rewrite <- IHm; auto. Qed. \end{coq_example} @@ -1344,13 +1324,13 @@ the constructors \verb:O: and \verb:S:: it computes to \verb:False: when its argument is \verb:O:, and to \verb:True: when its argument is of the form \verb:(S n):: \begin{coq_example} -Definition Is_S (n:nat) := match n with - | O => False - | S p => True - end. +Definition Is_S (n : nat) := match n with + | O => False + | S p => True + end. \end{coq_example} -Now we may use the computational power of \verb:Is_S: in order to prove +Now we may use the computational power of \verb:Is_S: to prove trivially that \verb:(Is_S (S n)):: \begin{coq_example} Lemma S_Is_S : forall n:nat, Is_S (S n). @@ -1389,8 +1369,11 @@ Actually, a specific tactic \verb:discriminate: is provided to produce mechanically such proofs, without the need for the user to define explicitly the relevant discrimination predicates: +\begin{coq_eval} +Abort. +\end{coq_eval} \begin{coq_example} -Restart. +Lemma no_confusion : forall n:nat, 0 <> S n. intro n; discriminate. Qed. \end{coq_example} @@ -1403,12 +1386,13 @@ may define inductive families, and for instance inductive predicates. Here is the definition of predicate $\le$ over type \verb:nat:, as given in \Coq's \verb:Prelude: module: \begin{coq_example*} -Inductive le (n:nat) : nat -> Prop := +Inductive le (n : nat) : nat -> Prop := | le_n : le n n - | le_S : forall m:nat, le n m -> le n (S m). + | le_S : forall m : nat, le n m -> le n (S m). \end{coq_example*} -This definition introduces a new predicate \verb+le:nat->nat->Prop+, +This definition introduces a new predicate +\verb+le : nat -> nat -> Prop+, and the two constructors \verb:le_n: and \verb:le_S:, which are the defining clauses of \verb:le:. That is, we get not only the ``axioms'' \verb:le_n: and \verb:le_S:, but also the converse property, that @@ -1426,7 +1410,7 @@ Check le_ind. Let us show how proofs may be conducted with this principle. First we show that $n\le m \Rightarrow n+1\le m+1$: \begin{coq_example} -Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m). +Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m). intros n m n_le_m. elim n_le_m. \end{coq_example} @@ -1442,10 +1426,14 @@ intros; apply le_S; trivial. Now we know that it is a good idea to give the defining clauses as hints, so that the proof may proceed with a simple combination of -\verb:induction: and \verb:auto:. +\verb:induction: and \verb:auto:. \verb:Hint Constructors le: +is just an abbreviation for \verb:Hint Resolve le_n le_S:. +\begin{coq_eval} +Abort. +\end{coq_eval} \begin{coq_example} -Restart. -Hint Resolve le_n le_S . +Hint Constructors le. +Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m). \end{coq_example} We have a slight problem however. We want to say ``Do an induction on @@ -1453,7 +1441,7 @@ hypothesis \verb:(le n m):'', but we have no explicit name for it. What we do in this case is to say ``Do an induction on the first unnamed hypothesis'', as follows. \begin{coq_example} -simple induction 1; auto. +induction 1; auto. Qed. \end{coq_example} @@ -1483,6 +1471,7 @@ Qed. \begin{coq_eval} Reset Initial. Set Printing Width 60. +Set Printing Compact Contexts. \end{coq_eval} \section{Opening library modules} @@ -1552,6 +1541,7 @@ known lemmas about both the successor and the less or equal relation, just ask: \begin{coq_eval} Reset Initial. Set Printing Width 60. +Set Printing Compact Contexts. \end{coq_eval} \begin{coq_example} Search S le. @@ -1562,14 +1552,13 @@ predicate appears at the head position in the conclusion. SearchHead le. \end{coq_example} -A new and more convenient search tool is \verb:SearchPattern: -developed by Yves Bertot. It allows finding the theorems with a -conclusion matching a given pattern, where \verb:_: can be used in -place of an arbitrary term. We remark in this example, that \Coq{} +The \verb:Search: commands also allows finding the theorems +containing a given pattern, where \verb:_: can be used in +place of an arbitrary term. As shown in this example, \Coq{} provides usual infix notations for arithmetic operators. \begin{coq_example} -SearchPattern (_ + _ = _). +Search (_ + _ = _). \end{coq_example} \section{Now you are on your own} diff --git a/engine/proofview.ml b/engine/proofview.ml index c542fd976..b4e2160f4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1072,13 +1072,6 @@ module Goal = struct end end - exception NotExactlyOneSubgoal - let _ = CErrors.register_handler begin function - | NotExactlyOneSubgoal -> - CErrors.user_err (Pp.str"Not exactly one subgoal.") - | _ -> raise CErrors.Unhandled - end - let enter_one f = let open Proof in Comb.get >>= function @@ -1090,7 +1083,7 @@ module Goal = struct let (e, info) = CErrors.push e in tclZERO ~info e end - | _ -> tclZERO NotExactlyOneSubgoal + | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *) let goals = Pv.get >>= fun step -> diff --git a/engine/proofview.mli b/engine/proofview.mli index e98f59f0f..530204501 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -498,7 +498,7 @@ module Goal : sig val enter : ([ `LZ ] t -> unit tactic) -> unit tactic (** Like {!enter}, but assumes exactly one goal under focus, raising *) - (** an error otherwise. *) + (** a fatal error otherwise. *) val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic (** Recover the list of current goals under focus, without evar-normalization. diff --git a/lib/hashset.ml b/lib/hashset.ml index 23ac2fed0..7f96627a6 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -181,7 +181,7 @@ module Make (E : EqType) = let sz = Weak.length bucket in let rec loop i = if i >= sz then ifnotfound index - else if h = hashes.(i) then begin + else if Int.equal h hashes.(i) then begin match Weak.get bucket i with | Some v when E.eq v d -> v | _ -> loop (i + 1) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 9fc2573ac..c498089ca 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -189,9 +189,14 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (t,con_pp,proji_sp_pp) -> + (fun (sign,env,t,con,proji_sp) -> + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in + let env = Termops.push_rels_assum sign env in + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in strbrk "Projection value has no head constant: " - ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " + ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) @@ -203,9 +208,9 @@ let compute_canonical_projections warn (con,ind) = let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in - let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in + let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in @@ -222,9 +227,7 @@ let compute_canonical_projections warn (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) - and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); l end | _ -> l) diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out new file mode 100644 index 000000000..a70f8ca45 --- /dev/null +++ b/test-suite/output/Warnings.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-22: +Warning: Projection value has no head constant: fun x : B => x in canonical +instance a of b, ignoring it. [projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v new file mode 100644 index 000000000..7465442ca --- /dev/null +++ b/test-suite/output/Warnings.v @@ -0,0 +1,5 @@ +(* Term in warning was not printed in the right environment at some time *) +Record A := { B:Type; b:B->B }. +Definition a B := {| B:=B; b:=fun x => x |}. +Canonical Structure a. + diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index c4afc930a..86be54d46 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -62,7 +62,7 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" +STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" # Coq binaries COQC ?= "$(COQBIN)coqc" |