From 63f876b112e1be016e8063e6a00ec47f841ee615 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 13 Mar 2007 13:21:56 +0000
Subject: [PATCH] elim tactic: now takes a pattern instead of just a term      
        works as before for now. the pattern wil be activated soon Procedural:
  cleaning up ProofEngineReduction: new subst_inv function exactly inverts
 subst

---
 components/acic_procedural/acic2Procedural.ml |  90 ++++-----------
 .../acic_procedural/proceduralConversion.ml   | 104 +-----------------
 .../acic_procedural/proceduralConversion.mli  |   7 +-
 components/acic_procedural/proceduralTypes.ml |   9 +-
 .../acic_procedural/proceduralTypes.mli       |   2 +-
 components/grafite/grafiteAst.ml              |   3 +-
 components/grafite/grafiteAstPp.ml            |   7 +-
 components/grafite_engine/grafiteEngine.ml    |   4 +-
 .../grafite_parser/grafiteDisambiguate.ml     |  12 +-
 components/grafite_parser/grafiteParser.ml    |   6 +-
 components/tactics/declarative.ml             |   9 +-
 components/tactics/eliminationTactics.ml      |  10 +-
 components/tactics/primitiveTactics.ml        |  36 +++++-
 components/tactics/primitiveTactics.mli       |   8 +-
 components/tactics/proofEngineReduction.ml    |  77 +++++++++++--
 components/tactics/proofEngineReduction.mli   |   3 +
 components/tactics/tactics.mli                |   8 +-
 matita/matitaGui.ml                           |   2 +-
 18 files changed, 174 insertions(+), 223 deletions(-)

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index e3545f62a..dbdfb9792 100644
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -55,10 +55,6 @@ type status = {
 
 (* helpers ******************************************************************)
 
-let identity x = x
-
-let comp f g x = f (g x)
-
 let cic = D.deannotate_term
 
 let split2_last l1 l2 =
@@ -166,39 +162,17 @@ let unused_premise = "UNUSED"
 
 let defined_premise = "DEFINED"
 
-let expanded_premise = "EXPANDED"
-
 let convert st ?name v = 
    match get_inner_types st v with
       | None          -> []
       | Some (st, et) ->
          let cst, cet = cic st, cic et in
 	 if PER.alpha_equivalence cst cet then [] else 
-	 let e = Cn.mk_pattern [] (T.mk_arel 1 "") in
+	 let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
 	 match name with
 	    | None    -> [T.Change (st, et, None, e, "")]
 	    | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
 
-let eta_expand n t =
-   let id = Ut.id_of_annterm t in
-   let ty = C.AImplicit ("", None) in
-   let name i = Printf.sprintf "%s%u" expanded_premise i in 
-   let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
-   let arg i n = T.mk_arel ((* n - *) succ i) (name (n - i - 1)) in
-   let rec aux i f a =
-      if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
-   in
-   let absts, args = aux 0 identity [] in
-   match Cn.lift 1 n t with
-      | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
-      | t                -> absts (C.AAppl ("", t :: args))  
-
-let appl_expand n = function
-   | C.AAppl (id, ts) -> 
-      let before, after = T.list_split (List.length ts + n) ts in
-      C.AAppl (id, C.AAppl ("", before) :: after)
-   | _                -> assert false
-
 let get_intro name t = 
 try
 match name with 
@@ -226,9 +200,8 @@ let rec mk_atomic st dtext what =
 
 and mk_fwd_rewrite st dtext name tl direction =   
    assert (List.length tl = 6);
-   let what, where = List.nth tl 5, List.nth tl 3 in
-   let rps, predicate = [List.nth tl 4], List.nth tl 2 in
-   let e = Cn.mk_pattern rps predicate in
+   let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
+   let e = Cn.mk_pattern 1 predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
          let script, what = mk_atomic st dtext what in
@@ -237,19 +210,19 @@ and mk_fwd_rewrite st dtext name tl direction =
 
 and mk_rewrite st dtext script t what qs tl direction = 
    assert (List.length tl = 5);
-   let rps, predicate = [List.nth tl 4], List.nth tl 2 in
-   let e = Cn.mk_pattern rps predicate in
+   let predicate = List.nth tl 2 in
+   let e = Cn.mk_pattern 1 predicate in
    List.rev script @ convert st t @
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 and mk_fwd_proof st dtext name = function
-   | C.ALetIn (_, n, v, t)                           ->
+   | C.ALetIn (_, n, v, t)      ->
       let entry = Some (n, C.Def (cic v, None)) in
       let intro = get_intro n t in
       let qt = mk_fwd_proof (add st entry intro) dtext name t in
       let qv = mk_fwd_proof st "" intro v in
       List.append qt qv
-   | C.AAppl (_, hd :: tl) as v                         -> 
+   | C.AAppl (_, hd :: tl) as v -> 
       if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
       if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
       let ty = get_type "TC1" st hd in
@@ -262,14 +235,9 @@ and mk_fwd_proof st dtext name = function
             let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
 	    [T.LetIn (name, v, dtext ^ text)]
       end
-(*   | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
-      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
-         | None   -> [T.LetIn (name, v, dtext)] 
-         | Some v -> mk_fwd_proof st dtext name v
-      end
-*)   | C.ACast (_, v, _)                                  ->
-      mk_fwd_proof st dtext name v
-   | v                                                  ->
+   | C.AMutCase _               -> assert false
+   | C.ACast _                  -> assert false 
+   | v                          ->
       match get_inner_types st v with
          | Some (ity, _) ->
 	    let qs = [[T.Id ""]; mk_proof (next st) v] in
@@ -278,11 +246,11 @@ and mk_fwd_proof st dtext name = function
             [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t)                     ->
+   | C.ALambda (_, name, v, t)        ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
       mk_proof (add st entry intro) t
-   | C.ALetIn (_, name, v, t) as what              ->
+   | C.ALetIn (_, name, v, t) as what ->
       let proceed, dtext = test_depth st in
       let script = if proceed then 
          let entry = Some (name, C.Def (cic v, None)) in
@@ -293,27 +261,22 @@ and mk_proof st = function
 	 [T.Apply (what, dtext)]
       in
       mk_intros st script
-   | C.ARel _ as what                              ->
+   | C.ARel _ as what                 ->
       let _, dtext = test_depth st in
       let text = "assumption" in
       let script = [T.Apply (what, dtext ^ text)] in 
       mk_intros st script
-   | C.AMutConstruct _ as what                     ->
+   | C.AMutConstruct _ as what        ->
       let _, dtext = test_depth st in
       let script = [T.Apply (what, dtext)] in 
       mk_intros st script   
-   | C.AAppl (_, hd :: tl) as t                    ->
+   | C.AAppl (_, hd :: tl) as t       ->
       let proceed, dtext = test_depth st in
       let script = if proceed then
          let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty in
          let premises, _ = P.split st.context ty in
-	 let decurry = List.length classes - List.length tl in
-         if decurry <> 0 then
-	    Printf.eprintf "DECURRY: %u %s\n" decurry (CicPp.ppterm (cic t));
-	 assert (decurry = 0);
-	 if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
-         if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
+	 assert (List.length classes - List.length tl = 0);
 	 let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
@@ -327,9 +290,12 @@ and mk_proof st = function
 	       else if is_rewrite_left hd then 
 	          mk_rewrite st dtext script t what qs tl true
 	       else   
-	          let using = Some hd in
+                  let l = succ (List.length tl) in
+		  let predicate = List.nth tl (l - i) in
+                  let e = Cn.mk_pattern j predicate in
+		  let using = Some hd in
 		  List.rev script @ convert st t @
-	          [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
+	          [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
 	    | _                                                  ->
 	       let qs = mk_bkd_proofs (next st) synth classes tl in
 	       let script, hd = mk_atomic st dtext hd in               
@@ -339,17 +305,9 @@ and mk_proof st = function
          [T.Apply (t, dtext)]
       in
       mk_intros st script
-   | C.AMutCase (id, uri, tyno, outty, arg, cases) as t ->
-      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
-         | _ (* None *)  -> 
-            let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
-            let script = [T.Note text] in
-            mk_intros st script
-(*         | Some t -> mk_proof st t *)
-      end
-   | C.ACast (_, t, _)                             ->
-      mk_proof st t
-   | t                                             ->
+   | C.AMutCase _                     -> assert false
+   | C.ACast _                        -> assert false
+   | t                                ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script
diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index d2d305ed4..5f705053a 100644
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -39,26 +39,6 @@ module M    = ProceduralMode
 
 let cic = D.deannotate_term
 
-let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
-      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
-      | _                                           -> assert false
-
-let get_default_eliminator context uri tyno ty =
-   let _, (name, _, _, _) = get_ind_type uri tyno in
-   let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in
-   let ext = match sort with
-      | C.Sort C.Prop     -> "_ind"
-      | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
-      | C.Sort (C.Type _) -> "_rect" 
-      | C.Meta (_,_)      -> assert false
-      | _                 -> assert false
-   in
-   let buri = UM.buri_of_uri uri in
-   let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
-   C.Const (uri, [])
-
 let rec list_sub start length = function
    | _  :: tl when start  > 0 -> list_sub (pred start) length tl
    | hd :: tl when length > 0 -> hd :: list_sub start (pred length) tl
@@ -98,46 +78,6 @@ let lift k n =
    in
    lift_term k
 
-let fake_annotate c =
-   let get_binder c m =
-      try match List.nth c (pred m) with
-	 | Some (C.Name s, _) -> s
-	 | _                  -> assert false
-      with
-         | Invalid_argument _ -> assert false 
-   in
-   let mk_decl n v = Some (n, C.Decl v) in
-   let mk_def n v = Some (n, C.Def (v, None)) in
-   let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
-   let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
-   let rec ann_xns c (uri, t) = uri, ann_term c t
-   and ann_ms c = function
-      | None   -> None
-      | Some t -> Some (ann_term c t)
-   and ann_fix newc c (name, i, ty, bo) =
-      "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
-   and ann_cofix newc c (name, ty, bo) =
-      "", name, ann_term c ty, ann_term (List.rev_append newc c) bo
-   and ann_term c = function
-      | C.Sort sort -> C.ASort ("", sort)
-      | C.Implicit ann -> C.AImplicit ("", ann)
-      | C.Rel m -> C.ARel ("", "", m, get_binder c m)
-      | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss)
-      | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss)
-      | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss)
-      | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss)
-      | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss)
-      | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts)
-      | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty)
-      | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)      
-      | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
-      | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
-      | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t)
-      | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
-      | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
-   in
-   ann_term c
-
 let clear_absts m =
    let rec aux k n = function
       | C.AImplicit (_, None) as t         -> t
