Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'ClearBody H' et 'Assert H := c'

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

12 files changed, 111 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 0f4b60eae..4577ae503 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,13 @@
+Changes from ??? to V7.1
+========================
+
+Tactics
+
+- New tactic "ClearBody H" to clear the body of definitions in local context
+- New tactic "Assert H := c" for forward reasoning
+
+
+----------------------------------------------------------------------------
 Changes from V6.3.1 and V7.0 to V7.1
 ====================================
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ea227c112..21e151c11 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -318,6 +318,11 @@ GEXTEND Gram
             | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c
             | _ -> assert false in
 	  <:ast< (TrueCut $t $id) >>
+      | IDENT "Assert"; c = constrarg; ":="; t = constrarg ->
+          let id = match c with 
+            | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c
+            | _ -> assert false in
+	  <:ast< (Forward $t $id) >>
       | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
       | IDENT "Specialize"; lcb = constrarg_binding_list ->
@@ -331,6 +336,8 @@ GEXTEND Gram
       | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
       | IDENT "Clear"; l = ne_idmetahyp_list -> 
                 <:ast< (Clear (CLAUSE ($LIST $l))) >>
+      | IDENT "ClearBody"; l = ne_idmetahyp_list -> 
+                <:ast< (ClearBody (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
                 <:ast< (MoveDep $id1 $id2) >>
 (*To do: put Abstract in Refiner*)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 40dce2349..38f2d1d0f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -246,6 +246,19 @@ let apply_to_hyp sign id f =
   in
   if (not !check) || !found then sign' else error "No such assumption"
 
+let apply_to_hyp2 env id f =
+  let found = ref false in
+  let env' =
+    fold_named_context_both_sides
+      (fun env (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f env d tail
+	 end else 
+	   push_named_decl d env)
+      (named_context env) (reset_context env)
+  in
+  if (not !check) || !found then env' else error "No such assumption"
+
 let global_vars_set_of_var = function
   | (_,None,t) -> global_vars_set (body_of_type t)
   | (_,Some c,t) ->
@@ -318,6 +331,36 @@ let remove_hyp env id =
        if !check then check_forward_dependencies id tail;
        env)
 
+let recheck_typability (what,id) env sigma t =
+  try let _ = type_of env sigma t in ()
+  with _ ->
+    let s = match what with
+      | None -> "the conclusion"
+      | Some id -> "hypothesis "^(string_of_id id) in
+    error
+      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
+  
+let remove_hyp_body env sigma id =
+  apply_to_hyp2 env id
+    (fun env (_,c,t) tail ->
+       match c with
+         | None -> error ((string_of_id id)^" is not a local definition")
+         | Some c ->
+             let env' = push_named_decl (id,None,t) env in
+             if !check then 
+               ignore
+                 (Sign.fold_named_context 
+                    (fun (id',c,t as d) env'' ->
+                       (match c with
+                          | None -> 
+                              recheck_typability (Some id',id) env'' sigma t
+                          | Some b ->
+                              let b' = mkCast (b,t) in
+                              recheck_typability (Some id',id) env'' sigma b');
+                       push_named_decl d env'')
+                    tail env');
+             env')
+
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
@@ -494,6 +537,16 @@ let prim_refiner r sigma goal =
      	let sg = mk_goal info sign' cl in
      	[sg]
 
+    | { name = ThinBody; hypspecs = ids } ->
+	let clear_aux env id =
+          let env' = remove_hyp_body env sigma id in
+          if !check then recheck_typability (None,id) env' sigma cl;
+          env'
+	in
+	let sign' = named_context (List.fold_left clear_aux env ids) in
+     	let sg = mk_goal info sign' cl in
+     	[sg]
+
     | { name = Move withdep; hypspecs = ids } ->
 	let (hfrom,hto) =
 	  match ids with [h1;h2] ->(h1,h2)| _ -> anomaly "prim_refiner:MOVE" in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2820f05f5..f427ec1f5 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -45,6 +45,7 @@ type prim_rule_name =
   | Convert_defbody
   | Convert_deftype
   | Thin
+  | ThinBody
   | Move of bool
 
 type prim_rule = {
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 16190b8ea..eb31544cb 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -48,6 +48,7 @@ type prim_rule_name =
   | Convert_defbody
   | Convert_deftype
   | Thin
+  | ThinBody
   | Move of bool
 
 type prim_rule = {
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d2f12d352..5c1a2c876 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -254,6 +254,10 @@ let thin ids gl =
   refiner (Prim { name = Thin; hypspecs = ids;
                   terms = []; newids = []; params = []}) gl
 
+let thin_body ids gl = 
+  refiner (Prim { name = ThinBody; hypspecs = ids;
+                  terms = []; newids = []; params = []}) gl
+
 let move_hyp with_dep id1 id2 gl = 
   refiner (Prim { name = Move with_dep;
                   hypspecs = [id1;id2]; terms = [];
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 930588fcb..640e29439 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -167,6 +167,7 @@ val convert_hyp     : identifier -> types -> tactic
 val convert_deftype : identifier -> types -> tactic
 val convert_defbody : identifier -> constr -> tactic
 val thin            : identifier list -> tactic
+val thin_body       : identifier list -> tactic
 val move_hyp        : bool -> identifier -> identifier -> tactic
 val mutual_fix      : identifier list -> int list -> constr list -> tactic
 val mutual_cofix    : identifier list -> constr list -> tactic
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 9a9a9ee67..f4718f2f2 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -207,6 +207,8 @@ Syntax tactic
 
   | clear [<<(Clear (CLAUSE ($LIST $l)))>>] ->
           [ [<hov 3> "Clear " (LISTSPC ($LIST $l))] ]
+  | clear_body [<<(ClearBody (CLAUSE ($LIST $l)))>>] ->
+          [ [<hov 3> "ClearBody " (LISTSPC ($LIST $l))] ]
 
   | move [<<(MoveDep $id1 $id2)>>] ->
           [ "Move " $id1 " after " $id2 ]
@@ -255,6 +257,10 @@ Syntax tactic
   | absurd [<<(Absurd $C)>>] -> ["Absurd " $C]
 
   | cut [<<(Cut $C)>>] -> ["Cut " $C]
+  | truecutid [<<(TrueCut $C $id)>>] -> ["Assert " $id " : " $C]
+  | truecut [<<(TrueCut $C)>>] -> ["Assert " $C]
+  | forward [<<(Forward $C $id)>>] -> ["Assert " $id " := " $C]
+
   | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> 
 	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))]
   | lettac_nil [<<(LetTac $id $c (LETPATTERNS))>>] -> 
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index 57bb5d975..b44054660 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -30,6 +30,7 @@ let v_left          = hide_tactic "Left"          dyn_left
 let v_right         = hide_tactic "Right"         dyn_right
 let v_split         = hide_tactic "Split"         dyn_split
 let v_clear         = hide_tactic "Clear"         dyn_clear
+let v_clear_body    = hide_tactic "ClearBody"     dyn_clear_body
 let v_move          = hide_tactic "Move"          dyn_move
 let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
 let v_apply         = hide_tactic "Apply"         dyn_apply
@@ -37,6 +38,7 @@ 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_forward       = hide_tactic "Forward"       dyn_forward
 let v_generalize    = hide_tactic "Generalize"    dyn_generalize
 let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
 let v_specialize    = hide_tactic "Specialize"    dyn_new_hyp
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 70266c09f..cb5cf8385 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -31,6 +31,7 @@ val v_left          : tactic_arg list -> tactic
 val v_right         : tactic_arg list -> tactic
 val v_split         : tactic_arg list -> tactic
 val v_clear         : tactic_arg list -> tactic
+val v_clear_body    : tactic_arg list -> tactic
 val v_move          : tactic_arg list -> tactic
 val v_move_dep      : tactic_arg list -> tactic
 val v_apply         : tactic_arg list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11c37aa3b..441cb2aad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -103,6 +103,7 @@ let refine          = Tacmach.refine
 let convert_concl   = Tacmach.convert_concl
 let convert_hyp     = Tacmach.convert_hyp
 let thin            = Tacmach.thin 
+let thin_body       = Tacmach.thin_body 
 let move_hyp        = Tacmach.move_hyp 
 
 let mutual_fix   = Tacmach.mutual_fix
@@ -769,17 +770,19 @@ let letin_tac with_eq name c occs gl =
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
   let args = instance_from_named_context depdecls in
-  let newcl =
+  let newcl = mkNamedLetIn id c t tmpcl in
+(*
     if with_eq then
-      mkNamedLetIn id c t tmpcl
     else (* To fix : add c to args, or use LetIn and clear the body *)
-      mkNamedProd id t tmpcl
+      mkNamed id t tmpcl
   in
+*)
   let lastlhyp = if marks=[] then None else snd (List.hd marks) in
   tclTHENLIST
     [ apply_type newcl args;
       thin (List.map (fun (id,_,_) -> id) depdecls);
       intro_gen (IntroMustBe id) lastlhyp false;
+      if with_eq then tclIDTAC else thin_body [id];
       intros_move marks ] gl
 
 let check_hypotheses_occurrences_list env occl =
@@ -802,6 +805,13 @@ let dyn_lettac args gl = match args with
       letin_tac true (Name id) c (o,l) gl
   | l -> bad_tactic_args "letin" l
 
+let dyn_forward args gl = match args with
+  | [Command com; Identifier id] ->
+      letin_tac false (Name id) (pf_interp_constr gl com) (None,[]) gl
+  | [Constr c; Identifier id]    ->
+      letin_tac false (Name id) c (None,[]) gl
+  | l -> bad_tactic_args "forward" l
+
 (********************************************************************)
 (*               Exact tactics                                      *)
 (********************************************************************)
@@ -864,7 +874,14 @@ let dyn_clear = function
   | [Clause ids] ->
       let out = function InHyp id -> id | _ -> assert false in
       clear (List.map out ids)
-  | _ -> assert false
+  | l -> bad_tactic_args "clear" l
+
+let clear_body = thin_body
+let dyn_clear_body = function
+  | [Clause ids] ->
+      let out = function InHyp id -> id | _ -> assert false in
+      clear_body (List.map out ids)
+  | l -> bad_tactic_args "clear_body" l
 
 (* Clears a list of identifiers clauses form the context *)
 (*
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a5244b7f8..8751fcb5c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -151,6 +151,9 @@ val clear         : identifier list -> tactic
 val clear_one     : identifier -> tactic
 val dyn_clear     : tactic_arg list -> tactic
 
+val clear_body    : identifier list -> tactic
+val dyn_clear_body : tactic_arg list -> tactic
+
 val clear_clauses : identifier list -> tactic
 val clear_clause  : identifier -> tactic
 
@@ -264,6 +267,7 @@ 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 dyn_forward                 : tactic_arg list -> tactic
 
 val generalize                  : constr list -> tactic
 val dyn_generalize              : tactic_arg list -> tactic