Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut

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

11 files changed, 57 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 818ee0b3ff..c76c20a3d3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,9 @@ Modifications depuis la V7.0
 - Correction bugs Cases en cas de prédicat dépendant
 - Le flag Delta n'inclut plus Zeta et Evar, nouveaux flags Zeta et Evar inclus
   dans Compute (à documenter)
+- Nouvelle tactique TrueCut qui fait la coupure du calcul des séquents
+  (et dans le sens attendu)
+- Amélioration de l'efficacité de l'ancien Cut
 
 Différences oubliées dans la V7.0beta :
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 647a4179e4..08deeb8d10 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -318,6 +318,7 @@ GEXTEND Gram
       | IDENT "Decompose"; "["; l = ne_qualidarg_list; "]"; c = constrarg ->
           <:ast< (DecomposeThese $c ($LIST $l)) >>
       | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
+      | IDENT "TrueCut"; c = constrarg -> <:ast< (TrueCut $c) >>
       | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
       | IDENT "Specialize"; lcb = constrarg_binding_list ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a5fe2d5962..36c928094d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -379,6 +379,12 @@ let prim_refiner r sigma goal =
 	       if !check then error "Introduction needs a product"
 	       else anomaly "Intro_replacing: expects a product")
 	
+    | { name = Cut b; terms = [t]; newids = [id] } ->
+        if occur_meta t then error_use_instantiate();
+        let sg1 = mk_goal info sign t in
+        let sg2 = mk_goal info (add_named_decl (id,None,t) sign) cl in
+        if b then [sg1;sg2] else [sg2;sg1]  
+
     | { name = Fix; hypspecs = []; terms = []; 
 	newids = [f]; params = [Num(_,n)] } ->
      	let rec check_ind k cl = 
@@ -533,7 +539,11 @@ let prim_extractor subfun vl pft =
 	       let cty = subst_vars vl ty in
 	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
-	
+
+    | {ref=Some(Prim{name=Cut b;terms=[t];newids=[id]},[spf1;spf2]) } ->
+        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)
+
     | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> 
 	let cty = subst_vars vl cl in 
 	let na = Name f in 
@@ -604,6 +614,12 @@ let pr_prim_rule = function
   | {name=Intro_replacing;newids=[id]} -> 
       [< 'sTR"intro replacing " ; pr_id id >]
 	
+  | {name=Cut b;terms=[t];newids=[id]} ->
+      if b then
+        [< 'sTR"TrueCut "; prterm t >]
+      else
+        [< 'sTR"Cut "; prterm t; 'sTR ";[Intro "; pr_id id; 'sTR "|Idtac]" >]
+	
   | {name=Fix;newids=[f];params=[Num(_,n)]} -> 
       [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>]
       
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 363dd09645..2820f05f5e 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -36,6 +36,7 @@ type prim_rule_name =
   | Intro
   | Intro_after
   | Intro_replacing
+  | Cut of bool
   | Fix
   | Cofix
   | Refine 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5d415d5a08..16190b8eae 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -39,6 +39,7 @@ type prim_rule_name =
   | Intro
   | Intro_after
   | Intro_replacing
+  | Cut of bool
   | Fix
   | Cofix
   | Refine 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8768dfd315..69697c809f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -223,6 +223,14 @@ let intro_replacing whereid pf =
   refiner (Prim { name = Intro_replacing; newids = [];
                   hypspecs = [whereid]; terms = []; params = [] }) pf
 
+let internal_cut id t pf = 
+  refiner (Prim { name = Cut true; newids = [id];
+                  hypspecs = []; terms = [t]; params = [] }) pf
+
+let internal_cut_rev id t pf = 
+  refiner (Prim { name = Cut false; newids = [id];
+                  hypspecs = []; terms = [t]; params = [] }) pf
+
 let refine c pf = 
   refiner (Prim { name = Refine; terms = [c];
 		  hypspecs = []; newids = []; params = [] }) pf
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e7742f2ecd..721f847243 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -161,8 +161,10 @@ val context       : ctxtty -> tactic
 val refiner         : rule -> tactic
 val introduction    : identifier -> tactic
 val intro_replacing : identifier -> tactic
+val internal_cut    : identifier -> types -> tactic
+val internal_cut_rev : identifier -> types -> tactic
 val refine          : constr -> tactic
-val convert_concl   : constr -> tactic
+val convert_concl   : types -> tactic
 val convert_hyp     : identifier -> types -> tactic
 val convert_deftype : identifier -> types -> tactic
 val convert_defbody : identifier -> constr -> tactic
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index 384341e663..57bb5d9753 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -35,6 +35,7 @@ let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
 let v_apply         = hide_tactic "Apply"         dyn_apply
 let v_cutAndResolve = hide_tactic "CutAndApply"   dyn_cut_and_apply
 let v_cut           = hide_tactic "Cut"           dyn_cut
+let v_truecut       = hide_tactic "TrueCut"       dyn_true_cut
 let v_lettac        = hide_tactic "LetTac"        dyn_lettac
 let v_generalize    = hide_tactic "Generalize"    dyn_generalize
 let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 6c73aa4719..8d8a664dd7 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -36,6 +36,7 @@ val v_move_dep      : tactic_arg list -> tactic
 val v_apply         : tactic_arg list -> tactic
 val v_cutAndResolve : tactic_arg list -> tactic
 val v_cut           : tactic_arg list -> tactic
+val v_truecut       : tactic_arg list -> tactic
 val v_lettac        : tactic_arg list -> tactic
 val v_generalize    : tactic_arg list -> tactic
 val v_generalize_dep : tactic_arg list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 72cd0efbd3..bfe2788d22 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -97,6 +97,8 @@ let bad_tactic_args s l =
 
 let introduction    = Tacmach.introduction 
 let intro_replacing = Tacmach.intro_replacing 
+let internal_cut    = Tacmach.internal_cut
+let internal_cut_rev = Tacmach.internal_cut_rev
 let refine          = Tacmach.refine
 let convert_concl   = Tacmach.convert_concl
 let convert_hyp     = Tacmach.convert_hyp
@@ -586,11 +588,27 @@ let dyn_cut_and_apply = function
 (*     Cut tactics        *)
 (**************************)
 
+let true_cut c gl =
+  match kind_of_term (hnf_type_of gl c) with
+    | IsSort _ ->
+        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+        internal_cut id c gl
+    | _  -> error "Not a proposition or a type"
+
+let dyn_true_cut = function
+  | [Command com] -> tactic_com_sort true_cut com
+  | [Constr  c]   -> true_cut c
+  | l             -> bad_tactic_args "true_cut" l
+
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
     | IsSort _ ->
-	apply_type (mkProd (Anonymous, c, pf_concl gl)) 
-          [mkMeta (new_meta())] gl
+        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+        let t = mkProd (Anonymous, c, pf_concl gl) in
+        tclTHENS
+          (internal_cut_rev id c)
+          [tclTHEN (apply_type t [mkVar id]) (thin [id]);
+           tclIDTAC] gl
     | _  -> error "Not a proposition or a type"
 
 let dyn_cut = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c31923ce7b..a5244b7f85 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -262,6 +262,7 @@ val cut_intro                   : constr -> tactic
 val cut_replacing               : identifier -> constr -> tactic
 val cut_in_parallel             : constr list -> tactic
 val dyn_cut                     : tactic_arg list -> tactic
+val dyn_true_cut                : tactic_arg list -> tactic
 val dyn_lettac                  : tactic_arg list -> tactic
 
 val generalize                  : constr list -> tactic