Mutually structurally recursive defs and rec using measures added.

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

7 files changed, 192 insertions, 70 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index bbf722dbb..ded069bf1 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -20,3 +20,27 @@ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
 End FixPoint.
 
 End Well_founded.
+
+Require Import Wf_nat.
+Require Import Lt.
+
+Section Well_founded_measure.
+Variable A : Set.
+Variable f : A -> nat.
+Definition R := fun x y => f x < f y.
+
+Section FixPoint.
+
+Variable P : A -> Set.
+
+Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
+ 
+Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
+   F_sub x (fun y: { y : A | f y < f x}  => Fix_measure_F_sub (proj1_sig y) 
+   (Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
+
+Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
+
+End FixPoint.
+
+End Well_founded_measure.
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 816f03ce4..c738d7a64 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -117,7 +117,8 @@ let interp_context sigma env params =
 
 let list_chop_hd i l = match list_chop i l with
   | (l1,x::l2) -> (l1,x,l2)
-  | _ -> assert false
+  | (x :: [], l2) -> ([], x, [])
+  | _ -> assert(false)
 
 let collect_non_rec env = 
   let rec searchrec lnonrec lnamerec ldefrec larrec nrec = 
@@ -183,11 +184,10 @@ let rec gen_rels = function
     0 -> []
   | n -> mkRel n :: gen_rels (pred n)
 
-let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
+let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
-  let n = out_some n in 
   let pr c = my_print_constr env c in
   let prr = Printer.pr_rel_context env in
   let pr_rel env = Printer.pr_rel_context env in
@@ -202,12 +202,24 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
   let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
   let before_length, after_length = List.length before, List.length after in
   let argid = match argname with Name n -> n | _ -> assert(false) in
-  let liftafter = lift_binders 1 after_length after in
+  let _liftafter = lift_binders 1 after_length after in
   let envwf = push_rel_context before env in
-  let wf_rel = interp_constr isevars envwf r in
-  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+  let wf_rel, measure_fn = 
+    let rconstr = interp_constr isevars envwf r in
+    if measure then
+      let lt_rel = constr_of_global (Lazy.force lt_ref) in
+      let name s = Name (id_of_string s) in
+	mkLambda (name "x", argtyp,
+		  mkLambda (name "y", argtyp,
+			    mkApp (lt_rel,
+				   [| mkApp (rconstr, [| mkRel 2 |]) ;
+				      mkApp (rconstr, [| mkRel 1 |]) |]))),
+	Some rconstr
+    else rconstr, None
+  in
+  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
+  in
   let argid' = id_of_string (string_of_id argid ^ "'") in
-  let full_length = before_length + 1 + after_length in
   let wfarg len = (Name argid', None, 
 		   mkSubset (Name argid') argtyp 
 		     (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
@@ -229,7 +241,6 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
   (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
   let intern_arity = substnl [projection] after_length top_arity in 
   (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
-  let intern_arity_prod = it_mkProd_or_LetIn intern_arity intern_bl in
   let intern_before_env = push_rel_context before env in
   let intern_fun_bl = after @ [wfarg 1]  in
   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
@@ -253,19 +264,25 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
 		   str "Intern body " ++ pr intern_body_lam)
       with _ -> ()
   in
-  let impl = 
+  let _impl = 
     if Impargs.is_implicit_args()
     then Impargs.compute_implicits top_env top_arity
     else [] 
   in
   let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
   let fix_def =
-    mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
-	  [| argtyp ;
-	     wf_rel ;
-	     make_existential dummy_loc intern_before_env isevars wf_proof ;
-	     prop ;
-	     intern_body_lam |])
+    match measure_fn with
+	None ->
+	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
+		 [| argtyp ;
+		    wf_rel ;
+		    make_existential dummy_loc intern_before_env isevars wf_proof ;
+		    prop ;
+		    intern_body_lam |])
+      | Some f ->
+	  mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
+		 [| argtyp ; f ; prop ;
+		    intern_body_lam |])
   in
   let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
   let def = it_mkLambda_or_LetIn def_appl binders_rel in
@@ -284,55 +301,45 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
   let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in 	
   let evars_typ = out_some evars_typ in
-  let evars_sum =
-    if evars = [] then None
-    else (
-      (try trace (str "Building evars sum for : ");
-	 List.iter
-	   (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
-	   evars;
-       with _ -> ());
-      let sum = Subtac_utils.build_dependent_sum evars in
-	(try trace (str "Evars sum: " ++ my_print_constr env (snd sum));
-	   trace (str "Evars type: " ++ my_print_constr env evars_typ);
-	 with _ -> ());
-	Some sum)
-  in
-    match evars_sum with
-      | Some (sum_tac, sumg) -> 
-	  let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
-	    Command.start_proof proofid goal_proof_kind sumg
-	      (fun strength gr -> 
-		 debug 2 (str "Proof finished");
-		 let def = constr_of_global gr in
-		 let args = Subtac_utils.destruct_ex def sumg in
-		 let _, newdef = decompose_lam_n (List.length args) evars_def in
-		 let constr = Term.substl (List.rev args) newdef in
-		 debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
-		 let ce = 
-		   { const_entry_body = constr;
-		     const_entry_type = Some fullctyp;
-		     const_entry_opaque = false;
-		     const_entry_boxed = boxed} 
-		 in
-		 let constant = Declare.declare_constant 
-		   recname (DefinitionEntry ce,IsDefinition Definition)
-		 in
-		 definition_message recname);
-	    trace (str "Started existentials proof");
-	    Pfedit.by sum_tac;
-	    trace (str "Applied sum tac")
-      | None -> ()
+  (try trace (str "Building evars sum for : ");
+     List.iter
+       (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+       evars;
+   with _ -> ());
+  let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in
+  (try trace (str "Evars sum: " ++ my_print_constr env sumg);
+     trace (str "Evars type: " ++ my_print_constr env evars_typ);
+   with _ -> ());
+  let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
+    Command.start_proof proofid goal_proof_kind sumg
+      (fun strength gr -> 
+	 debug 2 (str "Proof finished");
+	 let def = constr_of_global gr in
+	 let args = Subtac_utils.destruct_ex def sumg in
+	 let _, newdef = decompose_lam_n (List.length args) evars_def in
+	 let constr = Term.substl (List.rev args) newdef in
+	   debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
+	   let ce = 
+	     { const_entry_body = constr;
+	       const_entry_type = Some fullctyp;
+	       const_entry_opaque = false;
+	       const_entry_boxed = boxed} 
+	   in
+	   let _constant = Declare.declare_constant 
+			    recname (DefinitionEntry ce,IsDefinition Definition)
+	   in
+	     definition_message recname);
+    trace (str "Started existentials proof");
+    Pfedit.by sum_tac;
+    trace (str "Applied sum tac")  
 
-    
-let build_mutrec l boxed =
+let build_mutrec l boxed = 
   let sigma = Evd.empty
   and env0 = Global.env()
-  in ()
-(*
+  in 
   let lnameargsardef =
     (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
-    lnameargsardef
+    l
   in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
@@ -384,7 +391,6 @@ let build_mutrec l boxed =
 
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env0 lrecnames recdef arityl nv in
-  let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
   let declare arrec defrec =
     let recvec = 
       Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
@@ -394,7 +400,7 @@ let build_mutrec l boxed =
 		  my_print_constr env0 (recvec.(i)));
        with _ -> ());
       let ce = 
-	{ const_entry_body = mkFix ((nvrec',i),recdecls); 
+	{ const_entry_body = mkFix ((nvrec,i),recdecls); 
           const_entry_type = Some arrec.(i);
           const_entry_opaque = false;
           const_entry_boxed = boxed} in
@@ -485,6 +491,11 @@ let build_mutrec l boxed =
 		  match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
       defs
   in
+    match real_evars with
+	[] -> declare (List.rev_map (fun (id, c, _) ->
+				   snd (decompose_lam_n recdefs c)) defs)
+      | l ->
+
     Subtac_utils.and_tac real_evars
       (fun f _ gr ->
 	 let _ = trace (str "Got a proof of: " ++ pr_global gr ++
@@ -531,19 +542,24 @@ let build_mutrec l boxed =
 	     match cer with
 		 Environ.NoBody -> trace (str "Constant has no body")
 	       | Environ.Opaque -> trace (str "Constant is opaque")
-      )*)
+      )
+
+let out_n = function
+    Some n -> n
+  | None -> 0
 
 let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
   match lnameargsardef with
     | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> 
-	(*let body = Subtac_utils.rewrite_cases env body in*)
-	  build_wellfounded (id, n, bl, typ, body) r no boxed
+	build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
+    | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> 
+	build_wellfounded (id, out_n n, bl, typ, body) r true no boxed
     | l -> 
 	let lnameargsardef = 
 	  List.map (fun ((id, (n, ro), bl, typ, body), no) ->
 		 match ro with
-		     CStructRec -> (id, n, bl, typ, body), no
-		   | CWfRec _ -> 
+		     CStructRec -> (id, out_n n, bl, typ, body), no
+		   | CWfRec _ | CMeasureRec _ -> 
 		       errorlabstrm "Subtac_command.build_recursive"
 			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
 	    lnameargsardef
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 6089f3a64..f8ab27705 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -27,6 +27,8 @@ let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
 let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
+let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
+let lt_ref = make_ref ["Init";"Peano"] "lt"
 let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
 
 let make_ref s = Qualid (dummy_loc, qualid_of_string s)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a26793b67..4a7e81772 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -22,6 +22,8 @@ val well_founded_ref : global_reference lazy_t
 val acc_ref : global_reference lazy_t
 val acc_inv_ref : global_reference lazy_t
 val fix_sub_ref : global_reference lazy_t
+val fix_measure_sub_ref : global_reference lazy_t
+val lt_ref : global_reference lazy_t
 val lt_wf_ref : global_reference lazy_t
 val sig_ref : reference
 val proj1_sig_ref : reference
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354c..0b40ef82a 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,7 +1,13 @@
-Fixpoint f (a : nat) : nat := match a with 0 => 0
-| S a' => g a a'
+Program Fixpoint f (a : nat) : nat := 
+  match a with
+  | 0 => 0
+  | S a' => g a a'
   end
 with g (a b : nat) { struct b } : nat := 
-  match b with 0 => 0
+  match b with
+  | 0 => 0
   | S b' => f b'
-  end.
\ No newline at end of file
+  end.
+
+Check f.
+Check g.
\ No newline at end of file
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
new file mode 100644
index 000000000..4764037d9
--- /dev/null
+++ b/contrib/subtac/test/measure.v
@@ -0,0 +1,24 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Fixpoint size (a : nat) : nat :=
+  match a with
+  0 => 1
+  | S n => S (size n)
+  end.
+
+Program Fixpoint test_measure (a : nat) {measure a size}  : nat :=
+  match a with
+  | S (S n) => S (test_measure n)
+  | x => x
+  end.
+subst.
+unfold n0.
+auto with arith.
+Qed.
+
+Check test_measure.
+Print test_measure.
\ No newline at end of file
diff --git a/contrib/subtac/test/wf.v b/contrib/subtac/test/wf.v
new file mode 100644
index 000000000..49fec2b80
--- /dev/null
+++ b/contrib/subtac/test/wf.v
@@ -0,0 +1,48 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Ltac one_simpl_hyp :=
+ match goal with
+ | [H : (`exist _ _ _) = _ |- _] => simpl in H
+ | [H : _ = (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) < _ |- _] => simpl in H
+ | [H : _ < (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) <= _ |- _] => simpl in H
+ | [H : _ <= (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) > _ |- _] => simpl in H
+ | [H : _ > (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) >= _ |- _] => simpl in H
+ | [H : _ >= (`exist _ _ _) |- _] => simpl in H
+ end.
+
+Ltac one_simpl_subtac :=
+  destruct_exists ;
+  repeat one_simpl_hyp ; simpl.
+
+Ltac simpl_subtac :=  do 3 one_simpl_subtac ; simpl.
+
+Require Import Omega.
+Require Import Wf_nat.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
+  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
+  (S q' & r)
+  else (O & a).
+destruct b ; simpl_subtac.
+omega.
+simpl_subtac.
+assert(x0 * S q' = x0 + x0 * q').
+rewrite <- mult_n_Sm.
+omega.
+rewrite H2 ; omega.
+simpl_subtac.
+split ; auto with arith.
+omega.
+apply lt_wf.
+Defined.
+
+Check euclid_evars_proof.
\ No newline at end of file