name specifications added for elim_intros, elim_intros_simpl and elim_type

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
index dfdc49c5048de07d3f49c206b10f4c1dcf2b37b5..106bfe66cab6a2851a247ee4e8b7aa8637e27770 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
@@ -35,7 +35,7 @@ Require pr3_defs.
 (* case 2.1 : i0 = 0 *)
       DropGenBase; Inversion H2; Clear H2.
       Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
-      Subst0Subst0; Arith9'In H4 i; XDEAuto 7.
+      Subst0Subst0; Arith9'In H4 i. (*; XDEAuto 7.
 (* case 2.2 : i0 > 0 *)
       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
       Qed.
@@ -111,3 +111,4 @@ Require pr3_defs.
 
       Hints Resolve pr3_lift : ltlc.
 
+*)

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 5941b1126aa0525726b3d6999c2f015466f7d346..67f724ce0a71f30351b84996f528d682e3d396c6 100644 (file)
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -42,6 +42,7 @@
     <keyword>to</keyword>
     <keyword>as</keyword>
     <keyword>using</keyword>
+    <keyword>names</keyword>
   </keyword-list>
 
   <pattern-item _name = "Command [" style = "Keyword">

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 0e46c34d2236549a834ee624b2f11c353f4f1ea8..7f70736abbe22a30cbae66fcaf8db893429e49c2 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -40,9 +40,10 @@ let tactic_of_ast = function
   | TacticAst.DecideEquality _ -> Tactics.decide_equality
   | TacticAst.Decompose (_,term) -> Tactics.decompose term
   | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
-  | TacticAst.Elim (_, term, _) ->
-      Tactics.elim_intros term
-  | TacticAst.ElimType (_, term) -> Tactics.elim_type term
+  | TacticAst.Elim (_, what, using, depth, names) ->
+      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
+  | TacticAst.ElimType (_, what, using, depth, names) ->
+      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
   | TacticAst.Exact (_, term) -> Tactics.exact term
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fail _ -> Tactics.fail
@@ -447,16 +448,20 @@ let disambiguate_tactic status = function
   | TacticAst.Exact (loc, term) -> 
       let status, cic = disambiguate_term status term in
       status, TacticAst.Exact (loc, cic)
-  | TacticAst.Elim (loc, term, Some term') ->
-      let status, cic1 = disambiguate_term status term in
-      let status, cic2 = disambiguate_term status term' in
-      status, TacticAst.Elim (loc, cic1, Some cic2)
-  | TacticAst.Elim (loc, term, None) ->
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Elim (loc, cic, None)
-  | TacticAst.ElimType (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.ElimType (loc, cic)
+  | TacticAst.Elim (loc, what, Some using, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      let status, using = disambiguate_term status using in
+      status, TacticAst.Elim (loc, what, Some using, depth, idents)
+  | TacticAst.Elim (loc, what, None, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      status, TacticAst.Elim (loc, what, None, depth, idents)
+  | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      let status, using = disambiguate_term status using in
+      status, TacticAst.ElimType (loc, what, Some using, depth, idents)
+  | TacticAst.ElimType (loc, what, None, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      status, TacticAst.ElimType (loc, what, None, depth, idents)
   | TacticAst.Exists loc -> status, TacticAst.Exists loc 
   | TacticAst.Fail loc -> status,TacticAst.Fail loc
   | TacticAst.Fold (loc,reduction_kind, term, pattern) ->

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c9b387178bc8cd1c780de9940d481013a1d035a0..5ac24f8f66c9abdd262e6f477dd368188edc01e9 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -156,8 +156,8 @@ class gui () =
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
-      connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None)));
-      connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
+      connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, [])));
+      connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));
       connect_button tbar#leftButton (tac (A.Left loc));
       connect_button tbar#rightButton (tac (A.Right loc));

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index e42de00b50a9a530542696c461ae945caaa2459f..141e29776d009f8871290631e8c300ab01ddcad6 100644 (file)
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -94,5 +94,12 @@ qed.
 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
 intros 1.
 elim x. auto.
-fwd H1 [].
+fwd H1 [H0]. 
+elim H0 names [pippo; pappo].
+
+decompose H0 
+
+
+elim H0. clear H0. elim H1. clear H1.
+
 *)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 32d8ae54da64d11ac23e7a0ce0b2fee899921911..92a24ec8278b2d50dcb26598b3e81f4d17878160 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -66,7 +66,7 @@ let keywords = Hashtbl.create 17
 let _ =
   List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword))
     [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with";
-    "in"; "and"; "to"; "as"; "on"]
+    "in"; "and"; "to"; "as"; "on"; "names"]
 
 let error lexbuf msg =
   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 59bb1bc81c92159024c6ac3abb4db919639e1d80..9ce70062f7c31dd843e96ac7d7191c7aaa4ba2fc 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -398,11 +398,16 @@ EXTEND
         TacticAst.Decompose (loc, where)
     | IDENT "discriminate"; t = tactic_term ->
         TacticAst.Discriminate (loc, t)