@@ -152,42 +92,6 @@ let clear_absts m =
    in 
    aux m
 
-let mk_ind context id uri tyno outty arg cases =
-try
-   let sort_disp = 0 in
-   let is_recursive = function
-      | C.MutInd (u, no, _) -> UM.eq u uri && no = tyno
-      | _                   -> false
-   in
-   let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
-   let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in
-   let ps = match Rd.whd ~delta:true context inty with
-      | C.MutInd _                  -> []
-      | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args
-      | _                           -> assert false
-   in
-   let lps, rps = T.list_split lpsno ps in
-   let rpsno = List.length rps in
-   let eliminator = get_default_eliminator context uri tyno inty in
-   let eliminator = fake_annotate context eliminator in
-   let predicate = clear_absts rpsno (1 - sort_disp) outty in   
-   let map2 case (_, cty) = 
-      let map (h, case, k) premise = 
-         if h > 0 then pred h, lift k 1 case, k else
-	 if is_recursive premise then 0, lift (succ k) 1 case, succ k else
-	 0, case, succ k
-      in
-      let premises, _ = P.split context cty in
-      let _, lifted_case, _ =
-         List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
-      in
-      lifted_case
-   in
-   let lifted_cases = List.map2 map2 cases constructors in
-   let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   Some (C.AAppl (id, args))
-with Invalid_argument _ -> failwith "PCn.mk_ind"
-
 let hole id = C.AImplicit (id, Some `Hole)
 
 let meta id = C.AImplicit (id, None)
@@ -239,8 +143,6 @@ let generalize n =
    in
    gen_term 0
 
-let mk_pattern rps predicate =
-   let sort_disp = 0 in
-   let rpsno = List.length rps in
-   let body = generalize (rpsno + sort_disp) predicate in
-   clear_absts 0 (rpsno + sort_disp) body
+let mk_pattern rpsno predicate =
+   let body = generalize rpsno predicate in
+   clear_absts 0 rpsno body
diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli
index 3b6520014..5cbb75da2 100644
--- a/components/acic_procedural/proceduralConversion.mli
+++ b/components/acic_procedural/proceduralConversion.mli
@@ -25,9 +25,4 @@
 
 val lift: int -> int -> Cic.annterm -> Cic.annterm
 
-val mk_ind: 
-   Cic.context -> Cic.id -> UriManager.uri -> int -> 
-   Cic.annterm -> Cic.annterm -> Cic.annterm list ->
-   Cic.annterm option
-
-val mk_pattern: Cic.annterm list -> Cic.annterm -> Cic.annterm
+val mk_pattern: int -> Cic.annterm -> Cic.annterm
diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index 91f2408b9..3ef27ea40 100644
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -86,7 +86,7 @@ type step = Note of note
 	  | Cut of name * what * note
 	  | LetIn of name * what * note
 	  | Rewrite of how * what * where * pattern * note
-	  | Elim of what * using option * note
+	  | Elim of what * using option * pattern * note
 	  | Apply of what * note
 	  | Change of inferred * what * where * pattern * note 
 	  | ClearBody of name * note
@@ -137,8 +137,9 @@ let mk_rewrite direction what where pattern =
    let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
    mk_tactic tactic
 
-let mk_elim what using =
-   let tactic = G.Elim (floc, what, using, Some 0, []) in
+let mk_elim what using pattern =
+   let pattern = Some what, [], Some pattern in
+   let tactic = G.Elim (floc, pattern, using, Some 0, []) in
    mk_tactic tactic
 
 let mk_apply t =
@@ -178,7 +179,7 @@ let rec render_step sep a = function
    | Cut (n, t, s)           -> mk_note s :: cont sep (mk_cut n t :: a)
    | LetIn (n, t, s)         -> mk_note s :: cont sep (mk_letin n t :: a)
    | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a)
-   | Elim (t, xu, s)         -> mk_note s :: cont sep (mk_elim t xu :: a)
+   | Elim (t, xu, e, s)      -> mk_note s :: cont sep (mk_elim t xu e :: a)
    | Apply (t, s)            -> mk_note s :: cont sep (mk_apply t :: a)
    | Change (t, _, w, e, s)  -> mk_note s :: cont sep (mk_change t w e :: a)
    | ClearBody (n, s)        -> mk_note s :: cont sep (mk_clearbody n :: a)
diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli
index 33a7e9c05..97ca7fdbb 100644
--- a/components/acic_procedural/proceduralTypes.mli
+++ b/components/acic_procedural/proceduralTypes.mli
@@ -53,7 +53,7 @@ type step = Note of note
           | Cut of name * what * note
           | LetIn of name * what * note
 	  | Rewrite of how * what * where * pattern * note
-	  | Elim of what * using option * note
+	  | Elim of what * using option * pattern * note
 	  | Apply of what * note
 	  | Change of inferred * what * where * pattern * note
 	  | ClearBody of name * note
diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 1ec71be92..b5e75712f 100644
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -55,7 +55,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Decompose of loc * 'ident list
   | Demodulate of loc
   | Destruct of loc * 'term
-  | Elim of loc * 'term * 'term option * int option * 'ident list
+  | Elim of loc * ('term, 'lazy_term, 'ident) pattern * 'term option * 
+            int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
   | Exact of loc * 'term
   | Exists of loc
diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index e433c9b7b..e8fd2fe02 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -99,10 +99,11 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "decompose%s" (pp_intros_specs (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
-  | Elim (_, term, using, num, idents) ->
-      sprintf "elim " ^ term_pp term ^
+  | Elim (_, pattern, using, num, idents) ->
+      sprintf "elim %s%s%s" 
+      (pp_tactic_pattern pattern)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
-      ^ pp_intros_specs (num, idents) 
+      (pp_intros_specs (num, idents)) 
   | ElimType (_, term, using, num, idents) ->
       sprintf "elim type " ^ term_pp term ^
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index db08a6038..4c177fee7 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -87,9 +87,9 @@ let tactic_of_ast status ast =
       Tactics.demodulate 
 	~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
-  | GrafiteAst.Elim (_, what, using, depth, names) ->
+  | GrafiteAst.Elim (_, pattern, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
-        what
+        pattern
   | GrafiteAst.ElimType (_, what, using, depth, names) ->
       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what
diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index cc8360c28..97f0d5e85 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -158,13 +158,13 @@ let disambiguate_tactic
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
-    | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
-        let metasenv,what = disambiguate_term context metasenv what in
+    | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) ->
+	let pattern = disambiguate_pattern pattern in
         let metasenv,using = disambiguate_term context metasenv using in
-        metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
-    | GrafiteAst.Elim (loc, what, None, depth, idents) ->
-        let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
+        metasenv,GrafiteAst.Elim (loc, pattern, Some using, depth, idents)
+    | GrafiteAst.Elim (loc, pattern, None, depth, idents) ->
+	let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Elim (loc, pattern, None, depth, idents)
     | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 3653c4606..dac05d7bd 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -164,8 +164,12 @@ EXTEND
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
     | IDENT "elim"; what = tactic_term; using = using;
+       (num, idents) = intros_spec ->
+	let pattern = Some what, [], Some Ast.UserInput in
+	GrafiteAst.Elim (loc, pattern, using, num, idents)
+    | IDENT "elim"; pattern = pattern_spec; using = using;
       (num, idents) = intros_spec ->
-	GrafiteAst.Elim (loc, what, using, num, idents)
+	GrafiteAst.Elim (loc, pattern, using, num, idents)    
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
 	GrafiteAst.ElimType (loc, what, using, num, idents)
diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 110f72fb1..189cd9079 100644
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -127,11 +127,12 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
   let proof' = (n,metasenv,bo,ty,attrs) in
+   let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in
    ProofEngineTypes.apply_tactic (
    Tacticals.thens
     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
     ~continuations:
-     [ Tactics.elim_intros (Cic.Rel 1)
+     [ Tactics.elim_intros pattern 
         ~mk_fresh_name_callback:
           (let i = ref 0 in
             fun _ _ _  ~typ ->
@@ -146,7 +147,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
 ;;
 
 let andelim t id1 t1 id2 t2 = 
- Tactics.elim_intros t
+ Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
       ~mk_fresh_name_callback:
         (let i = ref 0 in
           fun _ _ _  ~typ ->
@@ -250,8 +251,8 @@ let we_proceed_by_cases_on t pat =
 ;;
 
 let we_proceed_by_induction_on t pat =
- (*BUG here: pat unused *)
- Tactics.elim_intros ~depth:0 t
+ let pattern = Some (fun c m u -> t, m, u), [], Some pat in
+ Tactics.elim_intros ~depth:0 pattern
 ;;
 
 let case id ~params =
diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index e74886e95..85eade2d0 100644
--- a/components/tactics/eliminationTactics.ml
+++ b/components/tactics/eliminationTactics.ml
@@ -127,9 +127,10 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
+      let pattern = PET.conclusion_pattern (Some (C.Rel index)) in
       let tac = 
          if check_type sorts metasenv context (S.lift index ty) then 
-            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern)
 	            ~continuation:(PESR.clear [what])
 	 else 
 	    let msg = "unexported elim_clear: not an decomposable type" in
@@ -144,12 +145,13 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
 let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
   ?using what
 =
-  let elim what =
-    P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what
+  let elim =
+    P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
   in
   let elim_type_tac status =
+    let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in
     let tac =
-      T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+      T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac]
     in
     PET.apply_tactic tac status
   in
diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 60eb4dc5b..2c22aa5ec 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -477,7 +477,7 @@ let exact_tac ~term =
   mk_tactic (exact_tac ~term)
 
 (* not really "primitive" tactics .... *)
-let elim_tac ?using ~term = 
+let elim_tac ?using pattern = 
  let elim_tac (proof, goal) =
   let module T = CicTypeChecker in
   let module U = UriManager in
@@ -485,6 +485,10 @@ let elim_tac ?using ~term =
   let module C = Cic in
    let (curi,metasenv,proofbo,proofty, attrs) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let term, metasenv, _ = match pattern with 
+       | Some f, [], Some _ -> f context metasenv CicUniv.empty_ugraph
+       | _                  -> assert false
+    in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let termty = CicReduction.whd context termty in
     let (termty,metasenv',arguments,fresh_meta) =
@@ -534,7 +538,27 @@ let elim_tac ?using ~term =
           | _ -> 0
         in
          let args_no = find_args_no ety in
-         let term_to_refine =
+(* we find the predicate for the eliminator as in the rewrite tactic ********)
+(*   
+   let fresh_name = 
+       FreshNamesGenerator.mk_fresh_name 
+       ~subst:[] metasenv' context C.Anonymous ~typ:termty in
+  let lifted_gty = S.lift 1 ty in
+  let lifted_conjecture =
+    metano, (Some (fresh_name, Cic.Decl ty)) :: context, lifted_gty in
+  let lifted_t1 = S.lift 1 t1x in
+  let lifted_pattern =
+    let lifted_concl_pat =
+      match concl_pat with
+      | None -> None
+      | Some term -> Some (S.lift 1 term) in
+    Some (fun c m u -> 
+       let distance  = pred (List.length c - List.length context) in
+       S.lift distance lifted_t1, m, u),[],lifted_concl_pat
+  in
+*)
+(****************************************************************************)
+	 let term_to_refine =
           let rec make_tl base_case =
            function
               0 -> [base_case]
@@ -660,15 +684,15 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
 
 
 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
-                    ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+                    ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
   ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 ;;
 
 (* The simplification is performed only on the conclusion *)
 let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-                          ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+                          ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
   ~continuation:
    (Tacticals.thens
      ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
diff --git a/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli
index 3e7a48581..2700fc27f 100644
--- a/components/tactics/primitiveTactics.mli
+++ b/components/tactics/primitiveTactics.mli
@@ -72,10 +72,14 @@ val letin_tac:
 
 val elim_intros_simpl_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 
+  ?depth:int -> ?using:Cic.term -> 
+  ProofEngineTypes.lazy_pattern ->
+  ProofEngineTypes.tactic 
 val elim_intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 
+  ?depth:int -> ?using:Cic.term -> 
+  ProofEngineTypes.lazy_pattern ->
+  ProofEngineTypes.tactic 
 
 val cases_intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index 6d198d4d1..c359313dd 100644
--- a/components/tactics/proofEngineReduction.ml
+++ b/components/tactics/proofEngineReduction.ml
@@ -46,8 +46,10 @@ exception WrongUriToInductiveDefinition;;
 exception WrongUriToConstant;;
 exception RelToHiddenHypothesis;;
 
+module C = Cic
+module S = CicSubstitution
+
 let alpha_equivalence =
- let module C = Cic in
   let rec aux t t' =
    if t = t' then true
    else
@@ -122,7 +124,6 @@ exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 (* "textual" replacement of several subterms with other ones *)
 let replace ~equality ~what ~with_what ~where =
- let module C = Cic in
   let find_image t =
    let rec find_image_aux =
     function
@@ -184,8 +185,6 @@ let replace ~equality ~what ~with_what ~where =
 (* replaces in a term a term with another one. *)
 (* Lifting are performed as usual.             *)
 let replace_lifting ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
   let find_image what t =
    let rec find_image_aux =
     function
@@ -282,8 +281,6 @@ let replace_lifting ~equality ~what ~with_what ~where =
 (* replaces in a term a list of terms with other ones. *)
 (* Lifting are performed as usual.                     *)
 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
   let find_image t =
    let rec find_image_aux =
     function
@@ -373,12 +370,72 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
   substaux 1 where
 ;;
 
+(* This is the inverse of the subst function. *)
+let subst_inv ~equality ~what =
+   let rec find_image t = function
+      | []       -> false
+      | hd :: tl -> equality t hd || find_image t tl 
+   in
+   let rec subst_term k t =
+      if find_image t what then C.Rel k else inspect_term k t
+   and inspect_term k = function
+      | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n)
+      | C.Sort _ as t -> t
+      | C.Implicit _ as t -> t
+      | C.Var (uri, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Var (uri, enss)
+      | C.Const (uri ,enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Const (uri, enss)
+     | C.MutInd (uri, tyno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutInd (uri, tyno, enss)
+     | C.MutConstruct (uri, tyno, consno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutConstruct (uri, tyno, consno, enss)
+     | C.Meta (i, mss) -> 
+         let mss = List.map (subst_ms k) mss in
+         C.Meta(i, mss)
+     | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
+     | C.Appl ts ->      
+         let ts = List.map (subst_term k) ts in
+         C.Appl ts
+     | C.MutCase (uri, tyno, outty, t, cases) ->
+         let cases = List.map (subst_term k) cases in
+	 C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
+     | C.Prod (n, v, t) ->
+        C.Prod (n, subst_term k v, subst_term (succ k) t)
+     | C.Lambda (n, v, t) ->
+        C.Lambda (n, subst_term k v, subst_term (succ k) t)
+     | C.LetIn (n, v, t) ->
+        C.LetIn (n, subst_term k v, subst_term (succ k) t)
+     | C.Fix (i, fixes) ->
+        let fixesno = List.length fixes in
+        let fixes = List.map (subst_fix fixesno k) fixes in
+        C.Fix (i, fixes)
+     | C.CoFix (i, cofixes) ->
+        let cofixesno = List.length cofixes in
+        let cofixes = List.map (subst_cofix cofixesno k) cofixes in
+         C.CoFix (i, cofixes)
+   and subst_ens k (uri, t) = uri, subst_term k t   
+   and subst_ms k = function
+      | None   -> None
+      | Some t -> Some (subst_term k t)
+   and subst_fix fixesno k (n, ind, ty, bo) =
+      n, ind, subst_term k ty, subst_term (k + fixesno) bo
+   and subst_cofix cofixesno k (n, ty, bo) =
+      n, subst_term k ty, subst_term (k + cofixesno) bo
+in
+subst_term
+   
+
+
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (match List.nth context (n-1) with
@@ -595,8 +652,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let module C = Cic in
- let module S = CicSubstitution in
  (* a simplified term is active if it can create a redex when used as an *)
  (* actual parameter                                                     *)
  let rec is_active =
@@ -805,8 +860,6 @@ let simpl context =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
  and try_delta_expansion context l term body =
-  let module C = Cic in
-  let module S = CicSubstitution in
    try
     let res,constant_args =
      let rec aux rev_constant_args l =
diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli
index 67247876a..c0318bdfe 100644
--- a/components/tactics/proofEngineReduction.mli
+++ b/components/tactics/proofEngineReduction.mli
@@ -44,6 +44,9 @@ val replace_lifting :
 val replace_lifting_csc :
   int -> equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
+val subst_inv :
+  equality:(Cic.term -> Cic.term -> bool) ->
+  what:Cic.term list -> int -> Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term
 val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term
diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index deaf84aa6..8cca5aee0 100644
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar  1 10:25:04 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 12 13:47:11 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -32,10 +32,12 @@ val demodulate :
 val destruct : 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
+  ?depth:int ->
+  ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val elim_intros_simpl :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  ?depth:int ->
+  ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val elim_type :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index a9faa592e..83fee2e15 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -990,7 +990,7 @@ class gui () =
       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, None, [])));
+        (A.Elim (loc, (Some hole, [], Some CicNotationPt.UserInput), None, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));
-- 
2.39.2