One can use a measure {mes f x} instead of a well-founded relation in GenFixpoint.

If the function takes only one argument, it can be deleted from the wf/mes part.


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

3 files changed, 103 insertions, 36 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index c02c83c3a..86a67866c 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -9,7 +9,8 @@ open Rawterm
 
 type annot = 
     Struct of identifier 
-  | Wf of Topconstr.constr_expr * identifier 
+  | Wf of Topconstr.constr_expr * identifier option
+  | Mes of Topconstr.constr_expr * identifier option
 
 
 type newfixpoint_expr =
@@ -171,7 +172,7 @@ let register_struct is_rec fixpoint_exprl =
     | _ -> 
 	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
 
-let register_wf fname wf_rel_expr wf_arg args ret_type body =  
+let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body =  
   let type_of_f = Command.generalize_constr_expr ret_type args in 
   let rec_arg_num = 
     let names = 
@@ -179,7 +180,12 @@ let register_wf fname wf_rel_expr wf_arg args ret_type body =
 	snd
 	(Topconstr.names_of_local_assums args) 
     in 
-    Util.list_index (Name wf_arg) names 
+    match wf_arg with 
+      | None -> 
+	  if List.length names = 1 then 1
+	  else error "Recursive argument must be specified"
+      | Some wf_arg -> 
+	  Util.list_index (Name wf_arg) names 
   in
   let unbounded_eq = 
     let f_app_args = 
@@ -199,8 +205,49 @@ let register_wf fname wf_rel_expr wf_arg args ret_type body =
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Command.generalize_constr_expr unbounded_eq args in 
-  Recdef.recursive_definition fname type_of_f wf_rel_expr rec_arg_num eq
+  Recdef.recursive_definition is_mes fname type_of_f wf_rel_expr rec_arg_num eq
     
+let register_mes fname wf_mes_expr wf_arg args ret_type body = 
+  let wf_arg_type,wf_arg = 
+    match wf_arg with 
+      | None -> 
+	  begin
+	    match args with 
+	      | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x 
+	      | _ -> error "Recursive argument must be specified" 
+	  end
+      | Some wf_args -> 
+	  try 
+	    match 
+	      List.find 
+		(function 
+		   | Topconstr.LocalRawAssum(l,t) -> 
+		       List.exists (function (_,Name id) -> id =  wf_args | _ -> false) l 
+		   | _ -> false
+		)
+		args 
+	    with 
+	      | Topconstr.LocalRawAssum(_,t)  ->	    t,wf_args
+	      | _ -> assert false 
+	  with Not_found -> assert false 
+  in
+  let ltof = 
+    let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in 
+    Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp 
+      (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
+  in
+  let fun_from_mes = 
+    let applied_mes = 
+      Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg])
+    in
+    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) 
+  in
+  let wf_rel_from_mes = 
+    Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
+  in
+  register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) args ret_type body
+	  
+
 
 
 let register (fixpoint_exprl :  newfixpoint_expr list) = 
@@ -210,6 +257,9 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
       | [((name,Wf (wf_rel,wf_x),args,types,body))] -> 
 	  register_wf name wf_rel wf_x args types body;
 	  false
+      | [((name,Mes (wf_mes,wf_x),args,types,body))] -> 
+	  register_mes name wf_mes wf_x args types body;
+	  false
       | _ -> 
 	  
 	  let old_fixpoint_exprl =  
@@ -223,7 +273,7 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
 		     in 
 		     let annot = Util.list_index (Name id) names - 1 in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
-		 | (_,Wf _,_,_,_) -> 
+		 | (_,Wf _,_,_,_) | (_,Mes _,_,_,_)  -> 
 		     error 
 		       ("Cannot use mutual definition with well-founded recursion")
 	      ) 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 55f67b5b8..fca784b46 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -101,7 +101,8 @@ END
 
 VERNAC ARGUMENT EXTEND rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
-| [ "{" "wf" constr(r) ident(id) "}" ] -> [ Wf(r,id) ]
+| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
+| [ "{" "mes" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
 END
 
 
@@ -124,12 +125,14 @@ VERNAC ARGUMENT EXTEND rec_definition2
                   Pp.str "the recursive argument needs to be specified");
 	   in
 	   let check_exists_args an =
