Many changes

Add a BetaRewritingStep tactic, for multiple 'or equivalently'
statements in theorems proofs

Remove old code

Add a key-value list to the tiny-cals stack (parameters list) for
context related infos. Can be used as a general purpose store for
key-value pairs

Adapt code that works on the stack to work with the new parameter list

Add function to add and retrieve key-value pairs to the parameters list

Add the concept of volatile-context: they are contexts that are cleared
after the application of some tactics. E.g., the context for a
beta_rewriting (sequence of 'or equivalently') is a volatile context, as
any tactic breaks the chain

Add a function to clear volatile parameters from the paramters list

Add a case in extract_first_goal_from_status for the case where the
stack is empty

Make the tactics that make use of distribute High tactics

Reimplement the dot tac on top of the stack to handle branching. This
makes use of the second iterator list of the stack

Add a "done_continuation" function that checks whether it needs to dot
or recursively merge branches after a done statement

Add a function to push goals from the focus iterator list of the
previous level on the stack to the second iteretaor list of the current
level

Change conclude and obtain to use a volatile context to obligate the
user to only use = inside it

Change the add_names_to_goals function to use the stack instead of the
metasenv directly

Add a unfocus_branch_tac to unfocus from goals in a stack level (useful
for cases and induction)

Change induction and cases to use a context to obligate the user to use
case only inside it. Furthermore, the new stack based branching for
declarative tactics obligates the user to only switch between cases of
the last level

Change induction and cases to start without focusing on any goal and
without automatically focusing on the next goal after a done. The user
is compelled to use case to switch between each case

Change the case to only change case when the current case has been dealt
with

Attempt to fix automation

Add first draft for matita's helper

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index c4ec503c797a2418b66ea0dcfc8c39359f747b80..c29babd55414b1fd3b1d7b75e23f3ebdb6eadf60 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -85,6 +85,7 @@ type ntactic =
    justification, conclusion, identifier, eqconcl *)
    | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
    identifier, equivnewcon *)
    justification, conclusion, identifier, eqconcl *)
    | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
    identifier, equivnewcon *)

+   | BetaRewritingStep of loc * nterm

    | Bydone of loc * just
    | ExistsElim of loc * just * string * nterm * nterm * string
    | AndElim of loc * just * nterm * string * nterm * string
    | Bydone of loc * just
    | ExistsElim of loc * just * string * nterm * nterm * string
    | AndElim of loc * just * nterm * string * nterm * string

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index a4a5788d9fbb4c1a637cb95259f5f4618137c5dc..e8864255d28e27a864429ad0df541a605e285ca7 100644 (file)
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -127,17 +127,20 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | By_just_we_proved (_, just, term1, ident, term2) -> pp_just status just  ^ "we proved" ^
   NotationPp.pp_term status term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match
   term2 with  None -> " " | Some term2 -> " that is equivalent to " ^ NotationPp.pp_term status term2)
   | By_just_we_proved (_, just, term1, ident, term2) -> pp_just status just  ^ "we proved" ^
   NotationPp.pp_term status term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match
   term2 with  None -> " " | Some term2 -> " that is equivalent to " ^ NotationPp.pp_term status term2)

-  | We_need_to_prove (_,term,ident,term1) -> "we need to prove" ^ NotationPp.pp_term status term ^
-  (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match term1 with None -> " " | Some t1
-  -> "or equivalently" ^ NotationPp.pp_term status t1)
+  | We_need_to_prove (_,term,ident,t) -> "we need to prove" ^ NotationPp.pp_term status term ^
+  (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match t with None -> "" | Some t ->
+      " or equivalently " ^ (NotationPp.pp_term status t))
+  | BetaRewritingStep (_,t) -> "or equivalently " ^ (NotationPp.pp_term status t)

   | Bydone (_, just) -> pp_just status just ^ "done"
   | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":"
   ^ NotationPp.pp_term status term ^ "such that " ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
   | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^
   NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2
   ^ " (" ^ ident2 ^ ")" 
   | Bydone (_, just) -> pp_just status just ^ "done"
   | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":"
   ^ NotationPp.pp_term status term ^ "such that " ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
   | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^
   NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2
   ^ " (" ^ ident2 ^ ")" 

-  | Thesisbecomes (_, term1, term2) -> "the thesis becomes " ^ NotationPp.pp_term status term1 ^ (match
-  term2 with None -> " " | Some term2 -> NotationPp.pp_term status term2)
+  | Thesisbecomes (_, t, t1) -> "the thesis becomes " ^ NotationPp.pp_term status t ^
+                                   (match t1 with None -> "" | Some t1 -> " or equivalently " ^
+                                                                          NotationPp.pp_term status
+                                                                            t1)

   | RewritingStep (_, rhs, just, cont) -> 
       "=" ^
       NotationPp.pp_term status rhs ^ 
   | RewritingStep (_, rhs, just, cont) -> 
       "=" ^
       NotationPp.pp_term status rhs ^ 


@@ -147,22 +150,6 @@ let rec pp_ntactic status ~map_unicode_to_tex =
       | `Proof -> " proof"
       | `SolveWith t -> " using " ^ NotationPp.pp_term status t)
       ^ (if cont then " done" else "")
       | `Proof -> " proof"
       | `SolveWith t -> " using " ^ NotationPp.pp_term status t)
       ^ (if cont then " done" else "")

-(*
-  | RewritingStep (_, term, term1, term2, cont) -> 
-      (match term with 
-      | None -> " " 
-      | Some (None,term) -> "conclude " ^ NotationPp.pp_term status term 
-      | Some (Some name,term) -> 
-          "obtain (" ^ name ^ ") " ^ NotationPp.pp_term status term) 
-      ^ "=" ^
-      NotationPp.pp_term status term1 ^ 
-      (match term2 with 
-      | `Auto params -> pp_auto_params params status
-      | `Term term2 -> " exact " ^ NotationPp.pp_term status term2 
-      | `Proof -> " proof"
-      | `SolveWith term -> " using " ^ NotationPp.pp_term status term)
-      ^ (if cont then " done" else "")
-*)

   | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ NotationPp.pp_term status t1
   | Conclude (_,t1) -> "conclude " ^ NotationPp.pp_term status t1
   | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status  term1
   | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ NotationPp.pp_term status t1
   | Conclude (_,t1) -> "conclude " ^ NotationPp.pp_term status t1
   | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status  term1

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index f2876d2a9b6fb977cd0a42e5103ed85dbd657545..ee0573ae741c828201dee08d05f09345fa611628 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -499,8 +499,9 @@ let eval_ng_tac tac =
   |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
   (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
   Some t2 -> (Some (text,prefix_len,t2)))
   |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
   (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
   Some t2 -> (Some (text,prefix_len,t2)))

-  |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id
-  (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+  |GrafiteAst.We_need_to_prove (_, t, id, t1) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+  (match t1 with None -> None | Some t1 -> Some (text,prefix_len,t1))
+  |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t)

   | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
   | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
      Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1)
   | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
   | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
      Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1)


@@ -508,7 +509,7 @@ let eval_ng_tac tac =
   | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
     text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
   | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1)
   | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
     text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
   | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1)

-  (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2)))
+  (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))

   | GrafiteAst.RewritingStep (_,rhs,just,cont) ->
      Declarative.rewritingstep (text,prefix_len,rhs)
                                 (match just with 
   | GrafiteAst.RewritingStep (_,rhs,just,cont) ->
      Declarative.rewritingstep (text,prefix_len,rhs)
                                 (match just with 

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index eaf0c4c01097e10ef8aa02ec60ee202ce7cb818a..5acdf2bd0b7e93a398d3d25e98e6520be9699819 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -267,10 +267,13 @@ EXTEND
          | BYC_wehaveand (id1,t1,id2,t2) ->
             G.AndElim (loc, just, t1, id1, t2, id2))
         ])
          | BYC_wehaveand (id1,t1,id2,t2) ->
             G.AndElim (loc, just, t1, id1, t2, id2))
         ])

-    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id =
+IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term ->
+t']->

         G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)])
         G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)])

+    | IDENT "or"; IDENT "equivalently"; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])

     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT
     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT

-    "equivalently"; t2 = tactic_term -> t2] ->
+"equivalently"; t2 = tactic_term -> t2] ->

         G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])
         G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])

diff --git a/matita/components/ng_tactics/continuationals.ml b/matita/components/ng_tactics/continuationals.ml
index b1087713009670ef9bcbedcfe8f1cea40942363c..5538a3c2d0f985cfeecaf72d046f299e58619032 100644 (file)
--- a/matita/components/ng_tactics/continuationals.ml
+++ b/matita/components/ng_tactics/continuationals.ml
@@ -35,21 +35,23 @@ let fail msg = raise (Error msg)
 
 type goal = int
 
 
 type goal = int
 

