diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-decl.tex | 823 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_expr.mli | 102 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 471 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_interp.mli | 15 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 136 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 79 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode_plugin.mlpack | 5 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 1554 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 108 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 387 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 216 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.mli | 14 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 18 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2640.v | 17 | ||||
| -rw-r--r-- | test-suite/ide/undo.v | 103 | ||||
| -rw-r--r-- | test-suite/ide/undo011.fake | 34 | ||||
| -rw-r--r-- | test-suite/success/decl_mode.v | 182 | ||||
| -rw-r--r-- | test-suite/success/decl_mode2.v | 249 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 1 |
23 files changed, 6 insertions, 4517 deletions
@@ -22,6 +22,10 @@ Standard Library - Real constants are now represented using IZR rather than R0 and R1; this might cause rewriting rules to fail to apply to constants. +Plugins + +- The mathematical proof language (also known as declarative mode) was removed. + Changes from V8.6beta1 to V8.6 ============================== diff --git a/Makefile.common b/Makefile.common index 1e71bcf7d..1d78d3fd5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -61,7 +61,7 @@ PLUGINDIRS:=\ omega romega micromega quote \ setoid_ring extraction fourier \ cc funind firstorder derive \ - rtauto nsatz syntax decl_mode btauto \ + rtauto nsatz syntax btauto \ ssrmatching ltac SRCDIRS:=\ diff --git a/Makefile.doc b/Makefile.doc index 9ae20ba76..39c3255f5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -48,7 +48,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-cic.v.tex RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.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 Universes.v.tex \ diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex deleted file mode 100644 index aae10e323..000000000 --- a/doc/refman/RefMan-decl.tex +++ /dev/null @@ -1,823 +0,0 @@ -\newcommand{\DPL}{Mathematical Proof Language} - -\chapter{The \DPL\label{DPL}\index{DPL}} - -\section{Introduction} - -\subsection{Foreword} - -In this chapter, we describe an alternative language that may be used -to do proofs using the Coq proof assistant. The language described -here uses the same objects (proof-terms) as Coq, but it differs in the -way proofs are described. This language was created by Pierre -Corbineau at the Radboud University of Nijmegen, The Netherlands. - -The intent is to provide language where proofs are less formalism-{} -and implementation-{}sensitive, and in the process to ease a bit the -learning of computer-{}aided proof verification. - -\subsection{What is a declarative proof?} -In vanilla Coq, proofs are written in the imperative style: the user -issues commands that transform a so called proof state until it -reaches a state where the proof is completed. In the process, the user -mostly described the transitions of this system rather than the -intermediate states it goes through. - -The purpose of a declarative proof language is to take the opposite -approach where intermediate states are always given by the user, but -the transitions of the system are automated as much as possible. - -\subsection{Well-formedness and Completeness} - -The \DPL{} introduces a notion of well-formed -proofs which are weaker than correct (and complete) -proofs. Well-formed proofs are actually proof script where only the -reasoning is incomplete. All the other aspects of the proof are -correct: -\begin{itemize} -\item All objects referred to exist where they are used -\item Conclusion steps actually prove something related to the - conclusion of the theorem (the {\tt thesis}. -\item Hypothesis introduction steps are done when the goal is an - implication with a corresponding assumption. -\item Sub-objects in the elimination steps for tuples are correct - sub-objects of the tuple being decomposed. -\item Patterns in case analysis are type-correct, and induction is well guarded. -\end{itemize} - -\subsection{Note for tactics users} - -This section explain what differences the casual Coq user will -experience using the \DPL. -\begin{enumerate} -\item The focusing mechanism is constrained so that only one goal at - a time is visible. -\item Giving a statement that Coq cannot prove does not produce an - error, only a warning: this allows going on with the proof and fill - the gap later. -\item Tactics can still be used for justifications and after -{\texttt{escape}}. -\end{enumerate} - -\subsection{Compatibility} - -The \DPL{} is available for all Coq interfaces that use -text-based interaction, including: -\begin{itemize} -\item the command-{}line toplevel {\texttt{coqtop}} -\item the native GUI {\CoqIDE} -\item the {\ProofGeneral} Emacs mode -\item Cezary Kaliszyk'{}s Web interface -\item L.E. Mamane'{}s tmEgg TeXmacs plugin -\end{itemize} - -However it is not supported by structured editors such as PCoq. - - - -\section{Syntax} - -Here is a complete formal description of the syntax for \DPL{} commands. - -\begin{figure}[htbp] -\begin{centerframe} -\begin{tabular}{lcl@{\qquad}r} - instruction & ::= & {\tt proof} \\ - & $|$ & {\tt assume } \nelist{statement}{\tt and} - \zeroone{[{\tt and } \{{\tt we have}\}-clause]} \\ - & $|$ & \{{\tt let},{\tt be}\}-clause \\ - & $|$ & \{{\tt given}\}-clause \\ - & $|$ & \{{\tt consider}\}-clause {\tt from} term \\ - & $|$ & ({\tt have} $|$ {\tt then} $|$ {\tt thus} $|$ {\tt hence}]) statement - justification \\ - & $|$ & \zeroone{\tt thus} ($\sim${\tt =}|{\tt =}$\sim$) \zeroone{\ident{\tt :}}\term\relax justification \\ & $|$ & {\tt suffices} (\{{\tt to have}\}-clause $|$ - \nelist{statement}{\tt and } \zeroone{{\tt and} \{{\tt to have}\}-clause})\\ - & & {\tt to show} statement justification \\ - & $|$ & ({\tt claim} $|$ {\tt focus on}) statement \\ - & $|$ & {\tt take} \term \\ - & $|$ & {\tt define} \ident \sequence{var}{,} {\tt as} \term\\ - & $|$ & {\tt reconsider} (\ident $|$ {\tt thesis}) {\tt as} type\\ - & $|$ & - {\tt per} ({\tt cases}$|${\tt induction}) {\tt on} \term \\ - & $|$ & {\tt per cases of} type justification \\ - & $|$ & {\tt suppose} \zeroone{\nelist{ident}{,} {\tt and}}~ - {\tt it is }pattern\\ - & & \zeroone{{\tt such that} \nelist{statement} {\tt and} \zeroone{{\tt and} \{{\tt we have}\}-clause}} \\ - & $|$ & {\tt end} - ({\tt proof} $|$ {\tt claim} $|$ {\tt focus} $|$ {\tt cases} $|$ {\tt induction}) \\ - & $|$ & {\tt escape} \\ - & $|$ & {\tt return} \medskip \\ - \{$\alpha,\beta$\}-clause & ::=& $\alpha$ \nelist{var}{,}~ - $\beta$ {\tt such that} \nelist{statement}{\tt and } \\ - & & \zeroone{{\tt and } \{$\alpha,\beta$\}-clause} \medskip\\ - statement & ::= & \zeroone{\ident {\tt :}} type \\ - & $|$ & {\tt thesis} \\ - & $|$ & {\tt thesis for} \ident \medskip \\ - var & ::= & \ident \zeroone{{\tt :} type} \medskip \\ - justification & ::= & - \zeroone{{\tt by} ({\tt *} | \nelist{\term}{,})} - ~\zeroone{{\tt using} tactic} \\ -\end{tabular} -\end{centerframe} -\caption{Syntax of mathematical proof commands} -\end{figure} - -The lexical conventions used here follows those of section \ref{lexical}. - - -Conventions:\begin{itemize} - - \item {\texttt{<{}tactic>{}}} stands for a Coq tactic. - - \end{itemize} - -\subsection{Temporary names} - -In proof commands where an optional name is asked for, omitting the -name will trigger the creation of a fresh temporary name (e.g. for a -hypothesis). Temporary names always start with an underscore `\_' -character (e.g. {\tt \_hyp0}). Temporary names have a lifespan of one -command: they get erased after the next command. They can however be safely in the step after their creation. - -\section{Language description} - -\subsection{Starting and Ending a mathematical proof} - -The standard way to use the \DPL{} is to first state a \texttt{Lemma} / -\texttt{Theorem} / \texttt{Definition} and then use the \texttt{proof} -command to switch the current subgoal to mathematical mode. After the -proof is completed, the \texttt{end proof} command will close the -mathematical proof. If any subgoal remains to be proved, they will be -displayed using the usual Coq display. - -\begin{coq_example} -Theorem this_is_trivial: True. -proof. - thus thesis. -end proof. -Qed. -\end{coq_example} - -The {\texttt{proof}} command only applies to \emph{one subgoal}, thus -if several sub-goals are already present, the {\texttt{proof ... end - proof}} sequence has to be used several times. - -\begin{coq_example*} -Theorem T: (True /\ True) /\ True. - split. split. -\end{coq_example*} -\begin{coq_example} - Show. - proof. (* first subgoal *) - thus thesis. - end proof. - trivial. (* second subgoal *) - proof. (* third subgoal *) - thus thesis. - end proof. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -As with all other block structures, the {\texttt{end proof}} command -assumes that your proof is complete. If not, executing it will be -equivalent to admitting that the statement is proved: A warning will -be issued and you will not be able to run the {\texttt{Qed}} -command. Instead, you can run {\texttt{Admitted}} if you wish to start -another theorem and come back -later. - -\begin{coq_example} -Theorem this_is_not_so_trivial: False. -proof. -end proof. (* here a warning is issued *) -Fail Qed. (* fails: the proof in incomplete *) -Admitted. (* Oops! *) -\end{coq_example} -\begin{coq_eval} -Reset this_is_not_so_trivial. -\end{coq_eval} - -\subsection{Switching modes} - -When writing a mathematical proof, you may wish to use procedural -tactics at some point. One way to do so is to write a using-{}phrase -in a deduction step (see section~\ref{justifications}). The other way -is to use an {\texttt{escape...return}} block. - -\begin{coq_eval} -Theorem T: True. -proof. -\end{coq_eval} -\begin{coq_example} - Show. - escape. - auto. - return. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -The return statement expects all subgoals to be closed, otherwise a -warning is issued and the proof cannot be saved anymore. - -It is possible to use the {\texttt{proof}} command inside an -{\texttt{escape...return}} block, thus nesting a mathematical proof -inside a procedural proof inside a mathematical proof... - -\subsection{Computation steps} - -The {\tt reconsider ... as} command allows changing the type of a hypothesis or of {\tt thesis} to a convertible one. - -\begin{coq_eval} -Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False). -intros a b. -proof. -assume H:(if a then True else False). -\end{coq_eval} -\begin{coq_example} - Show. - reconsider H as False. - reconsider thesis as True. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - - -\subsection{Deduction steps} - -The most common instruction in a mathematical proof is the deduction -step: it asserts a new statement (a formula/type of the \CIC) and tries -to prove it using a user-provided indication: the justification. The -asserted statement is then added as a hypothesis to the proof context. - -\begin{coq_eval} -Theorem T: forall x, x=2 -> 2+x=4. -proof. -let x be such that H:(x=2). -\end{coq_eval} -\begin{coq_example} - Show. - have H':(2+x=2+2) by H. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -It is often the case that the justifications uses the last hypothesis -introduced in the context, so the {\tt then} keyword can be used as a -shortcut, e.g. if we want to do the same as the last example: - -\begin{coq_eval} -Theorem T: forall x, x=2 -> 2+x=4. -proof. -let x be such that H:(x=2). -\end{coq_eval} -\begin{coq_example} - Show. - then (2+x=2+2). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -In this example, you can also see the creation of a temporary name {\tt \_fact}. - -\subsection{Iterated equalities} - -A common proof pattern when doing a chain of deductions is to do -multiple rewriting steps over the same term, thus proving the -corresponding equalities. The iterated equalities are a syntactic -support for this kind of reasoning: - -\begin{coq_eval} -Theorem T: forall x, x=2 -> x + x = x * x. -proof. -let x be such that H:(x=2). -\end{coq_eval} -\begin{coq_example} - Show. - have (4 = 4). - ~= (2 * 2). - ~= (x * x) by H. - =~ (2 + 2). - =~ H':(x + x) by H. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Notice that here we use temporary names heavily. - -\subsection{Subproofs} - -When an intermediate step in a proof gets too complicated or involves a -well contained set of intermediate deductions, it can be useful to insert -its proof as a subproof of the current proof. This is done by using the -{\tt claim ... end claim} pair of commands. - -\begin{coq_eval} -Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. -proof. -let x be such that H:(x + x = x * x). -\end{coq_eval} -\begin{coq_example} -Show. -claim H':((x - 2) * x = 0). -\end{coq_example} - -A few steps later... - -\begin{coq_example} -thus thesis. -end claim. -\end{coq_example} - -Now the rest of the proof can happen. - -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Conclusion steps} - -The commands described above have a conclusion counterpart, where the -new hypothesis is used to refine the conclusion. - -\begin{figure}[b] - \centering -\begin{tabular}{c|c|c|c|c|} - X & \,simple\, & \,with previous step\, & - \,opens sub-proof\, & \,iterated equality\, \\ -\hline -intermediate step & {\tt have} & {\tt then} & - {\tt claim} & {\tt $\sim$=/=$\sim$}\\ -conclusion step & {\tt thus} & {\tt hence} & - {\tt focus on} & {\tt thus $\sim$=/=$\sim$}\\ -\hline -\end{tabular} -\caption{Correspondence between basic forward steps and conclusion steps} -\end{figure} - -Let us begin with simple examples: - -\begin{coq_eval} -Theorem T: forall (A B:Prop), A -> B -> A /\ B. -intros A B HA HB. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -hence B. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -In the next example, we have to use {\tt thus} because {\tt HB} is no longer -the last hypothesis. - -\begin{coq_eval} -Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C. -intros A B C HA HB HC. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -thus B by HB. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -The command fails if the refinement process cannot find a place to fit -the object in a proof of the conclusion. - - -\begin{coq_eval} -Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. -intros A B C HA HB HC. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -Fail hence C. (* fails *) -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -The refinement process may induce non -reversible choices, e.g. when proving a disjunction it may {\it - choose} one side of the disjunction. - -\begin{coq_eval} -Theorem T: forall (A B:Prop), B -> A \/ B. -intros A B HB. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -hence B. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -In this example you can see that the right branch was chosen since {\tt D} remains to be proved. - -\begin{coq_eval} -Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D). -intros A B C D HC HD. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -thus C by HC. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Now for existential statements, we can use the {\tt take} command to -choose {\tt 2} as an explicit witness of existence. - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. -intros P HP. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -take 2. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -It is also possible to prove the existence directly. - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. -intros P HP. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -hence (P 2). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Here a more involved example where the choice of {\tt P 2} propagates -the choice of {\tt 2} to another part of the formula. - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y. -intros P R HP HR. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -thus (P 2) by HP. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Now, an example with the {\tt suffices} command. {\tt suffices} -is a sort of dual for {\tt have}: it allows replacing the conclusion -(or part of it) by a sufficient condition. - -\begin{coq_eval} -Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B. -intros A B P HP HA. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -suffices to have x such that HP':(P x) to show B by HP,HP'. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Finally, an example where {\tt focus} is handy: local assumptions. - -\begin{coq_eval} -Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). -intros A P HP HA. -proof. -\end{coq_eval} -\begin{coq_example} -Show. -focus on (forall x, x = 2 -> P x). -let x be such that (x = 2). -hence thesis by HP. -end focus. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Declaring an Abbreviation} - -In order to shorten long expressions, it is possible to use the {\tt - define ... as ...} command to give a name to recurring expressions. - -\begin{coq_eval} -Theorem T: forall x, x = 0 -> x + x = x * x. -proof. -let x be such that H:(x = 0). -\end{coq_eval} -\begin{coq_example} -Show. -define sqr x as (x * x). -reconsider thesis as (x + x = sqr x). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Introduction steps} - -When the {\tt thesis} consists of a hypothetical formula (implication -or universal quantification (e.g. \verb+A -> B+), it is possible to -assume the hypothetical part {\tt A} and then prove {\tt B}. In the -\DPL{}, this comes in two syntactic flavors that are semantically -equivalent: {\tt let} and {\tt assume}. Their syntax is designed so that -{\tt let} works better for universal quantifiers and {\tt assume} for -implications. - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -\end{coq_eval} -\begin{coq_example} -Show. -let x:nat. -assume HP:(P x). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -In the {\tt let} variant, the type of the assumed object is optional -provided it can be deduced from the command. The objects introduced by -let can be followed by assumptions using {\tt such that}. - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -\end{coq_eval} -\begin{coq_example} -Show. -Fail let x. (* fails because x's type is not clear *) -let x be such that HP:(P x). (* here x's type is inferred from (P x) *) -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -In the {\tt assume } variant, the type of the assumed object is mandatory -but the name is optional: - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. -proof. -let P:(nat -> Prop). -let x:nat. -\end{coq_eval} -\begin{coq_example} -Show. -assume (P x). (* temporary name created *) -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -After {\tt such that}, it is also the case: - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -\end{coq_eval} -\begin{coq_example} -Show. -let x be such that (P x). (* temporary name created *) -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Tuple elimination steps} - -In the \CIC, many objects dealt with in simple proofs are tuples: -pairs, records, existentially quantified formulas. These are so -common that the \DPL{} provides a mechanism to extract members of -those tuples, and also objects in tuples within tuples within -tuples... - -\begin{coq_eval} -Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. -proof. -let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). -\end{coq_eval} -\begin{coq_example} -Show. -consider x such that HP:(P x) and HA:A from H. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Here is an example with pairs: - -\begin{coq_eval} -Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p). -proof. -let p:(nat * nat)%type. -\end{coq_eval} -\begin{coq_example} -Show. -consider x:nat,y:nat from p. -reconsider thesis as (x >= y \/ x < y). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -It is sometimes desirable to combine assumption and tuple -decomposition. This can be done using the {\tt given} command. - -\begin{coq_eval} -Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> -(exists m, P m) -> P 0. -proof. -let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). -\end{coq_eval} -\begin{coq_example} -Show. -given m such that Hm:(P m). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Disjunctive reasoning} - -In some proofs (most of them usually) one has to consider several -cases and prove that the {\tt thesis} holds in all the cases. This is -done by first specifying which object will be subject to case -distinction (usually a disjunction) using {\tt per cases}, and then specifying which case is being proved by using {\tt suppose}. - - -\begin{coq_eval} -Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C. -proof. -let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C). -assume HAB:(A \/ B). -\end{coq_eval} -\begin{coq_example} -per cases on HAB. -suppose A. - hence thesis by HAC. -suppose HB:B. - thus thesis by HB,HBC. -end cases. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -The proof is well formed (but incomplete) even if you type {\tt end - cases} or the next {\tt suppose} before the previous case is proved. - -If the disjunction is derived from a more general principle, e.g. the -excluded middle axiom), it is desirable to just specify which instance -of it is being used: - -\begin{coq_eval} -Section Coq. -\end{coq_eval} -\begin{coq_example} -Hypothesis EM : forall P:Prop, P \/ ~ P. -\end{coq_example} -\begin{coq_eval} -Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. -proof. -let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). -\end{coq_eval} -\begin{coq_example} -per cases of (A \/ ~A) by EM. -suppose (~A). - hence thesis by HNAC. -suppose A. - hence thesis by HAC. -end cases. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Proofs per cases} - -If the case analysis is to be made on a particular object, the script -is very similar: it starts with {\tt per cases on }\emph{object} instead. - -\begin{coq_eval} -Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. -proof. -let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). -\end{coq_eval} -\begin{coq_example} -per cases on (EM A). -suppose (~A). -\end{coq_example} -\begin{coq_eval} -Abort. -End Coq. -\end{coq_eval} - -If the object on which a case analysis occurs in the statement to be -proved, the command {\tt suppose it is }\emph{pattern} is better -suited than {\tt suppose}. \emph{pattern} may contain nested patterns -with {\tt as} clauses. A detailed description of patterns is to be -found in figure \ref{term-syntax-aux}. here is an example. - -\begin{coq_eval} -Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B. -proof. -let A:Prop,B:Prop,x:bool. -\end{coq_eval} -\begin{coq_example} -per cases on x. -suppose it is true. - assume A. - hence A. -suppose it is false. - assume B. - hence B. -end cases. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Proofs by induction} - -Proofs by induction are very similar to proofs per cases: they start -with {\tt per induction on }{\tt object} and proceed with {\tt suppose - it is }\emph{pattern}{\tt and }\emph{induction hypothesis}. The -induction hypothesis can be given explicitly or identified by the -sub-object $m$ it refers to using {\tt thesis for }\emph{m}. - -\begin{coq_eval} -Theorem T: forall (n:nat), n + 0 = n. -proof. -let n:nat. -\end{coq_eval} -\begin{coq_example} -per induction on n. -suppose it is 0. - thus (0 + 0 = 0). -suppose it is (S m) and H:thesis for m. - then (S (m + 0) = S m). - thus =~ (S m + 0). -end induction. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{Justifications}\label{justifications} - - -Intuitively, justifications are hints for the system to understand how -to prove the statements the user types in. In the case of this -language justifications are made of two components: - -Justification objects: {\texttt{by}} followed by a comma-{}separated -list of objects that will be used by a selected tactic to prove the -statement. This defaults to the empty list (the statement should then -be tautological). The * wildcard provides the usual tactics behavior: -use all statements in local context. However, this wildcard should be -avoided since it reduces the robustness of the script. - -Justification tactic: {\texttt{using}} followed by a Coq tactic that -is executed to prove the statement. The default is a solver for -(intuitionistic) first-{}order with equality. - -\section{More details and Formal Semantics} - -I suggest the users looking for more information have a look at the -paper \cite{corbineau08types}. They will find in that paper a formal -semantics of the proof state transition induces by mathematical -commands. diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index dcb98d96b..291c07de4 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -98,7 +98,6 @@ Options A and B of the licence are {\em not} elected.} \include{RefMan-tac.v}% Tactics and tacticals \include{RefMan-ltac.v}% Writing tactics \include{RefMan-tacex.v}% Detailed Examples of tactics -\include{RefMan-decl.v}% The mathematical proof language \part{User extensions} \include{RefMan-syn.v}% The Syntax and the Grammar commands diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli deleted file mode 100644 index 29ecb94ca..000000000 --- a/plugins/decl_mode/decl_expr.mli +++ /dev/null @@ -1,102 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Tacexpr - -type 'it statement = - {st_label:Name.t; - st_it:'it} - -type thesis_kind = - Plain - | For of Id.t - -type 'this or_thesis = - This of 'this - | Thesis of thesis_kind - -type side = Lhs | Rhs - -type elim_type = - ET_Case_analysis - | ET_Induction - -type block_type = - B_proof - | B_claim - | B_focus - | B_elim of elim_type - -type ('it,'constr,'tac) cut = - {cut_stat: 'it; - cut_by: 'constr list option; - cut_using: 'tac option} - -type ('var,'constr) hyp = - Hvar of 'var - | Hprop of 'constr statement - -type ('constr,'tac) casee = - Real of 'constr - | Virtual of ('constr statement,'constr,'tac) cut - -type ('var,'constr,'pat,'tac) bare_proof_instr = - | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr - | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr - | Phence of ('var,'constr,'pat,'tac) bare_proof_instr - | Pcut of ('constr or_thesis statement,'constr,'tac) cut - | Prew of side * ('constr statement,'constr,'tac) cut - | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut - | Passume of ('var,'constr) hyp list - | Plet of ('var,'constr) hyp list - | Pgiven of ('var,'constr) hyp list - | Pconsider of 'constr*('var,'constr) hyp list - | Pclaim of 'constr statement - | Pfocus of 'constr statement - | Pdefine of Id.t * 'var list * 'constr - | Pcast of Id.t or_thesis * 'constr - | Psuppose of ('var,'constr) hyp list - | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list) - | Ptake of 'constr list - | Pper of elim_type * ('constr,'tac) casee - | Pend of block_type - | Pescape - -type emphasis = int - -type ('var,'constr,'pat,'tac) gen_proof_instr= - {emph: emphasis; - instr: ('var,'constr,'pat,'tac) bare_proof_instr } - - -type raw_proof_instr = - ((Id.t * (Constrexpr.constr_expr option)) Loc.located, - Constrexpr.constr_expr, - Constrexpr.cases_pattern_expr, - raw_tactic_expr) gen_proof_instr - -type glob_proof_instr = - ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located, - Tacexpr.glob_constr_and_expr, - Constrexpr.cases_pattern_expr, - Tacexpr.glob_tactic_expr) gen_proof_instr - -type proof_pattern = - {pat_vars: Term.types statement list; - pat_aliases: (Term.constr*Term.types) statement list; - pat_constr: Term.constr; - pat_typ: Term.types; - pat_pat: Glob_term.cases_pattern; - pat_expr: Constrexpr.cases_pattern_expr} - -type proof_instr = - (Term.constr statement, - Term.constr, - proof_pattern, - Geninterp.Val.t) gen_proof_instr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml deleted file mode 100644 index 3b233d6ef..000000000 --- a/plugins/decl_mode/decl_interp.ml +++ /dev/null @@ -1,471 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Ltac_plugin -open CErrors -open Util -open Names -open Constrexpr -open Tacintern -open Decl_expr -open Decl_mode -open Pretyping -open Glob_term -open Term -open Vars -open Pp -open Decl_kinds -open Misctypes - -(* INTERN *) - -let glob_app (loc,hd,args) = if List.is_empty args then hd else GApp(loc,hd,args) - -let intern_justification_items globs = - Option.map (List.map (intern_constr globs)) - -let intern_justification_method globs = - Option.map (intern_pure_tactic globs) - -let intern_statement intern_it globs st = - {st_label=st.st_label; - st_it=intern_it globs st.st_it} - -let intern_no_bind intern_it globs x = - globs,intern_it globs x - -let intern_constr_or_thesis globs = function - Thesis n -> Thesis n - | This c -> This (intern_constr globs c) - -let add_var id globs= - {globs with ltacvars = Id.Set.add id globs.ltacvars} - -let add_name nam globs= - match nam with - Anonymous -> globs - | Name id -> add_var id globs - -let intern_hyp iconstr globs = function - Hvar (loc,(id,topt)) -> add_var id globs, - Hvar (loc,(id,Option.map (intern_constr globs) topt)) - | Hprop st -> add_name st.st_label globs, - Hprop (intern_statement iconstr globs st) - -let intern_hyps iconstr globs hyps = - snd (List.fold_map (intern_hyp iconstr) globs hyps) - -let intern_cut intern_it globs cut= - let nglobs,nstat=intern_it globs cut.cut_stat in - {cut_stat=nstat; - cut_by=intern_justification_items nglobs cut.cut_by; - cut_using=intern_justification_method nglobs cut.cut_using} - -let intern_casee globs = function - Real c -> Real (intern_constr globs c) - | Virtual cut -> Virtual - (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut) - -let intern_hyp_list args globs = - let intern_one globs (loc,(id,opttyp)) = - (add_var id globs), - (loc,(id,Option.map (intern_constr globs) opttyp)) in - List.fold_map intern_one globs args - -let intern_suffices_clause globs (hyps,c) = - let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in - nglobs,(nhyps,intern_constr_or_thesis nglobs c) - -let intern_fundecl args body globs= - let nglobs,nargs = intern_hyp_list args globs in - nargs,intern_constr nglobs body - -let rec add_vars_of_simple_pattern globs = function - CPatAlias (loc,p,id) -> - add_vars_of_simple_pattern (add_var id globs) p -(* Loc.raise loc - (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) - | CPatOr (loc, _)-> - Loc.raise ~loc - (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here")) - | CPatDelimiters (_,_,p) -> - add_vars_of_simple_pattern globs p - | CPatCstr (_,_,pl1,pl2) -> - List.fold_left add_vars_of_simple_pattern - (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2 - | CPatNotation(_,_,(pl,pll),pl') -> - List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll)) - | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs - | _ -> globs - -let rec intern_bare_proof_instr globs = function - Pthus i -> Pthus (intern_bare_proof_instr globs i) - | Pthen i -> Pthen (intern_bare_proof_instr globs i) - | Phence i -> Phence (intern_bare_proof_instr globs i) - | Pcut c -> Pcut - (intern_cut - (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c) - | Psuffices c -> - Psuffices (intern_cut intern_suffices_clause globs c) - | Prew (s,c) -> Prew - (s,intern_cut - (intern_no_bind (intern_statement intern_constr)) globs c) - | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps) - | Pcase (params,pat,hyps) -> - let nglobs,nparams = intern_hyp_list params globs in - let nnglobs= add_vars_of_simple_pattern nglobs pat in - let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in - Pcase (nparams,pat,nhyps) - | Ptake witl -> Ptake (List.map (intern_constr globs) witl) - | Pconsider (c,hyps) -> Pconsider (intern_constr globs c, - intern_hyps intern_constr globs hyps) - | Pper (et,c) -> Pper (et,intern_casee globs c) - | Pend bt -> Pend bt - | Pescape -> Pescape - | Passume hyps -> Passume (intern_hyps intern_constr globs hyps) - | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps) - | Plet hyps -> Plet (intern_hyps intern_constr globs hyps) - | Pclaim st -> Pclaim (intern_statement intern_constr globs st) - | Pfocus st -> Pfocus (intern_statement intern_constr globs st) - | Pdefine (id,args,body) -> - let nargs,nbody = intern_fundecl args body globs in - Pdefine (id,nargs,nbody) - | Pcast (id,typ) -> - Pcast (id,intern_constr globs typ) - -let intern_proof_instr globs instr= - {emph = instr.emph; - instr = intern_bare_proof_instr globs instr.instr} - -(* INTERP *) - -let interp_justification_items env sigma = - Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c)))) - -let interp_constr check_sort env sigma c = - if check_sort then - fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *)) - else - fst (understand env sigma (fst c)) - -let special_whd env = - let infos=CClosure.create_clos_infos CClosure.all env in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) - -let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) - -let decompose_eq env id = - let typ = Environ.named_type id env in - let whd = special_whd env typ in - match kind_of_term whd with - App (f,args)-> - if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 - then args.(0) - else error "Previous step is not an equality." - | _ -> error "Previous step is not an equality." - -let get_eq_typ info env = - let typ = decompose_eq env (get_last env) in - typ - -let interp_constr_in_type typ env sigma c = - fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*) - -let interp_statement interp_it env sigma st = - {st_label=st.st_label; - st_it=interp_it env sigma st.st_it} - -let interp_constr_or_thesis check_sort env sigma = function - Thesis n -> Thesis n - | This c -> This (interp_constr check_sort env sigma c) - -let abstract_one_hyp inject h glob = - match h with - Hvar (loc,(id,None)) -> - GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) - | Hvar (loc,(id,Some typ)) -> - GProd (Loc.ghost,Name id, Explicit, fst typ, glob) - | Hprop st -> - GProd (Loc.ghost,st.st_label, Explicit, inject st.st_it, glob) - -let glob_constr_of_hyps inject hyps head = - List.fold_right (abstract_one_hyp inject) hyps head - -let glob_prop = GSort (Loc.ghost,GProp) - -let rec match_hyps blend names constr = function - [] -> [],substl names constr - | hyp::q -> - let (name,typ,body)=destProd constr in - let st= {st_label=name;st_it=substl names typ} in - let qnames= - match name with - Anonymous -> mkMeta 0 :: names - | Name id -> mkVar id :: names in - let qhyp = match hyp with - Hprop st' -> Hprop (blend st st') - | Hvar _ -> Hvar st in - let rhyps,head = match_hyps blend qnames body q in - qhyp::rhyps,head - -let interp_hyps_gen inject blend env sigma hyps head = - let constr= fst(*FIXME*) (understand env sigma (glob_constr_of_hyps inject hyps head)) in - match_hyps blend [] constr hyps - -let interp_hyps env sigma hyps = fst (interp_hyps_gen fst (fun x _ -> x) env sigma hyps glob_prop) - -let dummy_prefix= Id.of_string "__" - -let rec deanonymize ids = - function - PatVar (loc,Anonymous) -> - let (found,known) = !ids in - let new_id=Namegen.next_ident_away dummy_prefix known in - let _= ids:= (loc,new_id) :: found , new_id :: known in - PatVar (loc,Name new_id) - | PatVar (loc,Name id) as pat -> - let (found,known) = !ids in - let _= ids:= (loc,id) :: found , known in - pat - | PatCstr(loc,cstr,lpat,nam) -> - PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam) - -let rec glob_of_pat = - function - PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable") - | PatVar (loc,Name id) -> - GVar (loc,id) - | PatCstr(loc,((ind,_) as cstr),lpat,_) -> - let mind= fst (Global.lookup_inductive ind) in - let rec add_params n q = - if n<=0 then q else - add_params (pred n) (GHole(Loc.ghost, - Evar_kinds.TomatchTypeParameter(ind,n), Misctypes.IntroAnonymous, None)::q) in - let args = List.map glob_of_pat lpat in - glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None), - add_params mind.Declarations.mind_nparams args) - -let prod_one_hyp = function - (loc,(id,None)) -> - (fun glob -> - GProd (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)) - | (loc,(id,Some typ)) -> - (fun glob -> - GProd (Loc.ghost,Name id, Explicit, fst typ, glob)) - -let prod_one_id (loc,id) glob = - GProd (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) - -let let_in_one_alias (id,pat) glob = - GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob) - -let rec bind_primary_aliases map pat = - match pat with - PatVar (_,_) -> map - | PatCstr(loc,_,lpat,nam) -> - let map1 = - match nam with - Anonymous -> map - | Name id -> (id,pat)::map - in - List.fold_left bind_primary_aliases map1 lpat - -let bind_secondary_aliases map subst = - Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map - -let bind_aliases patvars subst patt = - let map = bind_primary_aliases [] patt in - let map1 = bind_secondary_aliases map subst in - List.rev map1 - -let interp_pattern env pat_expr = - let patvars,pats = Constrintern.intern_pattern env pat_expr in - match pats with - [] -> anomaly (Pp.str "empty pattern list") - | [subst,patt] -> - (patvars,bind_aliases patvars subst patt,patt) - | _ -> anomaly (Pp.str "undetected disjunctive pattern") - -let rec match_args dest names constr = function - [] -> [],names,substl names constr - | _::q -> - let (name,typ,body)=dest constr in - let st={st_label=name;st_it=substl names typ} in - let qnames= - match name with - Anonymous -> assert false - | Name id -> mkVar id :: names in - let args,bnames,body = match_args dest qnames body q in - st::args,bnames,body - -let rec match_aliases names constr = function - [] -> [],names,substl names constr - | _::q -> - let (name,c,typ,body)=destLetIn constr in - let st={st_label=name;st_it=(substl names c,substl names typ)} in - let qnames= - match name with - Anonymous -> assert false - | Name id -> mkVar id :: names in - let args,bnames,body = match_aliases qnames body q in - st::args,bnames,body - -let detype_ground env c = Detyping.detype false [] env Evd.empty c - -let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = - let et,pinfo = - match info.pm_stack with - Per(et,pi,_,_)::_ -> et,pi - | _ -> error "No proof per cases/induction/inversion in progress." in - let mib,oib=Global.lookup_inductive pinfo.per_ind in - let num_params = pinfo.per_nparams in - let _ = - let expected = mib.Declarations.mind_nparams - num_params in - if not (Int.equal (List.length params) expected) then - user_err ~hdr:"suppose it is" - (str "Wrong number of extra arguments: " ++ - (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ - str "expected.") in - let app_ind = - let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in - let rparams = List.map (detype_ground env) pinfo.per_params in - let rparams_rec = - List.map - (fun (loc,(id,_)) -> - GVar (loc,id)) params in - let dum_args= - List.init oib.Declarations.mind_nrealargs - (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),Misctypes.IntroAnonymous, None)) in - glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in - let pat_vars,aliases,patt = interp_pattern env pat in - let inject = function - Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) - | Thesis (For rec_occ) -> - if not (Id.List.mem rec_occ pat_vars) then - user_err ~hdr:"suppose it is" - (str "Variable " ++ Nameops.pr_id rec_occ ++ - str " does not occur in pattern."); - Glob_term.GSort(Loc.ghost,GProp) - | This (c,_) -> c in - let term1 = glob_constr_of_hyps inject hyps glob_prop in - let loc_ids,npatt = - let rids=ref ([],pat_vars) in - let npatt= deanonymize rids patt in - List.rev (fst !rids),npatt in - let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in - let term3=List.fold_right let_in_one_alias aliases term2 in - let term4=List.fold_right prod_one_id loc_ids term3 in - let term5=List.fold_right prod_one_hyp params term4 in - let constr = fst (understand env sigma term5)(*FIXME*) in - let tparams,nam4,rest4 = match_args destProd [] constr params in - let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in - let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in - let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in - let blend st st' = - match st'.st_it with - Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} - | This _ -> {st_it = This st.st_it;st_label=st.st_label} in - let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in - tparams,{pat_vars=tpatvars; - pat_aliases=taliases; - pat_constr=pat_pat; - pat_typ=pat_typ; - pat_pat=patt; - pat_expr=pat},thyps - -let interp_cut interp_it env sigma cut= - let nenv,nstat = interp_it env sigma cut.cut_stat in - { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using; - cut_stat=nstat; - cut_by=interp_justification_items nenv sigma cut.cut_by} - -let interp_no_bind interp_it env sigma x = - env,interp_it env sigma x - -let interp_suffices_clause env sigma (hyps,cot)= - let (locvars,_) as res = - match cot with - This (c,_) -> - let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in - nhyps,This nc - | Thesis Plain as th -> interp_hyps env sigma hyps,th - | Thesis (For n) -> error "\"thesis for\" is not applicable here." in - let push_one hyp env0 = - match hyp with - (Hprop st | Hvar st) -> - match st.st_label with - Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0 - | _ -> env in - let nenv = List.fold_right push_one locvars env in - nenv,res - -let interp_casee env sigma = function - Real c -> Real (fst (understand env sigma (fst c)))(*FIXME*) - | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) env sigma cut) - -let abstract_one_arg = function - (loc,(id,None)) -> - (fun glob -> - GLambda (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id),Misctypes.IntroAnonymous,None), glob)) - | (loc,(id,Some typ)) -> - (fun glob -> - GLambda (Loc.ghost,Name id, Explicit, fst typ, glob)) - -let glob_constr_of_fun args body = - List.fold_right abstract_one_arg args (fst body) - -let interp_fun env sigma args body = - let constr=fst (*FIXME*) (understand env sigma (glob_constr_of_fun args body)) in - match_args destLambda [] constr args - -let rec interp_bare_proof_instr info env sigma = function - Pthus i -> Pthus (interp_bare_proof_instr info env sigma i) - | Pthen i -> Pthen (interp_bare_proof_instr info env sigma i) - | Phence i -> Phence (interp_bare_proof_instr info env sigma i) - | Pcut c -> Pcut (interp_cut - (interp_no_bind (interp_statement - (interp_constr_or_thesis true))) - env sigma c) - | Psuffices c -> - Psuffices (interp_cut interp_suffices_clause env sigma c) - | Prew (s,c) -> Prew (s,interp_cut - (interp_no_bind (interp_statement - (interp_constr_in_type (get_eq_typ info env)))) - env sigma c) - - | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps) - | Pcase (params,pat,hyps) -> - let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in - Pcase (tparams,tpat,thyps) - | Ptake witl -> - Ptake (List.map (fun c -> fst (*FIXME*) (understand env sigma (fst c))) witl) - | Pconsider (c,hyps) -> Pconsider (interp_constr false env sigma c, - interp_hyps env sigma hyps) - | Pper (et,c) -> Pper (et,interp_casee env sigma c) - | Pend bt -> Pend bt - | Pescape -> Pescape - | Passume hyps -> Passume (interp_hyps env sigma hyps) - | Pgiven hyps -> Pgiven (interp_hyps env sigma hyps) - | Plet hyps -> Plet (interp_hyps env sigma hyps) - | Pclaim st -> Pclaim (interp_statement (interp_constr true) env sigma st) - | Pfocus st -> Pfocus (interp_statement (interp_constr true) env sigma st) - | Pdefine (id,args,body) -> - let nargs,_,nbody = interp_fun env sigma args body in - Pdefine (id,nargs,nbody) - | Pcast (id,typ) -> - Pcast(id,interp_constr true env sigma typ) - -let interp_proof_instr info env sigma instr= - {emph = instr.emph; - instr = interp_bare_proof_instr info env sigma instr.instr} - - - diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli deleted file mode 100644 index 4303ecdb4..000000000 --- a/plugins/decl_mode/decl_interp.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Tacintern -open Decl_expr - - -val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr -val interp_proof_instr : Decl_mode.pm_info -> - Environ.env -> Evd.evar_map -> glob_proof_instr -> proof_instr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml deleted file mode 100644 index 92d408901..000000000 --- a/plugins/decl_mode/decl_mode.ml +++ /dev/null @@ -1,136 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Evd -open CErrors -open Util - -let daimon_flag = ref false - -let set_daimon_flag () = daimon_flag:=true -let clear_daimon_flag () = daimon_flag:=false -let get_daimon_flag () = !daimon_flag - - - - -type split_tree= - Skip_patt of Id.Set.t * split_tree - | Split_patt of Id.Set.t * inductive * - (bool array * (Id.Set.t * split_tree) option) array - | Close_patt of split_tree - | End_patt of (Id.t * (int * int)) - -type elim_kind = - EK_dep of split_tree - | EK_nodep - | EK_unknown - -type recpath = int option*Declarations.wf_paths - -type per_info = - {per_casee:constr; - per_ctype:types; - per_ind:inductive; - per_pred:constr; - per_args:constr list; - per_params:constr list; - per_nparams:int; - per_wf:recpath} - -type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list - | Suppose_case - | Claim - | Focus_claim - -type pm_info = - { pm_stack : stack_info list} -let info = Store.field () - - -(* Current proof mode *) - -type command_mode = - Mode_tactic - | Mode_proof - | Mode_none - -let mode_of_pftreestate pts = - (* spiwack: it used to be "top_goal_..." but this should be fine *) - let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in - let goal = List.hd goals in - match Store.get (Goal.V82.extra sigma goal) info with - | None -> Mode_tactic - | Some _ -> Mode_proof - -let get_current_mode () = - try - mode_of_pftreestate (Pfedit.get_pftreestate ()) - with Proof_global.NoCurrentProof -> Mode_none - -let check_not_proof_mode str = - match get_current_mode () with - | Mode_proof -> error str - | _ -> () - -let get_info sigma gl= - match Store.get (Goal.V82.extra sigma gl) info with - | None -> invalid_arg "get_info" - | Some pm -> pm - -let try_get_info sigma gl = - Store.get (Goal.V82.extra sigma gl) info - -let get_goal_stack pts = - let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in - let info = get_info sigma (List.hd goals) in - info.pm_stack - - -let proof_focus = Proof.new_focus_kind () -let proof_cond = Proof.done_cond proof_focus - -let focus p = - let inf = get_goal_stack p in - Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) - -let unfocus () = - Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) - -let get_top_stack pts = - try - Proof.get_at_focus proof_focus pts - with Proof.NoSuchFocus -> - let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in - let info = get_info sigma gl in - info.pm_stack - -let get_stack pts = Proof.get_at_focus proof_focus pts - -let get_last env = match Environ.named_context env with - | decl :: _ -> Context.Named.Declaration.get_id decl - | [] -> error "no previous statement to use" - - -let get_end_command pts = - match get_top_stack pts with - | [] -> "\"end proof\"" - | Claim::_ -> "\"end claim\"" - | Focus_claim::_-> "\"end focus\"" - | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ -> - begin - match et with - Decl_expr.ET_Case_analysis -> - "\"end cases\" or start a new case" - | Decl_expr.ET_Induction -> - "\"end induction\" or start a new case" - end - | _ -> anomaly (Pp.str"lonely suppose") diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli deleted file mode 100644 index dfeee833c..000000000 --- a/plugins/decl_mode/decl_mode.mli +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Evd - -val set_daimon_flag : unit -> unit -val clear_daimon_flag : unit -> unit -val get_daimon_flag : unit -> bool - -type command_mode = - Mode_tactic - | Mode_proof - | Mode_none - -val mode_of_pftreestate : Proof.proof -> command_mode - -val get_current_mode : unit -> command_mode - -val check_not_proof_mode : string -> unit - -type split_tree= - Skip_patt of Id.Set.t * split_tree - | Split_patt of Id.Set.t * inductive * - (bool array * (Id.Set.t * split_tree) option) array - | Close_patt of split_tree - | End_patt of (Id.t * (int * int)) - -type elim_kind = - EK_dep of split_tree - | EK_nodep - | EK_unknown - -type recpath = int option*Declarations.wf_paths - -type per_info = - {per_casee:constr; - per_ctype:types; - per_ind:inductive; - per_pred:constr; - per_args:constr list; - per_params:constr list; - per_nparams:int; - per_wf:recpath} - -type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list - | Suppose_case - | Claim - | Focus_claim - -type pm_info = - {pm_stack : stack_info list } - -val info : pm_info Store.field - -val get_info : Evd.evar_map -> Proof_type.goal -> pm_info - -val try_get_info : Evd.evar_map -> Proof_type.goal -> pm_info option - -val get_stack : Proof.proof -> stack_info list - -val get_top_stack : Proof.proof -> stack_info list - -val get_last: Environ.env -> Id.t -(** [get_last] raises a [UserError] when it cannot find a previous - statement in the environment. *) - -val get_end_command : Proof.proof -> string - -val focus : Proof.proof -> unit - -val unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack deleted file mode 100644 index 1b84a0790..000000000 --- a/plugins/decl_mode/decl_mode_plugin.mlpack +++ /dev/null @@ -1,5 +0,0 @@ -Decl_mode -Decl_interp -Decl_proof_instr -Ppdecl_proof -G_decl_mode diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml deleted file mode 100644 index deb2ede1d..000000000 --- a/plugins/decl_mode/decl_proof_instr.ml +++ /dev/null @@ -1,1554 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Ltac_plugin -open CErrors -open Util -open Pp -open Evd - -open Tacmach -open Tacintern -open Decl_expr -open Decl_mode -open Decl_interp -open Glob_term -open Glob_ops -open Names -open Nameops -open Declarations -open Tactics -open Tacticals -open Term -open Vars -open Termops -open Namegen -open Goptions -open Misctypes -open Sigma.Notations -open Context.Named.Declaration - -module RelDecl = Context.Rel.Declaration -module NamedDecl = Context.Named.Declaration - -(* Strictness option *) - -let clear ids { it = goal; sigma } = - let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in - let env = Goal.V82.env sigma goal in - let sign = Goal.V82.hyps sigma goal in - let cl = Goal.V82.concl sigma goal in - let evdref = ref (Evd.clear_metas sigma) in - let (hyps, concl) = - try Evarutil.clear_hyps_in_evi env evdref sign cl ids - with Evarutil.ClearDependencyError (id, _) -> - user_err (str "Cannot clear " ++ pr_id id) - in - let sigma = !evdref in - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - { it = [gl]; sigma } - -let get_its_info gls = get_info gls.sigma gls.it - -let get_strictness,set_strictness = - let strictness = ref false in - (fun () -> (!strictness)),(fun b -> strictness:=b) - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "strict proofs"; - optkey = ["Strict";"Proofs"]; - optread = get_strictness; - optwrite = set_strictness } - -let tcl_change_info_gen info_gen = - (fun gls -> - let it = sig_it gls in - let concl = pf_concl gls in - let hyps = Goal.V82.hyps (project gls) it in - let extra = Goal.V82.extra (project gls) it in - let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in - let sigma = Goal.V82.partial_solution sigma it ev in - { it = [gl] ; sigma= sigma; } ) - -let tcl_change_info info gls = - let info_gen s = Store.set s Decl_mode.info info in - tcl_change_info_gen info_gen gls - -let tcl_erase_info gls = - let info_gen s = Store.remove s Decl_mode.info in - tcl_change_info_gen info_gen gls - -let special_whd gl= - let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) - -let special_nf gl= - let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) - -let is_good_inductive env ind = - let mib,oib = Inductive.lookup_mind_specif env ind in - Int.equal oib.mind_nrealargs 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) - -let check_not_per pts = - if not (Proof.is_done pts) then - match get_stack pts with - Per (_,_,_,_)::_ -> - error "You are inside a proof per cases/induction.\n\ -Please \"suppose\" something or \"end\" it now." - | _ -> () - -let mk_evd metalist gls = - let evd0= clear_metas (sig_sig gls) in - let add_one (meta,typ) evd = - meta_declare meta typ evd in - List.fold_right add_one metalist evd0 - -let is_tmp id = (Id.to_string id).[0] == '_' - -let tmp_ids gls = - let ctx = pf_hyps gls in - match ctx with - [] -> [] - | _::q -> List.filter is_tmp (ids_of_named_context q) - -let clean_tmp gls = - let clean_id id0 gls0 = - tclTRY (clear [id0]) gls0 in - let rec clean_all = function - [] -> tclIDTAC - | id :: rest -> tclTHEN (clean_id id) (clean_all rest) - in - clean_all (tmp_ids gls) gls - -let assert_postpone id t = - assert_before (Name id) t - -(* start a proof *) - - -let start_proof_tac gls= - let info={pm_stack=[]} in - tcl_change_info info gls - -let go_to_proof_mode () = - ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac)); - let p = Proof_global.give_me_the_proof () in - Decl_mode.focus p - -(* closing gaps *) - -(* spiwack: should use [Proofview.give_up] but that would require - moving the whole declarative mode into the new proof engine. It - will eventually have to be done. - - As far as I can tell, [daimon_tac] is used after a [thus thesis], - it will leave uninstantiated variables instead of giving a relevant - message at [Qed]. *) -let daimon_tac gls = - set_daimon_flag (); - {it=[];sigma=sig_sig gls;} - -let daimon_instr env p = - let (p,(status,_)) = - Proof.run_tactic env begin - Proofview.tclINDEPENDENT Proofview.give_up - end p - in - p,status - -let do_daimon () = - let env = Global.env () in - let status = - Proof_global.with_current_proof begin fun _ p -> - daimon_instr env p - end - in - if not status then Feedback.feedback Feedback.AddedAxiom else () - -(* post-instruction focus management *) - -let goto_current_focus () = - Decl_mode.unfocus () - -(* spiwack: used to catch errors indicating lack of "focusing command" - in the proof tree. In the current implementation, however, entering - the declarative mode puts a focus first, there should, therefore, - never be exception raised here. *) -let goto_current_focus_or_top () = - goto_current_focus () - -(* return *) - -let close_tactic_mode () = - try do_daimon ();goto_current_focus () - with Not_found -> - error "\"return\" cannot be used outside of Declarative Proof Mode." - -let return_from_tactic_mode () = - close_tactic_mode () - -(* end proof/claim *) - -let close_block bt pts = - if Proof.no_focused_goal pts then - goto_current_focus () - else - let stack = - if Proof.is_done pts then - get_top_stack pts - else - get_stack pts - in - match bt,stack with - B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - do_daimon ();goto_current_focus () - | _, Claim::_ -> - error "\"end claim\" expected." - | _, Focus_claim::_ -> - error "\"end focus\" expected." - | _, [] -> - error "\"end proof\" expected." - | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> - begin - match et with - ET_Case_analysis -> error "\"end cases\" expected." - | ET_Induction -> error "\"end induction\" expected." - end - | _,_ -> anomaly (Pp.str "Lonely suppose on stack.") - - -(* utility for suppose / suppose it is *) - -let close_previous_case pts = - if - Proof.is_done pts - then - match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...") - | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus () - | _ -> error "Not inside a proof per cases or induction." - else - match get_stack pts with - Per (et,_,_,_) :: _ -> () - | Suppose_case :: Per (et,_,_,_) :: _ -> - do_daimon ();goto_current_focus () - | _ -> error "Not inside a proof per cases or induction." - -(* Proof instructions *) - -(* automation *) - -let filter_hyps f gls = - let filter_aux id = - let id = NamedDecl.get_id id in - if f id then - tclIDTAC - else - tclTRY (clear [id]) in - tclMAP filter_aux (pf_hyps gls) gls - -let local_hyp_prefix = Id.of_string "___" - -let add_justification_hyps keep items gls = - let add_aux c gls= - match kind_of_term c with - Var id -> - keep:=Id.Set.add id !keep; - tclIDTAC gls - | _ -> - let id=pf_get_new_id local_hyp_prefix gls in - keep:=Id.Set.add id !keep; - tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere)) - (Proofview.V82.of_tactic (clear_body [id])) gls in - tclMAP add_aux items gls - -let prepare_goal items gls = - let tokeep = ref Id.Set.empty in - let auxres = add_justification_hyps tokeep items gls in - tclTHENLIST - [ (fun _ -> auxres); - filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls - -let my_automation_tac = ref - (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered"))) - -let register_automation_tac tac = my_automation_tac:= tac - -let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac) - -let warn_insufficient_justification = - CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode" - (fun () -> strbrk "Insufficient justification.") - -let justification tac gls= - tclORELSE - (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)]) - (fun gls -> - if get_strictness () then - error "Insufficient justification." - else - begin - warn_insufficient_justification (); - daimon_tac gls - end) gls - -let default_justification elems gls= - justification (tclTHEN (prepare_goal elems) (Proofview.V82.of_tactic automation_tac)) gls - -(* code for conclusion refining *) - -let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s) - -let _and = constant ["Init";"Logic"] "and" - -let _and_rect = constant ["Init";"Logic"] "and_rect" - -let _prod = constant ["Init";"Datatypes"] "prod" - -let _prod_rect = constant ["Init";"Datatypes"] "prod_rect" - -let _ex = constant ["Init";"Logic"] "ex" - -let _ex_ind = constant ["Init";"Logic"] "ex_ind" - -let _sig = constant ["Init";"Specif"] "sig" - -let _sig_rect = constant ["Init";"Specif"] "sig_rect" - -let _sigT = constant ["Init";"Specif"] "sigT" - -let _sigT_rect = constant ["Init";"Specif"] "sigT_rect" - -type stackd_elt = -{se_meta:metavariable; - se_type:types; - se_last_meta:metavariable; - se_meta_list:(metavariable*types) list; - se_evd: evar_map} - -let rec replace_in_list m l = function - [] -> raise Not_found - | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q - -let enstack_subsubgoals env se stack gls= - let hd,params = decompose_app (special_whd gls se.se_type) in - match kind_of_term hd with - Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *) - let mib,oib= - Inductive.lookup_mind_specif env ind in - let gentypes= - Inductive.arities_of_constructors indu (mib,oib) in - let process i gentyp = - let constructor = mkConstructU ((ind,succ i),u) - (* constructors numbering*) in - let appterm = applist (constructor,params) in - let apptype = prod_applist gentyp params in - let rc,_ = Reduction.dest_prod env apptype in - let rec meta_aux last lenv = function - [] -> (last,lenv,[]) - | decl::q -> - let nlast=succ last in - let (llast,holes,metas) = - meta_aux nlast (mkMeta nlast :: lenv) q in - (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in - let (nlast,holes,nmetas) = - meta_aux se.se_last_meta [] (List.rev rc) in - let refiner = applist (appterm,List.rev holes) in - let evd = meta_assign se.se_meta - (refiner,(Conv,TypeProcessed (* ? *))) se.se_evd in - let ncreated = replace_in_list - se.se_meta nmetas se.se_meta_list in - let evd0 = List.fold_left - (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in - List.iter (fun (m,typ) -> - Stack.push - {se_meta=m; - se_type=typ; - se_evd=evd0; - se_meta_list=ncreated; - se_last_meta=nlast} stack) (List.rev nmetas) - in - Array.iteri process gentypes - | _ -> () - -let rec nf_list evd = - function - [] -> [] - | (m,typ)::others -> - if meta_defined evd m then - nf_list evd others - else - (m,Reductionops.nf_meta evd typ)::nf_list evd others - -let find_subsubgoal c ctyp skip submetas gls = - let env= pf_env gls in - let concl = pf_concl gls in - let evd = mk_evd ((0,concl)::submetas) gls in - let stack = Stack.create () in - let max_meta = - List.fold_left (fun a (m,_) -> max a m) 0 submetas in - let _ = Stack.push - {se_meta=0; - se_type=concl; - se_last_meta=max_meta; - se_meta_list=[0,concl]; - se_evd=evd} stack in - let rec dfs n = - let se = Stack.pop stack in - try - let unifier = - Unification.w_unify env se.se_evd Reduction.CUMUL - ~flags:(Unification.elim_flags ()) ctyp se.se_type in - if n <= 0 then - {se with - se_evd=meta_assign se.se_meta - (c,(Conv,TypeNotProcessed (* ?? *))) unifier; - se_meta_list=replace_in_list - se.se_meta submetas se.se_meta_list} - else - dfs (pred n) - with e when CErrors.noncritical e -> - begin - enstack_subsubgoals env se stack gls; - dfs n - end in - let nse= try dfs skip with Stack.Empty -> raise Not_found in - nf_list nse.se_evd nse.se_meta_list,Reductionops.nf_meta nse.se_evd (mkMeta 0) - -let concl_refiner metas body gls = - let concl = pf_concl gls in - let evd = sig_sig gls in - let env = pf_env gls in - let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in - let rec aux env avoid subst = function - [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") - | (n,typ)::rest -> - let _A = subst_meta subst typ in - let x = id_of_name_using_hdchar env _A Anonymous in - let _x = fresh_id avoid x gls in - let nenv = Environ.push_named (LocalAssum (_x,_A)) env in - let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in - let nsubst = (n,mkVar _x)::subst in - if List.is_empty rest then - asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) - else - let bsort,_B,nbody = - aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in - let body = mkNamedLambda _x _A nbody in - if occur_term (mkVar _x) _B then - begin - let _P = mkNamedLambda _x _A _B in - match bsort,sort with - InProp,InProp -> - let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in - InProp,_AxB, - mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|]) - | InProp,_ -> - let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in - let _P0 = mkLambda(Anonymous,_AxB,concl) in - InType,_AxB, - mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|]) - | _,_ -> - let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in - let _P0 = mkLambda(Anonymous,_AxB,concl) in - InType,_AxB, - mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|]) - end - else - begin - match asort,bsort with - InProp,InProp -> - let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in - InProp,_AxB, - mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|]) - |_,_ -> - let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in - let _P0 = mkLambda(Anonymous,_AxB,concl) in - InType,_AxB, - mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|]) - end - in - let (_,_,prf) = aux env [] [] metas in - mkApp(prf,[|mkMeta 1|]) - -let thus_tac c ctyp submetas gls = - let list,proof = - try - find_subsubgoal c ctyp 0 submetas gls - with Not_found -> - error "I could not relate this statement to the thesis." in - if List.is_empty list then - Proofview.V82.of_tactic (exact_check proof) gls - else - let refiner = concl_refiner list proof gls in - Tacmach.refine refiner gls - -(* general forward step *) - -let mk_stat_or_thesis info gls = function - This c -> c - | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here." - | Thesis Plain -> pf_concl gls - -let just_tac _then cut info gls0 = - let last_item = - if _then then - try [mkVar (get_last (pf_env gls0))] - with UserError _ -> - error "\"then\" and \"hence\" require at least one previous fact" - else [] - in - let items_tac gls = - match cut.cut_by with - None -> tclIDTAC gls - | Some items -> prepare_goal (last_item@items) gls in - let method_tac gls = - match cut.cut_using with - None -> - Proofview.V82.of_tactic automation_tac gls - | Some tac -> - Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in - justification (tclTHEN items_tac method_tac) gls0 - -let instr_cut mkstat _thus _then cut gls0 = - let info = get_its_info gls0 in - let stat = cut.cut_stat in - let (c_id,_) = match stat.st_label with - Anonymous -> - pf_get_new_id (Id.of_string "_fact") gls0,false - | Name id -> id,true in - let c_stat = mkstat info gls0 stat.st_it in - let thus_tac gls= - if _thus then - thus_tac (mkVar c_id) c_stat [] gls - else tclIDTAC gls in - tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat)) - [tclTHEN tcl_erase_info (just_tac _then cut info); - thus_tac] gls0 - - -(* iterated equality *) -let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) - -let decompose_eq id gls = - let typ = pf_get_hyp_typ gls id in - let whd = (special_whd gls typ) in - match kind_of_term whd with - App (f,args)-> - if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 - then (args.(0), - args.(1), - args.(2)) - else error "Previous step is not an equality." - | _ -> error "Previous step is not an equality." - -let instr_rew _thus rew_side cut gls0 = - let last_id = - try get_last (pf_env gls0) - with UserError _ -> error "No previous equality." - in - let typ,lhs,rhs = decompose_eq last_id gls0 in - let items_tac gls = - match cut.cut_by with - None -> tclIDTAC gls - | Some items -> prepare_goal items gls in - let method_tac gls = - match cut.cut_using with - None -> - Proofview.V82.of_tactic automation_tac gls - | Some tac -> - Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in - let just_tac gls = - justification (tclTHEN items_tac method_tac) gls in - let (c_id,_) = match cut.cut_stat.st_label with - Anonymous -> - pf_get_new_id (Id.of_string "_eq") gls0,false - | Name id -> id,true in - let thus_tac new_eq gls= - if _thus then - thus_tac (mkVar c_id) new_eq [] gls - else tclIDTAC gls in - match rew_side with - Lhs -> - let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in - tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) - [tclTHEN tcl_erase_info - (tclTHENS (Proofview.V82.of_tactic (transitivity lhs)) - [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]); - thus_tac new_eq] gls0 - | Rhs -> - let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in - tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) - [tclTHEN tcl_erase_info - (tclTHENS (Proofview.V82.of_tactic (transitivity rhs)) - [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]); - thus_tac new_eq] gls0 - - -(* tactics for claim/focus *) - -let instr_claim _thus st gls0 = - let info = get_its_info gls0 in - let (id,_) = match st.st_label with - Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false - | Name id -> id,true in - let thus_tac gls= - if _thus then - thus_tac (mkVar id) st.st_it [] gls - else tclIDTAC gls in - let ninfo1 = {pm_stack= - (if _thus then Focus_claim else Claim)::info.pm_stack} in - tclTHENS (Proofview.V82.of_tactic (assert_postpone id st.st_it)) - [thus_tac; - tcl_change_info ninfo1] gls0 - -(* tactics for assume *) - -let push_intro_tac coerce nam gls = - let (hid,_) = - match nam with - Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false - | Name id -> id,true in - tclTHENLIST - [Proofview.V82.of_tactic (intro_mustbe_force hid); - coerce hid] - gls - -let assume_tac hyps gls = - List.fold_right - (fun (Hvar st | Hprop st) -> - tclTHEN - (push_intro_tac - (fun id -> - Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) - hyps tclIDTAC gls - -let assume_hyps_or_theses hyps gls = - List.fold_right - (function - (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> - tclTHEN - (push_intro_tac - (fun id -> - Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam) - | Hprop {st_label=nam;st_it=Thesis (tk)} -> - tclTHEN - (push_intro_tac - (fun id -> tclIDTAC) nam)) - hyps tclIDTAC gls - -let assume_st hyps gls = - List.fold_right - (fun st -> - tclTHEN - (push_intro_tac - (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) - hyps tclIDTAC gls - -let assume_st_letin hyps gls = - List.fold_right - (fun st -> - tclTHEN - (push_intro_tac - (fun id -> - Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label)) - hyps tclIDTAC gls - -(* suffices *) - -let rec metas_from n hyps = - match hyps with - _ :: q -> n :: metas_from (succ n) q - | [] -> [] - -let rec build_product args body = - match args with - (Hprop st| Hvar st )::rest -> - let pprod= lift 1 (build_product rest body) in - let lbody = - match st.st_label with - Anonymous -> pprod - | Name id -> subst_term (mkVar id) pprod in - mkProd (st.st_label, st.st_it, lbody) - | [] -> body - -let rec build_applist prod = function - [] -> [],prod - | n::q -> - let (_,typ,_) = destProd prod in - let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in - (n,typ)::ctx,head - -let instr_suffices _then cut gls0 = - let info = get_its_info gls0 in - let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in - let ctx,hd = cut.cut_stat in - let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in - let metas = metas_from 1 ctx in - let c_ctx,c_head = build_applist c_stat metas in - let c_term = applist (mkVar c_id,List.map mkMeta metas) in - let thus_tac gls= - thus_tac c_term c_head c_ctx gls in - tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat)) - [tclTHENLIST - [ assume_tac ctx; - tcl_erase_info; - just_tac _then cut info]; - thus_tac] gls0 - -(* tactics for consider/given *) - -let conjunction_arity id gls = - let typ = pf_get_hyp_typ gls id in - let hd,params = decompose_app (special_whd gls typ) in - let env =pf_env gls in - match kind_of_term hd with - Ind (ind,u as indu) when is_good_inductive env ind -> - let mib,oib= - Inductive.lookup_mind_specif env ind in - let gentypes= - Inductive.arities_of_constructors indu (mib,oib) in - let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in - let apptype = prod_applist gentypes.(0) params in - let rc,_ = Reduction.dest_prod env apptype in - List.length rc - | _ -> raise Not_found - -let rec intron_then n ids ltac gls = - if n<=0 then - ltac ids gls - else - let id = pf_get_new_id (Id.of_string "_tmp") gls in - tclTHEN - (Proofview.V82.of_tactic (intro_mustbe_force id)) - (intron_then (pred n) (id::ids) ltac) gls - - -let rec consider_match may_intro introduced available expected gls = - match available,expected with - [],[] -> - tclIDTAC gls - | _,[] -> error "Last statements do not match a complete hypothesis." - (* should tell which ones *) - | [],hyps -> - if may_intro then - begin - let id = pf_get_new_id (Id.of_string "_tmp") gls in - tclIFTHENELSE - (Proofview.V82.of_tactic (intro_mustbe_force id)) - (consider_match true [] [id] hyps) - (fun _ -> - error "Not enough sub-hypotheses to match statements.") - gls - end - else - error "Not enough sub-hypotheses to match statements." - (* should tell which ones *) - | id::rest_ids,(Hvar st | Hprop st)::rest -> - tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) - begin - match st.st_label with - Anonymous -> - consider_match may_intro ((id,false)::introduced) rest_ids rest - | Name hid -> - tclTHENLIST - [Proofview.V82.of_tactic (rename_hyp [id,hid]); - consider_match may_intro ((hid,true)::introduced) rest_ids rest] - end - begin - (fun gls -> - let nhyps = - try conjunction_arity id gls with - Not_found -> error "Matching hypothesis not found." in - tclTHENLIST - [Proofview.V82.of_tactic (simplest_case (mkVar id)); - intron_then nhyps [] - (fun l -> consider_match may_intro introduced - (List.rev_append l rest_ids) expected)] gls) - end - gls - -let consider_tac c hyps gls = - match kind_of_term (strip_outer_cast c) with - Var id -> - consider_match false [] [id] hyps gls - | _ -> - let id = pf_get_new_id (Id.of_string "_tmp") gls in - tclTHEN - (Proofview.V82.of_tactic (pose_proof (Name id) c)) - (consider_match false [] [id] hyps) gls - - -let given_tac hyps gls = - consider_match true [] [] hyps gls - -(* tactics for take *) - -let rec take_tac wits gls = - match wits with - [] -> tclIDTAC gls - | wit::rest -> - let typ = pf_unsafe_type_of gls wit in - tclTHEN (thus_tac wit typ []) (take_tac rest) gls - - -(* tactics for define *) - -let rec build_function args body = - match args with - st::rest -> - let pfun= lift 1 (build_function rest body) in - let id = match st.st_label with - Anonymous -> assert false - | Name id -> id in - mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) - | [] -> body - -let define_tac id args body gls = - let t = build_function args body in - Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls - -(* tactics for reconsider *) - -let cast_tac id_or_thesis typ gls = - match id_or_thesis with - | This id -> - Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls - | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here." - | Thesis Plain -> - Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls - -(* per cases *) - -let is_rec_pos (main_ind,wft) = - match main_ind with - None -> false - | Some index -> - match fst (Rtree.dest_node wft) with - Mrec (_,i) when Int.equal i index -> true - | _ -> false - -let rec constr_trees (main_ind,wft) ind = - match Rtree.dest_node wft with - Norec,_ -> - let itree = - (snd (Global.lookup_inductive ind)).mind_recargs in - constr_trees (None,itree) ind - | _,constrs -> main_ind,constrs - -let ind_args rp ind = - let main_ind,constrs = constr_trees rp ind in - let args ctree = - Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in - Array.map args constrs - -let init_tree ids ind rp nexti = - let indargs = ind_args rp ind in - let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in - Split_patt (ids,ind,Array.mapi do_i indargs) - -let map_tree_rp rp id_fun mapi = function - Split_patt (ids,ind,branches) -> - let indargs = ind_args rp ind in - let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in - Split_patt (id_fun ids,ind,Array.mapi do_i branches) - | _ -> failwith "map_tree_rp: not a splitting node" - -let map_tree id_fun mapi = function - Split_patt (ids,ind,branches) -> - let do_i i (recargs,bri) = recargs,mapi i bri in - Split_patt (id_fun ids,ind,Array.mapi do_i branches) - | _ -> failwith "map_tree: not a splitting node" - - -let start_tree env ind rp = - init_tree Id.Set.empty ind rp (fun _ _ -> None) - -let build_per_info etype casee gls = - let concl=pf_concl gls in - let env=pf_env gls in - let ctyp=pf_unsafe_type_of gls casee in - let is_dep = dependent casee concl in - let hd,args = decompose_app (special_whd gls ctyp) in - let (ind,u) = - try - destInd hd - with DestKO -> - error "Case analysis must be done on an inductive object." in - let mind,oind = Global.lookup_inductive ind in - let nparams,index = - match etype with - ET_Induction -> mind.mind_nparams_rec,Some (snd ind) - | _ -> mind.mind_nparams,None in - let params,real_args = List.chop nparams args in - let abstract_obj c body = - let typ=pf_unsafe_type_of gls c in - lambda_create env (typ,subst_term c body) in - let pred= List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term casee concl)) in - is_dep, - {per_casee=casee; - per_ctype=ctyp; - per_ind=ind; - per_pred=pred; - per_args=real_args; - per_params=params; - per_nparams=nparams; - per_wf=index,oind.mind_recargs} - -let per_tac etype casee gls= - let env=pf_env gls in - let info = get_its_info gls in - match casee with - Real c -> - let is_dep,per_info = build_per_info etype c gls in - let ek = - if is_dep then - EK_dep (start_tree env per_info.per_ind per_info.per_wf) - else EK_unknown in - tcl_change_info - {pm_stack= - Per(etype,per_info,ek,[])::info.pm_stack} gls - | Virtual cut -> - assert (cut.cut_stat.st_label == Anonymous); - let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in - let c = mkVar id in - let modified_cut = - {cut with cut_stat={cut.cut_stat with st_label=Name id}} in - tclTHEN - (instr_cut (fun _ _ c -> c) false false modified_cut) - (fun gls0 -> - let is_dep,per_info = build_per_info etype c gls0 in - assert (not is_dep); - tcl_change_info - {pm_stack= - Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) - gls - -(* suppose *) - -let register_nodep_subcase id= function - Per(et,pi,ek,clauses)::s -> - begin - match ek with - EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s - | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s - | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." - end - | _ -> anomaly (Pp.str "wrong stack state") - -let suppose_tac hyps gls0 = - let info = get_its_info gls0 in - let thesis = pf_concl gls0 in - let id = pf_get_new_id (Id.of_string "subcase_") gls0 in - let clause = build_product hyps thesis in - let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in - let old_clauses,stack = register_nodep_subcase id info.pm_stack in - let ninfo2 = {pm_stack=stack} in - tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause)) - [tclTHENLIST [tcl_change_info ninfo1; - assume_tac hyps; - clear old_clauses]; - tcl_change_info ninfo2] gls0 - -(* suppose it is ... *) - -(* pattern matching compiling *) - -let rec skip_args rest ids n = - if n <= 0 then - Close_patt rest - else - Skip_patt (ids,skip_args rest ids (pred n)) - -let rec tree_of_pats ((id,_) as cpl) pats = - match pats with - [] -> End_patt cpl - | args::stack -> - match args with - [] -> Close_patt (tree_of_pats cpl stack) - | (patt,rp) :: rest_args -> - match patt with - PatVar (_,v) -> - Skip_patt (Id.Set.singleton id, - tree_of_pats cpl (rest_args::stack)) - | PatCstr (_,(ind,cnum),args,nam) -> - let nexti i ati = - if Int.equal i (pred cnum) then - let nargs = - List.map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Id.Set.singleton id, - tree_of_pats cpl (nargs::rest_args::stack)) - else None - in init_tree Id.Set.empty ind rp nexti - -let rec add_branch ((id,_) as cpl) pats tree= - match pats with - [] -> - begin - match tree with - End_patt cpl0 -> End_patt cpl0 - (* this ensures precedence for overlapping patterns *) - | _ -> anomaly (Pp.str "tree is expected to end here") - end - | args::stack -> - match args with - [] -> - begin - match tree with - Close_patt t -> - Close_patt (add_branch cpl stack t) - | _ -> anomaly (Pp.str "we should pop here") - end - | (patt,rp) :: rest_args -> - match patt with - PatVar (_,v) -> - begin - match tree with - Skip_patt (ids,t) -> - Skip_patt (Id.Set.add id ids, - add_branch cpl (rest_args::stack) t) - | Split_patt (_,_,_) -> - map_tree (Id.Set.add id) - (fun i bri -> - append_branch cpl 1 (rest_args::stack) bri) - tree - | _ -> anomaly (Pp.str "No pop/stop expected here") - end - | PatCstr (_,(ind,cnum),args,nam) -> - match tree with - Skip_patt (ids,t) -> - let nexti i ati = - if Int.equal i (pred cnum) then - let nargs = - List.map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Id.Set.add id ids, - add_branch cpl (nargs::rest_args::stack) - (skip_args t ids (Array.length ati))) - else - Some (ids, - skip_args t ids (Array.length ati)) - in init_tree ids ind rp nexti - | Split_patt (_,ind0,_) -> - if (not (eq_ind ind ind0)) then error - (* this can happen with coercions *) - "Case pattern belongs to wrong inductive type."; - let mapi i ati bri = - if Int.equal i (pred cnum) then - let nargs = - List.map_i (fun j a -> (a,ati.(j))) 0 args in - append_branch cpl 0 - (nargs::rest_args::stack) bri - else bri in - map_tree_rp rp (fun ids -> ids) mapi tree - | _ -> anomaly (Pp.str "No pop/stop expected here") -and append_branch ((id,_) as cpl) depth pats = function - Some (ids,tree) -> - Some (Id.Set.add id ids,append_tree cpl depth pats tree) - | None -> - Some (Id.Set.singleton id,tree_of_pats cpl pats) -and append_tree ((id,_) as cpl) depth pats tree = - if depth<=0 then add_branch cpl pats tree - else match tree with - Close_patt t -> - Close_patt (append_tree cpl (pred depth) pats t) - | Skip_patt (ids,t) -> - Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t) - | End_patt _ -> anomaly (Pp.str "Premature end of branch") - | Split_patt (_,_,_) -> - map_tree (Id.Set.add id) - (fun i bri -> append_branch cpl (succ depth) pats bri) tree - -(* suppose it is *) - -let rec st_assoc id = function - [] -> raise Not_found - | st::_ when Name.equal st.st_label id -> st.st_it - | _ :: rest -> st_assoc id rest - -let thesis_for obj typ per_info env= - let rc,hd1=decompose_prod typ in - let cind,all_args=decompose_app typ in - let ind,u = destInd cind in - let _ = if not (eq_ind ind per_info.per_ind) then - user_err ~hdr:"thesis_for" - ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ - str"cannot give an induction hypothesis (wrong inductive type).") in - let params,args = List.chop per_info.per_nparams all_args in - let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - user_err ~hdr:"thesis_for" - ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ - str "cannot give an induction hypothesis (wrong parameters).") in - let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in - compose_prod rc (Reductionops.whd_beta Evd.empty hd2) - -let rec build_product_dep pat_info per_info args body gls = - match args with - (Hprop {st_label=nam;st_it=This c} - | Hvar {st_label=nam;st_it=c})::rest -> - let pprod= - lift 1 (build_product_dep pat_info per_info rest body gls) in - let lbody = - match nam with - Anonymous -> body - | Name id -> subst_var id pprod in - mkProd (nam,c,lbody) - | Hprop ({st_it=Thesis tk} as st)::rest -> - let pprod= - lift 1 (build_product_dep pat_info per_info rest body gls) in - let lbody = - match st.st_label with - Anonymous -> body - | Name id -> subst_var id pprod in - let ptyp = - match tk with - For id -> - let obj = mkVar id in - let typ = - try st_assoc (Name id) pat_info.pat_vars - with Not_found -> - snd (st_assoc (Name id) pat_info.pat_aliases) in - thesis_for obj typ per_info (pf_env gls) - | Plain -> pf_concl gls in - mkProd (st.st_label,ptyp,lbody) - | [] -> body - -let build_dep_clause params pat_info per_info hyps gls = - let concl= - thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in - let open_clause = - build_product_dep pat_info per_info hyps concl gls in - let prod_one st body = - match st.st_label with - Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body) - | Name id -> mkNamedProd id st.st_it (lift 1 body) in - let let_one_in st body = - match st.st_label with - Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) - | Name id -> - mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in - let aliased_clause = - List.fold_right let_one_in pat_info.pat_aliases open_clause in - List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause - -let rec register_dep_subcase id env per_info pat = function - EK_nodep -> error "Only \"suppose it is\" can be used here." - | EK_unknown -> - register_dep_subcase id env per_info pat - (EK_dep (start_tree env per_info.per_ind per_info.per_wf)) - | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree) - -let case_tac params pat_info hyps gls0 = - let info = get_its_info gls0 in - let id = pf_get_new_id (Id.of_string "subcase_") gls0 in - let et,per_info,ek,old_clauses,rest = - match info.pm_stack with - Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) - | _ -> anomaly (Pp.str "wrong place for cases") in - let clause = build_dep_clause params pat_info per_info hyps gls0 in - let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in - let nek = - register_dep_subcase (id,(List.length params,List.length hyps)) - (pf_env gls0) per_info pat_info.pat_pat ek in - let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in - tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause)) - [tclTHENLIST - [tcl_change_info ninfo1; - assume_st (params@pat_info.pat_vars); - assume_st_letin pat_info.pat_aliases; - assume_hyps_or_theses hyps; - clear old_clauses]; - tcl_change_info ninfo2] gls0 - -(* end cases *) - -type ('a, 'b) instance_stack = - ('b * (('a option * constr list) list)) list - -let initial_instance_stack ids : (_, _) instance_stack = - List.map (fun id -> id,[None,[]]) ids - -let push_one_arg arg = function - [] -> anomaly (Pp.str "impossible") - | (head,args) :: ctx -> - ((head,(arg::args)) :: ctx) - -let push_arg arg stacks = - List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks - - -let push_one_head c ids (id,stack) = - let head = if Id.Set.mem id ids then Some c else None in - id,(head,[]) :: stack - -let push_head c ids stacks = - List.map (push_one_head c ids) stacks - -let pop_one (id,stack) = - let nstack= - match stack with - [] -> anomaly (Pp.str "impossible") - | [c] as l -> l - | (Some head,args)::(head0,args0)::ctx -> - let arg = applist (head,(List.rev args)) in - (head0,(arg::args0))::ctx - | (None,args)::(head0,args0)::ctx -> - (head0,(args@args0))::ctx - in id,nstack - -let pop_stacks stacks = - List.map pop_one stacks - -let hrec_for fix_id per_info gls obj_id = - let obj=mkVar obj_id in - let typ=pf_get_hyp_typ gls obj_id in - let rc,hd1=decompose_prod typ in - let cind,all_args=decompose_app typ in - let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind); - let params,args= List.chop per_info.per_nparams all_args in - assert begin - try List.for_all2 eq_constr params per_info.per_params with - Invalid_argument _ -> false end; - let hd2 = applist (mkVar fix_id,args@[obj]) in - compose_lam rc (Reductionops.whd_beta gls.sigma hd2) - -let warn_missing_case = - CWarnings.create ~name:"declmode-missing-case" ~category:"declmode" - (fun () -> strbrk "missing case") - -let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = - match tree, objs with - Close_patt t,_ -> - let args0 = pop_stacks args in - execute_cases fix_name per_info tacnext args0 objs nhrec t gls - | Skip_patt (_,t),skipped::next_objs -> - let args0 = push_arg skipped args in - execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls - | End_patt (id,(nparams,nhyps)),[] -> - begin - match Id.List.assoc id args with - [None,br_args] -> - let all_metas = - List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in - let param_metas,hyp_metas = List.chop nparams all_metas in - tclTHEN - (tclDO nhrec (Proofview.V82.of_tactic introf)) - (tacnext - (applist (mkVar id, - List.append param_metas - (List.rev_append br_args hyp_metas)))) gls - | _ -> anomaly (Pp.str "wrong stack size") - end - | Split_patt (ids,ind,br), casee::next_objs -> - let (mind,oind) as spec = Global.lookup_inductive ind in - let nparams = mind.mind_nparams in - let concl=pf_concl gls in - let env=pf_env gls in - let ctyp=pf_unsafe_type_of gls casee in - let hd,all_args = decompose_app (special_whd gls ctyp) in - let ind', u = destInd hd in - let _ = assert (eq_ind ind' ind) in (* just in case *) - let params,real_args = List.chop nparams all_args in - let abstract_obj c body = - let typ=pf_unsafe_type_of gls c in - lambda_create env (typ,subst_term c body) in - let elim_pred = List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term casee concl)) in - let case_info = Inductiveops.make_case_info env ind RegularStyle in - let gen_arities = Inductive.arities_of_constructors (ind,u) spec in - let f_ids typ = - let sign = - (prod_assum (prod_applist typ params)) in - find_intro_names sign gls in - let constr_args_ids = Array.map f_ids gen_arities in - let case_term = - mkCase(case_info,elim_pred,casee, - Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in - let branch_tac i (recargs,bro) gls0 = - let args_ids = constr_args_ids.(i) in - let rec aux n = function - [] -> - assert (Int.equal n (Array.length recargs)); - next_objs,[],nhrec - | id :: q -> - let objs,recs,nrec = aux (succ n) q in - if recargs.(n) - then (mkVar id::objs),(id::recs),succ nrec - else (mkVar id::objs),recs,nrec in - let objs,recs,nhrec = aux 0 args_ids in - tclTHENLIST - [tclMAP (fun id -> Proofview.V82.of_tactic (intro_mustbe_force id)) args_ids; - begin - fun gls1 -> - let hrecs = - List.map - (fun id -> - hrec_for (out_name fix_name) per_info gls1 id) - recs in - Proofview.V82.of_tactic (generalize hrecs) gls1 - end; - match bro with - None -> - warn_missing_case (); - tacnext (mkMeta 1) - | Some (sub_ids,tree) -> - let br_args = - List.filter - (fun (id,_) -> Id.Set.mem id sub_ids) args in - let construct = - applist (mkConstruct(ind,succ i),params) in - let p_args = - push_head construct ids br_args in - execute_cases fix_name per_info tacnext - p_args objs nhrec tree] gls0 in - tclTHENSV - (refine case_term) - (Array.mapi branch_tac br) gls - | Split_patt (_, _, _) , [] -> - anomaly ~label:"execute_cases " (Pp.str "Nothing to split") - | Skip_patt _ , [] -> - anomaly ~label:"execute_cases " (Pp.str "Nothing to skip") - | End_patt (_,_) , _ :: _ -> - anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left") - -let understand_my_constr env sigma c concl = - let env = env in - let rawc = Detyping.detype false [] env Evd.empty c in - let rec frob = function - | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None) - | rc -> map_glob_constr frob rc - in - Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) - -let my_refine c gls = - let oc = { run = begin fun sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in - Sigma.Unsafe.of_pair (c, sigma) - end } in - Proofview.V82.of_tactic (Tactics.New.refine oc) gls - -(* end focus/claim *) - -let end_tac et2 gls = - let info = get_its_info gls in - let et1,pi,ek,clauses = - match info.pm_stack with - Suppose_case::_ -> - anomaly (Pp.str "This case should already be trapped") - | Claim::_ -> - error "\"end claim\" expected." - | Focus_claim::_ -> - error "\"end focus\" expected." - | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) - | [] -> - anomaly (Pp.str "This case should already be trapped") in - let et = match et1, et2 with - | ET_Case_analysis, ET_Case_analysis -> et1 - | ET_Induction, ET_Induction -> et1 - | ET_Case_analysis, _ -> error "\"end cases\" expected." - | ET_Induction, _ -> error "\"end induction\" expected." - in - tclTHEN - tcl_erase_info - begin - match et,ek with - _,EK_unknown -> - tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)] - | ET_Case_analysis,EK_nodep -> - tclTHEN - (Proofview.V82.of_tactic (simplest_case pi.per_casee)) - (default_justification (List.map mkVar clauses)) - | ET_Induction,EK_nodep -> - tclTHENLIST - [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])); - Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args)))); - default_justification (List.map mkVar clauses)] - | ET_Case_analysis,EK_dep tree -> - execute_cases Anonymous pi - (fun c -> tclTHENLIST - [my_refine c; - clear clauses; - justification (Proofview.V82.of_tactic assumption)]) - (initial_instance_stack clauses) [pi.per_casee] 0 tree - | ET_Induction,EK_dep tree -> - let nargs = (List.length pi.per_args) in - tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]))) - begin - fun gls0 -> - let fix_id = - pf_get_new_id (Id.of_string "_fix") gls0 in - let c_id = - pf_get_new_id (Id.of_string "_main_arg") gls0 in - tclTHENLIST - [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs)); - tclDO nargs (Proofview.V82.of_tactic introf); - Proofview.V82.of_tactic (intro_mustbe_force c_id); - execute_cases (Name fix_id) pi - (fun c -> - tclTHENLIST - [clear [fix_id]; - my_refine c; - clear clauses; - justification (Proofview.V82.of_tactic assumption)]) - (initial_instance_stack clauses) - [mkVar c_id] 0 tree] gls0 - end - end gls - -(* escape *) - -let escape_tac gls = - (* spiwack: sets an empty info stack to avoid interferences. - We could erase the info altogether, but that doesn't play - well with the Decl_mode.focus (used in post_processing). *) - let info={pm_stack=[]} in - tcl_change_info info gls - -(* General instruction engine *) - -let rec do_proof_instr_gen _thus _then instr = - match instr with - Pthus i -> - assert (not _thus); - do_proof_instr_gen true _then i - | Pthen i -> - assert (not _then); - do_proof_instr_gen _thus true i - | Phence i -> - assert (not (_then || _thus)); - do_proof_instr_gen true true i - | Pcut c -> - instr_cut mk_stat_or_thesis _thus _then c - | Psuffices c -> - instr_suffices _then c - | Prew (s,c) -> - assert (not _then); - instr_rew _thus s c - | Pconsider (c,hyps) -> consider_tac c hyps - | Pgiven hyps -> given_tac hyps - | Passume hyps -> assume_tac hyps - | Plet hyps -> assume_tac hyps - | Pclaim st -> instr_claim false st - | Pfocus st -> instr_claim true st - | Ptake witl -> take_tac witl - | Pdefine (id,args,body) -> define_tac id args body - | Pcast (id,typ) -> cast_tac id typ - | Pper (et,cs) -> per_tac et cs - | Psuppose hyps -> suppose_tac hyps - | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps - | Pend (B_elim et) -> end_tac et - | Pend _ -> anomaly (Pp.str "Not applicable") - | Pescape -> escape_tac - -let eval_instr {instr=instr} = - do_proof_instr_gen false false instr - -let rec preprocess pts instr = - match instr with - Phence i |Pthus i | Pthen i -> preprocess pts i - | Psuffices _ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ - | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ - | Pdefine (_,_,_) | Pper _ | Prew _ -> - check_not_per pts; - true - | Pescape -> - check_not_per pts; - true - | Pcase _ | Psuppose _ | Pend (B_elim _) -> - close_previous_case pts ; - true - | Pend bt -> - close_block bt pts ; - false - -let rec postprocess pts instr = - match instr with - Phence i | Pthus i | Pthen i -> postprocess pts i - | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) - | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> () - | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> - Decl_mode.focus pts - | Pescape -> - Decl_mode.focus pts; - Proof_global.set_proof_mode "Classic" - | Pend (B_elim ET_Induction) -> - begin - let pfterm = List.hd (Proof.partial_proof pts) in - let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in - let env = try - Goal.V82.env sigma (List.hd gls) - with Failure "hd" -> - Global.env () - in - try - Inductiveops.control_only_guard env pfterm; - goto_current_focus_or_top () - with - Type_errors.TypeError(env, - Type_errors.IllFormedRecBody(_,_,_,_,_)) -> - anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") - end - | Pend (B_elim ET_Case_analysis) -> goto_current_focus () - | Pend B_proof -> Proof_global.set_proof_mode "Classic" - | Pend _ -> () - -let do_instr raw_instr pts = - let has_tactic = preprocess pts raw_instr.instr in - (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the - current proof (and, actually so does [do_instr] later one, so - it's ok to do the same here. Ideally the proof should be properly - threaded through the commands here, but since the are interleaved - with actions on the proof mode, which is attached to the global - proof environment, it is not possible without heavy lifting. *) - let pts = Proof_global.give_me_the_proof () in - let pts = - if has_tactic then - let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in - let gl = { it=List.hd gls ; sigma=sigma; } in - let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; genv = env} in - let glob_instr = intern_proof_instr ist raw_instr in - let instr = - interp_proof_instr (get_its_info gl) env sigma glob_instr in - let (pts',_) = Proof.run_tactic (Global.env()) - (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in - pts' - else pts - in - Proof_global.simple_with_current_proof (fun _ _ -> pts); - postprocess pts raw_instr.instr - -let proof_instr raw_instr = - let p = Proof_global.give_me_the_proof () in - do_instr raw_instr p - -(* - -(* STUFF FOR ITERATED RELATIONS *) -let decompose_bin_app t= - let hd,args = destApp - -let identify_transitivity_lemma c = - let varx,tx,c1 = destProd c in - let vary,ty,c2 = destProd (pop c1) in - let varz,tz,c3 = destProd (pop c2) in - let _,p1,c4 = destProd (pop c3) in - let _,lp2,lp3 = destProd (pop c4) in - let p2=pop lp2 in - let p3=pop lp3 in -*) - diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli deleted file mode 100644 index 325969dad..000000000 --- a/plugins/decl_mode/decl_proof_instr.mli +++ /dev/null @@ -1,108 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Tacmach -open Decl_mode - -val go_to_proof_mode: unit -> unit -val return_from_tactic_mode: unit -> unit - -val register_automation_tac: unit Proofview.tactic -> unit - -val automation_tac : unit Proofview.tactic - -val concl_refiner: - Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr - -val do_instr: Decl_expr.raw_proof_instr -> Proof.proof -> unit -val proof_instr: Decl_expr.raw_proof_instr -> unit - -val tcl_change_info : Decl_mode.pm_info -> tactic - -val execute_cases : - Name.t -> - Decl_mode.per_info -> - (Term.constr -> Proof_type.tactic) -> - (Id.Set.elt * (Term.constr option * Term.constr list) list) list -> - Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic - -val tree_of_pats : - Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> - split_tree - -val add_branch : - Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> - split_tree -> split_tree - -val append_branch : - Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> - (Id.Set.t * Decl_mode.split_tree) option -> - (Id.Set.t * Decl_mode.split_tree) option - -val append_tree : - Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> - split_tree -> split_tree - -val build_dep_clause : Term.types Decl_expr.statement list -> - Decl_expr.proof_pattern -> - Decl_mode.per_info -> - (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) - Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types - -val register_dep_subcase : - Id.t * (int * int) -> - Environ.env -> - Decl_mode.per_info -> - Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind - -val thesis_for : Term.constr -> - Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr - -val close_previous_case : Proof.proof -> unit - -val pop_stacks : - (Id.t * - (Term.constr option * Term.constr list) list) list -> - (Id.t * - (Term.constr option * Term.constr list) list) list - -val push_head : Term.constr -> - Id.Set.t -> - (Id.t * - (Term.constr option * Term.constr list) list) list -> - (Id.t * - (Term.constr option * Term.constr list) list) list - -val push_arg : Term.constr -> - (Id.t * - (Term.constr option * Term.constr list) list) list -> - (Id.t * - (Term.constr option * Term.constr list) list) list - -val hrec_for: - Id.t -> - Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> - Id.t -> Term.constr - -val consider_match : - bool -> - (Id.Set.elt*bool) list -> - Id.Set.elt list -> - (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> - Proof_type.tactic - -val init_tree: - Id.Set.t -> - inductive -> - int option * Declarations.wf_paths -> - (int -> - (int option * Declarations.recarg Rtree.t) array -> - (Id.Set.t * Decl_mode.split_tree) option) -> - Decl_mode.split_tree diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 deleted file mode 100644 index a71d20f0d..000000000 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ /dev/null @@ -1,387 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "grammar/grammar.cma" i*) - -DECLARE PLUGIN "decl_mode_plugin" - -open Ltac_plugin -open Compat -open Pp -open Decl_expr -open Names -open Pcoq -open Vernacexpr -open Tok (* necessary for camlp4 *) - -open Pcoq.Constr -open Pltac -open Ppdecl_proof - -let pr_goal gs = - let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in - let env = Goal.V82.env sigma g in - let concl = Goal.V82.concl sigma g in - let goal = - Printer.pr_context_of env sigma ++ cut () ++ - str "============================" ++ cut () ++ - str "thesis :=" ++ cut () ++ - Printer.pr_goal_concl_style_env env sigma concl in - str " *** Declarative Mode ***" ++ fnl () ++ fnl () ++ - str " " ++ v 0 goal - -let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll = - match gll with - | [goal] when pr_first -> - pr_goal { Evd.it = goal ; sigma = sigma } - | _ -> - (* spiwack: it's not very nice to have to call proof global - here, a more robust solution would be to add a hook for - [Printer.pr_open_subgoals] in proof modes, in order to - compute the end command. Yet a more robust solution would be - to have focuses give explanations of their unfocusing - behaviour. *) - let p = Proof_global.give_me_the_proof () in - let close_cmd = Decl_mode.get_end_command p in - str "Subproof completed, now type " ++ str close_cmd ++ str "." - -let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= - Decl_interp.interp_proof_instr - (Decl_mode.get_info sigma gl) - (Goal.V82.env sigma gl) - (sigma) - -let vernac_decl_proof () = - let pf = Proof_global.give_me_the_proof () in - if Proof.is_done pf then - CErrors.error "Nothing left to prove here." - else - begin - Decl_proof_instr.go_to_proof_mode () ; - Proof_global.set_proof_mode "Declarative" - end - -(* spiwack: some bureaucracy is not performed here *) -let vernac_return () = - begin - Decl_proof_instr.return_from_tactic_mode () ; - Proof_global.set_proof_mode "Declarative" - end - -let vernac_proof_instr instr = - Decl_proof_instr.proof_instr instr - -(* Before we can write an new toplevel command (see below) - which takes a [proof_instr] as argument, we need to declare - how to parse it, print it, globalise it and interprete it. - Normally we could do that easily through ARGUMENT EXTEND, - but as the parsing is fairly complicated we will do it manually to - indirect through the [proof_instr] grammar entry. *) -(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) - -(* Only declared at raw level, because only used in vernac commands. *) -let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = - Genarg.make0 "proof_instr" - -(* We create a new parser entry [proof_mode]. The Declarative proof mode - will replace the normal parser entry for tactics with this one. *) -let proof_mode : vernac_expr Gram.entry = - Gram.entry_create "vernac:proof_command" -(* Auxiliary grammar entry. *) -let proof_instr : raw_proof_instr Gram.entry = - Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr) - -let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr - pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr - -let classify_proof_instr = function - | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow - | _ -> Vernac_classifier.classify_as_proofstep - -(* We use the VERNAC EXTEND facility with a custom non-terminal - to populate [proof_mode] with a new toplevel interpreter. - The "-" indicates that the rule does not start with a distinguished - string. *) -VERNAC proof_mode EXTEND ProofInstr - [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ] -END - -(* It is useful to use GEXTEND directly to call grammar entries that have been - defined previously VERNAC EXTEND. In this case we allow, in proof mode, - the use of commands like Check or Print. VERNAC EXTEND does quite a bit of - bureaucracy for us, but it is not needed in this sort of case, and it would require - to have an ARGUMENT EXTEND version of the "proof_mode" grammar entry. *) -GEXTEND Gram - GLOBAL: proof_mode ; - - proof_mode: LAST - [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ] - ; -END - -(* We register a new proof mode here *) - -let _ = - Proof_global.register_proof_mode { Proof_global. - name = "Declarative" ; (* name for identifying and printing *) - (* function [set] goes from No Proof Mode to - Declarative Proof Mode performing side effects *) - set = begin fun () -> - (* We set the command non terminal to - [proof_mode] (which we just defined). *) - Pcoq.set_command_entry proof_mode ; - (* We substitute the goal printer, by the one we built - for the proof mode. *) - Printer.set_printer_pr { Printer.default_printer_pr with - Printer.pr_goal = pr_goal; - pr_subgoals = pr_subgoals; } - end ; - (* function [reset] goes back to No Proof Mode from - Declarative Proof Mode *) - reset = begin fun () -> - (* We restore the command non terminal to - [noedit_mode]. *) - Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ; - (* We restore the goal printer to default *) - Printer.set_printer_pr Printer.default_printer_pr - end - } - -VERNAC COMMAND EXTEND DeclProof -[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] -END -VERNAC COMMAND EXTEND DeclReturn -[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ] -END - -let none_is_empty = function - None -> [] - | Some l -> l - -GEXTEND Gram -GLOBAL: proof_instr; - thesis : - [[ "thesis" -> Plain - | "thesis"; "for"; i=ident -> (For i) - ]]; - statement : - [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} - | i=ident -> {st_label=Anonymous; - st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)} - | c=constr -> {st_label=Anonymous;st_it=c} - ]]; - constr_or_thesis : - [[ t=thesis -> Thesis t ] | - [ c=constr -> This c - ]]; - statement_or_thesis : - [ - [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] - | - [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} - | i=ident -> {st_label=Anonymous; - st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))} - | c=constr -> {st_label=Anonymous;st_it=This c} - ] - ]; - justification_items : - [[ -> Some [] - | "by"; l=LIST1 constr SEP "," -> Some l - | "by"; "*" -> None ]] - ; - justification_method : - [[ -> None - | "using"; tac = tactic -> Some tac ]] - ; - simple_cut_or_thesis : - [[ ls = statement_or_thesis; - j = justification_items; - taco = justification_method - -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] - ; - simple_cut : - [[ ls = statement; - j = justification_items; - taco = justification_method - -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] - ; - elim_type: - [[ IDENT "induction" -> ET_Induction - | IDENT "cases" -> ET_Case_analysis ]] - ; - block_type : - [[ IDENT "claim" -> B_claim - | IDENT "focus" -> B_focus - | IDENT "proof" -> B_proof - | et=elim_type -> B_elim et ]] - ; - elim_obj: - [[ IDENT "on"; c=constr -> Real c - | IDENT "of"; c=simple_cut -> Virtual c ]] - ; - elim_step: - [[ IDENT "consider" ; - h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h) - | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj) - | IDENT "suffices"; ls=suff_clause; - j = justification_items; - taco = justification_method - -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] - ; - rew_step : - [[ "~=" ; c=simple_cut -> (Rhs,c) - | "=~" ; c=simple_cut -> (Lhs,c)]] - ; - cut_step: - [[ "then"; tt=elim_step -> Pthen tt - | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c) - | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) - | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c) - | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c) - | tt=elim_step -> tt - | tt=rew_step -> let s,c=tt in Prew (s,c); - | IDENT "have"; c=simple_cut_or_thesis -> Pcut c; - | IDENT "claim"; c=statement -> Pclaim c; - | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; - | "end"; bt = block_type -> Pend bt; - | IDENT "escape" -> Pescape ]] - ; - (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) - loc_id: - [[ id=ident -> fun x -> (!@loc,(id,x)) ]]; - hyp: - [[ id=loc_id -> id None ; - | id=loc_id ; ":" ; c=constr -> id (Some c)]] - ; - consider_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=consider_vars -> (Hvar name) :: v - | name=hyp; - IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h - ]] - ; - consider_hyps: - [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h - | st=statement; IDENT "and"; - IDENT "consider" ; v=consider_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]] - ; - assume_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=assume_vars -> (Hvar name) :: v - | name=hyp; - IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h - ]] - ; - assume_hyps: - [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h - | st=statement; IDENT "and"; - IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]] - ; - assume_clause: - [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v - | h=assume_hyps -> h ]] - ; - suff_vars: - [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> - [Hvar name],c - | name=hyp; ","; v=suff_vars -> - let (q,c) = v in ((Hvar name) :: q),c - | name=hyp; - IDENT "such"; IDENT "that"; h=suff_hyps -> - let (q,c) = h in ((Hvar name) :: q),c - ]]; - suff_hyps: - [[ st=statement; IDENT "and"; h=suff_hyps -> - let (q,c) = h in (Hprop st::q),c - | st=statement; IDENT "and"; - IDENT "to" ; IDENT "have" ; v=suff_vars -> - let (q,c) = v in (Hprop st::q),c - | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> - [Hprop st],c - ]] - ; - suff_clause: - [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v - | h=suff_hyps -> h ]] - ; - let_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=let_vars -> (Hvar name) :: v - | name=hyp; IDENT "be"; - IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h - ]] - ; - let_hyps: - [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h - | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]]; - given_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=given_vars -> (Hvar name) :: v - | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h - ]] - ; - given_hyps: - [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h - | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]]; - suppose_vars: - [[name=hyp -> [Hvar name] - |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v - |name=hyp; OPT[IDENT "be"]; - IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h - ]] - ; - suppose_hyps: - [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h - | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have"; - v=suppose_vars -> Hprop st::v - | st=statement_or_thesis -> [Hprop st] - ]] - ; - suppose_clause: - [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v; - | h=suppose_hyps -> h ]] - ; - intro_step: - [[ IDENT "suppose" ; h=assume_clause -> Psuppose h - | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; - po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ; - ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> - Pcase (none_is_empty po,c,none_is_empty ho) - | "let" ; v=let_vars -> Plet v - | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses - | IDENT "assume"; h=assume_clause -> Passume h - | IDENT "given"; h=given_vars -> Pgiven h - | IDENT "define"; id=ident; args=LIST0 hyp; - "as"; body=constr -> Pdefine(id,args,body) - | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ) - | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ) - ]] - ; - emphasis : - [[ -> 0 - | "*" -> 1 - | "**" -> 2 - | "***" -> 3 - ]] - ; - bare_proof_instr: - [[ c = cut_step -> c ; - | i = intro_step -> i ]] - ; - proof_instr : - [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]] - ; -END;; diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml deleted file mode 100644 index f5de638ed..000000000 --- a/plugins/decl_mode/ppdecl_proof.ml +++ /dev/null @@ -1,216 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Ltac_plugin -open CErrors -open Pp -open Decl_expr -open Names -open Nameops - -let pr_label = function - Anonymous -> mt () - | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () - -let pr_justification_items pr_constr = function - Some [] -> mt () - | Some (_::_ as l) -> - spc () ++ str "by" ++ spc () ++ - prlist_with_sep (fun () -> str ",") pr_constr l - | None -> spc () ++ str "by *" - -let pr_justification_method pr_tac = function - None -> mt () - | Some tac -> - spc () ++ str "using" ++ spc () ++ pr_tac tac - -let pr_statement pr_constr st = - pr_label st.st_label ++ pr_constr st.st_it - -let pr_or_thesis pr_this = function - Thesis Plain -> str "thesis" - | Thesis (For id) -> - str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id - | This c -> pr_this c - -let pr_cut pr_constr pr_tac pr_it c = - hov 1 (pr_it c.cut_stat) ++ - pr_justification_items pr_constr c.cut_by ++ - pr_justification_method pr_tac c.cut_using - -let type_or_thesis = function - Thesis _ -> Term.mkProp - | This c -> c - -let _I x = x - -let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps = - let pr_sep = if sep then str "and" ++ spc () else mt () in - match hyps with - (Hvar _ ::_) as rest -> - spc () ++ pr_sep ++ str _have ++ - pr_vars pr_var pr_constr gtyp false _be _have rest - | Hprop st :: rest -> - begin - (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) - spc() ++ pr_sep ++ pr_statement pr_constr st ++ - pr_hyps pr_var pr_constr gtyp true _be _have rest - end - | [] -> mt () - -and pr_vars pr_var pr_constr gtyp sep _be _have vars = - match vars with - Hvar st :: rest -> - begin - (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) - let pr_sep = if sep then pr_comma () else mt () in - spc() ++ pr_sep ++ - pr_var st ++ - pr_vars pr_var pr_constr gtyp true _be _have rest - end - | (Hprop _ :: _) as rest -> - let _st = if _be then - str "be such that" - else - str "such that" in - spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest - | [] -> mt () - -let pr_suffices_clause pr_var pr_constr (hyps,c) = - pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++ - str "to show" ++ spc () ++ pr_or_thesis pr_constr c - -let pr_elim_type = function - ET_Case_analysis -> str "cases" - | ET_Induction -> str "induction" - -let pr_block_type = function - B_elim et -> pr_elim_type et - | B_proof -> str "proof" - | B_claim -> str "claim" - | B_focus -> str "focus" - -let pr_casee pr_constr pr_tac =function - Real c -> str "on" ++ spc () ++ pr_constr c - | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut - -let pr_side = function - Lhs -> str "=~" - | Rhs -> str "~=" - -let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function - | Pescape -> str "escape" - | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i - | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i - | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i - | Pcut c -> - begin - match _then,_thus with - false,false -> str "have" ++ spc () ++ - pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c - | false,true -> str "thus" ++ spc () ++ - pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c - | true,false -> str "then" ++ spc () ++ - pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c - | true,true -> str "hence" ++ spc () ++ - pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c - end - | Psuffices c -> - str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c - | Prew (sid,c) -> - (if _thus then str "thus" else str " ") ++ spc () ++ - pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c - | Passume hyps -> - str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps - | Plet hyps -> - str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps - | Pclaim st -> - str "claim" ++ spc () ++ pr_statement pr_constr st - | Pfocus st -> - str "focus on" ++ spc () ++ pr_statement pr_constr st - | Pconsider (id,hyps) -> - str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps - ++ spc () ++ str "from " ++ pr_constr id - | Pgiven hyps -> - str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps - | Ptake witl -> - str "take" ++ spc () ++ - prlist_with_sep pr_comma pr_constr witl - | Pdefine (id,args,body) -> - str "define" ++ spc () ++ pr_id id ++ spc () ++ - prlist_with_sep spc - (fun st -> str "(" ++ - pr_var st ++ str ")") args ++ spc () ++ - str "as" ++ (pr_constr body) - | Pcast (id,typ) -> - str "reconsider" ++ spc () ++ - pr_or_thesis pr_id id ++ spc () ++ - str "as" ++ spc () ++ (pr_constr typ) - | Psuppose hyps -> - str "suppose" ++ - pr_hyps pr_var pr_constr _I false false "we have" hyps - | Pcase (params,pat,hyps) -> - str "suppose it is" ++ spc () ++ pr_pat pat ++ - (if params = [] then mt () else - (spc () ++ str "with" ++ spc () ++ - prlist_with_sep spc - (fun st -> str "(" ++ - pr_var st ++ str ")") params ++ spc ())) - ++ - (if hyps = [] then mt () else - (spc () ++ str "and" ++ - pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis - false false "we have" hyps)) - | Pper (et,c) -> - str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ - pr_casee pr_constr pr_tac c - | Pend blk -> str "end" ++ spc () ++ pr_block_type blk - -let pr_emph = function - 0 -> str " " - | 1 -> str "* " - | 2 -> str "** " - | 3 -> str "*** " - | _ -> anomaly (Pp.str "unknown emphasis") - -let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr = - pr_emph instr.emph ++ spc () ++ - pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr - - -let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) = - pr_gen_proof_instr - (fun (_,(id,otyp)) -> - match otyp with - None -> pr_id id - | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")" - ) - pconstr2 - Ppconstr.pr_cases_pattern_expr - (ptac Pptactic.ltop) - instr - -let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) = - pr_gen_proof_instr - (fun (_,(id,otyp)) -> - match otyp with - None -> pr_id id - | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")") - pconstr2 - Ppconstr.pr_cases_pattern_expr - (ptac Pptactic.ltop) - instr - -let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) = - pr_gen_proof_instr - (fun st -> pr_statement pconstr1 st) - pconstr2 - (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr) - (ptac Pptactic.ltop) - instr - diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli deleted file mode 100644 index 678fc0768..000000000 --- a/plugins/decl_mode/ppdecl_proof.mli +++ /dev/null @@ -1,14 +0,0 @@ - -open Decl_expr -open Pptactic - -val pr_gen_proof_instr : - ('var -> Pp.std_ppcmds) -> - ('constr -> Pp.std_ppcmds) -> - ('pat -> Pp.std_ppcmds) -> - ('tac -> Pp.std_ppcmds) -> - ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds - -val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer -val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer -val pr_proof_instr : proof_instr extra_genarg_printer diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index e28d6aa62..3c0319319 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -159,21 +159,3 @@ END open Proofview.Notations open Cc_plugin -open Decl_mode_plugin - -let default_declarative_automation = - Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *) - Tacticals.New.tclORELSE - (Tacticals.New.tclORELSE (Auto.h_trivial [] None) - (Cctac.congruence_tac !congruence_depth [])) - (Proofview.V82.tactic (gen_ground_tac true - (Some (Tacticals.New.tclTHEN - (snd (default_solver ())) - (Cctac.congruence_tac !congruence_depth []))) - [] [])) - - - -let () = - Decl_proof_instr.register_automation_tac default_declarative_automation - diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v deleted file mode 100644 index da0cc68a4..000000000 --- a/test-suite/bugs/closed/2640.v +++ /dev/null @@ -1,17 +0,0 @@ -(* Testing consistency of globalization and interpretation in some - extreme cases *) - -Section sect. - - (* Simplification of the initial example *) - Hypothesis Other: True. - - Lemma C2 : True. - proof. - Fail have True using Other. - Abort. - - (* Variant of the same problem *) - Lemma C2 : True. - Fail clear; Other. - Abort. diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v deleted file mode 100644 index ea3920551..000000000 --- a/test-suite/ide/undo.v +++ /dev/null @@ -1,103 +0,0 @@ -(* Here are a sequences of scripts to test interactively with undo and - replay in coqide proof sessions *) - -(* Undoing arbitrary commands, as first step *) - -Theorem a : O=O. (* 2 *) -Ltac f x := x. (* 1 * 3 *) -assert True by trivial. -trivial. -Qed. - -(* Undoing arbitrary commands, as non-first step *) - -Theorem b : O=O. -assert True by trivial. -Ltac g x := x. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, as first step *) -(* was bugged in 8.1 *) - -Theorem c : O=O. -Inductive T : Type := I. -trivial. -Qed. - -(* Undoing declarations, as first step *) -(* new in 8.2 *) - -Theorem d : O=O. -Definition e := O. -Definition f := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, as non-first step *) -(* new in 8.2 *) - -Theorem h : O=O. -assert True by trivial. -Definition i := O. -Definition j := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, interleaved with proof steps *) -(* new in 8.2 *) - -Theorem k : O=O. -assert True by trivial. -Definition l := O. -assert True by trivial. -Definition m := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, interleaved with proof steps and commands *) -(* new in 8.2 *) - -Theorem n : O=O. -assert True by trivial. -Definition o := O. -Ltac h x := x. -assert True by trivial. -Focus. -Definition p := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, not in proof *) - -Definition q := O. -Definition r := O. - -(* Bug 2082 : Follow the numbers *) -(* Broken due to proof engine rewriting *) - -Variable A : Prop. -Variable B : Prop. - -Axiom OR : A \/ B. - -Lemma MyLemma2 : True. -proof. -per cases of (A \/ B) by OR. -suppose A. - then (1 = 1). - then H1 : thesis. (* 4 *) - thus thesis by H1. (* 2 *) -suppose B. (* 1 *) (* 3 *) - then (1 = 1). - then H2 : thesis. - thus thesis by H2. -end cases. -end proof. -Qed. (* 5 if you made it here, there is no regression *) - diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake deleted file mode 100644 index 0be439b27..000000000 --- a/test-suite/ide/undo011.fake +++ /dev/null @@ -1,34 +0,0 @@ -# Script simulating a dialog between coqide and coqtop -ideslave -# Run it via fake_ide -# -# Bug 2082 -# Broken due to proof engine rewriting -# -ADD { Variable A : Prop. } -ADD { Variable B : Prop. } -ADD { Axiom OR : A \/ B. } -ADD { Lemma MyLemma2 : True. } -ADD { proof. } -ADD { per cases of (A \/ B) by OR. } -ADD { suppose A. } -ADD { then (1 = 1). } -ADD there { then H1 : thesis. } -ADD here { thus thesis by H1. } -ADD { suppose B. } -QUERY { Show. } -EDIT_AT here -# <replay> -ADD { suppose B. } -# </replay> -EDIT_AT there -# <replay> -ADD { thus thesis by H1. } -ADD { suppose B. } -# </replay> -QUERY { Show. } -ADD { then (1 = 1). } -ADD { then H2 : thesis. } -ADD { thus thesis by H2. } -ADD { end cases. } -ADD { end proof. } -ADD { Qed. } diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v deleted file mode 100644 index e569bcb49..000000000 --- a/test-suite/success/decl_mode.v +++ /dev/null @@ -1,182 +0,0 @@ -(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *) - -Set Firstorder Depth 1. -Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt. - -Lemma double_div2: forall n, div2 (double n) = n. -proof. - assume n:nat. - per induction on n. - suppose it is 0. - suffices (0=0) to show thesis. - thus thesis. - suppose it is (S m) and Hrec:thesis for m. - have (div2 (double (S m))= div2 (S (S (double m)))). - ~= (S (div2 (double m))). - thus ~= (S m) by Hrec. - end induction. -end proof. -Show Script. -Qed. - -Lemma double_inv : forall n m, double n = double m -> n = m . -proof. - let n, m be such that H:(double n = double m). -have (n = div2 (double n)) by double_div2,H. - ~= (div2 (double m)) by H. - thus ~= m by double_div2. -end proof. -Qed. - -Lemma double_mult_l : forall n m, (double (n * m)=n * double m). -proof. - assume n:nat and m:nat. - have (double (n * m) = n*m + n * m). - ~= (n * (m+m)) by * using ring. - thus ~= (n * double m). -end proof. -Qed. - -Lemma double_mult_r : forall n m, (double (n * m)=double n * m). -proof. - assume n:nat and m:nat. - have (double (n * m) = n*m + n * m). - ~= ((n + n) * m) by * using ring. - thus ~= (double n * m). -end proof. -Qed. - -Lemma even_is_even_times_even: forall n, even (n*n) -> even n. -proof. - let n be such that H:(even (n*n)). - per cases of (even n \/ odd n) by even_or_odd. - suppose (odd n). - hence thesis by H,even_mult_inv_r. - end cases. -end proof. -Qed. - -Lemma main_thm_aux: forall n,even n -> -double (double (div2 n *div2 n))=n*n. -proof. - given n such that H:(even n). - *** have (double (double (div2 n * div2 n)) - = double (div2 n) * double (div2 n)) - by double_mult_l,double_mult_r. - thus ~= (n*n) by H,even_double. -end proof. -Qed. - -Require Import Omega. - -Lemma even_double_n: (forall m, even (double m)). -proof. - assume m:nat. - per induction on m. - suppose it is 0. - thus thesis. - suppose it is (S mm) and thesis for mm. - then H:(even (S (S (mm+mm)))). - have (S (S (mm + mm)) = S mm + S mm) using omega. - hence (even (S mm +S mm)) by H. - end induction. -end proof. -Qed. - -Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0. -proof. - assume n0:nat. - define P n as (forall p, n*n=double (p*p) -> p=0). - claim rec_step: (forall n, (forall m,m<n-> P m) -> P n). - let n be such that H:(forall m : nat, m < n -> P m) and p:nat . - per cases of ({n=0}+{n<>0}) by eq_nat_dec. - suppose H1:(n=0). - per cases on p. - suppose it is (S p'). - assume (n * n = double (S p' * S p')). - =~ 0 by H1,mult_n_O. - ~= (S ( p' + p' * S p' + S p'* S p')) - by plus_n_Sm. - hence thesis . - suppose it is 0. - thus thesis. - end cases. - suppose H1:(n<>0). - assume H0:(n*n=double (p*p)). - have (even (double (p*p))) by even_double_n . - then (even (n*n)) by H0. - then H2:(even n) by even_is_even_times_even. - then (double (double (div2 n *div2 n))=n*n) - by main_thm_aux. - ~= (double (p*p)) by H0. - then H':(double (div2 n *div2 n)= p*p) by double_inv. - have (even (double (div2 n *div2 n))) by even_double_n. - then (even (p*p)) by even_double_n,H'. - then H3:(even p) by even_is_even_times_even. - have (double(double (div2 n * div2 n)) = n*n) - by H2,main_thm_aux. - ~= (double (p*p)) by H0. - ~= (double(double (double (div2 p * div2 p)))) - by H3,main_thm_aux. - then H'':(div2 n * div2 n = double (div2 p * div2 p)) - by double_inv. - then (div2 n < n) by lt_div2,neq_O_lt,H1. - then H4:(div2 p=0) by (H (div2 n)),H''. - then (double (div2 p) = double 0). - =~ p by even_double,H3. - thus ~= 0. - end cases. - end claim. - hence thesis by (lt_wf_ind n0 P). -end proof. -Qed. - -Require Import Reals Field. -(*Coercion INR: nat >->R. -Coercion IZR: Z >->R.*) - -Open Scope R_scope. - -Lemma square_abs_square: - forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p). -proof. - assume p:Z. - per cases on p. - suppose it is (0%Z). - thus thesis. - suppose it is (Zpos z). - thus thesis. - suppose it is (Zneg z). - have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) = - (IZR (Zpos z) * IZR (Zpos z))). - ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))). - thus ~= (IZR (Zneg z) * IZR (Zneg z)). - end cases. -end proof. -Admitted. - -Definition irrational (x:R):Prop := - forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q). - -Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)). -proof. - let p:Z,q:nat be such that H:(q<>0%nat) - and H0:(sqrt (INR 2%nat)=(IZR p/INR q)). - have H_in_R:(INR q<>0:>R) by H. - have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field. - have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def. - have (INR (Z.abs_nat p * Z.abs_nat p) - = (INR (Z.abs_nat p) * INR (Z.abs_nat p))) - by mult_INR. - ~= (IZR p* IZR p) by square_abs_square. - ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *) - ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring. - ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0. - ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR. - then (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat. - ~= ((q*q)+(q*q))%nat. - ~= (Div2.double (q*q)). - then (q=0%nat) by main_theorem. - hence thesis by H. -end proof. -Qed. diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v deleted file mode 100644 index 46174e481..000000000 --- a/test-suite/success/decl_mode2.v +++ /dev/null @@ -1,249 +0,0 @@ -Theorem this_is_trivial: True. -proof. - thus thesis. -end proof. -Qed. - -Theorem T: (True /\ True) /\ True. - split. split. -proof. (* first subgoal *) - thus thesis. -end proof. -trivial. (* second subgoal *) -proof. (* third subgoal *) - thus thesis. -end proof. -Abort. - -Theorem this_is_not_so_trivial: False. -proof. -end proof. (* here a warning is issued *) -Fail Qed. (* fails: the proof in incomplete *) -Admitted. (* Oops! *) - -Theorem T: True. -proof. -escape. -auto. -return. -Abort. - -Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False). -intros a b. -proof. -assume H:(if a then True else False). -reconsider H as False. -reconsider thesis as True. -Abort. - -Theorem T: forall x, x=2 -> 2+x=4. -proof. -let x be such that H:(x=2). -have H':(2+x=2+2) by H. -Abort. - -Theorem T: forall x, x=2 -> 2+x=4. -proof. -let x be such that H:(x=2). -then (2+x=2+2). -Abort. - -Theorem T: forall x, x=2 -> x + x = x * x. -proof. -let x be such that H:(x=2). -have (4 = 4). - ~= (2 * 2). - ~= (x * x) by H. - =~ (2 + 2). - =~ H':(x + x) by H. -Abort. - -Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. -proof. -let x be such that H:(x + x = x * x). -claim H':((x - 2) * x = 0). -thus thesis. -end claim. -Abort. - -Theorem T: forall (A B:Prop), A -> B -> A /\ B. -intros A B HA HB. -proof. -hence B. -Abort. - -Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C. -intros A B C HA HB HC. -proof. -thus B by HB. -Abort. - -Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. -intros A B C HA HB HC. -proof. -Fail hence C. (* fails *) -Abort. - -Theorem T: forall (A B:Prop), B -> A \/ B. -intros A B HB. -proof. -hence B. -Abort. - -Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D). -intros A B C D HC HD. -proof. -thus C by HC. -Abort. - -Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. -intros P HP. -proof. -take 2. -Abort. - -Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. -intros P HP. -proof. -hence (P 2). -Abort. - -Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y. -intros P R HP HR. -proof. -thus (P 2) by HP. -Abort. - -Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B. -intros A B P HP HA. -proof. -suffices to have x such that HP':(P x) to show B by HP,HP'. -Abort. - -Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). -intros A P HP HA. -proof. -(* BUG: the next line fails when it should succeed. -Waiting for someone to investigate the bug. -focus on (forall x, x = 2 -> P x). -let x be such that (x = 2). -hence thesis by HP. -end focus. -*) -Abort. - -Theorem T: forall x, x = 0 -> x + x = x * x. -proof. -let x be such that H:(x = 0). -define sqr x as (x * x). -reconsider thesis as (x + x = sqr x). -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -let x:nat. -assume HP:(P x). -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -Fail let x. (* fails because x's type is not clear *) -let x be such that HP:(P x). (* here x's type is inferred from (P x) *) -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. -proof. -let P:(nat -> Prop). -let x:nat. -assume (P x). (* temporary name created *) -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -let x be such that (P x). (* temporary name created *) -Abort. - -Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. -proof. -let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). -consider x such that HP:(P x) and HA:A from H. -Abort. - -(* Here is an example with pairs: *) - -Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p). -proof. -let p:(nat * nat)%type. -consider x:nat,y:nat from p. -reconsider thesis as (x >= y \/ x < y). -Abort. - -Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> -(exists m, P m) -> P 0. -proof. -let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). -given m such that Hm:(P m). -Abort. - -Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C. -proof. -let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C). -assume HAB:(A \/ B). -per cases on HAB. -suppose A. - hence thesis by HAC. -suppose HB:B. - thus thesis by HB,HBC. -end cases. -Abort. - -Section Coq. - -Hypothesis EM : forall P:Prop, P \/ ~ P. - -Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. -proof. -let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). -per cases of (A \/ ~A) by EM. -suppose (~A). - hence thesis by HNAC. -suppose A. - hence thesis by HAC. -end cases. -Abort. - -Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. -proof. -let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). -per cases on (EM A). -suppose (~A). -Abort. -End Coq. - -Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B. -proof. -let A:Prop,B:Prop,x:bool. -per cases on x. -suppose it is true. - assume A. - hence A. -suppose it is false. - assume B. - hence B. -end cases. -Abort. - -Theorem T: forall (n:nat), n + 0 = n. -proof. -let n:nat. -per induction on n. -suppose it is 0. - thus (0 + 0 = 0). -suppose it is (S m) and H:thesis for m. - then (S (m + 0) = S m). - thus =~ (S m + 0). -end induction. -Abort.
\ No newline at end of file diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 03f2328de..c58d23dad 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,7 +19,6 @@ Require Export Coq.Init.Tauto. (* Initially available plugins (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". -Declare ML Module "decl_mode_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". |