X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;h=a136a51dd88afc306661a18aee087139dadaf99f;hp=3a700ba961d28583bb89bb1c4e0d2c6a8e9b7984;hb=784f0d4d7cff3700363affe647f7b8b218726fcb;hpb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index 3a700ba96..a136a51dd 100644
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -43,26 +43,21 @@ let extract_first_goal_from_status status =
   let s = status#stack in
   match s with
   | [] -> fail (lazy "There's nothing to prove")
-  | (g1, _, k, tag1) :: tl ->
+  | (g1, _, _k, _tag1, _) :: _tl ->
     let goals = filter_open g1 in
-    let (loc::tl) = goals in 
-    let goal = goal_of_loc (loc) in
-    goal ;;
-  (*
-  let (_,_,metasenv,_,_) = status#obj in
-  match metasenv with
-  | [] -> fail (lazy "There's nothing to prove")
-  | (hd,_) :: tl -> hd
-  *)
+    match goals with
+      [] -> fail (lazy "No goals under focus")
+    | loc::_tl -> 
+      let goal = goal_of_loc (loc) in
+      goal ;;
 
 let extract_conclusion_type status goal =
   let gty = get_goalty status goal in
   let ctx = ctx_of gty in
-  let status,gty = term_of_cic_term status gty ctx in
-  gty
+  term_of_cic_term status gty ctx
 ;;
 
-let same_type_as_conclusion ty t status goal =
+let alpha_eq_tacterm_kerterm ty t status goal =
   let gty = get_goalty status goal in
   let ctx = ctx_of gty in
   let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
@@ -77,254 +72,189 @@ let same_type_as_conclusion ty t status goal =
 let are_convertible ty1 ty2 status goal =
   let gty = get_goalty status goal in
   let ctx = ctx_of gty in
-  let status,cicterm1 = disambiguate status ctx ty1 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
-  let status,cicterm2 = disambiguate status ctx ty2 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
+  let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
+  let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
   NTacStatus.are_convertible status ctx cicterm1 cicterm2
 
+let clear_volatile_params_tac status =
+  match status#stack with
+    [] -> fail (lazy "Empty stack")
+  | (g,t,k,tag,p)::tl -> 
+    let rec remove_volatile = function
+        [] -> []
+      | (k,_v as hd')::tl' ->
+        let re = Str.regexp "volatile_.*" in
+        if Str.string_match re k 0 then
+          remove_volatile tl'
+        else
+          hd'::(remove_volatile tl')
+    in
+    let newp = remove_volatile p in
+    status#set_stack ((g,t,k,tag,newp)::tl)
+;;
+
+let add_parameter_tac key value status =
+  match status#stack with
+    [] -> status
+  | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
+;;
+
+
 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
    the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
    \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
 *)
-let lambda_abstract_tac id t1 t2 status goal =
+let lambda_abstract_tac id t1 status goal =
   match extract_conclusion_type status goal with