+type parameters = (string * string) list
+

 module Stack =
 struct
   type switch = Open of goal | Closed of goal
   type locator = int * switch
   type tag = [ `BranchTag | `FocusTag | `NoTag ]
 module Stack =
 struct
   type switch = Open of goal | Closed of goal
   type locator = int * switch
   type tag = [ `BranchTag | `FocusTag | `NoTag ]

-  type entry = locator list * locator list * locator list * tag
+  type entry = locator list * locator list * locator list * tag * parameters

   type t = entry list
 
   type t = entry list
 

-  let empty = [ [], [], [], `NoTag ]
+  let empty = [ [], [], [], `NoTag , []]

 
   let fold ~env ~cont ~todo init stack =
     let rec aux acc depth =
       function
       | [] -> acc
 
   let fold ~env ~cont ~todo init stack =
     let rec aux acc depth =
       function
       | [] -> acc

-      | (locs, todos, conts, tag) :: tl ->
+      | (locs, todos, conts, tag, p) :: tl ->

           let acc = List.fold_left (fun acc -> env acc depth tag)  acc locs in
           let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
           let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
           let acc = List.fold_left (fun acc -> env acc depth tag)  acc locs in
           let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
           let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in


@@ -64,10 +66,10 @@ struct
   let map ~env ~cont ~todo =
     let depth = ref ~-1 in
     List.map
   let map ~env ~cont ~todo =
     let depth = ref ~-1 in
     List.map

-      (fun (s, t, c, tag) ->
+      (fun (s, t, c, tag, p) ->

         incr depth;
         let d = !depth in
         incr depth;
         let d = !depth in

-        env d tag s, todo d tag t, cont d tag c, tag)
+        env d tag s, todo d tag t, cont d tag c, tag, p)

 
   let is_open = function _, Open _ -> true | _ -> false
   let close = function n, Open g -> n, Closed g | l -> l
 
   let is_open = function _, Open _ -> true | _ -> false
   let close = function n, Open g -> n, Closed g | l -> l


@@ -103,39 +105,39 @@ struct
   let rec find_goal =
     function
     | [] -> raise (Failure "Continuationals.find_goal")
   let rec find_goal =
     function
     | [] -> raise (Failure "Continuationals.find_goal")

-    | (l :: _,   _   ,   _   , _) :: _ -> goal_of_loc l
-    | (  _   ,   _   , l :: _, _) :: _ -> goal_of_loc l
-    | (  _   , l :: _,   _   , _) :: _ -> goal_of_loc l
+    | (l :: _,   _   ,   _   , _, _) :: _ -> goal_of_loc l
+    | (  _   ,   _   , l :: _, _, _) :: _ -> goal_of_loc l
+    | (  _   , l :: _,   _   , _, _) :: _ -> goal_of_loc l

     | _ :: tl -> find_goal tl
 
   let is_empty =
     function
     | [] -> assert false
     | _ :: tl -> find_goal tl
 
   let is_empty =
     function
     | [] -> assert false

-    | [ [], [], [], `NoTag ] -> true
+    | [ [], [], [], `NoTag , _] -> true

     | _ -> false
 
   let of_nmetasenv metasenv =
     let goals = List.map (fun (g, _) -> g) metasenv in
     | _ -> false
 
   let of_nmetasenv metasenv =
     let goals = List.map (fun (g, _) -> g) metasenv in

-    [ zero_pos goals, [], [], `NoTag ]
+    [ zero_pos goals, [], [], `NoTag , []]

 
   let head_switches =
     function
 
   let head_switches =
     function

-    | (locs, _, _, _) :: _ -> List.map switch_of_loc locs
+    | (locs, _, _, _, _) :: _ -> List.map switch_of_loc locs

     | [] -> assert false
 
   let head_goals =
     function
     | [] -> assert false
 
   let head_goals =
     function