-    | IDENT "elim"; t1 = tactic_term;
-      using = OPT [ "using"; using = tactic_term -> using ] ->
-        TacticAst.Elim (loc, t1, using)
-    | IDENT "elimType"; t = tactic_term ->
-        TacticAst.ElimType (loc, t)
+    | IDENT "elim"; what = tactic_term;
+      using = OPT [ "using"; using = tactic_term -> using ];  
+      OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in
+       TacticAst.Elim (loc, what, using, num, idents)
+    | IDENT "elimType"; what = tactic_term;
+      using = OPT [ "using"; using = tactic_term -> using ];  
+      OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in
+       TacticAst.ElimType (loc, what, using, num, idents)
     | IDENT "exact"; t = tactic_term ->
         TacticAst.Exact (loc, t)
     | IDENT "exists" ->

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 0dfb48aedb81236788fb2d664a55d03800d9f28e..581b44698ef23de18ab618107f16abed5c192d2a 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -45,8 +45,8 @@ type ('term, 'ident) tactic =
   | DecideEquality of loc
   | Decompose of loc * 'term
   | Discriminate of loc * 'term
-  | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
-  | ElimType of loc * 'term
+  | Elim of loc * 'term * 'term option * int option * 'ident list
+  | ElimType of loc * 'term * 'term option * int option * 'ident list
   | Exact of loc * 'term
   | Exists of loc
   | Fail of loc

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 21bf33a0af6807a9429edf021a1468c67fe9a4ad..3275953651e01ddb1af92dca556b7917b78dc2ba 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -57,6 +57,12 @@ let pp_pattern (t, hyp, goal) =
   in
    pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
 
+let pp_intros_specs = function
+   | None, []         -> ""
+   | Some num, []     -> Printf.sprintf " names %i" num
+   | None, idents     -> Printf.sprintf " names %s" (pp_idents idents)
+   | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents)
+
 let rec pp_tactic = function
   | Absurd (_, term) -> "absurd" ^ pp_term_ast term
   | Apply (_, term) -> "apply " ^ pp_term_ast term
@@ -76,10 +82,14 @@ let rec pp_tactic = function
   | Decompose (_, term) ->
       sprintf "decompose %s" (pp_term_ast term)
   | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
-  | Elim (_, term, using) ->
+  | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ pp_term_ast term ^
       (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
-  | ElimType (_, term) -> "elim type " ^ pp_term_ast term
+      ^ pp_intros_specs (num, idents) 
+  | ElimType (_, term, using, num, idents) ->
+      sprintf "elim type " ^ pp_term_ast term ^
+      (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+      ^ pp_intros_specs (num, idents)
   | Exact (_, term) -> "exact " ^ pp_term_ast term
   | Exists _ -> "exists"
   | Fold (_, kind, term, pattern) ->

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 0f06351b4d8301e7f99cbb41b6731b0272bf2cb4..76b7337349bcc1dcec2d0e3850282704ba08ceb4 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -204,6 +204,7 @@ exception TwoDifferentSubtermsFound of int
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
+(* FG: METTERE I NOMI ANCHE QUI? *)
 let discriminate'_tac ~term =
  let discriminate'_tac ~term status = 
   let (proof, goal) = status in
@@ -287,7 +288,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
                     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(LibraryObjects.false_URI (),0,[])))
+                       (C.MutInd(LibraryObjects.false_URI (),0,[])))
                       status 
                     in
                      (match goals' with

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index 4f840764a8d17466acf6f094e98dec00f1cac49f..e52fff6e4452f671c2cc6e5634c41b2e03504716 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -57,18 +57,19 @@ let induction_tac ~term status =
 ;;
 *)
 
-let elim_type_tac ~term =
- let elim_type_tac ~term status =
+let elim_type_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+                  ?depth ?using what =
+ let elim_type_tac status =
    let module C = Cic in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
     ProofEngineTypes.apply_tactic 
      (T.thens
-      ~start: (P.cut_tac term)
-      ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ])
+      ~start: (P.cut_tac what)
+      ~continuations:[ P.elim_intros_simpl_tac ?depth ?using ~mk_fresh_name_callback (C.Rel 1) ; T.id_tac ])
      status
  in
-  ProofEngineTypes.mk_tactic (elim_type_tac ~term)
+  ProofEngineTypes.mk_tactic elim_type_tac
 ;;
 
 