-  | NCic.Prod (_,t,_) ->
-    if same_type_as_conclusion t1 t status goal then
-      match t2 with
-      | None ->
-        let (_,_,t1) = t1 in
-        exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
-                                       `JustOne))) (*status*)
-      | Some t2 ->
-        let status,res = are_convertible t1 t2 status goal in
-        if res then
-          let (_,_,t2) = t2 in
-          exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
-                                         `JustOne))) (*status*)
-        else
-          raise NotEquivalentTypes
+  | status,NCic.Prod (_,t,_) ->
+    if alpha_eq_tacterm_kerterm t1 t status goal then
+      let (_,_,t1) = t1 in
+      block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+                                                `JustOne))); clear_volatile_params_tac;
+                 add_parameter_tac "volatile_newhypo" id] status
     else
       raise FirstTypeWrong
   | _ -> raise NotAProduct
 
-let assume name ty eqty (*status*) =
-(*   let goal = extract_first_goal_from_status status in *)
-  distribute_tac (fun status goal -> 
-    try exec (lambda_abstract_tac name ty eqty status goal) status goal
-    with
-    | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
-    | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
-    | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
-  )
+let assume name ty status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac name ty status goal
+  with
+  | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
+  | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
+  | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
 ;;
 
-let suppose t1 id t2 (*status*) =
-(*   let goal = extract_first_goal_from_status status in *)
-  distribute_tac (fun status goal ->
-    try exec (lambda_abstract_tac id t1 t2 status goal) status goal
-    with
-    | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
-    | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
-    | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
-  )
+let suppose t1 id status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac id t1 status goal
+  with
+  | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
+  | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
+  | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
 ;;
 
 let assert_tac t1 t2 status goal continuation =
-  let t = extract_conclusion_type status goal in
-  if same_type_as_conclusion t1 t status goal then
+  let status,t = extract_conclusion_type status goal in
+  if alpha_eq_tacterm_kerterm t1 t status goal then
     match t2 with
     | None -> continuation
     | Some t2 ->
-      let status,res = are_convertible t1 t2 status goal in
+      let _status,res = are_convertible t1 t2 status goal in
       if res then continuation
       else
         raise NotEquivalentTypes
   else
     raise FirstTypeWrong
 
-let mustdot status =
-  let s = status#stack in
-  match s with
-  | [] -> fail (lazy "No goals to dot")
-  | (_, _, k, _) :: tl ->
-    if List.length k > 0 then
-      true
+let branch_dot_tac status =
+  match status#stack with 
+    ([],t,k,tag,p) :: tl ->
+    if List.length t > 0 then
+      status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
     else
-      false
+      status
+  | _ -> status
+;;
 
-let bydone just status =
-  let goal = extract_first_goal_from_status status in
-  let mustdot = mustdot status in
-(*
-  let goal,mustdot =
-    let s = status#stack in
-    match s with
-    | [] -> fail (lazy "Invalid use of done")
-    | (g1, _, k, tag1) :: tl ->
-      let goals = filter_open g1 in
-      let (loc::tl) = goals in 
-      let goal = goal_of_loc (loc) in
-      if List.length k > 0 then
-        goal,true
-      else
-        goal,false
-  in
+let status_parameter key status =
+  match status#stack with
+    [] -> ""
+  | (_g,_t,_k,_tag,p)::_ -> try List.assoc key p with _ -> ""
+;;
 
-   *)
-(*
-      let goals = filter_open g1 in
-      let (loc::tl) = goals in 
-      let goal = goal_of_loc (loc) in
-      if tag1 == `BranchTag then
-        if List.length (shift_goals s) > 0 then (* must simply shift *)
-          (
-            prerr_endline (pp status#stack); 
-            prerr_endline "Head goals:";
-            List.map (fun goal -> prerr_endline (string_of_int goal)) (head_goals status#stack);
-            prerr_endline "Shift goals:";
-            List.map (fun goal -> prerr_endline (string_of_int goal)) (shift_goals status#stack);
-            prerr_endline "Open goals:";
-            List.map (fun goal -> prerr_endline (string_of_int goal)) (open_goals status#stack);
-            if tag2 == `BranchTag && g2 <> [] then 
-              goal,true,false,false
-            else if tag2 == `BranchTag then
-              goal,false,true,true
-            else
-              goal,false,true,false
-          )
-        else
-          (
-           if tag2 == `BranchTag then
-              goal,false,true,true
-            else
-              goal,false,true,false
-          )
+let beta_rewriting_step t status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx <> "beta_rewrite" then 
+    (
+      let newhypo = status_parameter "volatile_newhypo" status in
+      if newhypo = "" then
+        fail (lazy "Invalid use of 'that is equivalent to'")
       else
-        goal,false,false,false (* It's a strange situation, there's is an underlying level on the
-                                  stack but the current one was not created by a branch? Should be
-                                  an error *)
-    | (g, _, _, tag) :: [] ->
-      let (loc::tl) = filter_open g in 
-      let goal = goal_of_loc (loc) in
-      if tag == `BranchTag then
-(*         let goals = filter_open g in *)
-          goal,false,true,false
+        change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status
+    )
+  else
+    change_tac ~where:("",0,(None,[],Some
+                               Ast.UserInput)) ~with_what:t status
+;;
+
+let done_continuation status =
+  let rec continuation l =
+    match l with
+      [] -> []
+    | (_,t,_,tag,p)::tl ->
+      if tag = `BranchTag then
+        if List.length t > 0 then
+          let continue =
+            let ctx =
+              try List.assoc "context" p
+              with Not_found -> ""
+            in
+              ctx <> "induction" && ctx <> "cases"
+          in
+          if continue then [clear_volatile_params_tac;branch_dot_tac] else
+            [clear_volatile_params_tac]
+        else 
+          [merge_tac] @ (continuation tl)
       else
-        goal,false,false,false 
+        []
   in
-   *)
-  let l = [mk_just status goal just] in
-  let l =
-    if mustdot then List.append l [dot_tac] else l
-  in
-  (*
-  let l =
-    if mustmerge then List.append l [merge_tac] else l
-  in
-  let l =
-    if mustmergetwice then List.append l [merge_tac]  else l
-  in 
-     *)
-    block_tac l status
-(*
-  let (_,_,metasenv,subst,_) = status#obj in
-  let goal,last =
-    match metasenv with
-    | [] -> fail (lazy "There's nothing to prove")
-    | (_,_) :: (hd,_) :: tl -> hd,false
-    | (hd,_) :: tl -> hd,true
-  in
-  if last then
-    mk_just status goal just status
-  else
-    block_tac [ mk_just status goal just; shift_tac ] status
-*)
+    continuation status#stack
 ;;
 
-let we_need_to_prove t id t1 status =
+let bydone just status =
+  let goal = extract_first_goal_from_status status in
+  let continuation = done_continuation status in
+  let l = [mk_just status goal just] @ continuation in
+  block_tac l status
+;;
+
+let push_goals_tac status = 
+  match status#stack with
+    [] -> fail (lazy "Error pushing goals")
+  | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
+    if List.length g2 > 0 then
+      status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
+    else status (* Nothing to push *)
+  | _ -> status
+
+let we_need_to_prove t id status =
   let goal = extract_first_goal_from_status status in
   match id with
   | None ->
     (
-      match t1 with
-      | None ->  (* We need to prove t *)
-        (
-          try assert_tac t None status goal (id_tac status)
-          with
-          | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
-        )
-      | Some t1 -> (* We need to prove t or equivalently t1 *)
-        (
-          try assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some
-                                                                             Ast.UserInput)) ~with_what:t1 status)
-          with
-          | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
-          | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
-        )
+      try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
+      with
+      | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
     )
   | Some id ->
     (
-      match t1 with
-      (* We need to prove t (id) *)
-      | None -> block_tac [cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac;
-                           dot_tac
+      block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+                 push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite"
                           ] status
-      (* We need to prove t (id) or equivalently t1 *)
-      | Some t1 ->  block_tac [cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
-                                                                                  Ast.UserInput))
-                                 ~with_what:t1; shift_tac; intro_tac id; merge_tac;
-                               dot_tac
-                              ]
-                      status
     )
 ;;
 
-let by_just_we_proved just ty id ty' (*status*) =
-  distribute_tac (fun status goal ->
-    let wrappedjust = just in
-    let just = mk_just status goal just in
-    match id with
-    | None ->
-      (match ty' with
-       | None -> (* just we proved P done *)
-         (
-           try
-             assert_tac ty None status goal (exec (bydone wrappedjust) status goal)
-           with
-           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
-           | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
-         )
-       | Some ty' -> (* just we proved P that is equivalent to P' done *)
-         (
-           try
-             assert_tac ty' (Some ty) status goal (exec (block_tac [change_tac
-                                                                ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; bydone
-                                                                wrappedjust]) status goal)
-           with
-           | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
-           | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
-         )
-      )
-    | Some id ->
-      (
-        match ty' with
-        | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
-                               id; merge_tac ]) status goal
-        | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
-                                   id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None))
-                                   ~with_what:ty'; merge_tac]) status goal
-      )
-  )
-;;
-
-let thesisbecomes t1 t2 status = we_need_to_prove t1 None t2 status
+let by_just_we_proved just ty id status =
+  let goal = extract_first_goal_from_status status in
+  let just = mk_just status goal just in
+  match id with
+  | None ->
+    assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac
+                                                 "volatile_context" "beta_rewrite"] status)
+  | Some id ->
+    (
+      block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+                 clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status
+    )
 ;;
 
-let existselim just id1 t1 t2 id2 (*status*) =
-  distribute_tac (fun status goal ->
-    let (_,_,t1) = t1 in
-    let (_,_,t2) = t2 in
-    let just = mk_just status goal just in
-    exec (block_tac [
+let existselim just id1 t1 t2 id2 status =
+  let goal = extract_first_goal_from_status status in
+  let (_,_,t1) = t1 in
+  let (_,_,t2) = t2 in
+  let just = mk_just status goal just in
+  (block_tac [
       cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
                                                                                  (id1,None), Some t1),t2)]));
       branch_tac ~force:false;
@@ -332,27 +262,26 @@ let existselim just id1 t1 t2 id2 (*status*) =
       shift_tac;
       case1_tac "_";
       intros_tac ~names_ref:(ref []) [id1;id2];
-      merge_tac
-    ]) status goal
-  )
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status
 ;;
 
-let andelim just t1 id1 t2 id2 (*status*) =
-(*   let goal = extract_first_goal_from_status status in *)
-  distribute_tac (fun status goal ->
-    let (_,_,t1) = t1 in
-    let (_,_,t2) = t2 in
-    let just = mk_just status goal just in
-    exec (block_tac [
+let andelim just t1 id1 t2 id2 status =
+  let goal = extract_first_goal_from_status status in
+  let (_,_,t1) = t1 in
+  let (_,_,t2) = t2 in
+  let just = mk_just status goal just in
+  (block_tac [
       cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
       branch_tac ~force:false;
       just;
       shift_tac;
       case1_tac "_";
       intros_tac ~names_ref:(ref []) [id1;id2];
-      merge_tac
-    ]) status goal
-  )
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status
 ;;
 
 let type_of_tactic_term status ctx t =
@@ -360,100 +289,349 @@ let type_of_tactic_term status ctx t =
   let (_,cicty) = typeof status ctx cicterm in
   cicty
 
-let rewritingstep lhs rhs just last_step status =
+let swap_first_two_goals_tac status =
+  let gstatus =
+    match status#stack with
+    | [] -> assert false
+    | (g,t,k,tag,p) :: s ->
+      match g with
+      | (loc1) :: (loc2) :: tl ->
+        ([loc2;loc1] @+ tl,t,k,tag,p) :: s
+      | _ -> assert false
+  in
+  status#set_stack gstatus
+
+let thesisbecomes t1 = we_need_to_prove t1 None
+;;
+
+let obtain id t1 status =
   let goal = extract_first_goal_from_status status in
   let cicgty = get_goalty status goal in
   let ctx = ctx_of cicgty in
-  let _,gty = term_of_cic_term status cicgty ctx in
-  let cicty = type_of_tactic_term status ctx rhs in
+  let cicty = type_of_tactic_term status ctx t1 in
   let _,ty = term_of_cic_term status cicty ctx in
-  let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
-    match just with
-      `Auto (univ, params) ->
-      let params =
-        if not (List.mem_assoc "timeout" params) then
-          ("timeout","3")::params
-        else params
-      in
-      let params' =
-        if not (List.mem_assoc "paramodulation" params) then
-          ("paramodulation","1")::params
-        else params
+  let (_,_,t1) = t1 in
+  block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
+                                         `JustOne]));
+              swap_first_two_goals_tac;
+              branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+              add_parameter_tac "volatile_context" "rewrite"
+            ]
+    status
+;;
+
+let conclude t1 status =
+  let goal = extract_first_goal_from_status status in
+  let cicgty = get_goalty status goal in
+  let ctx = ctx_of cicgty in
+  let _,gty = term_of_cic_term status cicgty ctx in
+  match gty with
+    (* The first term of this Appl should probably be "eq" *)
+    NCic.Appl [_;_;plhs;_] ->
+    if alpha_eq_tacterm_kerterm t1 plhs status goal then
+      add_parameter_tac "volatile_context" "rewrite" status
+    else
+      fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+  | _ -> fail (lazy "Your conclusion needs to be an equality")
+;;
+
+let rewritingstep rhs just last_step status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx = "rewrite" then 
+    (
+      let goal = extract_first_goal_from_status status in
+      let cicgty = get_goalty status goal in
+      let ctx = ctx_of cicgty in
+      let _,gty = term_of_cic_term status cicgty ctx in
+      let cicty = type_of_tactic_term status ctx rhs in
+      let _,ty = term_of_cic_term status cicty ctx in
+      let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
+        match just with
+          `Auto (univ, params) ->
+          let params =
+            if not (List.mem_assoc "timeout" params) then
+              ("timeout","3")::params
+            else params
+          in
+          let params' =
+            if not (List.mem_assoc "paramodulation" params) then
+              ("paramodulation","1")::params
+            else params
+          in
+          if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
+          else
+            first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
+                         ~params:(univ, params') status goal]
+        | `Term just -> apply_tac just
+        | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
+        | `Proof -> id_tac
       in
-      if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
-      else
-        first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
-                     ~params:(univ, params') status goal]
-    | `Term just -> apply_tac just
-    | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
-    | `Proof -> id_tac
-  in
-  let plhs,prhs,prepare =
-    match lhs with
-      None -> (* = E2 *)
-      let plhs,prhs =
+      let plhs,prhs,prepare =
         match gty with (* Extracting the lhs and rhs of the previous equality *)
-          NCic.Appl [_;_;plhs;prhs] -> plhs,prhs
+          NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
         | _ -> fail (lazy "You are not building an equaility chain")
       in
-      plhs,prhs,
-      (fun continuation -> continuation status)
-    | Some (None,lhs) -> (* conclude *) 
-      let plhs,prhs =
-        match gty with
-          NCic.Appl [_;_;plhs;prhs] -> plhs,prhs
-        | _ -> fail (lazy "You are not building an equaility chain")
+      let continuation =
+        if last_step then
+          let todo = [just'] @ (done_continuation status) in
+          block_tac todo
+        else
+          let (_,_,rhs) = rhs in
+          block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
+                                               rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
       in
-      (*TODO*)
-      (*CSC: manca check plhs convertibile con lhs *)
-      plhs,prhs,
-      (fun continuation -> continuation status)
-    | Some (Some name,lhs) -> (* obtain *)
-      fail (lazy "Not implemented")
-        (*
-      let plhs = lhs in
-      let prhs = Cic.Meta(newmeta,irl) in
-      plhs,prhs,
-      (fun continuation ->
-         let metasenv = (newmeta, ctx, ty)::metasenv in
-         let mk_fresh_name_callback =
-           fun metasenv ctx _ ~typ ->
-             FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv ctx
-               (Cic.Name name) ~typ
-         in
-         let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
-         let proof,goals =
-           ProofEngineTypes.apply_tactic
-             (Tacticals.thens
-                ~start:(Tactics.cut ~mk_fresh_name_callback
-                          (Cic.Appl [eq ; ty ; lhs ; prhs]))
-                ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
-         in
-         let goals =
-           match just,goals with
-             `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
-           | _, [g1;g2] -> [g2;newmeta;g1]
-           | _, l ->
-             prerr_endline (String.concat "," (List.map string_of_int l));
-             prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
-             assert false
-         in
-         proof,goals)
-           *)
+      prepare continuation
+    )
+  else
+    fail (lazy "You are not building an equality chain")
+;;
+
+let rec pp_metasenv_names (metasenv:NCic.metasenv) =
+  match metasenv with
+    [] -> ""
+  | hd :: tl ->
+    let n,conj = hd in
+    let meta_attrs,_,_ = conj in
+    let rec find_name_aux meta_attrs = match meta_attrs with
+        [] -> "Anonymous"
+      | hd :: tl -> match hd with
+          `Name n -> n
+        | _ -> find_name_aux tl
+    in
+    let name = find_name_aux meta_attrs
+    in
+    "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
+;;
+
+let print_goals_names_tac s (status:#NTacStatus.tac_status) =
+  let (_,_,metasenv,_,_) = status#obj in
+  prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
+
+(* Useful as it does not change the order in the list *)
+let rec list_change_assoc k v = function
+    [] -> []
+  | (k',_v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+;;
+
+let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
+  let add_name_to_goal name goal metasenv =
+    let (mattrs,ctx,t) = try List.assoc goal metasenv with _ -> assert false in
+    let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+    let newconj = (mattrs,ctx,t) in
+    list_change_assoc goal newconj metasenv
   in
-  let continuation =
-    if last_step then
-      (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
-      let todo = [just'] in
-      let todo = if mustdot status then List.append todo [dot_tac] else todo
+  let new_goals =
+    (* It's important that this tactic is called before branching and right after the creation of
+     * the new goals, when they are still under focus *)
+    match status#stack with
+      [] -> fail (lazy "Can not add names to an empty stack")
+    | (g,_,_,_,_) :: _tl -> 
+      let rec sublist n = function
+          [] -> []
+        | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
       in
-        block_tac todo
-    else
-      let (_,_,rhs) = rhs in
-      block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
-                                           rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
+      List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+  in
+  let rec add_names_to_goals g cl metasenv =
+    match g,cl with
+      [],[] -> metasenv
+    | hd::tl, (_,consname,_)::tl' -> 
+      add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+    | _,_ -> fail (lazy "There are less goals than constructors")
+  in
+  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+  let newmetasenv = add_names_to_goals new_goals !cl metasenv
+  in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+;;
+(*
+  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+  let remove_name_from_metaattrs =
+   List.filter (function `Name _ -> false | _ -> true) in
+  let rec add_names_to_metasenv cl metasenv =
+    match cl,metasenv with
+      [],_ -> metasenv
+    | hd :: tl, mhd :: mtl ->
+      let _,consname,_ = hd in
+        let gnum,conj = mhd in
+        let mattrs,ctx,t = conj in
+        let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
+        in
+        let newconj = mattrs,ctx,t in
+        let newmeta = gnum,newconj in
+        newmeta :: (add_names_to_metasenv tl mtl)
+    | _,[] -> assert false
   in
-    prepare continuation
+  let newmetasenv = add_names_to_metasenv !cl metasenv in
+  status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
+*)
+
+let unfocus_branch_tac status =
+  match status#stack with
+    [] -> status
+  | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
+;;
+
+let we_proceed_by_induction_on t1 t2 status =
+  let goal = extract_first_goal_from_status status in
+  let txt,len,t1 = t1 in
+  let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let sort = ref (NCic.Rel 1) in
+  let cl = ref [] in (* this is a ref on purpose, as the block of code after sort_of_goal_tac in
+  block_tac acts as a block of asynchronous code, in which cl gets modified with the info retrieved
+  with analize_indty_tac, and later used to label each new goal with a costructor name. Using a
+  plain list this doesn't seem to work, as add_names_to_goals_tac would immediately act on an empty
+  list, instead of acting on the list of constructors *)
+  try
+    assert_tac t2 None status goal (block_tac [
+        analyze_indty_tac ~what:t1 indtyinfo;
+        sort_of_goal_tac sort;
+        (fun status ->
+           let ity = HExtlib.unopt !indtyinfo in
+           let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
+           let name =
+             NUri.name_of_uri uri ^ "_" ^
+             snd (NCicElim.ast_of_sort
+                    (match !sort with NCic.Sort x -> x | _ -> assert false))
+           in
+           let eliminator =
+             let l = [Ast.Ident (name,None)] in
+             (* Generating an implicit for each argument of the inductive type, plus one the
+              * predicate, plus an implicit for each constructor of the inductive type *)
+             let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
+             let _,_,t1 = t1 in
+             let l = l @ [t1] in
+             Ast.Appl l
+           in
+           cl := ity.cl;
+           exact_tac ("",0,eliminator) status);
+        add_names_to_goals_tac cl; 
+        branch_tac; 
+        push_goals_tac;
+        unfocus_branch_tac;
+        add_parameter_tac "context" "induction"
+      ] status)
+  with
+  | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let we_proceed_by_cases_on ((txt,len,ast1) as t1)  t2 status =
+  let goal = extract_first_goal_from_status status in
+  let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let cl = ref [] in
+  try
+    assert_tac t2 None status goal (block_tac [
+        analyze_indty_tac ~what:npt1 indtyinfo;
+        cases_tac ~what:t1 ~where:("",0,(None,[],Some
+                                           Ast.UserInput));
+        (
+          fun status ->
+            let ity = HExtlib.unopt !indtyinfo in
+            cl := ity.cl; add_names_to_goals_tac cl status
+        );
+        branch_tac; push_goals_tac;
+        unfocus_branch_tac;
+        add_parameter_tac "context" "cases"
+      ] status)
+  with
+  | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let byinduction t1 id status =
+  let ctx = status_parameter "context" status in
+  if ctx <> "induction" then fail (lazy "You can't use this tactic outside of an induction context")
+  else suppose t1 id status
+;;
+
+let name_of_conj conj =
+  let mattrs,_,_ = conj in
+  let rec search_name mattrs =
+    match mattrs with
+      [] -> "Anonymous"
+    | hd::tl ->
+      match hd with
+        `Name n -> n
+      | _ -> search_name tl
+  in
+  search_name mattrs
+
+let rec loc_of_goal goal l =
+  match l with
+    [] -> fail (lazy "Reached the end")
+  | hd :: tl ->
+    let _,sw = hd in
+    let g = goal_of_switch sw in
+    if g = goal then hd
+    else loc_of_goal goal tl
+;;
+
+let has_focused_goal status =
+  match status#stack with
+    [] -> false
+  | ([],_,_,_,_) :: _tl -> false
+  | _ -> true
+;;
+
+let focus_on_case_tac case status =
+  let (_,_,metasenv,_,_) = status#obj in
+  let rec goal_of_case case metasenv =
+    match metasenv with
+      [] -> fail (lazy "The given case does not exist")
+    | (goal,conj) :: tl ->
+      if name_of_conj conj = case then goal
+      else goal_of_case case tl
+  in
+  let goal_to_focus = goal_of_case case metasenv in
+  let gstatus =
+    match status#stack with
+      [] -> fail (lazy "There is nothing to prove")
+    | (g,t,k,tag,p) :: s ->
+      let loc = 
+        try 
+          loc_of_goal goal_to_focus t 
+        with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
+        context")
+      in
+      let curloc = if has_focused_goal status then 
+          let goal = extract_first_goal_from_status status in
+          [loc_of_goal goal g]
+        else []
+      in
+      (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
+  in 
+  status#set_stack gstatus
+;;
+
+let case id l status =
+  let ctx = status_parameter "context" status in
+  if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
+  induction/cases analysis context")
+else
+  (
+    if has_focused_goal status then fail (lazy "Finish the current case before switching")
+    else
+      (
+(*
+        let goal = extract_first_goal_from_status status in
+        let (_,_,metasenv,_,_) = status#obj in
+        let conj = NCicUtils.lookup_meta goal metasenv in
+        let name = name_of_conj conj in
+*)
+        let continuation =
+          let rec aux l =
+            match l with
+              [] -> [id_tac]
+            | (id,ty)::tl ->
+              (try_tac (assume id ("",0,ty))) :: (aux tl)
+          in
+          aux l
+        in
+(*         if name = id then block_tac continuation status *)
+(*         else  *)
+          block_tac ([focus_on_case_tac id] @ continuation) status
+      )
+  )
 ;;
 
 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;