]> matita.cs.unibo.it Git - helm.git/commitdiff
- decompose now runs with no arguments (operates on the whole context)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 27 Jun 2006 16:57:46 +0000 (16:57 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 27 Jun 2006 16:57:46 +0000 (16:57 +0000)
- clear now takes a list of hypotheses (clears each)
- RELATIONAL-ARITHMETICS updated to use the new tactics
- tactics/Makefile fixed to correctly build tactics.mli

18 files changed:
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/Makefile
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/eliminationTactics.mli
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/fwdSimplTactic.ml
helm/software/components/tactics/proofEngineStructuralRules.ml
helm/software/components/tactics/proofEngineStructuralRules.mli
helm/software/components/tactics/ring.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma
helm/software/matita/help/C/sec_tactics.xml
helm/software/matita/help/C/tactic_quickref.xml

index a9ac1c6eb5a5cc418064febe5f88de7c283c6e46..c73657ae1b4f8c458e5d290e5a202b15db41f7c0 100644 (file)
@@ -51,12 +51,12 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Assumption of loc
   | Auto of loc * (string * string) list
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
-  | Clear of loc * 'ident
+  | Clear of loc * 'ident list
   | ClearBody of loc * 'ident
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
-  | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
+  | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
   | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
index 24d37c4f318d8c1f0ee1b90b6521d5d6333861fa..910ad5204f5d427de157dab1996a274b4f2cff08 100644 (file)
@@ -66,6 +66,10 @@ let pp_intros_specs = function
 
 let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
 
+let opt_string_pp = function
+   | None -> ""
+   | Some what -> what ^ " "
+
 let rec pp_tactic ~term_pp ~lazy_term_pp =
   let pp_reduction_kind = pp_reduction_kind ~term_pp in
   let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
@@ -79,7 +83,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Assumption _ -> "assumption"
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
-  | Clear (_,id) -> sprintf "clear %s" id
+  | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)
   | ClearBody (_,id) -> sprintf "clearbody %s" id
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
@@ -87,14 +91,14 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
      "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | Decompose (_, [], what, names) ->
-      sprintf "decompose %s%s" what (pp_intros_specs (None, names)) 
+      sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) 
   | Decompose (_, types, what, names) ->
       let to_ident = function
          | Ident id -> id
         | Type _   -> assert false 
       in
       let types = List.rev_map to_ident types in
-      sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) 
+      sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
   | Discriminate (_, term) -> "discriminate " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ term_pp term ^
index ae497fc12cbdd25db29b319643cfbe444d421aa0..52dde8979f72381e0c7d0297dd8628bc69f29632 100644 (file)
@@ -82,7 +82,7 @@ let tactic_of_ast ast =
       let user_types = List.rev_map to_type types in
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
-      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
index c0ce1c27d359097b676a436c05923127ffc53dda..e9f530f17f49df995ae551ad5f675aef0ec25556 100644 (file)
@@ -136,8 +136,8 @@ EXTEND
         LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
           string_of_int v | v = IDENT -> v ] -> i,v ] ->
         GrafiteAst.Auto (loc,params)
-    | IDENT "clear"; id = IDENT ->
-        GrafiteAst.Clear (loc,id)
+    | IDENT "clear"; ids = LIST1 IDENT ->
+        GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
@@ -148,9 +148,10 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
-      (num, idents) = intros_spec ->
+    | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
+        idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
         let types = match types with None -> [] | Some types -> types in
+       let idents = match idents with None -> [] | Some idents -> idents in
        let to_spec id = GrafiteAst.Ident id in
        GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "discriminate"; t = tactic_term ->
index 58d365b99b3a5f2a6eef84798d3765a941d65c29..f3e3a37a06c09e951ded3cb72ed8d77015ea591a 100644 (file)
@@ -30,7 +30,8 @@ tactics_mli_deps=tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli param
 tactics.mli: 
        $(H)echo "  OCAMLC -i $$(tactics_mli_deps) > $@"
        $(H)echo "(* GENERATED FILE, DO NOT EDIT. STAMP:`date` *)" > $@