-    | (locs, _, _, _) :: _ -> List.map goal_of_loc locs
+    | (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs

     | [] -> assert false
 
   let head_tag =
     function
     | [] -> assert false
 
   let head_tag =
     function

-    | (_, _, _, tag) :: _ -> tag
+    | (_, _, _, tag, _) :: _ -> tag

     | [] -> assert false
 
   let shift_goals =
     function
     | [] -> assert false
 
   let shift_goals =
     function

-    | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs
+    | _ :: (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs

     | [] -> assert false
     | _ -> []
 
     | [] -> assert false
     | _ -> []
 


@@ -163,9 +165,10 @@ struct
     let pp_loc (i, s) = string_of_int i ^ pp_switch s in
     let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
     let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
     let pp_loc (i, s) = string_of_int i ^ pp_switch s in
     let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
     let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in

-    let pp_stack_entry (env, todo, cont, tag) =
-      sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
-        (pp_tag tag)
+    let pp_par = function [] -> "" | _ as l -> List.fold_left (fun acc (k,v) -> acc ^ "K: " ^ k ^ " V: " ^ v ^ "; ") "" l in
+    let pp_stack_entry (env, todo, cont, tag, parameters) =
+      sprintf "(%s, %s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
+        (pp_tag tag) (pp_par parameters)

     in
     String.concat " :: " (List.map pp_stack_entry stack)
 end
     in
     String.concat " :: " (List.map pp_stack_entry stack)
 end


@@ -270,7 +273,7 @@ struct
     let ostatus, stack =
       match cmd, stack with
       | _, [] -> assert false
     let ostatus, stack =
       match cmd, stack with
       | _, [] -> assert false

-      | Tactical tac, (g, t, k, tag) :: s ->
+      | Tactical tac, (g, t, k, tag, p) :: s ->

 (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A 
  *   auto paramodulation.try assumption.
  * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO.
 (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A 
  *   auto paramodulation.try assumption.
  * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO.


@@ -300,49 +303,49 @@ struct
           debug_print (lazy ("closed: "
             ^ String.concat " " (List.map string_of_int gcn)));
           let stack =
           debug_print (lazy ("closed: "
             ^ String.concat " " (List.map string_of_int gcn)));
           let stack =

-            (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+            (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s

           in
           sn, stack
           in
           sn, stack

-      | Dot, ([], _, [], _) :: _ ->
+      | Dot, ([], _, [], _, _) :: _ ->

           (* backward compatibility: do-nothing-dot *)
           new_stack stack
           (* backward compatibility: do-nothing-dot *)
           new_stack stack

-      | Dot, (g, t, k, tag) :: s ->
+      | Dot, (g, t, k, tag, p) :: s ->

           (match filter_open g, k with
           (match filter_open g, k with

-          | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s)
+          | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag, p) :: s)

           | [], loc :: k ->
               assert (is_open loc);
           | [], loc :: k ->
               assert (is_open loc);

-              new_stack (([ loc ], t, k, tag) :: s)
+              new_stack (([ loc ], t, k, tag, p) :: s)

           | _ -> fail (lazy "can't use \".\" here"))
       | Semicolon, _ -> new_stack stack
           | _ -> fail (lazy "can't use \".\" here"))
       | Semicolon, _ -> new_stack stack

-      | Branch, (g, t, k, tag) :: s ->
+      | Branch, (g, t, k, tag, p) :: s ->

           (match init_pos g with
           | [] | [ _ ] -> fail (lazy "too few goals to branch");
           | loc :: loc_tl ->
               new_stack
           (match init_pos g with
           | [] | [ _ ] -> fail (lazy "too few goals to branch");
           | loc :: loc_tl ->
               new_stack

-                (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
-      | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+                (([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag,p) :: s))
+      | Shift, (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->

           (match g' with
           | [] -> fail (lazy "no more goals to shift")
           | loc :: loc_tl ->
               new_stack
           (match g' with
           | [] -> fail (lazy "no more goals to shift")
           | loc :: loc_tl ->
               new_stack

-                (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
-                :: (loc_tl, t', k', tag) :: s))
+                (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
+                :: (loc_tl, t', k', tag, p') :: s))

       | Shift, _ -> fail (lazy "can't shift goals here")
       | Shift, _ -> fail (lazy "can't shift goals here")

-      | Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+      | Pos i_s, ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s

         when is_fresh loc ->
           let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
           new_stack
         when is_fresh loc ->
           let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
           new_stack

-            ((l_js, t , [],`BranchTag)
-             :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+            ((l_js, t , [],`BranchTag, p)
+             :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)

       | Pos _, _ -> fail (lazy "can't use relative positioning here")
       | Pos _, _ -> fail (lazy "can't use relative positioning here")

-      | Wildcard, ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+      | Wildcard, ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s

           when is_fresh loc ->
             new_stack
           when is_fresh loc ->
             new_stack

-              (([loc] @+ g', t, [], `BranchTag)
-                :: ([], t', k', tag) :: s)
+              (([loc] @+ g', t, [], `BranchTag, p)
+                :: ([], t', k', tag, p') :: s)

       | Wildcard, _ -> fail (lazy "can't use wildcard here")
       | Wildcard, _ -> fail (lazy "can't use wildcard here")

-      | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
-          new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+      | Merge, (g, t, k,`BranchTag,_) :: (g', t', k', tag,p') :: s ->
+          new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag, p') :: s)

       | Merge, _ -> fail (lazy "can't merge goals here")
       | Focus [], _ -> assert false
       | Focus gs, s ->
       | Merge, _ -> fail (lazy "can't merge goals here")
       | Focus [], _ -> assert false
       | Focus gs, s ->


@@ -355,8 +358,8 @@ struct
               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
             gs;
               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
             gs;

-          new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
-      | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
+          new_stack ((zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s)
+      | Unfocus, ([], [], [], `FocusTag, _) :: s -> new_stack s

       | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
     in
     debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
       | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
     in
     debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));

diff --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli
index 1dcf4aa7dc8fcc2a61af433ec7bb661a42520e32..d3fdf716c895d7a86b3c58ac01b79d8e4684a17f 100644 (file)
--- a/matita/components/ng_tactics/continuationals.mli
+++ b/matita/components/ng_tactics/continuationals.mli
@@ -29,12 +29,15 @@ type goal = int
 
 (** {2 Goal stack} *)
 
 
 (** {2 Goal stack} *)
 

+(* Key value pairs *)
+type parameters = (string * string) list
+

 module Stack:
 sig
   type switch = Open of goal | Closed of goal
   type locator = int * switch
   type tag = [ `BranchTag | `FocusTag | `NoTag ]
 module Stack:
 sig
   type switch = Open of goal | Closed of goal
   type locator = int * switch
   type tag = [ `BranchTag | `FocusTag | `NoTag ]

-  type entry = locator list * locator list * locator list * tag
+  type entry = locator list * locator list * locator list * tag * parameters

   type t = entry list
 
   val empty: t
   type t = entry list
 
   val empty: t

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index b01f4259da6bf0a37aad09fc8970cfe7869b4825..41584d1d3803237b43639b8bce94118a83a6fc88 100644 (file)
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -43,11 +43,13 @@ let extract_first_goal_from_status status =
   let s = status#stack in
   match s with
   | [] -> fail (lazy "There's nothing to prove")
   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 goals = filter_open g1 in

-    let (loc::tl) = goals in
-    let goal = goal_of_loc (loc) in
-    goal ;;
+    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 extract_conclusion_type status goal =
   let gty = get_goalty status goal in


@@ -75,6 +77,23 @@ let are_convertible ty1 ty2 status goal =
   let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
   NTacStatus.are_convertible status ctx cicterm1 cicterm2
 
   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)
+;;
+

 (* 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. ?
 (* 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. ?


@@ -86,38 +105,36 @@ let lambda_abstract_tac id t1 t2 status goal =
       match t2 with
       | None ->
         let (_,_,t1) = t1 in
       match t2 with
       | None ->
         let (_,_,t1) = t1 in

-        exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
-                                       `JustOne))) (*status*)
+        block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+                                                  `JustOne))); clear_volatile_params_tac] status

       | Some t2 ->
         let status,res = are_convertible t1 t2 status goal in
         if res then
           let (_,_,t2) = t2 in
       | 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*)
+          block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
+                                                    `JustOne))); clear_volatile_params_tac] status

         else
           raise NotEquivalentTypes
     else
       raise FirstTypeWrong
   | _ -> raise NotAProduct
 
         else
           raise NotEquivalentTypes
     else
       raise FirstTypeWrong
   | _ -> raise NotAProduct
 

-let assume name ty eqty =
-  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 eqty status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac name ty eqty 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 =
-  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 t2 status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac id t1 t2 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 assert_tac t1 t2 status goal continuation =


@@ -133,26 +150,76 @@ let assert_tac t1 t2 status goal continuation =
   else
     raise FirstTypeWrong
 
   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
     else

-      false
+      status
+  | _ -> status
+;;
+
+let status_parameter key status =
+  match status#stack with
+    [] -> ""
+  | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
+;;
+
+let beta_rewriting_step t status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx <> "beta_rewrite" then fail (lazy "Invalid use of 'or equivalently'")
+  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
+        []
+  in
+    continuation status#stack
+;;

 
 let bydone just status =
   let goal = extract_first_goal_from_status status in
 
 let bydone just status =
   let goal = extract_first_goal_from_status status in

-  let mustdot = mustdot status in
-  let l = [mk_just status goal just] in
-  let l =
-    if mustdot then List.append l [dot_tac] else l
-  in
+  let continuation = done_continuation status in
+  let l = [mk_just status goal just] @ continuation in

   block_tac l status
 ;;
 
   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 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)
+;;
+

 let we_need_to_prove t id t1 status =
   let goal = extract_first_goal_from_status status in
   match id with
 let we_need_to_prove t id t1 status =
   let goal = extract_first_goal_from_status status in
   match id with


@@ -161,14 +228,17 @@ let we_need_to_prove t id t1 status =
       match t1 with
       | None ->  (* We need to prove t *)
         (
       match t1 with
       | None ->  (* We need to prove t *)
         (

-          try assert_tac t None status goal (id_tac status)
+          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 t1 -> (* We need to prove t or equivalently t1 *)
         (
           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)
+          try assert_tac t (Some t1) status goal (block_tac [change_tac ~where:("",0,(None,[],Some
+                                                                             Ast.UserInput))
+                                                               ~with_what:t1;
+                                                             add_parameter_tac "volatile_context"
+                                                               "beta_rewrite"] status)

           with
           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
           | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
           with
           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
           | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")


@@ -178,14 +248,14 @@ let we_need_to_prove t id t1 status =
     (
       match t1 with
       (* We need to prove t (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
+      | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+                           push_goals_tac

                           ] status
       (* We need to prove t (id) or equivalently t1 *)
                           ] 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
+      | Some t1 ->  block_tac [clear_volatile_params_tac; cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some

                                                                                   Ast.UserInput))
                                  ~with_what:t1; shift_tac; intro_tac id; merge_tac;
                                                                                   Ast.UserInput))
                                  ~with_what:t1; shift_tac; intro_tac id; merge_tac;

-                               dot_tac
+                               branch_tac; push_goals_tac

                               ]
                       status
     )
                               ]
                       status
     )


@@ -221,46 +291,47 @@ let by_just_we_proved just ty id ty' status =
   | Some id ->
     (
       match ty' with
   | Some id ->
     (
       match ty' with

-      | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac ] status
+      | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+                           clear_volatile_params_tac ] status

       | Some ty' -> 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';
       | Some ty' -> 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
+                               merge_tac; clear_volatile_params_tac] status

     )
 ;;
 
     )
 ;;
 

-let existselim just id1 t1 t2 id2 =
-  distribute_tac (fun status goal ->
-      let (_,_,t1) = t1 in
-      let (_,_,t2) = t2 in
-      let just = mk_just status goal just in
-      exec (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;
-          just;
-          shift_tac;
-          case1_tac "_";
-          intros_tac ~names_ref:(ref []) [id1;id2];
-          merge_tac
-        ]) status goal
-    )
+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;
+      just;
+      shift_tac;
+      case1_tac "_";
+      intros_tac ~names_ref:(ref []) [id1;id2];
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status

 ;;
 
 ;;
 

-let andelim just t1 id1 t2 id2  =
-  distribute_tac (fun status goal ->
-      let (_,_,t1) = t1 in
-      let (_,_,t2) = t2 in
-      let just = mk_just status goal just in
-      exec (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
-    )
+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;
+      clear_volatile_params_tac
+    ]) status

 ;;
 
 let type_of_tactic_term status ctx t =
 ;;
 
 let type_of_tactic_term status ctx t =


@@ -272,15 +343,15 @@ let swap_first_two_goals_tac status =
   let gstatus =
     match status#stack with
     | [] -> assert false
   let gstatus =
     match status#stack with
     | [] -> assert false

-    | (g,t,k,tag) :: s ->
+    | (g,t,k,tag,p) :: s ->

       match g with
       | (loc1) :: (loc2) :: tl ->
       match g with
       | (loc1) :: (loc2) :: tl ->

-        ([loc2;loc1] @+ tl,t,k,tag) :: s
+        ([loc2;loc1] @+ tl,t,k,tag,p) :: s

       | _ -> assert false
   in
   status#set_stack gstatus
 
       | _ -> assert false
   in
   status#set_stack gstatus
 

-let thesisbecomes t1 t2 = we_need_to_prove t1 None t2
+let thesisbecomes t1 l = we_need_to_prove t1 None l

 ;;
 
 let obtain id t1 status =
 ;;
 
 let obtain id t1 status =


@@ -293,72 +364,78 @@ let obtain id t1 status =
   block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
                                          `JustOne]));
               swap_first_two_goals_tac;
   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; dot_tac;
+              branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+              add_parameter_tac "volatile_context" "rewrite"

             ]
     status
 ;;
 
             ]
     status
 ;;
 

-let conclude t1 =
-  distribute_tac (fun status goal ->
-      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
-        NCic.Appl [_;_;plhs;_] ->
-        if alpha_eq_tacterm_kerterm t1 plhs status goal then
-          exec id_tac status goal
-        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 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
   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
+  match gty with
+    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
       in

-      let params' =
-        if not (List.mem_assoc "paramodulation" params) then
-          ("paramodulation","1")::params
-        else params
+      let plhs,prhs,prepare =
+        match gty with (* Extracting the lhs and rhs of the previous equality *)
+          NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+        | _ -> fail (lazy "You are not building an equaility chain")

       in
       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 gty with (* Extracting the lhs and rhs of the previous equality *)
-      NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
-    | _ -> fail (lazy "You are not building an equaility chain")
-  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 continuation =
+        if last_step then
+          (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
+          let todo = [just'] @ (done_continuation status) in
+          (*       let todo = if mustdot status then List.append todo [dot_tac] else todo *)
+          (*       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
       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
-  prepare continuation
+      prepare continuation
+    )
+  else
+    fail (lazy "You are not building an equality chain")

 ;;
 
 let rec pp_metasenv_names (metasenv:NCic.metasenv) =
 ;;
 
 let rec pp_metasenv_names (metasenv:NCic.metasenv) =


@@ -382,24 +459,51 @@ let print_goals_names_tac s (status:#NTacStatus.tac_status) =
   let (_,_,metasenv,_,_) = status#obj in
   prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); 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_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =

-  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
-  let rec remove_name_from_metaattrs mattrs =
-    match mattrs with
-      [] -> []
-    | hd :: tl ->
-      match hd with
-        `Name n -> remove_name_from_metaattrs tl
-      | _ as it -> it :: (remove_name_from_metaattrs tl)
+  let add_name_to_goal name goal metasenv =
+    let (mattrs,ctx,t as conj) = 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 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
+      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
   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 =
   let rec add_names_to_metasenv cl metasenv =

-    match cl with
-      [] -> metasenv
-    | hd :: tl ->
-      let _,consname,_ = hd
-      in match metasenv with
-        [] -> []
-      | mhd :: mtl ->
+    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)
         let gnum,conj = mhd in
         let mattrs,ctx,t = conj in
         let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)


@@ -407,9 +511,17 @@ let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.ta
         let newconj = mattrs,ctx,t in
         let newmeta = gnum,newconj in
         newmeta :: (add_names_to_metasenv tl mtl)
         let newconj = mattrs,ctx,t in
         let newmeta = gnum,newconj in
         newmeta :: (add_names_to_metasenv tl mtl)

+    | _,[] -> assert false

   in
   let newmetasenv = add_names_to_metasenv !cl metasenv in
   status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
   in
   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 we_proceed_by_induction_on t1 t2 status =
   let goal = extract_first_goal_from_status status in


@@ -431,16 +543,22 @@ let we_proceed_by_induction_on t1 t2 status =
                     (match !sort with NCic.Sort x -> x | _ -> assert false))
            in
            let eliminator =
                     (match !sort with NCic.Sort x -> x | _ -> assert false))
            in
            let eliminator =

-             let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
-             (* Generating as many implicits as open goals *)
-             let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
+             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);
              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; dot_tac] 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")
 ;;
   with
   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 ;;


@@ -455,14 +573,15 @@ let we_proceed_by_cases_on ((txt,len,ast1) as t1)  t2 status =
         analyze_indty_tac ~what:npt1 indtyinfo;
         cases_tac ~what:t1 ~where:("",0,(None,[],Some
                                            Ast.UserInput));
         analyze_indty_tac ~what:npt1 indtyinfo;
         cases_tac ~what:t1 ~where:("",0,(None,[],Some
                                            Ast.UserInput));

-        print_goals_names_tac "Pre Adding";

         (
           fun status ->
             let ity = HExtlib.unopt !indtyinfo in
             cl := ity.cl; add_names_to_goals_tac cl status
         );
         (
           fun status ->
             let ity = HExtlib.unopt !indtyinfo in
             cl := ity.cl; add_names_to_goals_tac cl status
         );

-        print_goals_names_tac "Post Adding";
-        dot_tac] 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")
 ;;
   with
   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 ;;


@@ -491,8 +610,14 @@ let rec loc_of_goal goal l =
     else loc_of_goal goal tl
 ;;
 
     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 focus_on_case_tac case status =

-  let goal = extract_first_goal_from_status status in

   let (_,_,metasenv,_,_) = status#obj in
   let rec goal_of_case case metasenv =
     match metasenv with
   let (_,_,metasenv,_,_) = status#obj in
   let rec goal_of_case case metasenv =
     match metasenv with


@@ -505,28 +630,52 @@ let focus_on_case_tac case status =
   let gstatus =
     match status#stack with
       [] -> fail (lazy "There is nothing to prove")
   let gstatus =
     match status#stack with
       [] -> fail (lazy "There is nothing to prove")

-    | (g,t,k,tag) :: s ->
-      let loc = loc_of_goal goal_to_focus k in
-      let curloc = loc_of_goal goal g in
-      (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s
-  in status#set_stack gstatus
+    | (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 case id l status =

-  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) None)) :: (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 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) None)) :: (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 ;;
 ;;
 
 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;

diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli
index 24b85a608f0db7dda26016c52a2991cd0d51d92b..cfbbac7dca14db2bcec4374b226b4a0eddc20a53 100644 (file)
--- a/matita/components/ng_tactics/declarative.mli
+++ b/matita/components/ng_tactics/declarative.mli
@@ -28,6 +28,7 @@ type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
 val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
 val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
 val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
 val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
 val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
 val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic

+val beta_rewriting_step : NTacStatus.tactic_term -> 's NTacStatus.tactic

 val bydone : just -> 's NTacStatus.tactic
 val by_just_we_proved : just -> NTacStatus.tactic_term -> string option  -> NTacStatus.tactic_term
 option -> 's NTacStatus.tactic
 val bydone : just -> 's NTacStatus.tactic
 val by_just_we_proved : just -> NTacStatus.tactic_term -> string option  -> NTacStatus.tactic_term
 option -> 's NTacStatus.tactic

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 8e73f53056b65dd117103e9d3e7ef17f7912c229..a8a78999a2b9c3b71a4ea20a93ffab8250d870d0 100644 (file)
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -31,16 +31,16 @@ let dot_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | ([], _, [], _) :: _ as stack ->
+    | ([], _, [], _, _) :: _ as stack ->

         (* backward compatibility: do-nothing-dot *)
         stack
         (* backward compatibility: do-nothing-dot *)
         stack

-    | (g, t, k, tag) :: s ->
+    | (g, t, k, tag, p) :: s ->

         match filter_open g, k with
         | loc :: loc_tl, _ -> 
         match filter_open g, k with
         | loc :: loc_tl, _ -> 

-             (([ loc ], t, loc_tl @+ k, tag) :: s) 
+             (([ loc ], t, loc_tl @+ k, tag, p) :: s) 

         | [], loc :: k ->
             assert (is_open loc);
         | [], loc :: k ->
             assert (is_open loc);

-            (([ loc ], t, k, tag) :: s)
+            (([ loc ], t, k, tag, p) :: s)

         | _ -> fail (lazy "can't use \".\" here")
   in
    status#set_stack gstatus
         | _ -> fail (lazy "can't use \".\" here")
   in
    status#set_stack gstatus


@@ -50,12 +50,12 @@ let branch_tac ?(force=false) status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | (g, t, k, tag) :: s ->
+    | (g, t, k, tag, p) :: s ->

           match init_pos g with (* TODO *)
           | [] -> fail (lazy "empty goals")
           | [_] when (not force) -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
           match init_pos g with (* TODO *)
           | [] -> fail (lazy "empty goals")
           | [_] when (not force) -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->

-               ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
+            ([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag, p) :: s

   in
    status#set_stack gstatus
 ;;
   in
    status#set_stack gstatus
 ;;


@@ -63,12 +63,12 @@ let branch_tac ?(force=false) status =
 let shift_tac status =
   let gstatus = 
     match status#stack with
 let shift_tac status =
   let gstatus = 
     match status#stack with

-    | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+    | (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->

           (match g' with
           | [] -> fail (lazy "no more goals to shift")
           | loc :: loc_tl ->
           (match g' with
           | [] -> fail (lazy "no more goals to shift")
           | loc :: loc_tl ->

-                (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
-                :: (loc_tl, t', k', tag) :: s))
+                (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
+                :: (loc_tl, t', k', tag, p') :: s))

      | _ -> fail (lazy "can't shift goals here")
   in
    status#set_stack gstatus
      | _ -> fail (lazy "can't shift goals here")
   in
    status#set_stack gstatus


@@ -78,11 +78,11 @@ let pos_tac i_s status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+    | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s

       when is_fresh loc ->
         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
       when is_fresh loc ->
         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in

-          ((l_js, t , [],`BranchTag)
-           :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+          ((l_js, t , [],`BranchTag, p)
+           :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)

     | _ -> fail (lazy "can't use relative positioning here")
   in
    status#set_stack gstatus
     | _ -> fail (lazy "can't use relative positioning here")
   in
    status#set_stack gstatus


@@ -92,7 +92,7 @@ let case_tac lab status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+    | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s

       when is_fresh loc ->
         let l_js =
           List.filter 
       when is_fresh loc ->
         let l_js =
           List.filter 


@@ -101,8 +101,8 @@ let case_tac lab status =
               match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
                   attrs,_,_ when List.mem (`Name lab) attrs -> true
                 | _ -> false) ([loc] @+ g') in
               match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
                   attrs,_,_ when List.mem (`Name lab) attrs -> true
                 | _ -> false) ([loc] @+ g') in

-          ((l_js, t , [],`BranchTag)
-           :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+          ((l_js, t , [],`BranchTag, p)
+           :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)

     | _ -> fail (lazy "can't use relative positioning here")
   in
    status#set_stack gstatus
     | _ -> fail (lazy "can't use relative positioning here")
   in
    status#set_stack gstatus


@@ -112,9 +112,9 @@ let wildcard_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+    | ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s

        when is_fresh loc ->
        when is_fresh loc ->

-            (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
+            (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: s)

     | _ -> fail (lazy "can't use wildcard here")
   in
    status#set_stack gstatus
     | _ -> fail (lazy "can't use wildcard here")
   in
    status#set_stack gstatus


@@ -124,8 +124,8 @@ let merge_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
-        ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+    | (g, t, k,`BranchTag, _) :: (g', t', k', tag, p) :: s ->
+        ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: s)

     | _ -> fail (lazy "can't merge goals here")
   in
    status#set_stack gstatus
     | _ -> fail (lazy "can't merge goals here")
   in
    status#set_stack gstatus


@@ -145,7 +145,7 @@ let focus_tac gs status =
               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
             gs;
               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
             gs;

-          (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
+          (zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s

   in
    status#set_stack gstatus
 ;;
   in
    status#set_stack gstatus
 ;;


@@ -154,7 +154,7 @@ let unfocus_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s
+    | (g, [], [], `FocusTag, _) :: s when filter_open g = [] -> s

     | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^
       Continuationals.Stack.pp s))
   in
     | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^
       Continuationals.Stack.pp s))
   in


@@ -165,12 +165,12 @@ let skip_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | (gl, t, k, tag) :: s -> 
+    | (gl, t, k, tag, p) :: s -> 

         let gl = List.map switch_of_loc gl in
         if List.exists (function Open _ -> true | Closed _ -> false) gl then 
           fail (lazy "cannot skip an open goal")
         else 
         let gl = List.map switch_of_loc gl in
         if List.exists (function Open _ -> true | Closed _ -> false) gl then 
           fail (lazy "cannot skip an open goal")
         else 

-          ([],t,k,tag) :: s
+          ([],t,k,tag,p) :: s

   in
    status#set_stack gstatus
 ;;
   in
    status#set_stack gstatus
 ;;


@@ -219,7 +219,7 @@ let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStat
 ;;
 
 let exec tac (low_status : #lowtac_status) g =
 ;;
 
 let exec tac (low_status : #lowtac_status) g =

-  let stack = [ [0,Open g], [], [], `NoTag ] in
+  let stack = [ [0,Open g], [], [], `NoTag, [] ] in

   let status = change_stack_type low_status stack in
   let status = tac status in
    (low_status#set_pstatus status)#set_obj status#obj
   let status = change_stack_type low_status stack in
   let status = tac status in
    (low_status#set_pstatus status)#set_obj status#obj


@@ -228,7 +228,7 @@ let exec tac (low_status : #lowtac_status) g =
 let distribute_tac tac (status : #tac_status) =
   match status#stack with
   | [] -> assert false
 let distribute_tac tac (status : #tac_status) =
   match status#stack with
   | [] -> assert false

-  | (g, t, k, tag) :: s ->
+  | (g, t, k, tag, p) :: s ->

       debug_print (lazy ("context length " ^string_of_int (List.length g)));
       let rec aux s go gc =
         function
       debug_print (lazy ("context length " ^string_of_int (List.length g)));
       let rec aux s go gc =
         function


@@ -258,7 +258,7 @@ let distribute_tac tac (status : #tac_status) =
       debug_print (lazy ("closed: "
         ^ String.concat " " (List.map string_of_int gcn)));
       let stack =
       debug_print (lazy ("closed: "
         ^ String.concat " " (List.map string_of_int gcn)));
       let stack =

-        (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+        (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s

       in
        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
 ;;
       in
        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
 ;;


@@ -704,7 +704,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
 let assert_tac seqs status =
  match status#stack with
   | [] -> assert false
 let assert_tac seqs status =
  match status#stack with
   | [] -> assert false

-  | (g,_,_,_) :: s ->
+  | (g,_,_,_,_) :: s ->

      assert (List.length g = List.length seqs);
      (match seqs with
          [] -> id_tac
      assert (List.length g = List.length seqs);
      (match seqs with
          [] -> id_tac

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 4873481ed9b7df99b93f06170483cad0e9563f6d..c2a739deaf492ba9396f268b9c89c1891d641e9f 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1005,7 +1005,7 @@ let rec stack_goals level gs =
   if level = 0 then []
   else match gs with 
     | [] -> assert false
   if level = 0 then []
   else match gs with 
     | [] -> assert false

-    | (g,_,_,_)::s -> 
+    | (g,_,_,_,_)::s -> 

         let is_open = function
           | (_,Continuationals.Stack.Open i) -> Some i
           | (_,Continuationals.Stack.Closed _) -> None
         let is_open = function
           | (_,Continuationals.Stack.Open i) -> Some i
           | (_,Continuationals.Stack.Closed _) -> None


@@ -1092,6 +1092,15 @@ let get_cands retrieve_for diff empty gty weak_gty =
             cands, diff more_cands cands
 ;;
 
             cands, diff more_cands cands
 ;;
 

+let is_a_needed_uri s d = 
+  prerr_endline ("DEBUG: " ^ d ^ ": "^ s);
+  s = "cic:/matita/basics/logic/eq.ind" ||
+  s = "cic:/matita/basics/logic/sym_eq.con" ||
+  s = "cic:/matita/basics/logic/trans_eq.con" ||
+  s = "cic:/matita/basics/logic/eq_f3.con" ||
+  s = "cic:/matita/basics/logic/eq_f2.con" ||
+  s = "cic:/matita/basics/logic/eq_f.con"
+

 let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
   let universe = status#auto_cache in
   let _,_,metasenv,subst,_ = status#obj in
 let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
   let universe = status#auto_cache in
   let _,_,metasenv,subst,_ = status#obj in


@@ -1124,26 +1133,31 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty
   in
   (* we now compute global candidates *)
   let global_cands, smart_global_cands =
   in
   (* we now compute global candidates *)
   let global_cands, smart_global_cands =

-   if flags.local_candidates then
-    let mapf s = 
-      let to_ast = function 
-        | NCic.Const r when true 
-             (*is_relevant statistics r*) -> Some (Ast.NRef r)
-     (* | NCic.Const _ -> None  *)
-        | _ -> assert false in
-          HExtlib.filter_map 
-            to_ast (NDiscriminationTree.TermSet.elements s) in
-      let g,l = 
-        get_cands
-          (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
-          NDiscriminationTree.TermSet.diff 
-          NDiscriminationTree.TermSet.empty
-          raw_gty raw_weak_gty in
-      mapf g, mapf l
-    else [],[] in
+  let mapf s = 
+    let to_ast = function 
+      | NCic.Const r when true 
+           (*is_relevant statistics r*) -> Some (Ast.NRef r)
+   (* | NCic.Const _ -> None  *)
+      | _ -> assert false in
+        HExtlib.filter_map 
+          to_ast (NDiscriminationTree.TermSet.elements s) in
+    let g,l = 
+      get_cands
+        (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
+        NDiscriminationTree.TermSet.diff 
+        NDiscriminationTree.TermSet.empty
+        raw_gty raw_weak_gty in
+    mapf g, mapf l
+  in 
+  let global_cands,smart_global_cands = 
+      if flags.local_candidates then global_cands,smart_global_cands
+      else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
+                                                                                   (NUri.string_of_uri
+                                                                                      uri) "GLOBAL" | _ -> false) 
+        in filter global_cands,filter smart_global_cands
+  in

   (* we now compute local candidates *)
   let local_cands,smart_local_cands = 
   (* we now compute local candidates *)
   let local_cands,smart_local_cands = 

-   if flags.local_candidates then

     let mapf s = 
       let to_ast t =
         let _status, t = term_of_cic_term status t context 
     let mapf s = 
       let to_ast t =
         let _status, t = term_of_cic_term status t context 


@@ -1154,7 +1168,14 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty
         (fun ty -> search_in_th ty cache)
         Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
       mapf g, mapf l
         (fun ty -> search_in_th ty cache)
         Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
       mapf g, mapf l

-   else [],[] in
+  in
+  let local_cands,smart_local_cands = 
+   if flags.local_candidates then local_cands,smart_local_cands
+   else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
+                                                                                (NUri.string_of_uri
+                                                                                   uri) "LOCAL" | _ -> false) 
+     in filter local_cands,filter smart_local_cands
+  in

   (* we now splits candidates in facts or not facts *)
   let test = is_a_fact_ast status subst metasenv context in
   let by,given_candidates =
   (* we now splits candidates in facts or not facts *)
   let test = is_a_fact_ast status subst metasenv context in
   let by,given_candidates =


@@ -1303,7 +1324,7 @@ let is_subsumed depth filter_depth status gty cache =
              NCicMetaSubst.mk_meta  
                metasenv ctx ~with_type:implication `IsType in
            let status = status#set_obj (n,h,metasenv,subst,obj) in
              NCicMetaSubst.mk_meta  
                metasenv ctx ~with_type:implication `IsType in
            let status = status#set_obj (n,h,metasenv,subst,obj) in

-           let status = status#set_stack [([1,Open j],[],[],`NoTag)] in 
+           let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in 

            try
              let status = NTactics.intro_tac "foo" status in
              let status =
            try
              let status = NTactics.intro_tac "foo" status in
              let status =


@@ -1481,7 +1502,7 @@ let sort_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | (goals, t, k, tag) :: s ->
+    | (goals, t, k, tag, p) :: s ->

         let g = head_goals status#stack in
         let sortedg = 
           (List.rev (MS.topological_sort g (deps status))) in
         let g = head_goals status#stack in
         let sortedg = 
           (List.rev (MS.topological_sort g (deps status))) in


@@ -1496,7 +1517,7 @@ let sort_tac status =
           let sorted_goals = 
             List.map (fun i -> List.find (is_it i) goals) sortedg
           in
           let sorted_goals = 
             List.map (fun i -> List.find (is_it i) goals) sortedg
           in

-            (sorted_goals, t, k, tag) :: s
+            (sorted_goals, t, k, tag, p) :: s

   in
    status#set_stack gstatus
 ;;
   in
    status#set_stack gstatus
 ;;


@@ -1505,13 +1526,13 @@ let clean_up_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
   let gstatus = 
     match status#stack with
     | [] -> assert false

-    | (g, t, k, tag) :: s ->
+    | (g, t, k, tag, p) :: s ->

         let is_open = function
           | (_,Continuationals.Stack.Open _) -> true
           | (_,Continuationals.Stack.Closed _) -> false
         in
         let g' = List.filter is_open g in
         let is_open = function
           | (_,Continuationals.Stack.Open _) -> true
           | (_,Continuationals.Stack.Closed _) -> false
         in
         let g' = List.filter is_open g in

-          (g', t, k, tag) :: s
+          (g', t, k, tag, p) :: s

   in
    status#set_stack gstatus
 ;;
   in
    status#set_stack gstatus
 ;;


@@ -1542,11 +1563,11 @@ let deep_focus_tac level focus status =
     if level = 0 then [],[],gs else
       match gs with 
         | [] -> assert false
     if level = 0 then [],[],gs else
       match gs with 
         | [] -> assert false

-        | (g, t, k, tag) :: s ->
+        | (g, t, k, tag,p) :: s ->

             let f,o,gs = slice (level-1) s in           
             let f1,o1 = List.partition in_focus g
             in
             let f,o,gs = slice (level-1) s in           
             let f1,o1 = List.partition in_focus g
             in

-            (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
+            (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs

   in
   let gstatus = 
     let f,o,s = slice level status#stack in f@o@s
   in
   let gstatus = 
     let f,o,s = slice level status#stack in f@o@s


@@ -1557,7 +1578,7 @@ let deep_focus_tac level focus status =
 let move_to_side level status =
 match status#stack with
   | [] -> assert false
 let move_to_side level status =
 match status#stack with
   | [] -> assert false

-  | (g,_,_,_)::tl ->
+  | (g,_,_,_,_)::tl ->

       let is_open = function
           | (_,Continuationals.Stack.Open i) -> Some i
           | (_,Continuationals.Stack.Closed _) -> None
       let is_open = function
           | (_,Continuationals.Stack.Open i) -> Some i
           | (_,Continuationals.Stack.Closed _) -> None


@@ -1880,7 +1901,7 @@ let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace
               let _ = debug_print (pptrace status trace) in
               let stack = 
                 match s#stack with
               let _ = debug_print (pptrace status trace) in
               let stack = 
                 match s#stack with

-                  | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+                  | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest

                   | _ -> assert false
               in
               let s = s#set_stack stack in
                   | _ -> assert false
               in
               let s = s#set_stack stack in


@@ -1911,7 +1932,7 @@ let auto_lowtac ~params:(univ,flags as params) status goal =
     let gty = get_goalty status goal in
     let ctx = ctx_of gty in
     let candidates = candidates_from_ctx univ ctx status in 
     let gty = get_goalty status goal in
     let ctx = ctx_of gty in
     let candidates = candidates_from_ctx univ ctx status in 

-    auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
+    auto_tac' candidates ~local_candidates:false ~use_given_only:true flags ~trace_ref:(ref [])

 
 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
     let candidates = candidates_from_ctx univ [] status in
 
 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
     let candidates = candidates_from_ctx univ [] status in

diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml
index bc0b424e0d3b0bb75ed6613a456fa904315136c8..9c1ed995cea4f717e813ecb9b1d596944ceeef60 100644 (file)
--- a/matita/matita/help/C/sec_declarative_tactics.xml
+++ b/matita/matita/help/C/sec_declarative_tactics.xml
@@ -14,13 +14,14 @@
   <sect1 id="tac_assume">
     <title>assume</title>
     <titleabbrev>assume</titleabbrev>
   <sect1 id="tac_assume">
     <title>assume</title>
     <titleabbrev>assume</titleabbrev>

-    <para><userinput>assume x : t</userinput></para>
+    <para><userinput>assume x : T that is equivalent to T'</userinput></para>

   <para>
     <variablelist>
       <varlistentry role="tactic.synopsis">
        <term>Synopsis:</term>
        <listitem>
   <para>
     <variablelist>
       <varlistentry role="tactic.synopsis">
        <term>Synopsis:</term>
        <listitem>

-         <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis> &sterm;</para>
+         <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis>
+             &sterm; [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</para>

        </listitem>
       </varlistentry>
       <varlistentry>
        </listitem>
       </varlistentry>
       <varlistentry>


@@ -36,9 +37,10 @@
       <varlistentry>
         <term>Action:</term>
        <listitem>
       <varlistentry>
         <term>Action:</term>
        <listitem>

-         <para>It adds to the context of the current sequent to prove a new
-          declaration <command>x : T </command>. The new conclusion becomes
-          <command>P</command>.</para>
+      <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
+      </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
+      <command>T'</command> is supplied and <command>T</command> and  <command>T'</command> are beta equivalent the new declaration that is added to the context is
+      <command>x:T'</command>.</para>

        </listitem>
       </varlistentry>
       <varlistentry>
        </listitem>
       </varlistentry>
       <varlistentry>


@@ -51,75 +53,126 @@
    </para>
   </sect1>
 
    </para>
   </sect1>
 

-    <sect1 id="tac_byinduction">
-      <title>by induction hypothesis we know</title>
-      <titleabbrev>by induction hypothesis we know</titleabbrev>
-      <para><userinput>by induction hypothesis we know t (id)</userinput></para>
-      <para>
-        <variablelist>
-         <varlistentry role="tactic.synopsis">
-           <term>Synopsis:</term>
-           <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
-           </listitem>
-         </varlistentry>
-         <varlistentry>
-           <term>Pre-condition:</term>
-           <listitem>
-        <para>To be used in a proof by induction to state the inductive
-          hypothesis.</para>
-           </listitem>
-         </varlistentry>
-         <varlistentry>
-           <term>Action:</term>
-             <listitem>
-               <para> Introduces the inductive hypothesis. </para>
-             </listitem>
-         </varlistentry>
-          <varlistentry>
-             <term>New sequents to prove:</term>
-                <listitem>
-                <para>None.</para>
-                </listitem>
-         </varlistentry>
-         </variablelist>
-      </para>
-    </sect1>  
+  <sect1 id="tac_suppose">
+    <title>suppose</title>
+    <titleabbrev>suppose</titleabbrev>
+    <para><userinput>suppose T (x) that is equivalent to T'</userinput></para>
+  <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+        <listitem>
+          <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; 
+            <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</para>
+        </listitem>
+       </varlistentry>
+      <varlistentry>
+         <term>Pre-condition:</term>
+        <listitem>
+          <para>The conclusion of the current proof must be
+          <command>∀x:T.P</command> or
+          <command>T→P</command> where <command>T</command> is
+          a proposition (i.e. <command>T</command> has type
+       <command>Prop</command> or <command>CProp</command>).</para>
+    </listitem>
+    </varlistentry>
+      <varlistentry>
+         <term>Action:</term>
+       <listitem>
+        <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
+            </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
+            <command>T'</command> is supplied and <command>T</command> and  <command>T'</command> are beta equivalent the new declaration that is added to the context is
+            <command>x:T'</command>.
+        </para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>New sequents to prove:</term>
+       <listitem>
+         <para>None.</para>
+       </listitem>
+      </varlistentry>
+    </variablelist>
+   </para>
+  </sect1>

 
 

-   <sect1 id="tac_case">
-     <title>case</title>
-     <titleabbrev>case</titleabbrev>
-     <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
+<sect1 id="tac_let">
+    <title>letin</title>
+    <titleabbrev>letin</titleabbrev>
+    <para><userinput>let x := T </userinput></para>
+  <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+        <listitem>
+         <para><emphasis role="bold">let</emphasis> &id; <emphasis role="bold"> = </emphasis> &term;</para>
+        </listitem>
+       </varlistentry>
+      <varlistentry>
+         <term>Pre-condition:</term>
+        <listitem>
+          <para>None</para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>Action:</term>
+       <listitem>
+        <para>It adds a new local definition <command>x := T</command> to the context of the sequent to prove.</para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>New sequents to prove:</term>
+       <listitem>
+         <para>None.</para>
+       </listitem>
+      </varlistentry>
+    </variablelist>
+   </para>
+  </sect1>
+
+ <sect1 id="tac_bytermweproved">
+   <title>we proved</title>
+     <titleabbrev>we proved</titleabbrev>
+     <para><userinput>justification we proved T (id) that is equivalent to T'</userinput></para>

      <para>
        <variablelist>
          <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
      <para>
        <variablelist>
          <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>

-            <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>] … </para>
-          </listitem>
-        </varlistentry>
-         <varlistentry>
-            <term>Pre-condition:</term>
-           <listitem>
-        <para>To be used in a proof by induction or by cases to start
-          a new case</para>
-           </listitem>
-        </varlistentry>
-         <varlistentry>
-            <term>Action:</term>
-            <listitem>
-              <para>Starts the new case <command>id</command> declaring
-                the local parameters <command>(id1:t1) … (idn:tn)</command></para>
-            </listitem>
-         </varlistentry>
-         <varlistentry>
-           <term>New sequents to prove:</term>
-           <listitem>
-               <para>None</para>
+            <para>&justification; <emphasis role="bold">we proved</emphasis> &term; 
+         <emphasis role="bold">(</emphasis> &id; 
+         <emphasis role="bold">)</emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term;] [ <emphasis role="bold">done</emphasis>]</para>

            </listitem>
            </listitem>

-         </varlistentry>
-       </variablelist>
-     </para>
-  </sect1> 
+          </varlistentry>
+          <varlistentry>
+            <term>Pre-condition:</term>
+            <listitem>
+              <para><command>T</command> must have type <command>Prop</command>.
+         </para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>Action:</term>
+            <listitem>
+         <para>It derives <command>T</command>
+           using the justification and labels the conclusion with
+           <command>id</command>. Alternatively, if a proposition
+            <command>T'</command> is supplied and <command>T</command> and  <command>T'</command> are beta equivalent the new hypothesis that is added to the context is
+            <command>id:T'</command>.
+
+            If the user does not supply a label and ends the command with <command>done</command> then if T is alpha equivalent to the conclusion of the current sequent then it closes it (if  <command>T'</command> is supplied this must be alpha equivalent to the conclusion, but in this case <command>T</command> does not need to).
+         </para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>New sequent to prove:</term>
+            <listitem>
+              <para>None.</para>
+            </listitem>
+          </varlistentry>
+        </variablelist>
+       </para>
+    </sect1>

 
  <sect1 id="tac_bydone">
    <title>done</title>
 
  <sect1 id="tac_bydone">
    <title>done</title>


@@ -155,8 +208,7 @@
      </para>
   </sect1>
 
      </para>
   </sect1>
 

-
-  <sect1 id="tac_exitselim">
+  <sect1 id="tac_existselim">

     <title>let such that</title>
     <titleabbrev>let such that</titleabbrev>
     <para><userinput>justification let x:t such that p (id)</userinput>
     <title>let such that</title>
     <titleabbrev>let such that</titleabbrev>
     <para><userinput>justification let x:t such that p (id)</userinput>


@@ -199,123 +251,47 @@
     </para>
   </sect1>
 
     </para>
   </sect1>
 

-  <sect1 id="tac_obtain">
-    <title>obtain</title>
-    <titleabbrev>obtain</titleabbrev>
-    <para><userinput>obtain H t1 = t2 justification</userinput></para>
+  <sect1 id="tac_andelim">
+    <title>we have</title>
+    <titleabbrev>we have</titleabbrev>
+    <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
+    </para>

     <para>
       <variablelist>
     <para>
       <variablelist>

-         <varlistentry role="tactic.synopsis">
-          <term>Synopsis:</term>
-          <listitem>
-            <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
-          </listitem>
-        </varlistentry>
-        <varlistentry>
-          <term>Pre-condition:</term>
-            <listitem>
-         <para><command>conclude</command> can be used only if the current
-           sequent is stating an equality. The left hand side must be omitted
-           in an equality chain.</para> 
-       </listitem>
-        </varlistentry>
-        <varlistentry>
-          <term>Action:</term>
-          <listitem>
-       <para>Starts or continues an equality chain. If the chain starts 
-         with <command>obtain H</command> a new subproof named 
-         <command>H</command> is started.</para>
-           </listitem>
-         </varlistentry>
-        <varlistentry>
-          <term>New sequent to prove:</term>
-            <listitem>
-               <para>If the chain starts 
-            with <command>obtain H</command> a nre sequent for
-            <command>t2 = ?</command> is opened.
-          </para>
-            </listitem>
-        </varlistentry>
-       </variablelist>
-     </para>
-   </sect1>
-
-  <sect1 id="tac_suppose">
-    <title>suppose</title>
-    <titleabbrev>suppose</titleabbrev>
-    <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
-  <para>
-     <variablelist>
-       <varlistentry role="tactic.synopsis">
-         <term>Synopsis:</term>
-        <listitem>
-          <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; 
-            <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</para>
-        </listitem>
-       </varlistentry>
-      <varlistentry>
-         <term>Pre-condition:</term>
-        <listitem>
-          <para>The conclusion of the current proof must be
-          <command>∀x:T.P</command> or
-          <command>T→P</command> where <command>T</command> is
-          a proposition (i.e. <command>T</command> has type
-          <command>Prop</command> or <command>CProp</command>).</para>
-        </listitem>
-      </varlistentry>
-      <varlistentry>
-        <term>Action:</term>
+        <varlistentry role="tactic_synopsis">
+         <term>Synopsis:</term>

          <listitem>
          <listitem>

-           <para>It adds to the context of the current sequent to prove a new
-          declaration <command>x : T </command>. The new conclusion becomes
-          <command>P</command>.</para>
+           <para>&justification; <emphasis role="bold">we have</emphasis> &term; 
+                   <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term; 
+                     <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
+          </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Pre-condition:</term>
+         <listitem>
+           <para></para>

          </listitem>
          </listitem>

-      </varlistentry>
-      <varlistentry>
-        <term>New sequents to prove:</term>
-        <listitem>
-            <para>None.</para>
-        </listitem>
-      </varlistentry>
-    </variablelist>
-   </para>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+      <para>It derives <command>t1∧t2</command> using the 
+        <command>justification</command> then it introduces in the context
+        <command>t1</command>   labelled with <command>id1</command> and
+        <command>t2</command>   labelled with <command>id2</command>.
+      </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>New sequent to prove:</term>
+         <listitem>
+            <para>None.</para>
+          </listitem>
+       </varlistentry>
+      </variablelist>
+    </para>

   </sect1>
 
   </sect1>
 

-   <sect1 id="tac_thesisbecomes">
-     <title>the thesis becomes</title>
-     <titleabbrev>the thesis becomes</titleabbrev>
-     <para><userinput>the thesis becomes t</userinput></para>
-     <para>
-        <variablelist>
-          <varlistentry role="tactic.synopsis">
-            <term>Synopsis:</term>
-            <listitem>
-              <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
-            </listitem>
-          </varlistentry>
-          <varlistentry>
-            <term>Pre-condition:</term>
-            <listitem>
-         <para>The provided term <command>t</command> must be convertible with
-           current sequent.</para>
-            </listitem>
-          </varlistentry>
-          <varlistentry>
-            <term>Action:</term>
-            <listitem>
-              <para>It changes the current goal to the one provided.</para>
-            </listitem>
-          </varlistentry>
-          <varlistentry>
-            <term>New sequent to prove:</term>
-            <listitem>
-              <para>None.</para>
-            </listitem>
-          </varlistentry>
-        </variablelist>
-       </para>
-   </sect1>
-   

   <sect1 id="tac_weneedtoprove">
     <title>we need to prove</title>
     <titleabbrev>we need to prove</titleabbrev>
   <sect1 id="tac_weneedtoprove">
     <title>we need to prove</title>
     <titleabbrev>we need to prove</titleabbrev>


@@ -358,44 +334,39 @@
     </para>
   </sect1>
 
     </para>
   </sect1>
 

-
-  <sect1 id="tac_andelim">
-    <title>we have</title>
-    <titleabbrev>we have</titleabbrev>
-    <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
-    </para>
+    <sect1 id="tac_weproceedbyinduction">
+    <title>we proceed by induction on</title>
+    <titleabbrev>we proceed by induction on</titleabbrev>
+    <para><userinput>we proceed by induction on t to prove th</userinput></para>        

     <para>
       <variablelist>
     <para>
       <variablelist>

-        <varlistentry role="tactic_synopsis">
+        <varlistentry role="tactic.synopsis">

          <term>Synopsis:</term>
          <listitem>
          <term>Synopsis:</term>
          <listitem>

-           <para>&justification; <emphasis role="bold">we have</emphasis> &term; 
-                   <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term; 
-                     <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
-          </listitem>
+           <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
+         </listitem>

        </varlistentry>
        </varlistentry>

-       <varlistentry>
+        <varlistentry>

          <term>Pre-condition:</term>
          <listitem>
          <term>Pre-condition:</term>
          <listitem>

-           <para></para>
+      <para><command>t</command> must inhabitant of an inductive type and 
+        <command>th</command> must be the conclusion to be proved by induction.
+        </para>

          </listitem>
        </varlistentry>
        <varlistentry>
          <term>Action:</term>
          </listitem>
        </varlistentry>
        <varlistentry>
          <term>Action:</term>

-         <listitem>
-      <para>It derives <command>t1∧t2</command> using the 
-        <command>justification</command> then it introduces in the context
-        <command>t1</command>   labelled with <command>id1</command> and
-        <command>t2</command>   labelled with <command>id2</command>.
-      </para>
-         </listitem>
-       </varlistentry>
-       <varlistentry>
-         <term>New sequent to prove:</term>
-         <listitem>
-            <para>None.</para>
-          </listitem>
+           <listitem>
+             <para>It proceed by induction on <command>t</command>.</para>
+           </listitem>

        </varlistentry>
        </varlistentry>

+        <varlistentry>
+            <term>New sequents to prove:</term>
+            <listitem>
+              <para>It opens one new sequent for each constructor of the
+                type of <command>t</command>.</para>
+            </listitem>
+        </varlistentry>

       </variablelist>
     </para>
   </sect1>
       </variablelist>
     </para>
   </sect1>


@@ -436,73 +407,100 @@
          </variablelist>
        </para>
     </sect1>
          </variablelist>
        </para>
     </sect1>

-    
-    <sect1 id="tac_weproceedbyinduction">
-    <title>we proceed by induction on</title>
-    <titleabbrev>we proceed by induction on</titleabbrev>
-    <para><userinput>we proceed by induction on t to prove th</userinput></para>        
-    <para>
-      <variablelist>
-        <varlistentry role="tactic.synopsis">
-         <term>Synopsis:</term>
-         <listitem>
-           <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
-         </listitem>
-       </varlistentry>
-        <varlistentry>
-         <term>Pre-condition:</term>
-         <listitem>
-      <para><command>t</command> must inhabitant of an inductive type and 
-        <command>th</command> must be the conclusion to be proved by induction.
-        </para>
-         </listitem>
-       </varlistentry>
-       <varlistentry>
-         <term>Action:</term>
-           <listitem>
-             <para>It proceed by induction on <command>t</command>.</para>
-           </listitem>
-       </varlistentry>
-        <varlistentry>
-            <term>New sequents to prove:</term>
-            <listitem>
-              <para>It opens one new sequent for each constructor of the
-                type of <command>t</command>.</para>
-            </listitem>
-        </varlistentry>
-      </variablelist>
-    </para>
-  </sect1>

 
 

-
- <sect1 id="tac_bytermweproved">
-   <title>we proved</title>
-     <titleabbrev>we proved</titleabbrev>
-     <para><userinput>justification we proved t (id)</userinput></para>
+   <sect1 id="tac_case">
+     <title>case</title>
+     <titleabbrev>case</titleabbrev>
+     <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>

      <para>
        <variablelist>
          <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
      <para>
        <variablelist>
          <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>

-            <para>&justification; <emphasis role="bold">we proved</emphasis> &term; 
-         <emphasis role="bold">(</emphasis> &id; 
-         <emphasis role="bold">)</emphasis></para>
+            <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>] … </para>
+          </listitem>
+        </varlistentry>
+         <varlistentry>
+            <term>Pre-condition:</term>
+           <listitem>
+        <para>To be used in a proof by induction or by cases to start
+          a new case</para>
+           </listitem>
+        </varlistentry>
+         <varlistentry>
+            <term>Action:</term>
+            <listitem>
+              <para>Starts the new case <command>id</command> declaring
+                the local parameters <command>(id1:t1) … (idn:tn)</command></para>
+            </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>New sequents to prove:</term>
+           <listitem>
+               <para>None</para>

            </listitem>
            </listitem>

+         </varlistentry>
+       </variablelist>
+     </para>
+  </sect1> 
+
+    <sect1 id="tac_byinduction">
+      <title>by induction hypothesis we know</title>
+      <titleabbrev>by induction hypothesis we know</titleabbrev>
+      <para><userinput>by induction hypothesis we know t (id)</userinput></para>
+      <para>
+        <variablelist>
+         <varlistentry role="tactic.synopsis">
+           <term>Synopsis:</term>
+           <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+           </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>Pre-condition:</term>
+           <listitem>
+        <para>To be used in a proof by induction to state the inductive
+          hypothesis.</para>
+           </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>Action:</term>
+             <listitem>
+               <para> Introduces the inductive hypothesis. </para>
+             </listitem>
+         </varlistentry>
+          <varlistentry>
+             <term>New sequents to prove:</term>
+                <listitem>
+                <para>None.</para>
+                </listitem>
+         </varlistentry>
+         </variablelist>
+      </para>
+    </sect1>  
+
+   <sect1 id="tac_thesisbecomes">
+     <title>the thesis becomes</title>
+     <titleabbrev>the thesis becomes</titleabbrev>
+     <para><userinput>the thesis becomes t</userinput></para>
+     <para>
+        <variablelist>
+          <varlistentry role="tactic.synopsis">
+            <term>Synopsis:</term>
+            <listitem>
+              <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
+            </listitem>

           </varlistentry>
           <varlistentry>
             <term>Pre-condition:</term>
             <listitem>
           </varlistentry>
           <varlistentry>
             <term>Pre-condition:</term>
             <listitem>

-              <para><command>t</command>must have type <command>Prop</command>.
-         </para>
+         <para>The provided term <command>t</command> must be convertible with
+           current sequent.</para>

             </listitem>
           </varlistentry>
           <varlistentry>
             <term>Action:</term>
             <listitem>
             </listitem>
           </varlistentry>
           <varlistentry>
             <term>Action:</term>
             <listitem>

-         <para>It derives <command>t</command>
-           using the justification and labels the conclusion with
-           <command>id</command>.
-         </para>
+              <para>It changes the current goal to the one provided.</para>

             </listitem>
           </varlistentry>
           <varlistentry>
             </listitem>
           </varlistentry>
           <varlistentry>


@@ -513,6 +511,53 @@
           </varlistentry>
         </variablelist>
        </para>
           </varlistentry>
         </variablelist>
        </para>

-    </sect1>
+   </sect1>

 
 

+  <sect1 id="tac_obtain">
+      <title>conclude/obtain</title>
+      <titleabbrev>conclude/obtain</titleabbrev>
+      <para><userinput>conclude/obtain (H) t1 = t2 justification</userinput></para>
+    <para>
+      <variablelist>
+         <varlistentry role="tactic.synopsis">
+          <term>Synopsis:</term>
+          <listitem>
+            <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Pre-condition:</term>
+            <listitem>
+         <para><command>conclude</command> can be used only if the current
+           sequent is stating an equality. The left hand side must be omitted
+           in an equality chain.</para> 
+       </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+       <para>Starts or continues an equality chain. If the chain starts 
+         with <command>obtain H</command> a new subproof named 
+         <command>H</command> is started.</para>
+           </listitem>
+         </varlistentry>
+        <varlistentry>
+          <term>New sequent to prove:</term>
+            <listitem>
+               <para>If the chain starts 
+            with <command>obtain H</command> a nre sequent for
+            <command>t2 = ?</command> is opened.
+          </para>
+            </listitem>
+        </varlistentry>
+       </variablelist>
+     </para>
+   </sect1>
+
+
+   
+
+
+
+    

 </chapter>
 </chapter>