aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES6
-rw-r--r--contrib/funind/functional_principles_proofs.ml2
-rw-r--r--contrib/interface/xlate.ml12
-rw-r--r--contrib/subtac/subtac.ml10
-rw-r--r--doc/refman/RefMan-gal.tex24
-rw-r--r--doc/refman/RefMan-tac.tex70
-rw-r--r--ide/coq.ml2
-rw-r--r--ide/highlight.mll2
-rw-r--r--parsing/g_tactic.ml417
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--parsing/pptactic.ml6
-rw-r--r--parsing/ppvernac.ml13
-rw-r--r--parsing/q_coqast.ml410
-rw-r--r--parsing/tactic_printer.ml14
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarutil.mli4
-rw-r--r--proofs/pfedit.ml11
-rw-r--r--proofs/pfedit.mli13
-rw-r--r--proofs/tacexpr.ml6
-rw-r--r--tactics/hiddentac.ml9
-rw-r--r--tactics/hiddentac.mli5
-rw-r--r--tactics/tacinterp.ml24
-rw-r--r--test-suite/output/Fixpoint.out14
-rw-r--r--test-suite/output/Fixpoint.v23
-rw-r--r--test-suite/success/fix.v38
-rw-r--r--toplevel/command.ml206
-rw-r--r--toplevel/command.mli7
-rw-r--r--toplevel/vernacentries.ml22
-rw-r--r--toplevel/vernacexpr.ml5
29 files changed, 474 insertions, 117 deletions
diff --git a/CHANGES b/CHANGES
index 1c3fe7b4c..af156f88b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,7 +1,7 @@
Changes from V8.1 to V8.2
=========================
-Language
+Language
- If a fixpoint is not written with an explicit { struct ... }, then
all arguments are tried successively (from left to right) until one is
@@ -16,8 +16,10 @@ Language
if omitted. (DOC TODO?)
- Record/Structure now usable for defining coinductive types
(e.g. "Record stream := { hd : nat; tl : stream }.")
+- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
+ statements.
-Commands
+Vernacular commands
- Added option Global to "Arguments Scope" for section surviving. (DOC TODO)
- Added option "Unset Elimination Schemes" to deactivate the automatic
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 895fa613f..558ca6c21 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1141,7 +1141,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
then
(* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
else
- h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+ h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos
| _ -> anomaly "Not a valid information"
in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 31465a7a7..82277be4d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -947,18 +947,22 @@ and xlate_tac =
xlate_error "TODO: injection as"
| TacFix (idopt, n) ->
CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
- | TacMutualFix (id, n, fixtac_list) ->
+ | TacMutualFix (false, id, n, fixtac_list) ->
let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in
CT_fixtactic
(ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
CT_fix_tac_list (List.map f fixtac_list))
+ | TacMutualFix (true, id, n, fixtac_list) ->
+ xlate_error "TODO: non user-visible fix"
| TacCofix idopt ->
CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
- | TacMutualCofix (id, cofixtac_list) ->
+ | TacMutualCofix (false, id, cofixtac_list) ->
let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in
CT_cofixtactic
(CT_coerce_ID_to_ID_OPT (xlate_ident id),
CT_cofix_tac_list (List.map f cofixtac_list))
+ | TacMutualCofix (true, id, cofixtac_list) ->
+ xlate_error "TODO: non user-visible cofix"
| TacIntrosUntil (NamedHyp id) ->
CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
| TacIntrosUntil (AnonHyp n) ->
@@ -1880,10 +1884,12 @@ let rec xlate_vernac =
| VernacBeginSection (_,id) ->
CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
| VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
- | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) ->
+ | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
CT_coerce_THEOREM_GOAL_to_COMMAND(
CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
xlate_binder_list bl, xlate_formula c))
+ | VernacStartTheoremProof _ ->
+ xlate_error "TODO: Mutually dependent theorems"
| VernacSuspend -> CT_suspend
| VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
| VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 1cfe69aa9..9641794be 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -67,10 +67,10 @@ let solve_tccs_in_type env id isevars evm c typ =
let start_proof_com env isevars sopt kind (bl,t) hook =
let id = match sopt with
- | Some id ->
+ | Some (loc,id) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
- errorlabstrm "start_proof" (pr_id id ++ str " already exists");
+ user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
id
| None ->
next_global_ident_away false (id_of_string "Unnamed_thm")
@@ -117,13 +117,13 @@ let subtac (loc, command) =
let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
- VernacDefinition (defkind, (locid, id), expr, hook) ->
+ VernacDefinition (defkind, (_, id as lid), expr, hook) ->
(match expr with
| ProveBody (bl, t) ->
if Lib.is_modtype () then
errorlabstrm "Subtac_command.StartProof"
(str "Proof editing mode not supported in module types");
- start_proof_and_print env isevars (Some id) (Global, DefinitionBody Definition) (bl,t)
+ start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
@@ -131,7 +131,7 @@ let subtac (loc, command) =
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
- | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
+ | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
if not(Pfedit.refining ()) then
if lettop then
errorlabstrm "Subtac_command.StartProof"
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 23c19d60b..28cb402f3 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1568,6 +1568,30 @@ All these commands are synonymous of \texttt{Theorem}
% %within the section will be replaced by the proof of {\ident}.
% Same as {\tt Remark} except
% that the innermost section name is dropped from the full name.
+\item {\tt Theorem \nelist{{\ident} : {\type}}{with}.}
+
+This command is useful for theorems that are proved by simultaneous
+induction over a mutually inductive assumption, or that state mutually
+dependent statements in some mutual coinductive type. It is equivalent
+to {\tt Fixpoint} (see Section~\ref{Fixpoint}) or {\tt CoFixpoint}
+(see Section~\ref{CoFixpoint}) but using tactics to build the proof of
+the statements (or the body of the specification, depending on the
+point of view). The inductive or coinductive types on which the
+induction or coinduction has to be done is assumed to be non ambiguous
+and is guessed by the system.
+
+Like in a {\tt Fixpoint} or {\tt CoFixpoint} definition, the induction
+hypotheses have to be used on {\em structurally smaller} arguments
+(for a {\tt Fixpoint}) or be {\em guarded by a constructor} (for a {\tt
+ CoFixpoint}). The verification that recursive proof arguments are
+correct is done only at the time of registering the lemma in the
+environment. To know if the use of induction hypotheses is correct at
+some time of the interactive development of a proof, use the command
+{\tt Guarded} (see Section~\ref{Guarded}).
+
+The command can be used also with {\tt Lemma},
+{\tt Remark}, etc. instead of {\tt Theorem}.
+
\item {\tt Definition {\ident} : {\type}.} \\
Allow to define a term of type {\type} using the proof editing mode. It
behaves as {\tt Theorem} but is intended for the interactive
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1ba08344c..cd32fb35a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -806,6 +806,76 @@ a hypothesis or in the body or the type of a local definition.
\end{Variants}
+\subsection{\tt fix {\ident} {\num}
+\tacindex{fix}
+\label{tactic:fix}}
+
+This tactic is a primitive tactic to start a proof by induction. In
+general, it is easier to rely on higher-level induction tactics such
+as the ones described in Section~\ref{Tac-induction}.
+
+In the syntax of the tactic, the identifier {\ident} is the name given
+to the induction hypothesis. The natural number {\num} tells on which
+premise of the current goal the induction acts, starting
+from 1 and counting both dependent and non dependent
+products. Especially, the current lemma must be composed of at least
+{\num} products.
+
+Like in a {\tt fix} expression, the induction
+hypotheses have to be used on structurally smaller arguments.
+The verification that inductive proof arguments are correct is done
+only at the time of registering the lemma in the environment. To know
+if the use of induction hypotheses is correct at some
+time of the interactive development of a proof, use the command {\tt
+ Guarded} (see Section~\ref{Guarded}).
+
+\begin{Variants}
+ \item {\tt fix} {\ident}$_1$ {\num} {\tt with (} {\ident}$_2$
+ \nelist{{\binder}$_{2}$}{} \zeroone{{\tt \{ struct {\ident$'_2$}
+ \}}} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt (} {\ident}$_1$
+ \nelist{{\binder}$_n$}{} \zeroone{{\tt \{ struct {\ident$'_n$} \}}}
+ {\tt :} {\type}$_n$ {\tt )}
+
+This starts a proof by mutual induction. The statements to be
+simultaneously proved are respectively {\tt forall}
+ \nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+ \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$. The identifiers
+{\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the induction
+hypotheses. The identifiers {\ident}$'_2$ {\ldots} {\ident}$'_n$ are the
+respective names of the premises on which the induction is performed
+in the statements to be simultaneously proved (if not given, the
+system tries to guess itself what they are).
+
+\end{Variants}
+
+\subsection{\tt cofix {\ident}
+\tacindex{cofix}
+\label{tactic:cofix}}
+
+This tactic starts a proof by coinduction. The identifier {\ident} is
+the name given to the coinduction hypothesis. Like in a {\tt cofix}
+expression, the use of induction hypotheses have to guarded by a
+constructor. The verification that the use of coinductive hypotheses
+is correct is done only at the time of registering the lemma in the
+environment. To know if the use of coinduction hypotheses is correct
+at some time of the interactive development of a proof, use the
+command {\tt Guarded} (see Section~\ref{Guarded}).
+
+
+\begin{Variants}
+ \item {\tt cofix} {\ident}$_1$ {\tt with (} {\ident}$_2$
+ \nelist{{\binder}$_2$}{} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt
+ (} {\ident}$_1$ \nelist{{\binder}$_1$}{} {\tt :} {\type}$_n$
+ {\tt )}
+
+This starts a proof by mutual coinduction. The statements to be
+simultaneously proved are respectively {\tt forall}
+\nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+ \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$. The identifiers
+ {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the
+ coinduction hypotheses.
+
+\end{Variants}
\section{Negation and contradiction}
diff --git a/ide/coq.ml b/ide/coq.ml
index 128717acf..e75f50721 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -351,7 +351,7 @@ let compute_reset_info = function
| VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
Reset (id, ref true)
| VernacDefinition (_, (_,id), ProveBody _, _)
- | VernacStartTheoremProof (_, (_,id), _, _, _) ->
+ | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
Reset (id, ref false)
| _ -> NoReset
diff --git a/ide/highlight.mll b/ide/highlight.mll
index c033a6af5..79b4e25aa 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -82,7 +82,7 @@ rule next_order = parse
{ comment_start := lexeme_start lexbuf; comment lexbuf }
| "Module Type"
{ lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
- | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
+ | "Program" space+ ident { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
| ident as id
{ if is_keyword id then
lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b6a3c985a..035bdced7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -297,14 +297,23 @@ GEXTEND Gram
| "-" -> false
| -> true ]]
;
+ simple_fix_binder:
+ [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
+ | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
+ ] ]
+ ;
fixdecl:
- [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
+ [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ann=fixannot;
":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
;
fixannot:
[ [ "{"; IDENT "struct"; id=name; "}" -> Some id
| -> None ] ]
;
+ cofixdecl:
+ [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ":"; ty=lconstr; ")" ->
+ (loc,id,bl,None,ty) ] ]
+ ;
hintbases:
[ [ "with"; "*" -> None
| "with"; l = LIST1 IDENT -> Some l
@@ -387,11 +396,11 @@ GEXTEND Gram
| "fix"; n = natural -> TacFix (None,n)
| "fix"; id = ident; n = natural -> TacFix (Some id,n)
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- TacMutualFix (id,n,List.map mk_fix_tac fd)
+ TacMutualFix (false,id,n,List.map mk_fix_tac fd)
| "cofix" -> TacCofix None
| "cofix"; id = ident -> TacCofix (Some id)
- | "cofix"; id = ident; "with"; fd = LIST1 fixdecl ->
- TacMutualCofix (id,List.map mk_cofix_tac fd)
+ | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
+ TacMutualCofix (false,id,List.map mk_cofix_tac fd)
| IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
TacLetTac (Names.Name id,b,nowhere)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index aea0cf27b..8285bbad3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -123,9 +123,11 @@ GEXTEND Gram
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = identref; bl = binders_let; ":";
- c = lconstr ->
- VernacStartTheoremProof (thm, id, (bl, c), false, no_hook)
+ [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
+ l = LIST0
+ [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
+ (Some id,(bl,c)) ] ->
+ VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
| stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
| stre = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2a46388c3..d4befac1e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -687,11 +687,13 @@ and pr_atom1 = function
hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
| TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
| TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
- | TacMutualFix (id,n,l) ->
+ | TacMutualFix (hidden,id,n,l) ->
+ if hidden then str "idtac" (* should caught before! *) else
hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
str"with " ++ prlist_with_sep spc pr_fix_tac l)
| TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
- | TacMutualCofix (id,l) ->
+ | TacMutualCofix (hidden,id,l) ->
+ if hidden then str "idtac" (* should be caught before! *) else
hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
str"with " ++ prlist_with_sep spc pr_cofix_tac l)
| TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9fe24f4d4..57e21c2ce 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -534,12 +534,13 @@ let rec pr_vernac = function
| None -> mt()
| Some cc -> str" :=" ++ spc() ++ cc))
- | VernacStartTheoremProof (ki,id,(bl,c),b,d) ->
- hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++
- (match bl with
- | [] -> mt()
- | _ -> pr_binders bl ++ spc())
- ++ str":" ++ pr_spc_lconstr c)
+ | VernacStartTheoremProof (ki,l,_,_) ->
+ hov 1 (pr_thm_token ki ++ spc() ++
+ prlist_with_sep (fun () -> str "with ") (fun (id,(bl,c)) -> hov 0
+ (pr_opt pr_lident id ++ spc() ++
+ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+ str":" ++ pr_spc_lconstr c)) l)
+
| VernacEndProof Admitted -> str"Admitted"
| VernacEndProof (Proved (opac,o)) -> (match o with
| None -> if opac then str"Qed" else str"Defined"
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6313a553e..a8ddfadb2 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -313,20 +313,22 @@ let rec mlexpr_of_atomic_tactic = function
let ido = mlexpr_of_ident_option ido in
let n = mlexpr_of_int n in
<:expr< Tacexpr.TacFix $ido$ $n$ >>
- | Tacexpr.TacMutualFix (id,n,l) ->
+ | Tacexpr.TacMutualFix (b,id,n,l) ->
+ let b = mlexpr_of_bool b in
let id = mlexpr_of_ident id in
let n = mlexpr_of_int n in
let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in
let l = mlexpr_of_list f l in
- <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >>
+ <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >>
| Tacexpr.TacCofix ido ->
let ido = mlexpr_of_ident_option ido in
<:expr< Tacexpr.TacCofix $ido$ >>
- | Tacexpr.TacMutualCofix (id,l) ->
+ | Tacexpr.TacMutualCofix (b,id,l) ->
+ let b = mlexpr_of_bool b in
let id = mlexpr_of_ident id in
let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in
let l = mlexpr_of_list f l in
- <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
+ <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >>
| Tacexpr.TacCut c ->
<:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 91c1bc0c4..11b755fa0 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -34,7 +34,7 @@ let pr_rule = function
| Nested(cmpd,_) ->
begin
match cmpd with
- Tactic (texp,_) -> hov 0 (pr_tactic texp)
+ | Tactic (texp,_) -> hov 0 (pr_tactic texp)
| Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
end
| Daimon -> str "<Daimon>"
@@ -50,6 +50,14 @@ let pr_rule_dot = function
| r ->
pr_rule r ++ if uses_default_tac r then str "..." else str"."
+let pr_rule_dot_fnl = function
+ | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
+ | TacMutualCofix (true,_,_))),_),_) ->
+ (* Very big hack to not display hidden tactics in "Theorem with" *)
+ (* (would not scale!) *)
+ mt ()
+ | r -> pr_rule_dot r ++ fnl ()
+
exception Different
(* We remove from the var context of env what is already in osign *)
@@ -155,7 +163,7 @@ let rec print_script nochange sigma pf =
(print_script nochange sigma) spfl )
| Some(rule,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
- pr_rule_dot rule ++ fnl () ++
+ pr_rule_dot_fnl rule ++
prlist_with_sep pr_fnl
(print_script nochange sigma) spfl )
@@ -189,7 +197,7 @@ let print_treescript nochange sigma pf =
| Some(r,spfl) ->
let indent = if List.length spfl >= 2 then 1 else 0 in
(if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
- hv indent (pr_rule_dot r ++ fnl () ++ prlist_with_sep fnl aux spfl)
+ hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl aux spfl)
in hov 0 (aux pf)
let rec print_info_script sigma osign pf =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d80fdac9d..1701a84c9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -226,10 +226,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
and f2 i =
if sp1 = sp2 then
ise_and i
- [(fun i -> ise_array2 i
- (fun i -> evar_conv_x env i CONV) al1 al2);
- (fun i -> ise_list2 i
- (fun i -> evar_conv_x env i CONV) l1 l2)]
+ [(fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 l2);
+ (fun i -> solve_refl evar_conv_x env i sp1 al1 al2,
+ true)]
else (i,false)
in
ise_try evd [f1; f2]
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7df11d332..c5a3cbe3b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -71,6 +71,10 @@ val non_instantiated : evar_map -> (evar * evar_info) list
(* Unification utils *)
val is_ground_term : evar_defs -> constr -> bool
+val solve_refl :
+ (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
+ -> env -> evar_defs -> existential_key -> constr array -> constr array ->
+ evar_defs
val solve_simple_eqn :
(env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-> env -> evar_defs -> conv_pb * existential * constr ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 81216d169..6dad6471d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,6 +33,7 @@ open Safe_typing
type proof_topstate = {
mutable top_end_tac : tactic option;
+ top_init_tac : tactic option;
top_goal : goal;
top_strength : Decl_kinds.goal_kind;
top_hook : declaration_hook }
@@ -118,8 +119,6 @@ let delete_proof (loc,id) =
user_err_loc
(loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
-let init_proofs () = Edit.clear proof_edits
-
let mutate f =
try
Edit.mutate proof_edits (fun _ pfs -> f pfs)
@@ -128,7 +127,8 @@ let mutate f =
(str"No focused proof" ++ msg_proofs true)
let start (na,ts) =
- let pfs = mk_pftreestate ts.top_goal in
+ let pfs = mk_pftreestate ts.top_goal in
+ let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
add_proof(na,pfs,ts)
let restart_proof () =
@@ -238,7 +238,7 @@ let check_no_pending_proofs () =
let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
-let delete_all_proofs = init_proofs
+let delete_all_proofs () = Edit.clear proof_edits
(*********************************************************************)
(* Modifying the end tactic of the current profftree *)
@@ -251,10 +251,11 @@ let set_end_tac tac =
(* Modifying the current prooftree *)
(*********************************************************************)
-let start_proof na str sign concl hook =
+let start_proof na str sign concl ?init_tac hook =
let top_goal = mk_goal sign concl None in
let ts = {
top_end_tac = None;
+ top_init_tac = init_tac;
top_goal = top_goal;
top_strength = str;
top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5de956d46..ad7c5e51a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -71,13 +71,16 @@ val current_proof_depth: unit -> int
val set_undo : int option -> unit
val get_undo : unit -> int option
-(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion
- [t]; [hook] is optionally a function to be applied at proof end (e.g. to
- declare the built constructions as a coercion or a setoid morphism) *)
+(*s [start_proof s str env t hook tac] starts a proof of name [s] and
+ conclusion [t]; [hook] is optionally a function to be applied at
+ proof end (e.g. to declare the built constructions as a coercion
+ or a setoid morphism); init_tac is possibly a tactic to
+ systematically apply at initialization time (e.g. to start the
+ proof of mutually dependent theorems) *)
val start_proof :
- identifier -> goal_kind -> named_context_val -> constr
- -> declaration_hook -> unit
+ identifier -> goal_kind -> named_context_val -> constr ->
+ ?init_tac:tactic -> declaration_hook -> unit
(* [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a13f8bf70..34699c5fd 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -26,6 +26,7 @@ type evars_flag = bool (* true = pose evars false = fail on evars *)
type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type split_flag = bool (* true = exists false = split *)
+type hidden_flag = bool (* true = internal use false = user-level *)
type raw_red_flag =
| FBeta
@@ -140,9 +141,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacCase of evars_flag * 'constr with_bindings
| TacCaseType of 'constr
| TacFix of identifier option * int
- | TacMutualFix of identifier * int * (identifier * int * 'constr) list
+ | TacMutualFix of hidden_flag * identifier * int * (identifier * int *
+ 'constr) list
| TacCofix of identifier option
- | TacMutualCofix of identifier * (identifier * 'constr) list
+ | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
| TacCut of 'constr
| TacAssert of 'tac option * intro_pattern_expr * 'constr
| TacGeneralize of 'constr list
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0cb314201..c3b7e0a8b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -49,14 +49,15 @@ let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c)
let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb)
let h_case_type c = abstract_tactic (TacCaseType (inj_open c)) (case_type c)
let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n)
-let h_mutual_fix id n l =
+let h_mutual_fix b id n l =
abstract_tactic
- (TacMutualFix (id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
+ (TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
(mutual_fix id n l)
+
let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido)
-let h_mutual_cofix id l =
+let h_mutual_cofix b id l =
abstract_tactic
- (TacMutualCofix (id,List.map (fun (id,c) -> (id,inj_open c)) l))
+ (TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l))
(mutual_cofix id l)
let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 8cbc28d1e..49415649b 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -43,10 +43,11 @@ val h_elim_type : constr -> tactic
val h_case : evars_flag -> constr with_ebindings -> tactic
val h_case_type : constr -> tactic
-val h_mutual_fix : identifier -> int ->
+val h_mutual_fix : hidden_flag -> identifier -> int ->
(identifier * int * constr) list -> tactic
val h_fix : identifier option -> int -> tactic
-val h_mutual_cofix : identifier -> (identifier * constr) list -> tactic
+val h_mutual_cofix : hidden_flag -> identifier ->
+ (identifier * constr) list -> tactic
val h_cofix : identifier option -> tactic
val h_cut : constr -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3367f89f1..068ae8e96 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -657,13 +657,13 @@ let rec intern_atomic lf ist x =
| TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
| TacCaseType c -> TacCaseType (intern_type ist c)
| TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
- | TacMutualFix (id,n,l) ->
+ | TacMutualFix (b,id,n,l) ->
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
- TacMutualFix (intern_ident lf ist id, n, List.map f l)
+ TacMutualFix (b,intern_ident lf ist id, n, List.map f l)
| TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
- | TacMutualCofix (id,l) ->
+ | TacMutualCofix (b,id,l) ->
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
- TacMutualCofix (intern_ident lf ist id, List.map f l)
+ TacMutualCofix (b,intern_ident lf ist id, List.map f l)
| TacCut c -> TacCut (intern_type ist c)
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_tactic ist) otac,
@@ -2016,13 +2016,13 @@ and interp_atomic ist gl = function
| TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
| TacCaseType c -> h_case_type (pf_interp_type ist gl c)
| TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n
- | TacMutualFix (id,n,l) ->
+ | TacMutualFix (b,id,n,l) ->
let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c)
- in h_mutual_fix (interp_fresh_ident ist gl id) n (List.map f l)
+ in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l)
| TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt)
- | TacMutualCofix (id,l) ->
+ | TacMutualCofix (b,id,l) ->
let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in
- h_mutual_cofix (interp_fresh_ident ist gl id) (List.map f l)
+ h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l)
| TacCut c -> h_cut (pf_interp_type ist gl c)
| TacAssert (t,ipat,c) ->
let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
@@ -2350,11 +2350,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
| TacCaseType c -> TacCaseType (subst_rawconstr subst c)
| TacFix (idopt,n) as x -> x
- | TacMutualFix (id,n,l) ->
- TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
+ | TacMutualFix (b,id,n,l) ->
+ TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
| TacCofix idopt as x -> x
- | TacMutualCofix (id,l) ->
- TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
+ | TacMutualCofix (b,id,l) ->
+ TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
| TacCut c -> TacCut (subst_rawconstr subst c)
| TacAssert (b,na,c) ->
TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 62c9d3952..cbb387ce9 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,3 +9,17 @@ let fix f (m : nat) : nat := match m with
| S m' => f m'
end in f 0
: nat
+fix even_pos_odd_pos 2
+ with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+ omega.
+
+ apply odd_pos_even_pos in H.
+ omega.
+
+ intros.
+ destruct H.
+ apply even_pos_odd_pos in H.
+ omega.
+
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index fc27e8d28..2b13c2041 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -16,3 +16,26 @@ Check
end
in f 0.
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0.
+Proof.
+fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+ omega.
+ apply odd_pos_even_pos in H.
+ omega.
+ intros.
+ destruct H.
+ apply even_pos_odd_pos in H.
+ omega.
+Show Script.
+Qed.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 108886cf5..78b01f3e1 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -57,3 +57,41 @@ Lemma bx0bx : decomp bx0 = bx1.
simpl. (* used to return bx0 in V8.1 and before instead of bx1 *)
reflexivity.
Qed.
+
+(* Check mutually inductive statements *)
+
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0
+with odd_pos_even_pos : forall n, odd n -> n >= 1.
+Proof.
+ intros.
+ destruct H.
+ omega.
+ apply odd_pos_even_pos in H.
+ omega.
+ intros.
+ destruct H.
+ apply even_pos_odd_pos in H.
+ omega.
+Qed.
+
+CoInductive a : Prop := acons : b -> a
+with b : Prop := bcons : a -> b.
+
+Lemma a1 : a
+with b1 : b.
+Proof.
+apply acons.
+assumption.
+
+apply bcons.
+assumption.
+Qed.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d04bbafe3..860a542f4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -136,7 +136,7 @@ let red_constant_entry bl ce = function
let declare_global_definition ident ce local imps =
let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
if local = Local && Flags.is_verbose() then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
@@ -188,7 +188,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
let kn =
declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
assumption_message ident;
if local=Local & Flags.is_verbose () then
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -338,28 +338,23 @@ let (inDec,outDec) =
let start_hook = ref ignore
let set_start_hook = (:=) start_hook
-let start_proof id kind c hook =
+let start_proof id kind c ?init_tac hook =
let sign = Global.named_context () in
let sign = clear_proofs sign in
- !start_hook c;
- Pfedit.start_proof id kind sign c hook
+ !start_hook c;
+ Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
let save id const (locality,kind) hook =
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
+ let k = logical_kind_of_goal_kind kind in
let l,r = match locality with
| Local when Lib.sections_are_opened () ->
- let k = logical_kind_of_goal_kind kind in
let c = SectionLocalDef (pft, tpo, opacity) in
let _ = declare_variable id (Lib.cwd(), c, k) in
(Local, VarRef id)
- | Local ->
- let k = logical_kind_of_goal_kind kind in
- let kn = declare_constant id (DefinitionEntry const, k) in
- (Global, ConstRef kn)
- | Global ->
- let k = logical_kind_of_goal_kind kind in
+ | Local | Global ->
let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn) in
Pfedit.delete_current_proof ();
@@ -392,7 +387,7 @@ let make_eq_decidability ind =
then (message (bl_name^" is already declared."))
else (
start_proof (id_of_string bl_name)
- (Global,Proof Theorem)
+ (Global,Proof Theorem)
(Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec)
(fun _ _ -> ());
Auto_ind_decl.compute_bl_tact ind lnamesparrec nparrec;
@@ -789,7 +784,7 @@ let declare_fix boxed kind f def t imps =
} in
let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
gr
let prepare_recursive_declaration fixnames fixtypes fixdefs =
@@ -1036,24 +1031,171 @@ let build_combined_scheme name schemes =
if_verbose ppnl (recursive_message Fixpoint None [snd name])
(* 4| Goal declaration *)
-let start_proof_com sopt kind (bl,t) hook =
- let id = match sopt with
- | Some id ->
- (* We check existence here: it's a bit late at Qed time *)
- if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
- errorlabstrm "start_proof" (pr_id id ++ str " already exists");
- id
- | None ->
- next_global_ident_away false (id_of_string "Unnamed_thm")
- (Pfedit.get_all_proof_names ())
- in
- let env = Global.env () in
- let t = generalize_constr_expr t bl in
- let it, imps = interp_type_evars_impls env t in
- start_proof id kind it
- (fun str cst ->
- maybe_declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
- hook str cst)
+
+(* 4.1| Support for mutually proved theorems *)
+
+let retrieve_first_recthm = function
+ | VarRef id ->
+ (pi2 (Global.lookup_named id),variable_opacity id)
+ | ConstRef cst ->
+ let {const_body=body;const_opaque=opaq} =
+ Global.lookup_constant cst in
+ (Option.map Declarations.force body,opaq)
+ | _ -> assert false
+
+let compute_proof_name = function
+ | Some (loc,id) ->
+ (* We check existence here: it's a bit late at Qed time *)
+ if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+ user_err_loc (loc,"",pr_id id ++ str " already exists");
+ id
+ | None ->
+ next_global_ident_away false (id_of_string "Unnamed_thm")
+ (Pfedit.get_all_proof_names ())
+
+let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
+ match body with
+ | None ->
+ (match local with
+ | Local ->
+ let impl=false and keep=false in (* copy values from Vernacentries *)
+ let k = IsAssumption Conjectural in
+ let c = SectionLocalAssum (t_i,impl,keep) in
+ let _ = declare_variable id (Lib.cwd(),c,k) in
+ (Local,VarRef id,imps)
+ | Global ->
+ let k = IsAssumption Conjectural in
+ let kn = declare_constant id (ParameterEntry (t_i,false), k) in
+ (Global,ConstRef kn,imps))
+ | Some body ->
+ let k = logical_kind_of_goal_kind kind in
+ let body_i = match kind_of_term body with
+ | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+ | CoFix (0,decls) -> mkCoFix (i,decls)
+ | _ -> anomaly "Not a proof by induction" in
+ match local with
+ | Local ->
+ let c = SectionLocalDef (body_i, Some t_i, opaq) in
+ let _ = declare_variable id (Lib.cwd(), c, k) in
+ (Local,VarRef id,imps)
+ | Global ->
+ let const =
+ { const_entry_body = body_i;
+ const_entry_type = Some t_i;
+ const_entry_opaque = opaq;
+ const_entry_boxed = false (* copy of what cook_proof does *)} in
+ let kn = declare_constant id (DefinitionEntry const, k) in
+ (Global,ConstRef kn,imps)
+
+let look_for_mutual_statements thms =
+ if List.tl thms <> [] then
+ (* More than one statement: we look for a common inductive hyp or a *)
+ (* common coinductive conclusion *)
+ let n = List.length thms in
+ let inds = List.map (fun (id,(t,_) as x) ->
+ let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in
+ let whnf_hyp_hds = map_rel_context_with_binders
+ (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
+ hyps in
+ let ind_hyps =
+ List.filter ((<>) None) (list_map_i (fun i (_,b,t) ->
+ match kind_of_term t with
+ | Ind (kn,_ as ind) when
+ let mind = Global.lookup_mind kn in
+ mind.mind_ntypes = n & mind.mind_finite & b = None ->
+ Some (ind,x,i)
+ | _ ->
+ None) 1 whnf_hyp_hds) in
+ let ind_ccl =
+ let cclenv = push_rel_context hyps (Global.env()) in
+ let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+ match kind_of_term whnf_ccl with
+ | Ind (kn,_ as ind) when
+ let mind = Global.lookup_mind kn in
+ mind.mind_ntypes = n & not mind.mind_finite ->
+ Some (ind,x,0)
+ | _ ->
+ None in
+ ind_hyps,ind_ccl) thms in
+ let inds_hyps,ind_ccls = List.split inds in
+ let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in
+ let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in
+ (* Check if all conclusions are coinductive in the same type *)
+ let same_indccl =
+ match ind_ccls with
+ | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest
+ -> Some (x :: List.map Option.get rest)
+ | _ -> None in
+ (* Check if some hypotheses are inductive in the same type *)
+ let common_same_indhyp =
+ let rec find_same_ind inds =
+ match inds with
+ | []::_ ->
+ []
+ | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms ->
+ let others' = List.map (List.filter (is_same_ind kn)) other_thms in
+ (x,others')::find_same_ind (hyps_thms1::other_thms)
+ | (None::hyps_thm1)::other_thms ->
+ find_same_ind (hyps_thm1::other_thms)
+ | [] ->
+ assert false in
+ find_same_ind inds_hyps in
+ let common_inds,finite =
+ match same_indccl, common_same_indhyp with
+ | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest ->
+ (* One occurrence of common inductive hyps and no common coind ccls *)
+ Option.get x::List.map (fun x -> Option.get (List.hd x)) rest,
+ false
+ | Some indccl, [] ->
+ (* One occurrence of common coind ccls and no common inductive hyps *)
+ indccl, true
+ | _ ->
+ error
+ ("Cannot find a common mutual inductive premise or coinductive" ^
+ " conclusion in the statements") in
+ let ordered_inds = List.sort compare_kn common_inds in
+ list_iter_i (fun i' ((kn,i),_,_) ->
+ if i <> i' then
+ error
+ ("Cannot find distinct (co)inductive types of the same family" ^
+ "of mutual (co)inductive types"))
+ ordered_inds;
+ let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
+ let rec_tac =
+ if finite then
+ match List.map (fun (id,(t,_)) -> (id,t)) thms with
+ | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
+ | _ -> assert false
+ else
+ match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+ | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
+ | _ -> assert false in
+ Some rec_tac,thms
+ else
+ None, thms
+
+(* 4.2| General support for goals *)
+
+let start_proof_com kind thms hook =
+ let thms = List.map (fun (sopt,(bl,t)) ->
+ (compute_proof_name sopt,
+ interp_type_evars_impls (Global.env()) (generalize_constr_expr t bl)))
+ thms in
+ let rec_tac,thms = look_for_mutual_statements thms in
+ match thms with
+ | [] -> anomaly "No proof to start"
+ | (id,(t,imps))::other_thms ->
+ let hook strength ref =
+ let other_thms_data =
+ if other_thms = [] then [] else
+ (* there are several theorems defined mutually *)
+ let body,opaq = retrieve_first_recthm ref in
+ list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
+ let thms_data = (strength,ref,imps)::other_thms_data in
+ List.iter (fun (strength,ref,imps) ->
+ maybe_declare_manual_implicits false ref (is_implicit_args ()) imps;
+ hook strength ref) thms_data in
+ start_proof id kind t ?init_tac:rec_tac hook
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8a987ef6c..b37c6c359 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -108,10 +108,11 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val set_start_hook : (types -> unit) -> unit
val start_proof : identifier -> goal_kind -> types ->
- declaration_hook -> unit
+ ?init_tac:Proof_type.tactic -> declaration_hook -> unit
-val start_proof_com : identifier option -> goal_kind ->
- (local_binder list * constr_expr) -> declaration_hook -> unit
+val start_proof_com : goal_kind ->
+ (lident option * (local_binder list * constr_expr)) list ->
+ declaration_hook -> unit
(* A hook the next three functions pass to cook_proof *)
val set_save_hook : (Refiner.pftreestate -> unit) -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 54228e273..473985aed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -295,12 +295,12 @@ let vernac_notation = Metasyntax.add_notation
(***********)
(* Gallina *)
-let start_proof_and_print idopt k t hook =
- start_proof_com idopt k t hook;
+let start_proof_and_print k l hook =
+ start_proof_com k l hook;
print_subgoals ();
if !pcoq <> None then (Option.get !pcoq).start_proof ()
-let vernac_definition (local,_,_ as k) id def hook =
+let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
match def with
| ProveBody (bl,t) -> (* local binders, typ *)
if Lib.is_modtype () then
@@ -308,7 +308,8 @@ let vernac_definition (local,_,_ as k) id def hook =
(str "Proof editing mode not supported in module types")
else
let hook _ _ = () in
- start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook
+ start_proof_and_print (local,DefinitionBody Definition)
+ [Some lid,(bl,t)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -317,7 +318,7 @@ let vernac_definition (local,_,_ as k) id def hook =
Some (interp_redexp env evc r) in
declare_definition id k bl red_option c typ_opt hook
-let vernac_start_proof kind sopt (bl,t) lettop hook =
+let vernac_start_proof kind l lettop hook =
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
@@ -325,7 +326,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
if Lib.is_modtype () then
errorlabstrm "Vernacentries.StartProof"
(str "Proof editing mode not supported in module types");
- start_proof_and_print sopt (Global, Proof kind) (bl,t) hook
+ start_proof_and_print (Global, Proof kind) l hook
let vernac_end_proof = function
| Admitted -> admit ()
@@ -1051,7 +1052,7 @@ let vernac_goal = function
| Some c ->
if not (refining()) then begin
let unnamed_kind = Lemma (* Arbitrary *) in
- start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->());
+ start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->());
print_subgoals ()
end else
error "repeated Goal not permitted in refining mode"
@@ -1186,9 +1187,8 @@ let interp c = match c with
| VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
(* Gallina *)
- | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
- | VernacStartTheoremProof (k,(_,id),t,top,f) ->
- vernac_start_proof k (Some id) t top f
+ | VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f
+ | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f
| VernacEndProof e -> vernac_end_proof e
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
@@ -1279,7 +1279,7 @@ let interp c = match c with
| VernacNop -> ()
(* Proof management *)
- | VernacGoal t -> vernac_start_proof Theorem None ([],t) false (fun _ _ ->())
+ | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->())
| VernacAbort id -> vernac_abort id
| VernacAbortAll -> vernac_abort_all ()
| VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 976677f8c..7c9998fb4 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -199,8 +199,9 @@ type vernac_expr =
(* Gallina *)
| VernacDefinition of definition_kind * lident * definition_expr *
declaration_hook
- | VernacStartTheoremProof of theorem_kind * lident *
- (local_binder list * constr_expr) * bool * declaration_hook
+ | VernacStartTheoremProof of theorem_kind *
+ (lident option * (local_binder list * constr_expr)) list *
+ bool * declaration_hook
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
| VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 11:07:28 +0000