@@ -107,7 +108,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term =
          | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> 
                (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist)
          | _ -> urilist
-         (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *)
+         (* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *)
        in 
        let rec purge_duplicates urilist = 
         let rec aux triple urilist =
@@ -148,7 +149,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term =
                    warn ("elim " ^ CicPp.ppterm termty);
                   ProofEngineTypes.apply_tactic 
                    (T.then_ 
-                      ~start:(P.elim_intros_simpl_tac ~term:term')
+                      ~start:(P.elim_intros_simpl_tac term')
                       ~continuation:(
                         (* clear the hyp that has just been eliminated *)
                         ProofEngineTypes.mk_tactic (fun status -> 

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index 92d9eee016ebdcbb2d941d4ee54614f69f651760..111bc57470eb826265fb3fde1992c9bf8216477a 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -23,7 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
+val elim_type_tac: 
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
 
 (* The default callback always decomposes the term as much as possible *)
 val decompose_tac:

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index ee76921b23ff0729649bed6030e1fedeffae67a6..0e3c0c142180a9f5570233f4a03528780711224c 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -46,6 +46,7 @@ let absurd_tac ~term =
    ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
+(* FG: METTERE I NOMI ANCHE QUI? *)
 let contradiction_tac =
  let contradiction_tac status =
   let module C = Cic in
@@ -60,8 +61,7 @@ let contradiction_tac =
         T.then_
            ~start:
              (EliminationTactics.elim_type_tac 
-                ~term:
-                  (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+                (C.MutInd (LibraryObjects.false_URI (), 0, [])))
            ~continuation: VariousTactics.assumption_tac))
     status
    with 

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 3fefc662a5bcb7915e83ffb70bb9df4ea44a3bfd..06e83a125335ea218df3a3e25f2c02f197910397 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -574,17 +574,19 @@ let elim_tac ~term =
   mk_tactic (elim_tac ~term)
 ;;
 
-let elim_intros_tac ~term =
- Tacticals.then_ ~start:(elim_tac ~term)
-  ~continuation:(intros_tac ())
+let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+                    ?depth ?using what =
+ Tacticals.then_ ~start:(elim_tac ~term:what)
+  ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 ;;
 
 (* The simplification is performed only on the conclusion *)
-let elim_intros_simpl_tac ~term =
- Tacticals.then_ ~start:(elim_tac ~term)
+let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+                          ?depth ?using what =
+ Tacticals.then_ ~start:(elim_tac ~term:what)
   ~continuation:
    (Tacticals.thens
-     ~start:(intros_tac ())
+     ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
      ~continuations:
        [ReductionTactics.simpl_tac
          ~pattern:(ProofEngineTypes.conclusion_pattern None)])

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 2e35f4250477bdb12eff077c3204d6206599c10d..6dac987248f579b05506c8df855e2159914e9b60 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.mli
+++ b/helm/ocaml/tactics/primitiveTactics.mli
@@ -52,6 +52,8 @@ val letin_tac:
    ProofEngineTypes.tactic 
 
 val elim_intros_simpl_tac:
-  term: Cic.term -> ProofEngineTypes.tactic 
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 
 val elim_intros_tac:
-  term: Cic.term -> ProofEngineTypes.tactic 
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 298a87f3c8df8361fc4bcaee9f9cbaa5dc12c5d9..1d5fd903dead5cc09649faf676e9bb310e080b88 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -388,12 +388,13 @@ let elim_type_tac ~term status =
     @param term term to cut
     @param proof term used to prove second subgoal generated by elim_type
   *)
+(* FG: METTERE I NOMI ANCHE QUI? *)  
 let elim_type2_tac ~term ~proof =
  let elim_type2_tac ~term ~proof status =
   let module E = EliminationTactics in
   warn "in Ring.elim_type2";
   ProofEngineTypes.apply_tactic 
-   (Tacticals.thens ~start:(E.elim_type_tac ~term)
+   (Tacticals.thens ~start:(E.elim_type_tac term)
     ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
  in
   ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 32bbf2c6aef5fccbfc9ad8a9ee696e50e6afeb4c..ff888d78b02e800627dcb6d8a68c5a95ed6343ff 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -25,9 +25,15 @@ val decompose :
                          list) ->
   Cic.term -> ProofEngineTypes.tactic
 val discriminate : term:Cic.term -> ProofEngineTypes.tactic
-val elim_intros : term:Cic.term -> ProofEngineTypes.tactic
-val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
-val elim_type : term:Cic.term -> ProofEngineTypes.tactic
+val elim_intros :
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+val elim_intros_simpl :
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+val elim_type :
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
 val exact : term:Cic.term -> ProofEngineTypes.tactic
 val exists : ProofEngineTypes.tactic
 val fail : ProofEngineTypes.tactic