-	     let id = match an with Struct id -> id | Wf(_,id) -> id in 
-	     (try ignore(Util.list_index (Name id) names - 1); annot
-	      with Not_found ->  Util.user_err_loc
-                (Util.dummy_loc,"GenFixpoint",
-                 Pp.str "No argument named " ++ Nameops.pr_id id)
-	     )
+	     try 
+	       let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in 
+	       (try ignore(Util.list_index (Name id) names - 1); annot
+		with Not_found ->  Util.user_err_loc
+                  (Util.dummy_loc,"GenFixpoint",
+                   Pp.str "No argument named " ++ Nameops.pr_id id)
+	       )
+	     with Failure "check_exists_args" ->  check_one_name ();annot
 	   in
           let ni =
             match annot with
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index a416e3882..157c822cd 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -189,12 +189,14 @@ let well_founded_induction = lazy(coq_constant "well_founded_induction")
 let well_founded = lazy (coq_constant "well_founded")
 let acc_rel = lazy (coq_constant "Acc")
 let acc_inv_id = lazy (coq_constant "Acc_inv")
-
+let well_founded_ltof = lazy (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
 let iter_ref = lazy(find_reference ["Recdef"] "iter")
 let max_ref = lazy(find_reference ["Recdef"] "max")
 let iter = lazy(constr_of_reference (Lazy.force iter_ref))
 let max_constr = lazy(constr_of_reference (Lazy.force max_ref))
 
+let ltof_ref = lazy (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") 
+
 (* These are specific to experiments in nat with lt as well_founded_relation,
    but this should be made more general. *)
 let nat = lazy(coq_constant "nat")
@@ -246,16 +248,19 @@ let simpl_iter () =
         rConst = [ EvalConstRef (const_of_ref (Lazy.force iter_ref))]})
     onConcl
     
-let tclUSER l g = 
+let tclUSER is_mes l g = 
   let b,l = 
     match l with 
 	None -> true,[]
       | Some l -> false,l
   in
-  tclTHEN 
-    (h_clear b l)
-    (*     (tclIDTAC_MESSAGE (str "USER"++fnl()))  *)
-    tclIDTAC
+  tclTHENSEQ 
+    [
+      (h_clear b l);
+      if is_mes 
+      then unfold_in_concl [([], evaluable_of_global_reference (Lazy.force ltof_ref))]
+      else tclIDTAC
+    ]
     g
     
     
@@ -395,7 +400,7 @@ let retrieve_acc_var g =
        with _ -> failwith "")
     hyps 
 
-let rec introduce_all_values acc_inv func context_fn
+let rec introduce_all_values is_mes acc_inv func context_fn
     eqs  hrec args values specs =
     (match args with
     [] -> 
@@ -410,7 +415,7 @@ let rec introduce_all_values acc_inv func context_fn
 	let rec_res = next_ident_away rec_res_id ids in
         let ids = rec_res::ids in
 	let hspec = next_ident_away hspec_id ids in
-	let tac = introduce_all_values acc_inv func context_fn eqs 
+	let tac = introduce_all_values is_mes acc_inv func context_fn eqs 
 	  hrec args
 	  (rec_res::values)(hspec::specs) in
 	(tclTHENS
@@ -422,7 +427,7 @@ let rec introduce_all_values acc_inv func context_fn
 		 [ h_assumption
 		 ;
 		   (fun g ->  
-		      tclUSER (Some (hrec::hspec::(retrieve_acc_var g)@specs)) g
+		      tclUSER is_mes (Some (hrec::hspec::(retrieve_acc_var g)@specs)) g
 		   )
 		 ]
 	    )
@@ -431,12 +436,12 @@ let rec introduce_all_values acc_inv func context_fn
     )
  
 	   
-let rec_leaf acc_inv hrec (func:global_reference) eqs expr =
+let rec_leaf is_mes acc_inv hrec (func:global_reference) eqs expr =
   match find_call_occs (mkVar (get_f (constr_of_reference func))) expr with
   | context_fn, args ->
-      introduce_all_values acc_inv func context_fn eqs  hrec args  [] []
+      introduce_all_values is_mes acc_inv func context_fn eqs  hrec args  [] []
 
-let rec proveterminate acc_inv (hrec:identifier)  (* (proofs:constr list) *)
+let rec proveterminate is_mes acc_inv (hrec:identifier)  
   (f_constr:constr) (func:global_reference) (eqs:constr list) (expr:constr)  =
 try
 (*  let _ = msgnl (str "entering proveterminate") in *)
@@ -452,7 +457,7 @@ try
 			   v
 			)
    	         (List.map (mk_intros_and_continue true
-                              (proveterminate acc_inv hrec f_constr func)
+                              (proveterminate is_mes acc_inv hrec f_constr func)
                               eqs) 
 	            (Array.to_list l))
 	   | _, _::_ -> 
