From: Ferruccio Guidi Date: Tue, 27 Jun 2006 16:57:46 +0000 (+0000) Subject: - decompose now runs with no arguments (operates on the whole context) X-Git-Tag: 0.4.95@7852~1272 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1beb5e1624ac1db045e36dff93d0cfafa6a70995;p=helm.git - decompose now runs with no arguments (operates on the whole context) - 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 --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index a9ac1c6eb..c73657ae1 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -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 diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 24d37c4f3..910ad5204 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -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 ^ diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index ae497fc12..52dde8979 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -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) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index c0ce1c27d..e9f530f17 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -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 -> diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 58d365b99..f3e3a37a0 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -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) diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml index e98bcd3c8..22bdd0a4f 100644 --- a/components/tactics/eliminationTactics.ml +++ b/components/tactics/eliminationTactics.ml @@ -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 -*) diff --git a/components/tactics/eliminationTactics.mli b/components/tactics/eliminationTactics.mli index cf6589f9a..45fbed6e8 100644 --- a/components/tactics/eliminationTactics.mli +++ b/components/tactics/eliminationTactics.mli @@ -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 diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index b1727fb7d..29f057479 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -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 diff --git a/components/tactics/fwdSimplTactic.ml b/components/tactics/fwdSimplTactic.ml index 0bae64f6c..5d78a4ed6 100644 --- a/components/tactics/fwdSimplTactic.ml +++ b/components/tactics/fwdSimplTactic.ml @@ -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 diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml index 4677a33ac..b1e23751f 100644 --- a/components/tactics/proofEngineStructuralRules.ml +++ b/components/tactics/proofEngineStructuralRules.ml @@ -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 *) diff --git a/components/tactics/proofEngineStructuralRules.mli b/components/tactics/proofEngineStructuralRules.mli index 91ebfecfb..7eb8fcc6b 100644 --- a/components/tactics/proofEngineStructuralRules.mli +++ b/components/tactics/proofEngineStructuralRules.mli @@ -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 *) diff --git a/components/tactics/ring.ml b/components/tactics/ring.ml index 4c58f1004..4d05ab333 100644 --- a/components/tactics/ring.ml +++ b/components/tactics/ring.ml @@ -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 diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 2ff482ff1..5bacca20c 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -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 diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma index 8037f8ba7..168cfbc2b 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma @@ -1,4 +1,4 @@ -(**************************************************************************) +clear(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -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. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma b/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma index 6d2bef823..ab59c3a51 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma @@ -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. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma index de3eb4487..99ec088f9 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma @@ -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". diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index bc5095fae..56c2a6616 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -163,27 +163,40 @@ clear clear - clear H + + clear H1 ... Hm + Synopsis: - clear &id; + + clear + &id; [&id;…] + Pre-conditions: - H must be an hypothesis of the - current sequent to prove. + + + H1 ... Hm + must be hypotheses of the + current sequent to prove. + Action: - It hides the hypothesis H from the - current sequent. + + It hides the hypotheses + + H1 ... Hm + from the current sequent. + @@ -382,7 +395,8 @@ decompose decompose - decompose (T1 ... Tn) H hips + decompose (T1 ... Tn) + H as H1 ... Hm @@ -391,8 +405,11 @@ decompose - [([&id;]…)] - &id; &intros-spec; + [( + &id;… + )] + [&id;] + [as &id;…] @@ -412,9 +429,13 @@ Action: - Runs elim H hyps, clears H and tries to run - itself recursively on each new identifier introduced by - elim in the opened sequents. + Runs + elim H H1 ... Hm + , clears H and tries to run itself + recursively on each new identifier introduced by + elim in the opened sequents. + If H is not provided tries this operation on + each premise in the current context. @@ -1048,7 +1069,16 @@ its constructor takes no arguments. Synopsis: - lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]…] [as &id;] + + lapply + [depth=&nat;] + &sterm; + [to + &sterm; + [,&sterm;…] + ] + [as &id;] + @@ -1065,12 +1095,12 @@ its constructor takes no arguments. Action: - It invokes letin H ≝ (t ? ... ?) + Invokes letin H ≝ (t ? ... ?) with enough ?'s to reach the d-th independent premise of t (d is maximum if unspecified). - Then it istantiates (by apply) with + Then istantiates (by apply) with t1, ..., tn the ?'s corresponding to the first n independent premises of diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index 6a735eee2..45e097e1b 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -19,7 +19,10 @@ change pattern with sterm - clear id + + clear + id [id…] + clearbody id @@ -40,8 +43,11 @@ decompose - [([id]…)] - id intros-spec + [( + id… + )] + [id] + [as id…] @@ -109,7 +115,16 @@ inversion sterm - lapply [depth=nat] sterm [to sterm [sterm]…] [as id] + + lapply + [depth=nat] + sterm + [to + sterm + [,sterm…] + ] + [as id] +