diff options
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-decl.tex | 33 | ||||
| -rw-r--r-- | parsing/tactic_printer.ml | 5 | ||||
| -rw-r--r-- | proofs/refiner.ml | 31 | ||||
| -rw-r--r-- | proofs/refiner.mli | 3 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 10 |
8 files changed, 51 insertions, 35 deletions
diff --git a/dev/include b/dev/include index 364773753..6ed62e1e9 100644 --- a/dev/include +++ b/dev/include @@ -26,6 +26,7 @@ #install_printer (* goal *) ppgoal;; #install_printer (* sigma goal *) ppsigmagoal;; #install_printer (* proof *) pproof;; +#install_printer (* pftreestate *) pppftreestate;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; #install_printer (* evar_defs *) ppevd;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4881c3eef..f60fb222d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -103,6 +103,7 @@ let ppevm evd = pp(pr_evar_defs evd) let ppevd evd = pp(pr_evar_defs evd) let ppclenv clenv = pp(pr_clenv clenv) let ppgoal g = pp(db_pr_goal g) +let pppftreestate p = pp(print_pftreestate p) let pr_gls gls = hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex index b5684f929..ba8a5ac63 100644 --- a/doc/refman/RefMan-decl.tex +++ b/doc/refman/RefMan-decl.tex @@ -35,7 +35,7 @@ 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 refered to exist where they are used +\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 @@ -50,7 +50,7 @@ correct: This section explain what differences the casual Coq user will experience using the \DPL . \begin{enumerate} -\item The focussing mechanism is constrained so that only one goal at +\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 to go on with the proof and fill @@ -133,7 +133,7 @@ Conventions:\begin{itemize} \subsection{Temporary names} -In proof commands where an optional name is asked for, ommiting the +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 undescore '\_' character (e.g. {\tt \_hyp0}). Temporary names have a lifespan of one @@ -143,8 +143,7 @@ command: they get erased after the next command. They can however be safely in t \subsection{Starting and Ending a mathematical proof} - - The standard way to use the \DPL is to first state a {\texttt{Lemma/Theorem/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 proven, they will be displayed using the usual Coq display. + The standard way to use the \DPL is to first state a {\texttt{Lemma/Theorem/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. @@ -178,7 +177,7 @@ Abort. 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 tehe statement is proven: A warning will +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 @@ -348,7 +347,7 @@ conclusion step & {\tt thus} & {\tt hence} & {\tt focus on} & {\tt thus $\sim$=/=$\sim$}\\ \hline \end{tabular} -\caption{Correspondance between basic forward steps and conclusion steps} +\caption{Correspondence between basic forward steps and conclusion steps} \end{figure} Let us begin with simple examples : @@ -462,7 +461,7 @@ hence (P 2). Abort. \end{coq_eval} -Here a more involved exmaple where the choice of {\tt P 2} propagates +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} @@ -534,10 +533,10 @@ Abort. \subsection{Introduction steps} -When the {\tt thesis} consists of a hypothestical formula (implication +When the {\tt thesis} consists of a hypothetical formula (implication or universal quantification (e.g. \verb+A -> B+) , it is possible to -assume the hypotetical part {\tt A} and then prove {\tt B}. In the -\DPL{}, this comes in two syntactic flavours that are semantically +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} @@ -554,7 +553,7 @@ assume HP:(P x). Abort. \end{coq_eval} -In the {\tt let} variant, the type of the assumed objet is optional +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}. @@ -572,7 +571,7 @@ let x be such that HP:(P x). (* here x's type is inferred from (P x) *) Abort. \end{coq_eval} -In the {\tt assume } variant, the type of the assumed objet is mandatory but the name is optional : +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. @@ -606,8 +605,8 @@ Abort. \subsection{Tuple elimination steps} In the \CIC, many objects dealt with in simple proofs are tuples : -pairs , records, existentially quantified formulae. These are so -comman that the \DPL{} provides a mechanism to extract members of +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... @@ -735,7 +734,7 @@ End Coq. 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 detailled description of patterns is to be +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} @@ -793,7 +792,7 @@ 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 behaviour: +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. diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index d50e520f9..49cec626f 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -72,7 +72,7 @@ let thin_sign osign sign = with Not_found | Different -> Environ.push_named_context_val d sign) sign ~init:Environ.empty_named_context_val -let rec print_proof sigma osign pf = +let rec print_proof _sigma osign pf = let hyps = Environ.named_context_of_val pf.goal.evar_hyps in let hyps' = thin_sign osign hyps in match pf.ref with @@ -84,7 +84,7 @@ let rec print_proof sigma osign pf = spc () ++ str" BY " ++ hov 0 (pr_rule r) ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)) + hov 0 (prlist_with_sep pr_fnl (print_proof _sigma hyps) spfl)) let pr_change gl = str"change " ++ @@ -221,4 +221,5 @@ let print_subscript sigma sign pf = format_print_info_script sigma sign pf let _ = Refiner.set_info_printer print_subscript +let _ = Refiner.set_proof_printer print_proof diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 9dd35a8c2..b0239eeb4 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -53,17 +53,14 @@ let descend n p = | left,(wanted::right) -> (wanted, (fun pfl' -> - if (List.length pfl' = 1) - & (List.hd pfl').goal = wanted.goal - then - let pf' = List.hd pfl' in - let spfl = left@(pf'::right) in - let newstatus = and_status (List.map pf_status spfl) in - { p with - open_subgoals = newstatus; - ref = Some(r,spfl) } - else - error "descend: validation")) + if false (* debug *) then assert + (List.length pfl'=1 & (List.hd pfl').goal = wanted.goal); + let pf' = List.hd pfl' in + let spfl = left@(pf'::right) in + let newstatus = and_status (List.map pf_status spfl) in + { p with + open_subgoals = newstatus; + ref = Some(r,spfl) })) | _ -> assert false) else error "Too few subproofs" @@ -929,3 +926,15 @@ let tclINFO (tac : tactic) gls = msgnl (hov 0 (str "Info failed to apply validation")) end; res + +let pp_proof = ref (fun _ _ _ -> assert false) +let set_proof_printer f = pp_proof := f + +let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } = + (if stack = [] + then str "Rooted proof tree is:" + else (str "Proof tree at occurrence [" ++ + prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n) + (List.rev stack) ++ str "] is:")) ++ fnl() ++ + !pp_proof sigma (Global.named_context()) pf ++ + Evd.pr_evar_defs sigma diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 5cbc2bde8..d6bd73ca4 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -236,3 +236,6 @@ open Pp (*i*) val set_info_printer : (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit +val set_proof_printer : + (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit +val print_pftreestate : pftreestate -> Pp.std_ppcmds diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index ef2f77069..e909a1f4f 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt = let mark_as_done pts = map_pftreestate (fun _ -> mark_proof_tree_as_done) - (traverse 0 pts) + (up_to_matching_rule is_focussing_command pts) (* post-instruction focus management *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6bf3e34b0..f9de72757 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -234,15 +234,17 @@ let add_hints_iff l2r lc n bl = Auto.add_hints true bl (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIff +VERNAC COMMAND EXTEND HintResolveIffLR [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ add_hints_iff true lc n bl ] -| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ add_hints_iff false lc n bl ] | [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] -> [ add_hints_iff true lc n ["core"] ] +END +VERNAC COMMAND EXTEND HintResolveIffRL + [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) + ":" preident_list(bl) ] -> + [ add_hints_iff false lc n bl ] | [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] -> [ add_hints_iff false lc n ["core"] ] END |