-       $(H)$(OCAMLC) -I paramodulation -i $(tactics_mli_deps) >> $@
+       $(H)$(OCAMLC) -I paramodulation -i tactics.ml >> $@
+# FG: tactics.ml was (wrongly) $(tactics_mli_deps)
 
 UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions)
 STR=$(shell $(OCAMLFIND) query str)
index e98bcd3c878d6fa597ffda35b85a4ee2e0d4d906..22bdd0a4f5b78fac9d0146093bd70516b2ed3add 100644 (file)
@@ -33,27 +33,6 @@ module F = FreshNamesGenerator
 module E = ProofEngineTypes
 module H = ProofEngineHelpers
 
-(*
-let induction_tac ~term status =
-  let (proof, goal) = status in
-  let module C = Cic in
-  let module R = CicReduction in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-  let module S = ProofEngineStructuralRules in
-  let module U = UriManager in 
-   let (_,metasenv,_,_) = proof in
-    let _,context,ty = CicUtil.lookup_meta goal metasenv in
-     let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *)
-
-     T.then_ ~start:(T.repeat_tactic 
-                       ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *)
-                       ~continuation:(P.intros))
-             ~continuation:(P.elim_intros_simpl ~term)
-             status
-;;
-*)
-
 (* unexported tactics *******************************************************)
 
 let get_name context index =
@@ -95,7 +74,7 @@ let elim_clear_tac ~mk_fresh_name_callback ~types ~what =
       let index, ty = H.lookup_type metasenv context what in
       if check_inductive_types types ty then 
          let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
-                          ~continuation:(S.clear what)
+                          ~continuation:(S.clear [what])
         in
         E.apply_tactic tac status
       else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
@@ -143,75 +122,21 @@ let search_inductive_types ty =
 (* roba seria ------------------------------------------------------------- *)
 
 let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
-                  ?(user_types=[]) ~dbd what =
+                  ?(user_types=[]) ?what ~dbd =
    let decompose_tac status =
       let (proof, goal) = status in
       let _, metasenv,_,_ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
       let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in
-      let old_context_length = List.length context in
-      let tac = T.then_ ~start:(tactic ~what)
-                        ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
+      let old_context_length = List.length context in      
+      let tac = match what with
+        | Some what -> 
+           T.then_ ~start:(tactic ~what)
+                    ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
+        | None      ->
+            scan_tac ~old_context_length ~index:old_context_length ~tactic
       in
       E.apply_tactic tac status
    in
    E.mk_tactic decompose_tac
