diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-05 21:57:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-05 21:57:15 +0200 |
| commit | 2bb05717bde540332aa814a59da3745f2097dedf (patch) | |
| tree | 86f5753cb84e300e13e9bda8fb8c3835bd66b41a | |
| parent | e76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (diff) | |
| parent | dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 (diff) | |
Merge branch 'v8.5'
56 files changed, 609 insertions, 1024 deletions
@@ -20,6 +20,9 @@ Tactics will eventually fail and backtrack. * "Strict" changes the behavior of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. +- New compatibility flag "Universal Lemma Under Conjunction" which + let tactics working under conjunctions apply sublemmas of the form + "forall A, ... -> A". API @@ -35,7 +38,6 @@ API * A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. - Tools - Added an option -w to control the output of coqtop warnings. @@ -359,6 +361,10 @@ Tactics trace anymore. Use "Info 1 auto" instead. The same goes for "info_trivial". On the other hand "info_eauto" still works fine, while "Info 1 eauto" prints a trivial trace. +- When using a lemma of the prototypical form "forall A, {a:A & P a}", + "apply" and "apply in" do not instantiate anymore "A" with the + current goal and use "a" as the proof, as they were sometimes doing, + now considering that it is a too powerful decision. Program diff --git a/Makefile.common b/Makefile.common index 15ac13ff1..a28ca1dfc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -127,13 +127,14 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \ + Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \ + RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ + AsyncProofs.tex ) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps diff --git a/README.doc b/README.doc index 4e72c894b..4e72c894b 100755..100644 --- a/README.doc +++ b/README.doc diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f969f0132..f9f2e1b09 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -229,6 +229,11 @@ let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") +let ppenvwithcst e = pp + (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ + str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ + str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") + let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 0e820008e..0e820008e 100755..100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex diff --git a/doc/common/title.tex b/doc/common/title.tex index 4716c3156..4716c3156 100755..100644 --- a/doc/common/title.tex +++ b/doc/common/title.tex diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index b03aa6409..c8dd220ba 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -849,26 +849,41 @@ mapped to {\Prop}. Use some theorem or assumption or use the {\split} tactic. \begin{coq_example} -Goal forall A B:Prop, A->B-> A/\B. +Goal forall A B:Prop, A -> B -> A/\B. intros. split. assumption. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal contains a conjunction as an hypothesis, how can I use it?} -If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic: +If you want to decompose a hypothesis into several hypotheses, you can +use the {\destruct} tactic: \begin{coq_example} -Goal forall A B:Prop, A/\B-> B. +Goal forall A B:Prop, A/\B -> B. intros. -decompose [and] H. +destruct H as [H1 H2]. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} + +You can also perform the destruction at the time of introduction: +\begin{coq_example} +Goal forall A B:Prop, A/\B -> B. +intros A B [H1 H2]. +assumption. +\end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a disjunction, how can I prove it?} @@ -878,26 +893,28 @@ reasoning step, use the {\tt classic} axiom to prove the right part with the ass that the left part of the disjunction is false. \begin{coq_example} -Goal forall A B:Prop, A-> A\/B. +Goal forall A B:Prop, A -> A\/B. intros. left. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} An example using classical reasoning: \begin{coq_example} Require Import Classical. -Ltac classical_right := -match goal with -| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +Ltac classical_right := +match goal with +| _:_ |- ?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) end. -Ltac classical_left := -match goal with -| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +Ltac classical_left := +match goal with +| _:_ |- _ \/ ?X1 => (elim (classic X1);intro;[right;trivial|left]) end. @@ -905,8 +922,10 @@ Goal forall A B:Prop, (~A -> B) -> A\/B. intros. classical_right. auto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an universally quantified statement, how can I prove it?} @@ -935,8 +954,10 @@ Goal exists x:nat, forall y, x+y=y. exists 0. intros. auto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is solvable by some lemma, how can I prove it?} @@ -954,8 +975,10 @@ Qed. Goal 3+0 = 3. apply mylemma. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -972,8 +995,10 @@ Just use the {\reflexivity} tactic. Goal forall x, 0+x = x. intros. reflexivity. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a {\tt let x := a in ...}, how can I prove it?} @@ -987,13 +1012,21 @@ Just use the {\destruct} c as (a,...,b) tactic. \Question{My goal contains some existential hypotheses, how can I use it?} -You can use the tactic {\elim} with you hypotheses as an argument. - -\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?} +As with conjunctive hypotheses, you can use the {\destruct} tactic or +the {\intros} tactic to decompose them into several hypotheses. -\begin{verbatim} -Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H. -\end{verbatim} +\begin{coq_example*} +Require Import Arith. +\end{coq_example*} +\begin{coq_example} +Goal forall x, (exists y, x * y = 1) -> x = 1. +intros x [y H]. +apply mult_is_one in H. +easy. +\end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality, how can I swap the left and right hand terms?} @@ -1004,8 +1037,10 @@ Goal forall x y : nat, x=y -> y=x. intros. symmetry. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My hypothesis is an equality, how can I swap the left and right hand terms?} @@ -1016,8 +1051,10 @@ Goal forall x y : nat, x=y -> y=x. intros. symmetry in H. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality, how can I prove it by transitivity?} @@ -1029,8 +1066,10 @@ intros. transitivity y. assumption. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it?} @@ -1066,7 +1105,6 @@ eapply trans. apply H. auto. Qed. - \end{coq_example} \Question{My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?} @@ -1103,8 +1141,10 @@ Use the {\assumption} tactic. Goal 1=1 -> 1=1. intro. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?} @@ -1114,8 +1154,10 @@ Use the {\exact} tactic. Goal 1=1 -> 1=1 -> 1=1. intros. exact H0. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{What can be the difference between applying one hypothesis or another in the context of the last question?} @@ -1131,8 +1173,10 @@ Just use the {\tauto} tactic. Goal forall A B:Prop, A-> (A\/B) /\ A. intros. tauto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a first order formula, how can I prove it?} @@ -1149,8 +1193,10 @@ Just use the {\congruence} tactic. Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a. intros. congruence. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?} @@ -1161,8 +1207,10 @@ Just use the {\congruence} tactic. Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b. intros. congruence. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?} @@ -1173,11 +1221,13 @@ Just use the {\ring} tactic. Require Import ZArith. Require Ring. Local Open Scope Z_scope. -Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. +Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. intros. ring. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?} @@ -1187,30 +1237,30 @@ Just use the {\field} tactic. Require Import Reals. Require Ring. Local Open Scope R_scope. -Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. +Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. intros. field. -cut (b*a <>0 -> a<>0). -cut (b*a <>0 -> b<>0). -auto. -auto with real. -auto with real. -Qed. +split ; auto with real. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} -\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?} +\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from $+$, $-$, constants, and variables), how can I prove it?} \begin{coq_example} Require Import ZArith. Require Omega. Local Open Scope Z_scope. -Goal forall a : Z, a>0 -> a+a > a. +Goal forall a : Z, a>0 -> a+a > a. intros. omega. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?} @@ -1233,16 +1283,22 @@ assert (A->C). intro;apply H0;apply H;assumption. apply H2. assumption. +\end{coq_example} +\begin{coq_example*} Qed. +\end{coq_example*} +\begin{coq_example} Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. intros. cut (A->C). intro. apply H2;assumption. intro;apply H0;apply H;assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -1333,8 +1389,10 @@ H1 *) intros A B C H H0 H1. repeat split;assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{I want to automatize the use of some tactic, how can I do it?} @@ -1347,8 +1405,10 @@ Goal forall A B C : Prop, A -> B/\C -> A/\B/\C. Proof with assumption. intros. split... -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it?} @@ -1360,8 +1420,10 @@ Local Open Scope Z_scope. Goal forall a b c : Z, a+b=b+a. Proof with try solve [ring]. intros... -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{How can I do the opposite of the {\intro} tactic?} @@ -1373,8 +1435,10 @@ intros. generalize H. intro. auto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?} @@ -1512,8 +1576,10 @@ You can use the {\discriminate} tactic. Inductive toto : Set := | C1 : toto | C2 : toto. Goal C1 <> C2. discriminate. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?} @@ -1561,7 +1627,7 @@ If you type for instance the following ``definition'': Reset Initial. \end{coq_eval} \begin{coq_example} -Definition max (n p : nat) := if n <= p then p else n. +Fail Definition max (n p : nat) := if n <= p then p else n. \end{coq_example} As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a @@ -1729,7 +1795,7 @@ mergesort} as an example). the arguments of the loop. \begin{coq_eval} -Open Scope R_scope. +Reset Initial. Require Import List. \end{coq_eval} @@ -1742,21 +1808,25 @@ Definition R (a b:list nat) := length a < length b. \begin{coq_example*} Lemma Rwf : well_founded R. \end{coq_example*} +\begin{coq_eval} +Admitted. +\end{coq_eval} \item Define the step function (which needs proofs that recursive calls are on smaller arguments). -\begin{verbatim} -Definition split (l : list nat) - : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} - := (* ... *) . -Definition concat (l1 l2 : list nat) : list nat := (* ... *) . +\begin{coq_example*} +Definition split (l : list nat) + : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}. +Admitted. +Definition concat (l1 l2 : list nat) : list nat. +Admitted. Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) := let (lH1,lH2) := (split l) in let (l1,H1) := lH1 in let (l2,H2) := lH2 in concat (f l1 H1) (f l2 H2). -\end{verbatim} +\end{coq_example*} \item Define the recursive function by fixpoint on the step function. @@ -1811,9 +1881,9 @@ induction 1. inversion 1. inversion 1. apply IHeven; trivial. \end{coq_example} -\begin{coq_eval} +\begin{coq_example*} Qed. -\end{coq_eval} +\end{coq_example*} In case the type of the second induction hypothesis is not dependent, {\tt inversion} can just be replaced by {\tt destruct}. @@ -1848,10 +1918,10 @@ Double induction (or induction on pairs) is a restriction of the lexicographic induction. Here is an example of double induction. \begin{coq_example} -Lemma nat_double_ind : -forall P : nat -> nat -> Prop, P 0 0 -> - (forall m n, P m n -> P m (S n)) -> - (forall m n, P m n -> P (S m) n) -> +Lemma nat_double_ind : +forall P : nat -> nat -> Prop, P 0 0 -> + (forall m n, P m n -> P m (S n)) -> + (forall m n, P m n -> P (S m) n) -> forall m n, P m n. intros P H00 HmS HSn; induction m. (* case 0 *) @@ -1859,9 +1929,9 @@ induction n; [assumption | apply HmS; apply IHn]. (* case Sm *) intro n; apply HSn; apply IHm. \end{coq_example} -\begin{coq_eval} +\begin{coq_example*} Qed. -\end{coq_eval} +\end{coq_example*} \Question{How to define a function by nested recursion?} @@ -1896,7 +1966,7 @@ Set Implicit Arguments. CoInductive Stream (A:Set) : Set := Cons : A -> Stream A -> Stream A. CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)). -Lemma Stream_unfold : +Lemma Stream_unfold : forall n:nat, nats n = Cons n (nats (S n)). Proof. intro; @@ -1904,8 +1974,10 @@ Proof. | Cons x s => Cons x s end). case (nats n); reflexivity. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -2586,8 +2658,10 @@ eapply eq_trans. Show Existentials. eassumption. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{What can I do if I get ``Cannot solve a second-order unification problem''?} diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 47dc1ac1a..7cf500400 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -5,7 +5,7 @@ \index{Asynchronous and Parallel Proof Processing!presentation} This chapter explains how proofs can be asynchronously processed by Coq. -This feature improves the reactiveness of the system when used in interactive +This feature improves the reactivity of the system when used in interactive mode via CoqIDE. In addition to that, it allows Coq to take advantage of parallel hardware when used as a batch compiler by decoupling the checking of statements and definitions from the construction and checking of proofs @@ -24,7 +24,7 @@ are universe inconsistencies. Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. -\subsection{Proof annotations} +\section{Proof annotations} To process a proof asynchronously Coq needs to know the precise statement of the theorem without looking at the proof. This requires some annotations @@ -52,7 +52,7 @@ The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a \texttt{Qed} command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. -\subsection{Interactive mode} +\section{Interactive mode} At the time of writing the only user interface supporting asynchronous proof processing is CoqIDE. @@ -85,7 +85,7 @@ reduce the reactivity of the master process to user commands. To disable this feature, one can pass the \texttt{-async-proofs off} flag to CoqIDE. -\subsection{Batch mode} +\section{Batch mode} When Coq is used as a batch compiler by running \texttt{coqc} or \texttt{coqtop -compile}, it produces a \texttt{.vo} file for each @@ -148,7 +148,7 @@ globally consistent. Hence this compilation mode is only useful for quick regression testing and on developments not making heavy use of the $Type$ hierarchy. -\subsection{Limiting the number of parallel workers} +\section{Limiting the number of parallel workers} \label{coqworkmgr} Many Coq processes may run on the same computer, and each of them may start diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 187fe5342..74c8374de 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -110,17 +110,14 @@ even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. Concerning Haskell, type-preserving optimizations are less useful -because of lazyness. We still make some optimizations, for example in +because of laziness. We still make some optimizations, for example in order to produce more readable code. The type-preserving optimizations are controlled by the following \Coq\ options: \begin{description} -\item \optindex{Extraction Optimize} -{\tt Set Extraction Optimize.} - -\item {\tt Unset Extraction Optimize.} +\item \optindex{Extraction Optimize} {\tt Unset Extraction Optimize.} Default is Set. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also @@ -130,8 +127,6 @@ ML term as close as possible to the Coq term. \item \optindex{Extraction Conservative Types} {\tt Set Extraction Conservative Types.} -\item {\tt Unset Extraction Conservative Types.} - Default is Unset. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy types). Turn this option to Set to make sure that {\tt e:t} @@ -141,8 +136,6 @@ code of {\tt e} and {\tt t} respectively. \item \optindex{Extraction KeepSingleton} {\tt Set Extraction KeepSingleton.} -\item {\tt Unset Extraction KeepSingleton.} - Default is Unset. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and only one argument to this constructor), the inductive structure is @@ -150,21 +143,15 @@ removed and this type is seen as an alias to the inner type. The typical example is {\tt sig}. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -\item \optindex{Extraction AutoInline} -{\tt Set Extraction AutoInline.} - -\item {\tt Unset Extraction AutoInline.} +\item \optindex{Extraction AutoInline} {\tt Unset Extraction AutoInline.} -Default is Set, so by default, the extraction mechanism is free to -inline the bodies of some defined constants, according to some heuristics +Default is Set. The extraction mechanism +inlines the bodies of some defined constants, according to some heuristics like size of bodies, uselessness of some arguments, etc. Those heuristics are not always perfect; if you want to disable this feature, do it by Unset. -\item \comindex{Extraction Inline} -{\tt Extraction Inline} \qualid$_1$ \dots\ \qualid$_n$. - -\item \comindex{Extraction NoInline} -{\tt Extraction NoInline} \qualid$_1$ \dots\ \qualid$_n$. +\item \comindex{Extraction Inline} \comindex{Extraction NoInline} +{\tt Extraction [Inline|NoInline] \qualid$_1$ \dots\ \qualid$_n$}. In addition to the automatic inline feature, you can tell to inline some more constants by the {\tt Extraction Inline} command. Conversely, @@ -265,28 +252,28 @@ extracted files. The extraction recognizes whether the realized axiom should become a ML type constant or a ML object declaration. \Example -\begin{coq_example} +\begin{coq_example*} Axiom X:Set. Axiom x:X. Extract Constant X => "int". Extract Constant x => "0". -\end{coq_example} +\end{coq_example*} Notice that in the case of type scheme axiom (i.e. whose type is an arity, that is a sequence of product finished by a sort), then some type -variables has to be given. The syntax is then: +variables have to be given. The syntax is then: \begin{description} -\item{\tt Extract Constant} \qualid\ \str$_1$ \dots\ \str$_n$ {\tt =>} \str. +\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.} \end{description} The number of type variables is checked by the system. \Example -\begin{coq_example} +\begin{coq_example*} Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a*'b ". -\end{coq_example} +\end{coq_example*} Realizing an axiom via {\tt Extract Constant} is only useful in the case of an informative axiom (of sort Type or Set). A logical axiom @@ -308,7 +295,7 @@ types and constructors. For instance, the user may want to use the ML native boolean type instead of \Coq\ one. The syntax is the following: \begin{description} -\item{\tt Extract Inductive} \qualid\ {\tt =>} \str\ {\tt [} \str\ \dots\ \str\ {\tt ]}\ {\it optstring}.\par +\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots\ \str\ ] {\it optstring}.}\par Give an ML extraction for the given inductive type. You must specify extractions for the type itself (first \str) and all its constructors (between square brackets). If given, the final optional @@ -412,7 +399,7 @@ For example, here are two kinds of problem that can occur: \begin{itemize} \item If some part of the program is {\em very} polymorphic, there may be no ML type for it. In that case the extraction to ML works - all right but the generated code may be refused by the ML + alright but the generated code may be refused by the ML type-checker. A very well known example is the {\em distr-pair} function: \begin{verbatim} @@ -549,34 +536,34 @@ Some pathological examples of extraction are grouped in the file \asubsection{Users' Contributions} - Several of the \Coq\ Users' Contributions use extraction to produce - certified programs. In particular the following ones have an automatic - extraction test (just run {\tt make} in those directories): - - \begin{itemize} - \item Bordeaux/Additions - \item Bordeaux/EXCEPTIONS - \item Bordeaux/SearchTrees - \item Dyade/BDDS - \item Lannion - \item Lyon/CIRCUITS - \item Lyon/FIRING-SQUAD - \item Marseille/CIRCUITS - \item Muenchen/Higman - \item Nancy/FOUnify - \item Rocq/ARITH/Chinese - \item Rocq/COC - \item Rocq/GRAPHS - \item Rocq/HIGMAN - \item Sophia-Antipolis/Stalmarck - \item Suresnes/BDD - \end{itemize} - - Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are - examples of developments where {\tt Obj.magic} are needed. - This is probably due to an heavy use of impredicativity. - After compilation those two examples run nonetheless, - thanks to the correction of the extraction~\cite{Let02}. +Several of the \Coq\ Users' Contributions use extraction to produce +certified programs. In particular the following ones have an automatic +extraction test: + +\begin{itemize} +\item {\tt additions} +\item {\tt bdds} +\item {\tt canon-bdds} +\item {\tt chinese} +\item {\tt continuations} +\item {\tt coq-in-coq} +\item {\tt exceptions} +\item {\tt firing-squad} +\item {\tt founify} +\item {\tt graphs} +\item {\tt higman-cf} +\item {\tt higman-nw} +\item {\tt hardware} +\item {\tt multiplier} +\item {\tt search-trees} +\item {\tt stalmarck} +\end{itemize} + +{\tt continuations} and {\tt multiplier} are a bit particular. They are +examples of developments where {\tt Obj.magic} are needed. This is +probably due to an heavy use of impredicativity. After compilation, those +two examples run nonetheless, thanks to the correction of the +extraction~\cite{Let02}. %%% Local Variables: %%% mode: latex diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 4a4fab153..1efed6ef7 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -1,4 +1,4 @@ -\achapter{Micromega : tactics for solving arithmetic goals over ordered rings} +\achapter{Micromega: tactics for solving arithmetic goals over ordered rings} \aauthor{Frédéric Besson and Evgeny Makarov} \newtheorem{theorem}{Theorem} @@ -6,33 +6,40 @@ \asection{Short description of the tactics} \tacindex{psatz} \tacindex{lra} \label{sec:psatz-hurry} -The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over - {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}: +The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to +several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and +{\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by + pre-processing the goal with the {\tt zify} tactic.} \begin{itemize} \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); \item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); -\item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is -is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. - Note that the {\tt csdp} driver is generating - a \emph{proof cache} which allows rerunning scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). +\item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and + {\tt n} is an optional integer limiting the proof search depth is is an + incomplete proof procedure for non-linear arithmetic. It is based on + John Harrison's HOL Light driver to the external prover {\tt + csdp}\footnote{Sources and binaries can be found at + \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} + driver is generating a \emph{proof cache} which makes it possible to + rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). \end{itemize} -The tactics solve propositional formulas parameterised by atomic arithmetics expressions +The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain $D \in \{\mathbb{Z}, \mathbb{Q}, \mathbb{R} \}$. The syntax of the formulas is the following: \[ \begin{array}{lcl} - F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \sim F\\ + F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \neg F\\ A &::=& p_1 = p_2 \mid p_1 > p_2 \mid p_1 < p_2 \mid p_1 \ge p_2 \mid p_1 \le p_2 \\ p &::=& c \mid x \mid {-}p \mid p_1 - p_2 \mid p_1 + p_2 \mid p_1 \times p_2 \mid p \verb!^! n - \end{array} - \] - where $c$ is a numeric constant, $x\in D$ is a numeric variable and the operators $-$, $+$, $\times$, are - respectively subtraction, addition, product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an - arbitrary proposition. +\end{array} +\] +where $c$ is a numeric constant, $x\in D$ is a numeric variable, the +operators $-$, $+$, $\times$ are respectively subtraction, addition, +product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an +arbitrary proposition. % - For {\tt Q}, equality is not leibnitz equality {\tt =} but the equality of rationals {\tt ==}. + For {\tt Q}, equality is not Leibniz equality {\tt =} but the equality of rationals {\tt ==}. For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants). %% The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. @@ -47,79 +54,89 @@ For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational %% \hline %% \end{array} %% \] -For {\tt R}, the tactic recognises as real constants the following expressions: +For {\tt R}, the tactic recognizes as real constants the following expressions: \begin{verbatim} -c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c +c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q + | Rdiv(c,c) | Rinv c \end{verbatim} -where ${\tt z}$ is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. +where {\tt z} is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}. \asection{\emph{Positivstellensatz} refutations} \label{sec:psatz-back} The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which -generalises Hilbert's \emph{nullstellensatz}. +generalizes Hilbert's \emph{nullstellensatz}. % -It relies on the notion of $\mathit{Cone}$. Given a (finite) set of polynomials $S$, $Cone(S)$ is -inductively defined as the smallest set of polynomials closed under the following rules: +It relies on the notion of $\mathit{Cone}$. Given a (finite) set of +polynomials $S$, $\mathit{Cone}(S)$ is inductively defined as the +smallest set of polynomials closed under the following rules: \[ \begin{array}{l} -\dfrac{p \in S}{p \in Cone(S)} \quad -\dfrac{}{p^2 \in Cone(S)} \quad -\dfrac{p_1 \in Cone(S) \quad p_2 \in Cone(S) \quad \Join \in \{+,*\}} {p_1 \Join p_2 \in Cone(S)}\\ +\dfrac{p \in S}{p \in \mathit{Cone}(S)} \quad +\dfrac{}{p^2 \in \mathit{Cone}(S)} \quad +\dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad +\Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\ \end{array} \] -The following theorem provides a proof principle for checking that a set of polynomial inequalities do not have solutions\footnote{Variants deal with equalities and strict inequalities.}: +The following theorem provides a proof principle for checking that a set +of polynomial inequalities does not have solutions.\footnote{Variants + deal with equalities and strict inequalities.} \begin{theorem} \label{thm:psatz} Let $S$ be a set of polynomials.\\ - If ${-}1$ belongs to $Cone(S)$ then the conjunction $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. + If ${-}1$ belongs to $\mathit{Cone}(S)$ then the conjunction + $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. \end{theorem} A proof based on this theorem is called a \emph{positivstellensatz} refutation. % -The tactics work as follows. Formulas are normalised into conjonctive normal form $\bigwedge_i C_i$ where +The tactics work as follows. Formulas are normalized into conjunctive normal form $\bigwedge_i C_i$ where $C_i$ has the general form $(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})$ and $\Join \in \{>,\ge,=\}$ for $D\in \{\mathbb{Q},\mathbb{R}\}$ and $\Join \in \{\ge, =\}$ for $\mathbb{Z}$. % For each conjunct $C_i$, the tactic calls a oracle which searches for $-1$ within the cone. % -Upon success, the oracle returns a \emph{cone expression} that is normalised by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be +Upon success, the oracle returns a \emph{cone expression} that is normalized by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be $-1$. -\asection{{\tt lra} : a decision procedure for linear real and rational arithmetic} +\asection{{\tt lra}: a decision procedure for linear real and rational arithmetic} \label{sec:lra} The {\tt lra} tactic is searching for \emph{linear} refutations using -Fourier elimination\footnote{More efficient linear programming techniques could equally be employed}. As a -result, this tactic explores a subset of the $Cone$ defined as: +Fourier elimination.\footnote{More efficient linear programming + techniques could equally be employed.} As a result, this tactic +explores a subset of the $\mathit{Cone}$ defined as \[ -LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\} +\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right| +~\alpha_p \mbox{ are positive constants} \right\}. \] The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. % There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. -\asection{ {\tt psatz} : a proof procedure for non-linear arithmetic} +\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} \label{sec:psatz} -The {\tt psatz} tactic explores the $Cone$ by increasing degrees -- hence the depth parameter $n$. +The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a +Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a refutation. -To illustrate the working of the tactic, consider we wish to prove the following Coq goal.\\ +To illustrate the working of the tactic, consider we wish to prove the following Coq goal. \begin{coq_eval} - Require Import ZArith Psatz. - Open Scope Z_scope. +Require Import ZArith Psatz. +Open Scope Z_scope. \end{coq_eval} \begin{coq_example*} - Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. \end{coq_example*} \begin{coq_eval} intro x; psatz Z 2. \end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the cone expression $2 \times -(\mathbf{x-1}) + \mathbf{x-1}\times\mathbf{x-1} + \mathbf{-x^2}$ (polynomial hypotheses are printed in bold). By construction, this -expression belongs to $Cone(\{-x^2, x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the +cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times +(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in +bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, +x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By Theorem~\ref{thm:psatz}, the goal is valid. % @@ -128,37 +145,39 @@ Theorem~\ref{thm:psatz}, the goal is valid. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. % -\asection{ {\tt lia} : a tactic for linear integer arithmetic } +\asection{{\tt lia}: a tactic for linear integer arithmetic} \tacindex{lia} \label{sec:lia} -The tactic {\tt lia} ({\tt Require Lia.}) offers an alternative to the {\tt omega} and {\tt romega} tactic (see -Chapter~\ref{OmegaChapter}). +The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt + romega} tactic (see Chapter~\ref{OmegaChapter}). % -Rougthly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. +Roughly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. % However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. \begin{coq_example*} - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. +Goal forall x y, + 27 <= 11 * x + 13 * y <= 45 -> + -10 <= 7 * x - 9 * y <= 4 -> False. \end{coq_example*} \begin{coq_eval} -intro x; lia. +intros x y; lia. \end{coq_eval} -The estimation of the relative efficiency of lia \emph{vs} {\tt omega} +The estimation of the relative efficiency of {\tt lia} \emph{vs} {\tt omega} and {\tt romega} is under evaluation. \paragraph{High level view of {\tt lia}.} -Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete proof principle\footnote{In practice, the oracle might fail to produce such a refutation.}. +Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete +proof principle.\footnote{In practice, the oracle might fail to produce + such a refutation.} % However, this is not the case over $\mathbb{Z}$. % -Actually, \emph{positivstellensatz} refutations are not even sufficient to decide linear \emph{integer} -arithmetics. +Actually, \emph{positivstellensatz} refutations are not even sufficient +to decide linear \emph{integer} arithmetic. % -The canonical exemple is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. +The canonical example is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. % To remedy this weakness, the {\tt lia} tactic is using recursively a combination of: % @@ -177,17 +196,18 @@ To remedy this weakness, the {\tt lia} tactic is using recursively a combination p \ge c \Rightarrow p \ge \lceil c \rceil \] \end{theorem} -For instance, from $2 * x = 1$ we can deduce +For instance, from $2 x = 1$ we can deduce \begin{itemize} \item $x \ge 1/2$ which cut plane is $ x \ge \lceil 1/2 \rceil = 1$; \item $ x \le 1/2$ which cut plane is $ x \le \lfloor 1/2 \rfloor = 0$. \end{itemize} -By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge 0$, we conclude by exhibiting a -\emph{positivstellensatz} refutation ($-1 \equiv \mathbf{x-1} + \mathbf{-x} \in Cone(\{x-1,x\})$). +By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge +0$, we conclude by exhibiting a \emph{positivstellensatz} refutation: $-1 +\equiv \mathbf{x-1} + \mathbf{-x} \in \mathit{Cone}(\{x-1,x\})$. Cutting plane proofs and linear \emph{positivstellensatz} refutations are a complete proof principle for integer linear arithmetic. -\paragraph{Case split} allow to enumerate over the possible values of an expression. +\paragraph{Case split} enumerates over the possible values of an expression. \begin{theorem} Let $p$ be an integer and $c_1$ and $c_2$ integer constants. \[ @@ -199,7 +219,7 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2] We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and recursively search for a proof. -\asection{ {\tt nia} : a proof procedure for non-linear integer arithmetic} +\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} \tacindex{nia} \label{sec:nia} The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. @@ -212,7 +232,8 @@ This pre-processing does the following: monomial, the context is enriched with $x^2\ge 0$; \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. \end{itemize} -After pre-processing, the linear prover of {\tt lia} is searching for a proof by abstracting monomials by variables. +After pre-processing, the linear prover of {\tt lia} searches for a proof +by abstracting monomials by variables. diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex deleted file mode 100644 index f33c0d356..000000000 --- a/doc/refman/Natural.tex +++ /dev/null @@ -1,425 +0,0 @@ -\achapter{\texttt{Natural} : proofs in natural language} -\aauthor{Yann Coscoy} - -\asection{Introduction} - -\Natural~ is a package allowing the writing of proofs in natural -language. For instance, the proof in \Coq~of the induction principle on pairs -of natural numbers looks like this: - -\begin{coq_example*} -Require Natural. -\end{coq_example*} -\begin{coq_example} -Print nat_double_ind. -\end{coq_example} - -Piping it through the \Natural~pretty-printer gives: - -\comindex{Print Natural} -\begin{coq_example} -Print Natural nat_double_ind. -\end{coq_example} - -\asection{Activating \Natural} - -To enable the printing of proofs in natural language, you should -type under \texttt{coqtop} or \texttt{coqtop -full} the command - -\begin{coq_example*} -Require Natural. -\end{coq_example*} - -By default, proofs are transcripted in english. If you wish to print them -in French, set the French option by - -\comindex{Set Natural} -\begin{coq_example*} -Set Natural French. -\end{coq_example*} - -If you want to go back to English, type in - -\begin{coq_example*} -Set Natural English. -\end{coq_example*} - -Currently, only \verb=French= and \verb=English= are available. - -You may see for example the natural transcription of the proof of -the induction principle on pairs of natural numbers: - -\begin{coq_example*} -Print Natural nat_double_ind. -\end{coq_example*} - -You may also show in natural language the current proof in progress: - -\comindex{Show Natural} -\begin{coq_example} -Goal (n:nat)(le O n). -Induction n. -Show Natural Proof. -\end{coq_example} - -\subsection*{Restrictions} - -For \Natural, a proof is an object of type a proposition (i.e. an -object of type something of type {\tt Prop}). Only proofs are written -in natural language when typing {\tt Print Natural \ident}. All other -objects (the objects of type something which is of type {\tt Set} or -{\tt Type}) are written as usual $\lambda$-terms. - -\asection{Customizing \Natural} - -The transcription of proofs in natural language is mainly a paraphrase of -the formal proofs, but some specific hints in the transcription -can be given. -Three kinds of customization are available. - -\asubsection{Implicit proof steps} - -\subsubsection*{Implicit lemmas} - -Applying a given lemma or theorem \verb=lem1= of statement, say $A -\Rightarrow B$, to an hypothesis, say $H$ (assuming $A$) produces the -following kind of output translation: - -\begin{verbatim} -... -Using lem1 with H we get B. -... -\end{verbatim} - -But sometimes, you may prefer not to see the explicit invocation to -the lemma. You may prefer to see: - -\begin{verbatim} -... -With H we have A. -... -\end{verbatim} - -This is possible by declaring the lemma as implicit. You should type: - -\comindex{Add Natural} -\begin{coq_example*} -Add Natural Implicit lem1. -\end{coq_example*} - -By default, the lemmas \verb=proj1=, \verb=proj2=, \verb=sym_equal= -and \verb=sym_eqT= are declared implicit. To remove a lemma or a theorem -previously declared as implicit, say \verb=lem1=, use the command - -\comindex{Remove Natural} -\begin{coq_example*} -Remove Natural Implicit lem1. -\end{coq_example*} - -To test if the lemma or theorem \verb=lem1= is, or is not, -declared as implicit, type - -\comindex{Test Natural} -\begin{coq_example*} -Test Natural Implicit for lem1. -\end{coq_example*} - -\subsubsection*{Implicit proof constructors} - -Let \verb=constr1= be a proof constructor of a given inductive -proposition (or predicate) -\verb=Q= (of type \verb=Prop=). Assume \verb=constr1= proves -\verb=(x:A)(P x)->(Q x)=. Then, applying \verb=constr1= to an hypothesis, -say \verb=H= (assuming \verb=(P a)=) produces the following kind of output: - -\begin{verbatim} -... -By the definition of Q, with H we have (Q a). -... -\end{verbatim} - -But sometimes, you may prefer not to see the explicit invocation to -this constructor. You may prefer to see: - -\begin{verbatim} -... -With H we have (Q a). -... -\end{verbatim} - -This is possible by declaring the constructor as implicit. You should -type, as before: - -\comindex{Add Natural Implicit} -\begin{coq_example*} -Add Natural Implicit constr1. -\end{coq_example*} - -By default, the proposition (or predicate) constructors - -\verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=, -\verb=eq_refl= and \verb=exist= - -\noindent are declared implicit. Note that declaring implicit the -constructor of a datatype (i.e. an inductive type of type \verb=Set=) -has no effect. - -As above, you can remove or test a constant declared implicit. - -\subsubsection*{Implicit inductive constants} - -Let \verb=Ind= be an inductive type (either a proposition (or a -predicate) -- on \verb=Prop= --, or a datatype -- on \verb=Set=). -Suppose the proof proceeds by induction on an hypothesis \verb=h= -proving \verb=Ind= (or more generally \verb=(Ind A1 ... An)=). The -following kind of output is produced: - -\begin{verbatim} -... -With H, we will prove A by induction on the definition of Ind. -Case 1. ... -Case 2. ... -... -\end{verbatim} - -But sometimes, you may prefer not to see the explicit invocation to -\verb=Ind=. You may prefer to see: - -\begin{verbatim} -... -We will prove A by induction on H. -Case 1. ... -Case 2. ... -... -\end{verbatim} - -This is possible by declaring the inductive type as implicit. You should -type, as before: - -\comindex{Add Natural Implicit} -\begin{coq_example*} -Add Natural Implicit Ind. -\end{coq_example*} - -This kind of parameterization works for any inductively defined -proposition (or predicate) or datatype. Especially, it works whatever -the definition is recursive or purely by cases. - -By default, the data type \verb=nat= and the inductive connectives -\verb=and=, \verb=or=, \verb=sig=, \verb=False=, \verb=eq=, -\verb=eqT=, \verb=ex= and \verb=exT= are declared implicit. - -As above, you can remove or test a constant declared implicit. Use -{\tt Remove Natural Contractible $id$} or {\tt Test Natural -Contractible for $id$}. - -\asubsection{Contractible proof steps} - -\subsubsection*{Contractible lemmas or constructors} - -Some lemmas, theorems or proof constructors of inductive predicates are -often applied in a row and you obtain an output of this kind: - -\begin{verbatim} -... -Using T with H1 and H2 we get P. - * By H3 we have Q. - Using T with theses results we get R. -... -\end{verbatim} - -where \verb=T=, \verb=H1=, \verb=H2= and \verb=H3= prove statements -of the form \verb=(X,Y:Prop)X->Y->(L X Y)=, \verb=A=, \verb=B= and \verb=C= -respectively (and thus \verb=R= is \verb=(L (L A B) C)=). - -You may obtain a condensed output of the form - -\begin{verbatim} -... -Using T with H1, H2, and H3 we get R. -... -\end{verbatim} - -by declaring \verb=T= as contractible: - -\comindex{Add Natural Contractible} -\begin{coq_example*} -Add Natural Contractible T. -\end{coq_example*} - -By default, the lemmas \verb=proj1=, \verb=proj2= and the proof -constructors \verb=conj=, \verb=or_introl=, \verb=or_intror= are -declared contractible. As for implicit notions, you can remove or -test a lemma or constructor declared contractible. - -\subsubsection*{Contractible induction steps} - -Let \verb=Ind= be an inductive type. When the proof proceeds by -induction in a row, you may obtain an output of this kind: - -\begin{verbatim} -... -We have (Ind A (Ind B C)). -We use definition of Ind in a study in two cases. -Case 1: We have A. -Case 2: We have (Ind B C). - We use definition of Ind in a study of two cases. - Case 2.1: We have B. - Case 2.2: We have C. -... -\end{verbatim} - -You may prefer to see - -\begin{verbatim} -... -We have (Ind A (Ind B C)). -We use definition of Ind in a study in three cases. -Case 1: We have A. -Case 2: We have B. -Case 3: We have C. -... -\end{verbatim} - -This is possible by declaring \verb=Ind= as contractible: - -\begin{coq_example*} -Add Natural Contractible T. -\end{coq_example*} - -By default, only \verb=or= is declared as a contractible inductive -constant. -As for implicit notions, you can remove or test an inductive notion declared -contractible. - -\asubsection{Transparent definitions} - -``Normal'' definitions are all constructions except proofs and proof constructors. - -\subsubsection*{Transparent non inductive normal definitions} - -When using the definition of a non inductive constant, say \verb=D=, the -following kind of output is produced: - -\begin{verbatim} -... -We have proved C which is equivalent to D. -... -\end{verbatim} - -But you may prefer to hide that D comes from the definition of C as -follows: - -\begin{verbatim} -... -We have prove D. -... -\end{verbatim} - -This is possible by declaring \verb=C= as transparent: - -\comindex{Add Natural Transparent} -\begin{coq_example*} -Add Natural Transparent D. -\end{coq_example*} - -By default, only \verb=not= (normally written \verb=~=) is declared as -a non inductive transparent definition. -As for implicit and contractible definitions, you can remove or test a -non inductive definition declared transparent. -Use \texttt{Remove Natural Transparent} \ident or -\texttt{Test Natural Transparent for} \ident. - -\subsubsection*{Transparent inductive definitions} - -Let \verb=Ind= be an inductive proposition (more generally: a -predicate \verb=(Ind x1 ... xn)=). Suppose the definition of -\verb=Ind= is non recursive and built with just -one constructor proving something like \verb=A -> B -> Ind=. -When coming back to the definition of \verb=Ind= the -following kind of output is produced: - -\begin{verbatim} -... -Assume Ind (H). - We use H with definition of Ind. - We have A and B. - ... -\end{verbatim} - -When \verb=H= is not used a second time in the proof, you may prefer -to hide that \verb=A= and \verb=B= comes from the definition of -\verb=Ind=. You may prefer to get directly: - -\begin{verbatim} -... -Assume A and B. -... -\end{verbatim} - -This is possible by declaring \verb=Ind= as transparent: - -\begin{coq_example*} -Add Natural Transparent Ind. -\end{coq_example*} - -By default, \verb=and=, \verb=or=, \verb=ex=, \verb=exT=, \verb=sig= -are declared as inductive transparent constants. As for implicit and -contractible constants, you can remove or test an inductive -constant declared transparent. - -As for implicit and contractible constants, you can remove or test an -inductive constant declared transparent. - -\asubsection{Extending the maximal depth of nested text} - -The depth of nested text is limited. To know the current depth, do: - -\comindex{Set Natural Depth} -\begin{coq_example} -Set Natural Depth. -\end{coq_example} - -To change the maximal depth of nested text (for instance to 125) do: - -\begin{coq_example} -Set Natural Depth 125. -\end{coq_example} - -\asubsection{Restoring the default parameterization} - -The command \verb=Set Natural Default= sets back the parameterization tables of -\Natural~ to their default values, as listed in the above sections. -Moreover, the language is set back to English and the max depth of -nested text is set back to its initial value. - -\asubsection{Printing the current parameterization} - -The commands {\tt Print Natural Implicit}, {\tt Print Natural -Contractible} and {\tt Print \\ Natural Transparent} print the list of -constructions declared {\tt Implicit}, {\tt Contractible}, -{\tt Transparent} respectively. - -\asubsection{Interferences with \texttt{Reset}} - -The customization of \texttt{Natural} is dependent of the \texttt{Reset} -command. If you reset the environment back to a point preceding an -\verb=Add Natural ...= command, the effect of the command will be -erased. Similarly, a reset back to a point before a -\verb=Remove Natural ... = command invalidates the removal. - -\asection{Error messages} - -An error occurs when trying to \verb=Print=, to \verb=Add=, to -\verb=Test=, or to \verb=remove= an undefined ident. Similarly, an -error occurs when trying to set a language unknown from \Natural. -Errors may also occur when trying to parameterize the printing of -proofs: some parameterization are effectively forbidden. -Note that to \verb=Remove= an ident absent from a table or to -\verb=Add= to a table an already present ident does not lead to an -error. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 76bcaaae6..8e078e981 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -42,20 +42,20 @@ operation (see Section~\ref{Caseexpr}). generalized by the corresponding equality. As an example, the expression: -\begin{coq_example*} +\begin{verbatim} match x with | 0 => t | S n => u end. -\end{coq_example*} +\end{verbatim} will be first rewritten to: -\begin{coq_example*} +\begin{verbatim} (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t | S n => fun H : x = S n -> u end) (eq_refl n). -\end{coq_example*} - +\end{verbatim} + This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index d63d22a71..d21c91201 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -749,9 +749,12 @@ Function plus (n m : nat) {struct n} : nat := each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~: +\begin{coq_eval} +Require List. +\end{coq_eval} \begin{coq_example*} - Function wrong (C:nat) : nat := - List.hd(List.map wrong (C::nil)). +Fail Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). \end{coq_example*} For now dependent cases are not treated for non structurally terminating functions. @@ -1633,13 +1636,11 @@ one of the other arguments, then only the type of the first of these arguments is taken into account, and not an upper type of all of them. As a consequence, the inference of the implicit argument of ``='' fails in - \begin{coq_example*} -Check nat = Prop. +Fail Check nat = Prop. \end{coq_example*} -but succeeds in - +but succeeds in \begin{coq_example*} Check Prop = nat. \end{coq_example*} @@ -2010,7 +2011,7 @@ binding as well as those introduced by tactic binding. The expression {\expr} can be any tactic expression as described at section~\ref{TacticLanguage}. \begin{coq_example*} -Definition foo (x : A) : A := $( exact x )$. +Definition foo (x : nat) : nat := $( exact x )$. \end{coq_example*} This construction is useful when one wants to define complicated terms using diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index cf83d0c72..9b527053c 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -587,6 +587,9 @@ is a variable, the {\tt as} clause can be omitted and the term being matched can serve itself as binding name in the return type. For instance, the following alternative definition is accepted and has the same meaning as the previous one. +\begin{coq_eval} +Reset bool_case. +\end{coq_eval} \begin{coq_example*} Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b return or (eq bool b true) (eq bool b false) with @@ -623,7 +626,7 @@ For instance, in the following example: \begin{coq_example*} Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with - | eq_refl => eq_refl A x + | eq_refl _ _ => eq_refl A x end. \end{coq_example*} the type of the branch has type {\tt eq~A~x~x} because the third @@ -1120,7 +1123,7 @@ This is an alternative definition of lists where we specify the arguments of the constructors rather than their full type. \item \begin{coq_example*} -Variant sum (A B:Set) : Set := left : A->sum A B | right : B->Sum A B. +Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. \end{coq_example*} The {\tt Variant} keyword is identical to the {\tt Inductive} keyword, except that it disallows recursive definition of types (in particular diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 7a1189ee3..315acc081 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -485,7 +485,24 @@ apply Rmp. Reset R. \end{coq_eval} +\noindent {\bf Remark: } When the conclusion of the type of the term +to apply is an inductive type isomorphic to a tuple type and {\em apply} +looks recursively whether a component of the tuple matches the goal, +it excludes components whose statement would result in applying an +universal lemma of the form {\tt forall A, ... -> A}. Excluding this +kind of lemma can be avoided by setting the following option: + +\begin{quote} +\optindex{Universal Lemma Under Conjunction} +{\tt Set Universal Lemma Under Conjunction} +\end{quote} + +This option, which preserves compatibility with versions of {\Coq} +prior to 8.4 is also available for {\tt apply {\term} in {\ident}} +(see Section~\ref{apply-in}). + \subsection{\tt apply {\term} in {\ident}} +\label{apply-in} \tacindex{apply \dots\ in} This tactic applies to any goal. The argument {\term} is a term @@ -3129,7 +3146,7 @@ follows: \comindex{Arguments} A constant can be marked to be never unfolded by \texttt{cbn} or \texttt{simpl}: \begin{coq_example*} -Arguments minus x y : simpl never. +Arguments minus n m : simpl never. \end{coq_example*} After that command an expression like \texttt{(minus (S x) y)} is left untouched by the tactics \texttt{cbn} and \texttt{simpl}. @@ -3156,7 +3173,7 @@ A constant can be marked to be unfolded only if an entire set of arguments evaluates to a constructor. The {\tt !} symbol can be used to mark such arguments. \begin{coq_example*} -Arguments minus !x !y. +Arguments minus !n !m. \end{coq_example*} After that command, the expression {\tt (minus (S x) y)} is left untouched by {\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}. @@ -3164,7 +3181,7 @@ After that command, the expression {\tt (minus (S x) y)} is left untouched by A special heuristic to determine if a constant has to be unfolded can be activated with the following command: \begin{coq_example*} -Arguments minus x y : simpl nomatch. +Arguments minus n m : simpl nomatch. \end{coq_example*} The heuristic avoids to perform a simplification step that would expose a {\tt match} construct in head position. For example the diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 907b30b3e..ac28e0ba0 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -114,16 +114,14 @@ Options A and B of the licence are {\em not} elected.} \include{Coercion.v}% \include{CanonicalStructures.v}% \include{Classes.v}% -%%SUPPRIME \include{Natural.v}% \include{Omega.v}% \include{Micromega.v} -%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring \include{Nsatz.v}% \include{Setoid.v}% Tactique pour les setoides -\include{AsyncProofs.v}% Paral-ITP +\include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes \include{Misc.v} %BEGIN LATEX diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 3770ba574..2c9602a22 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -658,17 +658,17 @@ arguments (or whatever subrelation of the pointwise extension). For example, one could declare the \texttt{map} combinator on lists as a morphism: \begin{coq_eval} -Require Import List. +Require Import List Setoid Morphisms. Set Implicit Arguments. Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) := | eq_nil : list_equiv eqA nil nil -| eq_cons : forall x y, eqA x y -> +| eq_cons : forall x y, eqA x y -> forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l'). +Generalizable All Variables. \end{coq_eval} \begin{coq_example*} Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : - Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) - (@map A B). + Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). \end{coq_example*} where \texttt{list\_equiv} implements an equivalence on lists diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 44a0b1d36..44a0b1d36 100755..100644 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 836944ab1..836944ab1 100755..100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex diff --git a/kernel/environ.ml b/kernel/environ.ml index 30b28177c..109e3830c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = let ctxt = env.env_rel_context in { env with - env_rel_context = List.firstn (List.length ctxt - n) ctxt; + env_rel_context = List.skipn n ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = diff --git a/kernel/names.ml b/kernel/names.ml index f217c932c..ae2b3b638 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -453,6 +453,9 @@ module KNset = KNmap.Set - when user and canonical parts differ, we cannot be in a section anymore, hence the dirpath must be empty - two pairs with the same user part should have the same canonical part + in a given environment (though with backtracking, the hash-table can + contains pairs with same user part but different canonical part from + a previous state of the session) Note: since most of the time the canonical and user parts are equal, we handle this case with a particular constructor to spare some memory *) @@ -504,7 +507,7 @@ module KerPair = struct let debug_print kp = str (debug_to_string kp) (** For ordering kernel pairs, both user or canonical parts may make - sense, according to your needs : user for the environments, canonical + sense, according to your needs: user for the environments, canonical for other uses (ex: non-logical things). *) module UserOrd = struct @@ -521,16 +524,9 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - (** Default comparison is on the canonical part *) + (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal - - (** Hash-consing : we discriminate only on the user part, since having - the same user part implies having the same canonical part - (invariant of the system). *) - - let hash = function - | Same kn -> KerName.hash kn - | Dual (kn, _) -> KerName.hash kn + let hash = CanOrd.hash module Self_Hashcons = struct @@ -539,8 +535,20 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let equal x y = (user x) == (user y) - let hash = hash + let equal x y = (* physical comparison on subterms *) + x == y || + match x,y with + | Same x, Same y -> x == y + | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy + | (Same _ | Dual _), _ -> false + (** Hash-consing (despite having the same user part implies having + the same canonical part is a logical invariant of the system, it + is not necessarily an invariant in memory, so we treat kernel + names as they are syntactically for hash-consing) *) + let hash = function + | Same kn -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) end module HashKP = Hashcons.Make(Self_Hashcons) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 03fe2122c..2858a5c1f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -270,6 +270,18 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function str"It cannot be used in a binder.") else n +let ltac_interp_name_env k0 lvar env = + (* envhd is the initial part of the env when pretype was called first *) + (* (in practice is is probably 0, but we have to grant the + specification of pretype which accepts to start with a non empty + rel_context) *) + (* tail is the part of the env enriched by pretyping *) + let n = rel_context_length (rel_context env) - k0 in + let ctxt,_ = List.chop n (rel_context env) in + let env = pop_rel_context n env in + let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in + push_rel_context ctxt env + let invert_ltac_bound_name lvar env id0 id = let id = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id (rel_context env))) @@ -285,17 +297,14 @@ let protected_get_type_of env sigma c = (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") -let pretype_id pretype loc env evdref lvar id = +let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try - let id = - try Id.Map.find id lvar.ltac_idents - with Not_found -> id - in let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> + let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in @@ -413,10 +422,10 @@ let is_GHole = function let evars = ref Id.Map.empty -let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in - let pretype_type = pretype_type resolve_tc in - let pretype = pretype resolve_tc in + let pretype_type = pretype_type k0 resolve_tc in + let pretype = pretype k0 resolve_tc in match t with | GRef (loc,ref,u) -> inh_conv_coerce_to_tycon loc env evdref @@ -425,7 +434,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var | GVar (loc, id) -> inh_conv_coerce_to_tycon loc env evdref - (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id) + (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) tycon | GEvar (loc, id, inst) -> @@ -436,12 +445,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var with Not_found -> user_err_loc (loc,"",str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in - let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in + let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> + let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with | Some ty -> ty @@ -450,6 +460,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, naming, None) -> + let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with | Some ty -> ty @@ -458,6 +469,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (loc, k, _naming, Some arg) -> + let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with | Some ty -> ty @@ -474,12 +486,14 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = (na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl + let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in + type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in + let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in + type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in let ctxtv = Array.map (type_bl env empty_rel_context) bl in let larj = Array.map2 @@ -647,9 +661,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let name = ltac_interp_name lvar name in let var = (name,None,j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in + let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -658,7 +672,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let name = ltac_interp_name lvar name in let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in @@ -668,6 +681,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let env' = push_rel_assum var env in pretype_type empty_valcon env' evdref lvar c2 in + let name = ltac_interp_name lvar name in let resj = try judge_of_product env name j j' @@ -689,10 +703,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let name = ltac_interp_name lvar name in let var = (name,Some j.uj_val,t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in + let name = ltac_interp_name lvar name in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } @@ -712,8 +726,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var if not (Int.equal (List.length nal) cs.cs_nargs) then user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); - let nal = List.map (fun na -> ltac_interp_name lvar na) nal in - let na = ltac_interp_name lvar na in let fsign, record = match get_projections env indf with | None -> List.map2 (fun na (_,c,t) -> (na,c,t)) @@ -729,10 +741,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (na, c, t) :: aux (n+1) k names l | [], [] -> [] | _ -> assert false - in aux 1 1 (List.rev nal) cs.cs_args, true - in + in aux 1 1 (List.rev nal) cs.cs_args, true in let obj ind p v f = if not record then + let nal = List.map (fun na -> ltac_interp_name lvar na) nal in + let nal = List.rev nal in + let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) @@ -818,7 +832,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var | None -> let p = match tycon with | Some ty -> ty - | None -> new_type_evar env evdref loc + | None -> + let env = ltac_interp_name_env k0 lvar env in + new_type_evar env evdref loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -854,9 +870,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> - let (tml,eqns) = - Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns - in Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) @@ -903,13 +916,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon -and pretype_instance resolve_tc env evdref lvar loc hyps evk update = +and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f (id,_,t) (subst,update) = let t = replace_vars subst t in let c, update = try let c = List.assoc id update in - let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in + let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in c.uj_val, List.remove_assoc id update with Not_found -> try @@ -929,7 +942,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type resolve_tc valcon env evdref lvar = function +and pretype_type k0 resolve_tc valcon env evdref lvar = function | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> @@ -945,11 +958,12 @@ and pretype_type resolve_tc valcon env evdref lvar = function { utj_val = v; utj_type = s } | None -> + let env = ltac_interp_name_env k0 lvar env in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) | c -> - let j = pretype resolve_tc empty_tycon env evdref lvar c in + let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -962,13 +976,14 @@ and pretype_type resolve_tc valcon env evdref lvar = function let ise_pretype_gen flags env sigma lvar kind c = let evdref = ref sigma in + let k0 = rel_context_length (rel_context env) in let c' = match kind with | WithoutTypeConstraint -> - (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val | OfType exptyp -> - (pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val | IsType -> - (pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val + (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in process_inference_flags flags env sigma (!evdref,c') @@ -1003,14 +1018,16 @@ let on_judgment f j = let understand_judgment env sigma c = let evdref = ref sigma in - let j = pretype true empty_tycon env evdref empty_lvar c in + let k0 = rel_context_length (rel_context env) in + let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let j = pretype true empty_tycon env evdref empty_lvar c in + let k0 = rel_context_length (rel_context env) in + let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in evdref := evd; c) j diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 142b54513..a6aa08657 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -123,11 +123,11 @@ val check_evars_are_solved : (**/**) (** Internal of Pretyping... *) val pretype : - bool -> type_constraint -> env -> evar_map ref -> + int -> bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - bool -> val_constraint -> env -> evar_map ref -> + int -> bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val ise_pretype_gen : diff --git a/stm/stm.ml b/stm/stm.ml index 9e82dd156..bf91c3aa4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1688,7 +1688,10 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, None, accn, name, delegate name) - | `Sideff _ -> `Sync (no_name,None,`NestedProof) + | `Sideff _ -> + Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^ + "stop working in the next Coq version"))); + `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in let make_sync why = function | `Sync(name,pua,_) -> `Sync (name,pua,why) @@ -1837,7 +1840,6 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, _, `Immediate) -> (fun () -> - assert (Stateid.equal view.next eop); reach eop; vernac_interp id x; Proof_global.discard_all () ), `Yes, true | `Sync (name, pua, reason) -> (fun () -> @@ -1856,9 +1858,8 @@ let known_state ?(redefine_qed=false) ~cache id = Some(Proof_global.close_proof ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - reach view.next; - if keep == VtKeepAsAxiom then - Option.iter (vernac_interp id) pua; + if keep != VtKeepAsAxiom then + reach view.next; let wall_clock2 = Unix.gettimeofday () in vernac_interp id ?proof x; let wall_clock3 = Unix.gettimeofday () in @@ -2306,9 +2307,7 @@ let edit_at id = let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else match VCS.visit tip with - | { next } when next = root -> root - | { step = `Fork _ } -> tip - | { step = `Sideff (`Ast(_,id)|`Id id) } -> id + | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 402a9e88a..6d81a4870 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -109,6 +109,24 @@ let _ = optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } +(* Compatibility option useful in developments using apply intensively + in ltac code *) + +let universal_lemma_under_conjunctions = ref false + +let accept_universal_lemma_under_conjunctions () = + !universal_lemma_under_conjunctions + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "trivial unification in tactics applying under conjunctions"; + optkey = ["Universal";"Lemma";"Under";"Conjunction"]; + optread = (fun () -> !universal_lemma_under_conjunctions) ; + optwrite = (fun b -> universal_lemma_under_conjunctions := b) } + + (*********************************************) (* Tactics *) (*********************************************) @@ -1332,7 +1350,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) && not (isEvar (fst (whd_betaiota_stack sigma t))) - && not (isRel t && destRel t > n-i) + && (accept_universal_lemma_under_conjunctions () || not (isRel t)) then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v new file mode 100644 index 000000000..eb0d206c5 --- /dev/null +++ b/test-suite/bugs/closed/3779.v @@ -0,0 +1,11 @@ +Set Universe Polymorphism. +Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }. +Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T. +Section foo. + Universes sm lg. + Context (O : UnitSubuniverse@{sm lg}). + Context {A : Type@{sm}}. + Context (H' : forall (C : Type@{lg}) `{In@{sm lg} O C} (f : A -> C), In@{sm lg} O C). + Fail Check (H' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C). + Fail Context (H'' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C). +End foo. diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v new file mode 100644 index 000000000..bc120fb1f --- /dev/null +++ b/test-suite/bugs/closed/4221.v @@ -0,0 +1,9 @@ +(* Some test checking that interpreting binder names using ltac + context does not accidentally break the bindings *) + +Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False. + intros H0 x. + lazymatch goal with + | [ x : forall k : nat, _ |- _ ] + => specialize (fun H0 => x 1 H0) + end. diff --git a/test-suite/bugs/closed/4254.v b/test-suite/bugs/closed/4254.v new file mode 100644 index 000000000..ef219973d --- /dev/null +++ b/test-suite/bugs/closed/4254.v @@ -0,0 +1,13 @@ +Inductive foo (V:Type):Type := + | Foo : list (bar V) -> foo V +with bar (V:Type): Type := + | bar1: bar V + | bar2 : V -> bar V. + +Module WithPoly. +Polymorphic Inductive foo (V:Type):Type := + | Foo : list (bar V) -> foo V +with bar (V:Type): Type := + | bar1: bar V + | bar2 : V -> bar V. +End WithPoly. diff --git a/test-suite/interactive/4289.v b/test-suite/interactive/4289.v new file mode 100644 index 000000000..610a509c9 --- /dev/null +++ b/test-suite/interactive/4289.v @@ -0,0 +1,14 @@ +(* Checking backtracking with modules which used to fail due to an + hash-consing bug *) + +Module Type A. + Axiom B : nat. +End A. +Module C (a : A). + Include a. + Definition c : nat := B. +End C. +Back 4. +Module C (a : A). + Include a. + Definition c : nat := B. diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index 0d75d52a3..0d75d52a3 100755..100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 0d75d52a3..0d75d52a3 100755..100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index a4ed76c5a..074004fa1 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -333,13 +333,10 @@ exact (refl_equal 3). exact (refl_equal 4). Qed. -(* From 12612, descent in conjunctions is more powerful *) +(* From 12612, Dec 2009, descent in conjunctions is more powerful *) (* The following, which was failing badly in bug 1980, is now properly rejected, as descend in conjunctions builds an - ill-formed elimination from Prop to Type. - - Added Aug 2014: why it fails is now that trivial unification ?x = goal is - rejected by the descent in conjunctions to avoid surprising results. *) + ill-formed elimination from Prop to the domain of ex which is in Type. *) Goal True. Fail eapply ex_intro. @@ -351,28 +348,32 @@ Fail eapply (ex_intro _). exact I. Qed. -(* Note: the following succeed directly (i.e. w/o "exact I") since - Aug 2014 since the descent in conjunction does not use a "cut" - anymore: the iota-redex is contracted and we get rid of the - uninstantiated evars - - Is it good or not? Maybe it does not matter so much. +(* No failure here, because the domain of ex is in Prop *) Goal True. -eapply (ex_intro (fun _ => True) I). -exact I. (* Not needed since Aug 2014 *) +eapply (ex_intro (fun _ => 0=0) I). +reflexivity. Qed. Goal True. -eapply (ex_intro (fun _ => True) I _). -exact I. (* Not needed since Aug 2014 *) +eapply (ex_intro (fun _ => 0=0) I _). +Unshelve. (* In 8.4: Grab Existential Variables. *) +reflexivity. Qed. Goal True. eapply (fun (A:Prop) (x:A) => conj I x). -exact I. (* Not needed since Aug 2014 *) +Unshelve. (* In 8.4: the goal ?A was there *) +exact I. Qed. -*) + +(* Testing compatibility mode with v8.4 *) + +Goal True. +Fail eapply existT. +Set Universal Lemma Under Conjunction. +eapply existT. +Abort. (* The following was not accepted from r12612 to r12657 *) @@ -463,6 +464,7 @@ Abort. Goal forall H:0=0, H = H. intros. Fail apply eq_sym in H. +Abort. (* Check that unresolved evars not originally present in goal prevent apply in to work*) diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index badce063e..f9df021dc 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,3 +298,11 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. + +(* Check instantiation of binders using ltac names *) + +Goal True. +let x := ipattern:y in assert (forall x y, x = y + 0). +intro. +destruct y. (* Check that the name is y here *) +Abort. diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex deleted file mode 100755 index 655de34ca..000000000 --- a/theories/Arith/intro.tex +++ /dev/null @@ -1,55 +0,0 @@ -\section{Arith}\label{Arith} - -The {\tt Arith} library deals with various arithmetical notions and -their properties. - -\subsection*{Standard {\tt Arith} library} - -The following files are automatically loaded by {\tt Require Arith}. - -\begin{itemize} - -\item {\tt Le.v} states and proves properties of the large order {\tt le}. - -\item {\tt Lt.v} states and proves properties of the strict order {\tt -lt} (especially, the relationship with {\tt le}). - -\item {\tt Plus.v} states and proves properties on the addition. - -\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. - -\item {\tt Minus.v} defines the difference on -{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is -{\tt O} if {\tt n} $<$ {\tt p}. - -\item {\tt Mult.v} states and proves properties on the multiplication. - -\item {\tt Between.v} defines modalities on {\tt nat} and proves properties -of them. - -\end{itemize} - -\subsection*{Additional {\tt Arith} library} - -\begin{itemize} - -\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state -and prove various decidability results on {\tt nat}. - -\item {\tt Wf\_nat.v} states and proves various induction and recursion -principles on {\tt nat}. Especially, recursion for objects measurable by -a natural number and recursion on {\tt nat * nat} are provided. - -\item {\tt Min.v} defines the minimum of two natural numbers and proves -properties of it. - -\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows -the equivalence with Leibniz' equality. - -\item {\tt Euclid.v} proves that the euclidean -division specification is realisable. Conversely, {\tt Div.v} exhibits -two different algorithms and semi-automatically reconstruct the proof of -their correctness. These files emphasize the extraction of program vs -reconstruction of proofs paradigm. - -\end{itemize} diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex deleted file mode 100644 index 22ee38aab..000000000 --- a/theories/Bool/intro.tex +++ /dev/null @@ -1,16 +0,0 @@ -\section{Bool}\label{Bool} - -The BOOL library includes the following files: - -\begin{itemize} - -\item {\tt Bool.v} defines standard operations on booleans and states - and proves simple facts on them. -\item {\tt IfProp.v} defines a disjunction which contains its proof - and states its properties. -\item {\tt Zerob.v} defines the test against 0 on natural numbers and - states and proves properties of it. -\item {\tt Orb.v} states and proves facts on the boolean or. -\item {\tt DecBool.v} defines a conditional from a proof of - decidability and states its properties. -\end{itemize} diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex deleted file mode 100755 index d372de8ed..000000000 --- a/theories/Lists/intro.tex +++ /dev/null @@ -1,20 +0,0 @@ -\section{Lists}\label{Lists} - -This library includes the following files: - -\begin{itemize} - -\item {\tt List.v} contains definitions of (polymorphic) lists, - functions on lists such as head, tail, map, append and prove some - properties of these functions. Implicit arguments are used in this - library, so you should read the Reference Manual about implicit - arguments before using it. - -\item {\tt ListSet.v} contains definitions and properties of finite - sets, implemented as lists. - -\item {\tt Streams.v} defines the type of infinite lists (streams). It is a - co-inductive type. Basic facts are stated and proved. The streams are - also polymorphic. - -\end{itemize} diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex deleted file mode 100755 index 1fb294f2f..000000000 --- a/theories/Logic/intro.tex +++ /dev/null @@ -1,8 +0,0 @@ -\section{Logic}\label{Logic} - -This library deals with classical logic and its properties. -The main file is {\tt Classical.v}. - -This library also provides some facts on equalities for dependent -types. See the files {\tt Eqdep.v} and {\tt JMeq.v}. - diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex deleted file mode 100644 index bf39bc36c..000000000 --- a/theories/NArith/intro.tex +++ /dev/null @@ -1,5 +0,0 @@ -\section{Binary natural numbers : NArith}\label{NArith} - -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex deleted file mode 100644 index ffce881ed..000000000 --- a/theories/PArith/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Binary positive integers : PArith}\label{PArith} - -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex deleted file mode 100644 index 433172585..000000000 --- a/theories/Reals/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Reals}\label{Reals} - -This library contains an axiomatization of real numbers. -The main file is \texttt{Reals.v}. diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex deleted file mode 100755 index 5056f36f9..000000000 --- a/theories/Relations/intro.tex +++ /dev/null @@ -1,23 +0,0 @@ -\section{Relations}\label{Relations} - -This library develops closure properties of relations. - -\begin{itemize} -\item {\tt Relation\_Definitions.v} deals with the general notions - about binary relations (orders, equivalences, ...) - -\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various - closures of relations (by symmetry, by transitivity, ...) and - lexicographic orderings. - -\item {\tt Operators\_Properties.v} states and proves facts on the - various closures of a relation. - -\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt - Relation\_Operators.v} and \\ - {\tt Operators\_Properties.v} together. - -\item {\tt Newman.v} proves Newman's lemma on noetherian and locally - confluent relations. - -\end{itemize} diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex deleted file mode 100644 index 50cd025de..000000000 --- a/theories/Setoids/intro.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Setoids}\label{Setoids} diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex deleted file mode 100755 index 83c2177fd..000000000 --- a/theories/Sets/intro.tex +++ /dev/null @@ -1,24 +0,0 @@ -\section{Sets}\label{Sets} - -This is a library on sets defined by their characteristic predicate. -It contains the following modules: - -\begin{itemize} -\item {\tt Ensembles.v} -\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v} -\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, - {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\ - {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v} -\item {\tt Partial\_Order.v}, {\tt Cpo.v} -\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, - {\tt Powerset\_Classical\_facts.v} -\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v} -\item {\tt Image.v} -\item {\tt Infinite\_sets.v} -\item {\tt Integers.v} -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex deleted file mode 100644 index 64ae4c888..000000000 --- a/theories/Sorting/intro.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Sorting}\label{Sorting} diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex deleted file mode 100755 index 126071e28..000000000 --- a/theories/Wellfounded/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Well-founded relations}\label{Wellfounded} - -This library gives definitions and results about well-founded relations. - diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex deleted file mode 100755 index 21e52c198..000000000 --- a/theories/ZArith/intro.tex +++ /dev/null @@ -1,6 +0,0 @@ -\section{Binary integers : ZArith} -The {\tt ZArith} library deals with binary integers (those used -by the {\tt Omega} decision tactic). -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/tools/README.coq-tex b/tools/README.coq-tex deleted file mode 100755 index 5c7606a96..000000000 --- a/tools/README.coq-tex +++ /dev/null @@ -1,13 +0,0 @@ -DESCRIPTION. - -The coq-tex filter extracts Coq phrases embedded in LaTeX files, -evaluates them, and insert the outcome of the evaluation after each -phrase. - -The filter is written in Perl, so you'll need Perl version 4 installed -on your machine. - -USAGE. See the manual page (coq-tex.1). - -AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr) - from caml-tex of Xavier Leroy. diff --git a/tools/README.emacs b/tools/README.emacs index 4d8e3697a..4d8e3697a 100755..100644 --- a/tools/README.emacs +++ b/tools/README.emacs diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty index 9f6e5480c..9f6e5480c 100755..100644 --- a/tools/coq-sl.sty +++ b/tools/coq-sl.sty diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 954c21d58..e902370c3 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -843,11 +843,9 @@ let do_makefile args = if not (makefile = None) then close_out !output_channel; exit 0 -let main () = +let _ = let args = if Array.length Sys.argv = 1 then usage (); List.tl (Array.to_list Sys.argv) in do_makefile args - -let _ = Printexc.catch main () diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index fc652f584..dbdc2e9db 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -24,10 +24,7 @@ let hrule = ref false let small = ref false let boot = ref false -let coq_prompt = Str.regexp "Coq < " -let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < " - -let remove_prompt s = Str.replace_first any_prompt "" s +let any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < " (* First pass: extract the Coq phrases to evaluate from [texfile] * and put them into the file [inputv] *) @@ -58,30 +55,19 @@ let extract texfile inputv = ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); outside () with End_of_file -> - begin close_in chan_in; close_out chan_out end + (* a dummy command, just in case the last line was a comment *) + output_string chan_out "Set Printing Width 78.\n"; + close_in chan_in; + close_out chan_out (* Second pass: insert the answers of Coq from [coq_output] into the * TeX file [texfile]. The result goes in file [result]. *) -let begin_coq_example = - Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" -let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" - -let has_match r s = - try let _ = Str.search_forward r s 0 in true with Not_found -> false - -let percent = Str.regexp "%" -let bang = Str.regexp "!" -let expos = Str.regexp "^" - let tex_escaped s = - let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in - let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in + let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in let adapt_delim = function - | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "_" -> "{\\char`\\_}" | "\\" -> "{\\char'134}" | "^" -> "{\\char'136}" | "~" -> "{\\char'176}" @@ -111,99 +97,106 @@ let insert texfile coq_output result = let c_tex = open_in texfile in let c_coq = open_in coq_output in let c_out = open_out result in - (* next_block k : this function reads the next block of Coq output - * removing the k leading prompts. - * it returns the block as a list of string) *) - let last_read = ref "" in - let next_block k = - if !last_read = "" then last_read := input_line c_coq; - (* skip k prompts *) - for _i = 1 to k do - last_read := remove_prompt !last_read; - done; + (* read lines until a prompt is found (starting from the second line), + purge prompts on the first line and return their number *) + let last_read = ref (input_line c_coq) in + let read_output () = + let first = !last_read in + let nb = ref 0 in + (* remove the leading prompts *) + let rec skip_prompts pos = + if Str.string_match any_prompt first pos then + let () = incr nb in + skip_prompts (Str.match_end ()) + else pos in + let first = + let start = skip_prompts 0 in + String.sub first start (String.length first - start) in (* read and return the following lines until a prompt is found *) let rec read_lines () = let s = input_line c_coq in if Str.string_match any_prompt s 0 then begin last_read := s; [] end else - s :: (read_lines ()) - in - let first = !last_read in first :: (read_lines ()) - in - (* we are just after \end{coq_...} block *) - let rec just_after () = + s :: read_lines () in + (first :: read_lines (), !nb) in + let unhandled_output = ref None in + let read_output () = + match !unhandled_output with + | Some some -> unhandled_output := None; some + | None -> read_output () in + (* we are inside a \begin{coq_...} ... \end{coq_...} block + * show_... tell what kind of block it is *) + let rec inside show_answers show_questions not_first discarded = let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 false - end - else begin - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - output_string c_out "\\end{flushleft}\n"; - if !small then output_string c_out "\\end{small}\n"; - if Str.string_match begin_coq_eval s 0 then - eval 0 + if s = "" then + inside show_answers show_questions not_first (discarded + 1) + else if not (Str.string_match end_coq s 0) then begin + let (bl,n) = read_output () in + assert (n > discarded); + let n = n - discarded in + if not_first then output_string c_out "\\medskip\n"; + if !verbose then Printf.printf "Coq < %s\n" s; + if show_questions then encapsule false c_out ("Coq < " ^ s); + let rec read_lines k = + if k = 0 then [] + else + let s = input_line c_tex in + if Str.string_match end_coq s 0 then [] + else s :: read_lines (k - 1) in + let al = read_lines (n - 1) in + if !verbose then List.iter (Printf.printf " %s\n") al; + if show_questions then + List.iter (fun s -> encapsule false c_out (" " ^ s)) al; + let la = n - 1 - List.length al in + if la <> 0 then + (* this happens when the block ends with a comment; the output + is for the command at the beginning of the next block *) + unhandled_output := Some (bl, la) else begin - output_string c_out (s ^ "\n"); - outside () + if !verbose then List.iter print_endline bl; + if show_answers then print_block c_out bl; + inside show_answers show_questions (show_answers || show_questions) 0 end - end + end else if discarded > 0 then begin + (* this happens when the block ends with an empty line *) + let (bl,n) = read_output () in + assert (n > discarded); + unhandled_output := Some (bl, n - discarded) + end in (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) - and outside () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin + let rec outside just_after = + let start_block () = if !small then output_string c_out "\\begin{small}\n"; output_string c_out "\\begin{flushleft}\n"; + if !hrule then output_string c_out "\\hrulefill\\\\\n" in + let end_block () = if !hrule then output_string c_out "\\hrulefill\\\\\n"; - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 true - end else if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - (* we are inside a \begin{coq_example?} ... \end{coq_example?} block - * show_answers tells what kind of block it is - * k is the number of lines read until now *) - and inside show_answers show_questions k first_block = + output_string c_out "\\end{flushleft}\n"; + if !small then output_string c_out "\\end{small}\n" in let s = input_line c_tex in - if Str.string_match end_coq_example s 0 then begin - just_after () + if Str.string_match begin_coq s 0 then begin + let kind = Str.matched_group 1 s in + if kind = "eval" then begin + if just_after then end_block (); + inside false false false 0; + outside false + end else begin + let show_answers = kind <> "example*" in + let show_questions = kind <> "example#" in + if not just_after then start_block (); + inside show_answers show_questions just_after 0; + outside true + end end else begin - let prompt = if k = 0 then "Coq < " else " " in - if !verbose then Printf.printf "%s%s\n" prompt s; - if (not first_block) && k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out (prompt ^ s); - if has_match dot_end_line s then begin - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - if show_answers then print_block c_out bl; - inside show_answers show_questions 0 false - end else - inside show_answers show_questions (succ k) first_block - end - (* we are inside a \begin{coq_eval} ... \end{coq_eval} block - * k is the number of lines read until now *) - and eval k = - let s = input_line c_tex in - if Str.string_match end_coq_eval s 0 then - outside () - else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if has_match dot_end_line s then - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - eval 0 - else - eval (succ k) - end - in + if just_after then end_block (); + output_string c_out (s ^ "\n"); + outside false + end in try - let _ = next_block 0 in (* to skip the Coq banner *) - let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *) - outside () + let _ = read_output () in (* to skip the Coq banner *) + let _ = read_output () in (* to skip the Coq answer to Set Printing Width *) + outside false with End_of_file -> begin close_in c_tex; close_in c_coq; @@ -212,7 +205,7 @@ let insert texfile coq_output result = (* Process of one TeX file *) -let rm f = try Sys.remove f with any -> () +let rm f = try Sys.remove f with _ -> () let one_file texfile = let inputv = Filename.temp_file "coq_tex" ".v" in @@ -281,7 +274,7 @@ let find_coqtop () = "coqtop" end -let main () = +let _ = parse_cl (); if !image = "" then image := Filename.quote (find_coqtop ()); if !boot then image := !image ^ " -boot"; @@ -294,5 +287,3 @@ let main () = flush stdout end; List.iter one_file (List.rev !files) - -let _ = Printexc.catch main () diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 9531cd2b0..2554ed495 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -557,10 +557,8 @@ let produce_output fl = (*s \textbf{Main program.} Print the banner, parse the command line, read the files and then call [produce_document] from module [Web]. *) -let main () = +let _ = let files = parse () in Index.init_coqlib_library (); if not !quiet then banner (); if files <> [] then produce_output files - -let _ = Printexc.catch main () diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 417ec5355..9a42553da 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -276,7 +276,7 @@ let rec parse = function (*s Main program. *) -let main () = +let _ = let files = parse (List.tl (Array.to_list Sys.argv)) in if not (!spec_only || !proof_only) then printf " spec proof comments\n"; @@ -285,8 +285,6 @@ let main () = | [f] -> process_file f | _ -> List.iter process_file files; print_totals () -let _ = Printexc.catch main () - (*i*)}(*i*) diff --git a/tools/gallina.ml b/tools/gallina.ml index 279919c58..5ce19e7f8 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -39,7 +39,7 @@ let traite_stdin () = with Sys_error _ -> () -let gallina () = +let _ = let lg_command = Array.length Sys.argv in if lg_command < 2 then begin output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n"; @@ -59,6 +59,3 @@ let gallina () = traite_stdin () else List.iter traite_fichier !vfiles - -let _ = Printexc.catch gallina () - diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 15065afda..3c87533a9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -41,8 +41,8 @@ let toploop = ref None let color : [`ON | `AUTO | `OFF] ref = ref `AUTO let set_color = function -| "on" -> color := `ON -| "off" -> color := `OFF +| "yes" | "on" -> color := `ON +| "no" | "off" -> color := `OFF | "auto" -> color := `AUTO | _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 @@ -326,8 +326,8 @@ let get_priority opt s = prerr_endline ("Error: low/high expected after "^opt); exit 1 let get_async_proofs_mode opt = function - | "off" -> Flags.APoff - | "on" -> Flags.APon + | "no" | "off" -> Flags.APoff + | "yes" | "on" -> Flags.APon | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 @@ -341,8 +341,8 @@ let set_worker_id opt s = Flags.async_proofs_worker_id := s let get_bool opt = function - | "yes" -> true - | "no" -> false + | "yes" | "on" -> true + | "no" | "off" -> false | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 let get_int opt n = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 281fb7ef7..1144ffb94 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -58,7 +58,7 @@ let print_usage_channel co command = \n\ \n -quiet unset display of extra information (implies -w none)\ \n -w (all|none) configure display of warnings\ -\n -color (on|off|auto) configure color output\ +\n -color (yes|no|auto) configure color output\ \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ |