new intro:

- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 97dbb04868ebf2c76ebdbd55b491f6c5403aed8e..ae4dc23f76b4e477f2276d268b96670bd5decdc2 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -65,6 +65,7 @@ type ntactic =
    | NGeneralize of loc * npattern
    | NId of loc
    | NIntro of loc * string
+   | NIntros of loc * string list
    | NInversion of loc * CicNotationPt.term * npattern  
    | NLApply of loc * CicNotationPt.term
    | NLetIn of loc * npattern * CicNotationPt.term * string
@@ -201,6 +202,7 @@ type nmacro =
   | NCheck of loc * CicNotationPt.term
   | Screenshot of loc * string
   | NAutoInteractive of loc * CicNotationPt.term auto_params
+  | NIntroGuess of loc
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index e8abb057295acf3a49dedc8e0b7df19e28fc1e2e..e55df286b87b5a0d6f069bb4f7de9228cc3f00e4 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -808,6 +808,7 @@ let eval_ng_tac tac =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
   | GrafiteAst.NInversion (_loc, what, where) ->
       NTactics.inversion_tac 
         ~what:(text,prefix_len,what)

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index faa17124edd09053a0634267af03ae4fdb3acb35..d7aae9ee8c1bc9021686b619ae096943a3d4c4a0 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -276,6 +276,7 @@ EXTEND
        | Some `Trace ->
           G.NMacro(loc,
              G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
+    | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
     | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
     | IDENT "screenshot"; fname = QSTRING -> 
         G.NMacro(loc,G.Screenshot (loc, fname))
@@ -315,7 +316,7 @@ EXTEND
             (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
         G.NTactic(loc,[G.NBlock (loc,l)])
     | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
-    | SYMBOL "#"; n=IDENT -> G.NTactic(loc,[ G.NIntro (loc,n)])
+    | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
     | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f6d8bfaec3055f456c70615207ed3fc74f98aa8b..f3d74050f9247cb07cc14d231428c5108ba683da 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -556,6 +556,25 @@ let intro_tac name =
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
+let name_counter = ref 0;;
+let intros_tac ?names_ref names s =
+  let names_ref, prefix = 
+    match names_ref with | None -> ref [], "__" | Some r -> r, "H" 
+  in
+  if names = [] then
+   repeat_tac 
+     (fun s ->
+        incr name_counter;
+        (* TODO: generate better names *)
+        let name = prefix ^ string_of_int !name_counter in
+        let s = intro_tac name s in 
+        names_ref := !names_ref @ [name];
+        s)
+     s
+   else
+     block_tac (List.map intro_tac names) s
+;;
+
 let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status (ctx_of gty) what None in

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index a4c48e68681b7171985bb30a812f2548b51a1199..822421a24eebe3716663c45d765712aaccaa2a07 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -43,6 +43,8 @@ val elim_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
 val intro_tac: string -> 's NTacStatus.tactic
+val intros_tac: 
+     ?names_ref:string list ref -> string list -> 's NTacStatus.tactic
 val cases_tac: 
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 4449d3b1df8757728de30a7aafef143700efb1ab..1e63cc3d18c9d3e2af250576bf25b20e428e5aab 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -393,6 +393,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
       [status, parsed_text], "", parsed_text_length
+  | TA.NIntroGuess _loc ->
+      let names_ref = ref [] in
+      let s = 
+        NTactics.intros_tac ~names_ref [] script#grafite_status 
+      in
+      let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+      let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+      [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
   | TA.NAutoInteractive (_loc, (None,a)) -> 
       let trace_ref = ref [] in
       let s = 

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index f8916ee5a5759682c9808c1c4238444780cadbe7..300812ce89ccff39d7be66f2b507ad6097496684 100644 (file)
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -65,14 +65,7 @@ nqed. *)
 
 nlemma in_l_inv_e:
  ∀S,w. in_l S w (e ?) → w = [].
- #S; #w; #H; ninversion H
-  [ #a; #b; ndestruct; //
-  | #a; #b; #c; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; ndestruct
-  | #a; #b; #c; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
+ #S; #w; #H; ninversion H; #; ndestruct; //.
 nqed.
 
 naxiom in_l_inv_s: 
@@ -141,7 +134,7 @@ ntheorem eclose_true:
   true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
  #S; #E; nelim E; nnormalize; //
   [ #H; ncases (?: False); /2/
-  | #x; #H; ncases (?: False); /2/
+  | #x H; #H; ncases (?: False); /2/
   | #x; #H; ncases (?: False); /2/
   | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
     #_; #_; #H; ncases (?:False); /2/
@@ -165,15 +158,10 @@ nqed.
 ntheorem in_l_empty_c:
  ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
  #S; #E1; #E2; #H; ninversion H
-  [ #_; #H2; ndestruct
-  | #x; #K; ndestruct
+  [##1,2,4,5,6,7: #; ndestruct
   | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
     nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
-    ndestruct; //
-  | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
-  | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
-  | #E; #_; #K; ndestruct 
-  | #w1; #w2; #w3; #H1; #H2; #H3; #H4; #H5; #H6; ndestruct ]
+    ndestruct; // ]
 nqed.
 
 ntheorem eclose_true':
@@ -185,25 +173,15 @@ ntheorem eclose_true':
   | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
      [ #H1; #H2; #H3; ninversion H3; /3/;
    ##| #H1; #H2; #H3; ninversion H3
-        [ #_; #K; ndestruct
-        | #x; #K; ndestruct
+        [ ##1,2,4,5,6,7: #; ndestruct
         | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
-          napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //
-        | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
-        | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
-        | #E'; #_; #K; ndestruct
-        | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]##]
+          napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##]
 ##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
     #E2; #H1; #H2; #H3; ninversion H3
-     [ #_; #K; ndestruct
-     | #w; #_; #K; ndestruct
-     | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
+     [ ##1,2,3,5,6,7: #; ndestruct; /2/
      | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
        ncases (?: False); napply (absurd ?? (not_eq_true_false …));
-       /2/
-     | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/
-     | #a; #b; #c; ndestruct
-     | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##]
+       /2/ ]##]
 nqed.     
 
 (*