@@ -460,7 +465,7 @@ try
 		 match find_call_occs  f_constr expr with
 	     	     _,[] -> base_leaf func eqs expr
 		   | _, _:: _ -> 
-		       rec_leaf acc_inv hrec  func eqs expr
+		       rec_leaf is_mes acc_inv hrec  func eqs expr
 	       )
 	)
     | _ ->  (match find_call_occs  f_constr expr with
@@ -469,7 +474,7 @@ try
 		    base_leaf func eqs expr
 		   with e -> (msgerrnl (str "failure in base case");raise e ))
 	       | _, _::_ -> 
-		   rec_leaf acc_inv hrec  func eqs expr) in
+		   rec_leaf is_mes acc_inv hrec  func eqs expr) in
   (*  let _ = msgnl(str "exiting proveterminate") in *)
   v
 with e -> 
@@ -507,7 +512,14 @@ let hyp_terminates func =
   compose_prod rev_args value
 	     
 
-let start input_type ids args_id relation rec_arg_num rec_arg_id tac : tactic = 
+
+let tclUSER_if_not_mes is_mes = 
+  if is_mes 
+  then 
+    tclCOMPLETE (h_apply (Lazy.force well_founded_ltof,Rawterm.NoBindings))
+  else tclUSER is_mes None
+
+let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac : tactic = 
   begin 
     fun g -> 
       let nargs = List.length args_id in
@@ -559,7 +571,7 @@ let start input_type ids args_id relation rec_arg_num rec_arg_id tac : tactic =
 	       )
 	       [ 
 		 (* interactive proof of the well_foundness of the relation *) 
-		 tclUSER None;
+		 tclUSER_if_not_mes is_mes;
 		 (* well_foundness -> Acc for any element *)
 		 observe_tac 
 		   "apply wf_thm" 
@@ -596,7 +608,7 @@ let rec instantiate_lambda t l =
 ;;
 
 
-let whole_start func input_type relation rec_arg_num  : tactic = 
+let whole_start is_mes func input_type relation rec_arg_num  : tactic = 
   begin 
     fun g -> 
       let ids = ids_of_named_context (pf_hyps g) in
@@ -623,6 +635,7 @@ let whole_start func input_type relation rec_arg_num  : tactic =
       let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
       let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in 
       start 
+	is_mes
 	input_type
 	ids
 	n_ids
@@ -631,6 +644,7 @@ let whole_start func input_type relation rec_arg_num  : tactic =
 	rec_arg_id
 	(fun hrec acc_inv g ->  
            (proveterminate 
+	      is_mes
 	      acc_inv 
 	      hrec
 	      (mkVar f_id)
@@ -645,13 +659,13 @@ let whole_start func input_type relation rec_arg_num  : tactic =
 
 
 
-let com_terminate fonctional_ref input_type relation rec_arg_num
+let com_terminate is_mes fonctional_ref input_type relation rec_arg_num
     thm_name hook =
   let (evmap, env) = Command.get_current_context() in
   start_proof thm_name
     (Global, Proof Lemma) (Environ.named_context_val env)
     (hyp_terminates fonctional_ref) hook;
-  by (whole_start fonctional_ref
+  by (whole_start is_mes fonctional_ref
 	input_type relation rec_arg_num )
     
 
@@ -899,7 +913,7 @@ let (com_eqn : identifier ->
      Command.save_named true);;
 
 
-let recursive_definition f type_of_f r  rec_arg_num eq =
+let recursive_definition is_mes f type_of_f r  rec_arg_num eq =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_rel (Name f,None,function_type) (Global.env()) in
   let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in 
@@ -934,7 +948,7 @@ let recursive_definition f type_of_f r  rec_arg_num eq =
 (*     let _ = message "start second proof" in *)
     com_eqn equation_id functional_ref f_ref term_ref eq
   in
-  com_terminate functional_ref rec_arg_type relation  rec_arg_num term_id  hook 
+  com_terminate is_mes functional_ref rec_arg_type relation  rec_arg_num term_id  hook 
 ;;
 
 VERNAC COMMAND EXTEND RecursiveDefinition
@@ -946,8 +960,8 @@ VERNAC COMMAND EXTEND RecursiveDefinition
 	| None -> 1
 	| Some n -> n 
     in
-    recursive_definition f type_of_f r rec_arg_num eq ]
+    recursive_definition false f type_of_f r rec_arg_num eq ]
 | [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
      "[" ne_constr_list(proof) "]" constr(eq) ] ->
-  [ ignore(proof);ignore(wf);recursive_definition f type_of_f r 1 eq ]
+  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq ]
 END