Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve

des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 192 insertions, 48 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d04bbafe38..860a542f41 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 8a987ef6c3..b37c6c359c 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 54228e2735..473985aed4 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 976677f8cd..7c9998fb4d 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