-      
-(*
-module R = CicReduction
-
-       let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status =
-         let (proof, goal) = status in
-         warn (lazy ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)));
-         if nr_of_hyp_still_to_elim <> 0 then
-          let _,metasenv,_,_ = proof in
-           let _,context,_ = CicUtil.lookup_meta goal metasenv in
-            let old_context_len = List.length context in
-            let termty,_ = 
-             CicTypeChecker.type_of_aux' metasenv context term' 
-               CicUniv.empty_ugraph in
-             warn (lazy ("elim_clear termty= " ^ CicPp.ppterm termty));
-             match termty with
-                C.MutInd (uri,typeno,exp_named_subst)
-              | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) 
-                 when (List.mem (uri,typeno,exp_named_subst) urilist) ->
-                   warn (lazy ("elim " ^ CicPp.ppterm termty));
-                  ProofEngineTypes.apply_tactic 
-                   (T.then_ 
-                      ~start:(P.elim_intros_simpl_tac term')
-                      ~continuation:(
-                        (* clear the hyp that has just been eliminated *)
-                        ProofEngineTypes.mk_tactic (fun status -> 
-                          let (proof, goal) = status in
-                          let _,metasenv,_,_ = proof in
-                           let _,context,_ = CicUtil.lookup_meta goal metasenv in
-                            let new_context_len = List.length context in   
-                             warn (lazy ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)));
-                             let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
-                             let hyp_name =
-                              match List.nth context new_nr_of_hyp_still_to_elim with
-                                 None
-                               | Some (Cic.Anonymous,_) -> assert false
-                               | Some (Cic.Name name,_) -> name
-                             in
-                            ProofEngineTypes.apply_tactic
-                             (T.then_ 
-                                ~start:(
-                                  if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) 
-                                   then begin debug_print (lazy ("%%%%%%% no clear")); T.id_tac end
-                                   else begin debug_print (lazy ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim)))); (S.clear ~hyp:hyp_name) end)
-                                ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)))
-                                status
-                        )))
-                      status
-              | _ ->
-                   let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in 
-                    warn (lazy ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)));
-                    elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status
-         else (* no hyp to elim left in this goal *)
-          ProofEngineTypes.apply_tactic T.id_tac status
-
-        in
-         elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status
-*)
index cf6589f9a5bb3c83c9d6d6d5f6718ff7e2332b8b..45fbed6e851342c19f08b7f0cbe4cb115f1c9c6a 100644 (file)
@@ -30,4 +30,4 @@ val elim_type_tac:
 val decompose_tac:
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  ?user_types:((UriManager.uri * int) list) ->
dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
index b1727fb7d401d35fa761a2dd9c4cbb3540c9bf6e..29f0574794b649704f87959c4505f4c22b755b35 100644 (file)
@@ -80,7 +80,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
                 ~pattern:
                   (None,[name,Cic.Implicit (Some `Hole)], None)
                 (ProofEngineTypes.const_lazy_term typ);
-               ProofEngineStructuralRules.clear dummy
+               ProofEngineStructuralRules.clear [dummy]
               ]),
          Some pat,gty
     | _::_ -> assert false
@@ -289,15 +289,15 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
                        (function ((proof,goal) as status) ->
                          let _,metasenv,_,_ = proof in
                          let _,context,_ = CicUtil.lookup_meta goal metasenv in
-                         let hyp =
+                         let hyps =
                           try
                            match List.hd context with
-                              Some (Cic.Name name,_) -> name
+                              Some (Cic.Name name,_) -> [name]
                             | _ -> assert false
                           with (Failure "hd") -> assert false
                          in
                           ProofEngineTypes.apply_tactic
-                           (ProofEngineStructuralRules.clear ~hyp) status))
+                           (ProofEngineStructuralRules.clear ~hyps) status))
                     ~continuation:(aux_tac (n + 1) tl));
               T.id_tac])
          status
index 0bae64f6c6fb7bb1e22a1ac84d4400cc4e0ae20a..5d78a4ed6949ef4fc57567a2aff7ab8400587fcc 100644 (file)
@@ -138,7 +138,7 @@ let fwd_simpl_tac
          | uri :: _ -> 
            Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
            let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in  
-            let tac = T.then_ ~start ~continuation:(PESR.clear hyp) in
+            let tac = T.then_ ~start ~continuation:(PESR.clear ~hyps:[hyp]) in
             PET.apply_tactic tac status
    in
    PET.mk_tactic fwd_simpl_tac
index 4677a33ac8221a1080d7d0f6953e9fe2b8a822ba..b1e23751f413afb1b7280bc56a2b1879ca943f73 100644 (file)
@@ -97,8 +97,8 @@ let clearbody ~hyp =
  in
   mk_tactic (clearbody ~hyp)
 
-let clear ~hyp =
- let clear ~hyp (proof, goal) =
+let clear_one ~hyp =
+ let clear_one ~hyp (proof, goal) =
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
     let metano,context,ty =
@@ -154,7 +154,19 @@ let clear ~hyp =
      in
       (curi,metasenv',pbo,pty), [goal]
  in
-  mk_tactic (clear ~hyp)
+  mk_tactic (clear_one ~hyp)
+
+let clear ~hyps =
+   let clear hyps status =
+      let aux status hyp = 
+         match apply_tactic (clear_one ~hyp) status with
+           | proof, [g] -> proof, g
+           | _          -> raise (Fail (lazy "clear: internal error"))
+      in
+      let proof, g = List.fold_left aux status hyps in
+      proof, [g]
+   in
+   mk_tactic (clear hyps)
 
 (* Warning: this tactic has no effect on the proof term.
    It just changes the name of an hypothesis in the current sequent *)
index 91ebfecfb4ba94a682967d26f77e928edf30552d..7eb8fcc6b8c9190bf866eb1ee23e760513eb20cc 100644 (file)
@@ -24,7 +24,7 @@
  *)
 
 val clearbody: hyp:string -> ProofEngineTypes.tactic
-val clear: hyp:string -> ProofEngineTypes.tactic
+val clear: hyps:string list -> ProofEngineTypes.tactic
 
 (* Warning: this tactic has no effect on the proof term.
    It just changes the name of an hypothesis in the current sequent *)
index 4c58f1004ff86e63c014437e41fb50d18a5520cb..4d05ab3333cafba2b10fddfa9b383c7450602d39 100644 (file)
@@ -444,7 +444,7 @@ let purge_hyps_tac ~count =
         in
          aux (n-1) tl
           (status_of_single_goal_tactic_result 
-          (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
+          (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in
index 2ff482ff1c6cc7ac10fc41f2c433b825b9169278..5bacca20cd706898e9e432efd8e4e3c831d36d31 100644 (file)
@@ -1,14 +1,14 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 12 11:46:23 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Jun 27 17:58:26 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
-val auto : 
+val auto :
   params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.lazy_pattern ->
   Cic.lazy_term -> ProofEngineTypes.tactic
-val clear : hyp:string -> ProofEngineTypes.tactic
+val clear : hyps:string list -> ProofEngineTypes.tactic
 val clearbody : hyp:string -> ProofEngineTypes.tactic
 val constructor : n:int -> ProofEngineTypes.tactic
 val contradiction : ProofEngineTypes.tactic
@@ -18,7 +18,7 @@ val cut :
 val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->
-  dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
+  ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
 val demodulate :
   dbd:HMysql.dbd ->
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
index 8037f8ba7fce7ad98e8323cfff5cb719ff7952bc..168cfbc2b7632936cd6b13fff9db052b45c5a1d5 100644 (file)
@@ -1,4 +1,4 @@
-(**************************************************************************)
+clear(**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_gen".
+set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_fwd".
 
-include "nat_gen.ma".
+include "nat_fwd.ma".
 include "add_defs.ma".
 
 (* primitive generation lemmas proved by elimination and inversion *)
 
 theorem add_gen_O_1: \forall q,r. add O q r \to q = r.
 intros. elim H; clear H; clear q; clear r; intros;
intros. elim H; clear H q r; intros;
  [ reflexivity
  | clear H1. auto
  ].
@@ -28,18 +28,18 @@ qed.
 
 theorem add_gen_S_1: \forall p,q,r. add (S p) q r \to 
                      \exists s. r = (S s) \land add p q s.
- intros. elim H; clear H; clear q; clear r; intros;
+ intros. elim H; clear H q r; intros;
  [
- | clear H1. 
-  decompose H2.
-  rewrite > H1. clear H1. clear n2
+ | clear H1.
+   decompose.
+   rewrite > H1. clear H1 n2
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
 theorem add_gen_O_2: \forall p,r. add p O r \to p = r.
  intros. inversion H; clear H; intros;
  [ auto
- | clear H. clear H1.
+ | clear H H1.
    lapply eq_gen_O_S to H2 as H0. apply H0
  ].
 qed.
@@ -48,18 +48,18 @@ theorem add_gen_S_2: \forall p,q,r. add p (S q) r \to
                      \exists s. r = (S s) \land add p q s.
  intros. inversion H; clear H; intros;
  [ lapply eq_gen_S_O to H as H0. apply H0
- | clear H1. clear H3. clear r.
+ | clear H1 H3 r.
    lapply eq_gen_S_S to H2 as H0. clear H2.
-   rewrite > H0. clear H0. clear q.
+   rewrite > H0. clear H0 q.
    apply ex_intro; [| auto ] (**)
  ].
 qed.
 
 theorem add_gen_O_3: \forall p,q. add p q O \to p = O \land q = O.
  intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1. clear p.
+ [ rewrite < H1. clear H1 p.
    auto
- | clear H. clear H1.
+ | clear H H1.
    lapply eq_gen_O_S to H3 as H0. apply H0
  ].
 qed.
@@ -68,10 +68,10 @@ theorem add_gen_S_3: \forall p,q,r. add p q (S r) \to
                      \exists s. p = S s \land add s q r \lor
                                 q = S s \land add p s r.
  intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1. clear p
+ [ rewrite < H1. clear H1 p
  | clear H1.
    lapply eq_gen_S_S to H3 as H0. clear H3.
-   rewrite > H0. clear H0. clear r.
+   rewrite > H0. clear H0 r.
  ]; apply ex_intro; [| auto || auto ] (**)
 qed.
 (*
@@ -80,11 +80,11 @@ qed.
 variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O.
  intros 2. elim q; clear q; intros;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p.
+   rewrite > H0. clear H0 p.
    auto
  | clear H.
    lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
+   decompose.
    lapply eq_gen_O_S to H1 as H0. apply H0
  ].
 qed.
@@ -94,12 +94,12 @@ variant add_gen_S_3_alt: \forall p,q,r. add p q (S r) \to
                                     q = S s \land add p s r.
  intros 2. elim q; clear q; intros;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p
+   rewrite > H0. clear H0 p
  | clear H.
    lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
+   decompose.
    lapply eq_gen_S_S to H1 as H0. clear H1.
-   rewrite > H0. clear H0. clear r.
+   rewrite > H0. clear H0 r.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 *)
@@ -108,21 +108,21 @@ qed.
 theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O.
  intros 2. elim q; clear q; intros;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p
+   rewrite > H0. clear H0 p
  | lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
+   decompose.
    lapply eq_gen_S_S to H2 as H0. clear H2.
-   rewrite < H0 in H3. clear H0. clear a
+   rewrite < H0 in H3. clear H0 a
  ]; auto.
 qed.
 
 theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O.
  intros 1. elim p; clear p; intros;
  [ lapply add_gen_O_1 to H as H0. clear H.
-   rewrite > H0. clear H0. clear q
+   rewrite > H0. clear H0 q
  | lapply add_gen_S_1 to H1 as H0. clear H1.
-   decompose H0.
+   decompose.
    lapply eq_gen_S_S to H2 as H0. clear H2.
-   rewrite < H0 in H3. clear H0. clear a
+   rewrite < H0 in H3. clear H0 a
  ]; auto.
 qed.
index 6d2bef8232e910d91938fdea03fcde7d37812a3f..ab59c3a516a7846272400b16194e4128511775d4 100644 (file)
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_props".
 
-include "add_gen.ma".
+include "add_fwd.ma".
 
 theorem add_O_1: \forall q. add O q q.
  intros. elim q; clear q; auto.
@@ -23,36 +23,36 @@ qed.
 theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r).
  intros 2. elim q; clear q;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p
+   rewrite > H0. clear H0 p
  | lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
-   rewrite > H2. clear H2. clear r
+   decompose.
+   rewrite > H2. clear H2 r
  ]; auto.
 qed.
 
 theorem add_sym: \forall p,q,r. add p q r \to add q p r.
  intros 2. elim q; clear q;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p
+   rewrite > H0. clear H0 p
  | lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
-   rewrite > H2. clear H2. clear r
+   decompose.
+   rewrite > H2. clear H2 r
  ]; auto.
 qed.
 
 theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r.
  intros.
  lapply add_gen_S_2 to H as H0. clear H.
- decompose H0.
- rewrite > H1. clear H1. clear r.
+ decompose.
+ rewrite > H1. clear H1 r.
  auto.
 qed.
 
 theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r.
  intros.
  lapply add_gen_S_1 to H as H0. clear H.
- decompose H0.
- rewrite > H1. clear H1. clear r.
+ decompose.
+ rewrite > H1. clear H1 r.
  auto.
 qed.
 
@@ -61,15 +61,15 @@ theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to
                      \exists q. add q1 q2 q \land add p q r2.
  intros 2; elim q1; clear q1; intros;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p
+   rewrite > H0. clear H0 p
  | lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
-   rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
+   decompose.
+   rewrite > H3. rewrite > H3 in H2. clear H3 r1.
    lapply add_gen_S_1 to H2 as H0. clear H2.
-   decompose H0.
-   rewrite > H2. clear H2. clear r2.
-   lapply H to H4, H3 as H0. clear H. clear H4. clear H3.
-   decompose H0.
+   decompose.
+   rewrite > H2. clear H2 r2.
+   lapply H to H4, H3 as H0. clear H H4 H3.
+   decompose.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
@@ -78,15 +78,15 @@ theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to
                      \exists p. add p1 p2 p \land add p q r2.
  intros 2; elim q; clear q; intros;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0. clear H0. clear p1
+   rewrite > H0. clear H0 p1
  | lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
-   rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
+   decompose.
+   rewrite > H3. rewrite > H3 in H2. clear H3 r1.
    lapply add_gen_S_2 to H2 as H0. clear H2.
-   decompose H0.
-   rewrite > H2. clear H2. clear r2.
-   lapply H to H4, H3 as H0. clear H. clear H4. clear H3. 
-   decompose H0.
+   decompose.
+   rewrite > H2. clear H2 r2.
+   lapply H to H4, H3 as H0. clear H H4 H3. 
+   decompose.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
@@ -94,12 +94,12 @@ theorem add_conf: \forall p,q,r1. add p q r1 \to
                   \forall r2. add p q r2 \to r1 = r2.
  intros 2. elim q; clear q; intros;
  [ lapply add_gen_O_2 to H as H0. clear H.
-   rewrite > H0 in H1. clear H0. clear p
+   rewrite > H0 in H1. clear H0 p
  | lapply add_gen_S_2 to H1 as H0. clear H1.
-   decompose H0.
-   rewrite > H3. clear H3. clear r1.
+   decompose.
+   rewrite > H3. clear H3 r1.
    lapply add_gen_S_2 to H2 as H0. clear H2.
-   decompose H0.
-   rewrite > H2. clear H2. clear r2.
+   decompose.
+   rewrite > H2. clear H2 r2.
  ]; auto.
 qed.
index de3eb4487ff5b0845051781e5663c021b6074e5f..99ec088f9ede59224af66ee0302a8f85d294fc2c 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_gen".
+set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_fwd".
 
 include "library/logic/equality.ma".
 include "nat_defs.ma".
index bc5095fae94061d264bf51662680b1da622db51f..56c2a66167b4e47c17f14cecb6ec5a7cde65a809 100644 (file)
   <sect1 id="tac_clear">
     <title>clear</title>
     <titleabbrev>clear</titleabbrev>
-    <para><userinput>clear H</userinput></para>
+    <para><userinput>
+     clear H<subscript>1</subscript> ... H<subscript>m</subscript>
+    </userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">clear</emphasis> &id;</para>
+            <para>
+            <emphasis role="bold">clear</emphasis>
+            &id; [&id;…]
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para><command>H</command> must be an hypothesis of the
-             current sequent to prove.</para>
+            <para>
+            <command>
+             H<subscript>1</subscript> ... H<subscript>m</subscript>
+            </command> must be hypotheses of the
+             current sequent to prove.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
-            <para>It hides the hypothesis <command>H</command> from the
-             current sequent.</para>
+            <para>
+            It hides the hypotheses 
+             <command>
+             H<subscript>1</subscript> ... H<subscript>m</subscript>
+             </command> from the current sequent.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
     <title>decompose</title>
     <titleabbrev>decompose</titleabbrev>
     <para><userinput>
-     decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) H hips
+     decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) 
+     H as H<subscript>1</subscript> ... H<subscript>m</subscript>
     </userinput></para>
     <para>
       <variablelist>
           <listitem>
             <para>
             <emphasis role="bold">decompose</emphasis>
-            [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
-            &id; &intros-spec;
+            [<emphasis role="bold">(</emphasis>
+            &id;…
+            <emphasis role="bold">)</emphasis>]
+            [&id;] 
+            [<emphasis role="bold">as</emphasis> &id;…]
            </para>
           </listitem>
         </varlistentry>
           <term>Action:</term>
           <listitem>
             <para>
-            Runs <command>elim H hyps</command>, clears H and tries to run
-             itself recursively on each new identifier introduced by 
-            <command>elim</command> in the opened sequents.
+            Runs <command>
+             elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
+            </command>, clears <command>H</command> and tries to run itself
+            recursively on each new identifier introduced by 
+            <command>elim</command> in the opened sequents. 
+            If <command>H</command> is not provided tries this operation on
+            each premise in the current context.
            </para>
           </listitem>
         </varlistentry>
@@ -1048,7 +1069,16 @@ its constructor takes no arguments.</para>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">as</emphasis> &id;]</para>
+            <para>
+            <emphasis role="bold">lapply</emphasis> 
+            [<emphasis role="bold">depth=</emphasis>&nat;] 
+            &sterm; 
+            [<emphasis role="bold">to</emphasis>
+             &sterm;
+             [<emphasis role="bold">,</emphasis>&sterm;…]
+            ] 
+            [<emphasis role="bold">as</emphasis> &id;]
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -1065,12 +1095,12 @@ its constructor takes no arguments.</para>
           <term>Action:</term>
           <listitem>
             <para>
-            It invokes <command>letin H ≝ (t ? ... ?)</command>
+            Invokes <command>letin H ≝ (t ? ... ?)</command>
             with enough <command>?</command>'s to reach the 
             <command>d</command>-th independent premise of
             <command>t</command>
             (<command>d</command> is maximum if unspecified).       
-            Then it istantiates (by <command>apply</command>) with
+            Then istantiates (by <command>apply</command>) with
             t<subscript>1</subscript>, ..., t<subscript>n</subscript>
             the <command>?</command>'s corresponding to the first 
             <command>n</command> independent premises of
index 6a735eee247779b3bb19494190ebb2c3e556b92c..45e097e1bd1691f7436da434bfd804aef3a7afa0 100644 (file)
     <para><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
+    <para>
+            <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
+            <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
+           </para>
   </listitem>
   <listitem>
     <para><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
   <listitem>
     <para>
             <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
-            [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
-            <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis>
+            [<emphasis role="bold">(</emphasis>
+            <emphasis><link linkend="grammar.id">id</link></emphasis>…
+            <emphasis role="bold">)</emphasis>]
+            [<emphasis><link linkend="grammar.id">id</link></emphasis>] 
+            [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
            </para>
   </listitem>
   <listitem>
     <para><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">to</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>]…] [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
+    <para>
+            <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> 
+            [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] 
+            <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> 
+            [<emphasis role="bold">to</emphasis>
+             <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
+             [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
+            ] 
+            [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
+           </para>
   </listitem>
   <listitem>
     <para>