From f68f452173a5077c58f93587faad65fcced77223 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 28 Jun 2006 17:24:38 +0000 Subject: [PATCH] - "linear" flag added to lapply (automatic clearing) - RELATIONAL-ARITHMETICS updated to use this flag --- components/grafite/grafiteAst.ml | 2 +- components/grafite/grafiteAstPp.ml | 7 ++-- components/grafite_engine/grafiteEngine.ml | 6 +-- .../grafite_parser/grafiteDisambiguate.ml | 4 +- components/grafite_parser/grafiteParser.ml | 6 ++- components/tactics/eliminationTactics.ml | 8 +--- components/tactics/fwdSimplTactic.ml | 40 ++++++++++++++++--- components/tactics/fwdSimplTactic.mli | 3 +- components/tactics/proofEngineHelpers.ml | 19 +++++++++ components/tactics/proofEngineHelpers.mli | 6 +++ components/tactics/tactics.mli | 3 +- .../RELATIONAL-ARITHMETICS/add_fwd.ma | 30 +++++++------- .../RELATIONAL-ARITHMETICS/add_props.ma | 34 ++++++++-------- matita/help/C/sec_tactics.xml | 7 +++- matita/help/C/tactic_quickref.xml | 1 + 15 files changed, 117 insertions(+), 59 deletions(-) diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index c73657ae1..32625f39f 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -72,7 +72,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Injection of loc * 'term | Intros of loc * int option * 'ident list | Inversion of loc * 'term - | LApply of loc * int option * 'term list * 'term * 'ident option + | LApply of loc * bool * int option * 'term list * 'term * 'ident option | Left of loc | LetIn of loc * 'term * 'ident | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 910ad5204..18f14c5ce 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -130,9 +130,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) - | LApply (_, level_opt, terms, term, ident_opt) -> - sprintf "lapply %s%s%s%s" - (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") + | LApply (_, linear, level_opt, terms, term, ident_opt) -> + sprintf "lapply %s%s%s%s%s" + (if linear then " linear " else "") + (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") (term_pp term) (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms) (match ident_opt with None -> "" | Some ident -> " as " ^ ident) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 52dde8979..d7343c98c 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -130,10 +130,10 @@ let tactic_of_ast ast = ~mk_fresh_name_callback:(namer_of names) () | GrafiteAst.Inversion (_, term) -> Tactics.inversion term - | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> + | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) -> let names = match ident with None -> [] | Some id -> [id] in - Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many - ~to_what what + Tactics.lapply ~mk_fresh_name_callback:(namer_of names) + ~linear ?how_many ~to_what what | GrafiteAst.Left _ -> Tactics.left | GrafiteAst.LetIn (loc,term,name) -> Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 16421efaf..5babe3604 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -212,14 +212,14 @@ let disambiguate_tactic | GrafiteAst.Inversion (loc, term) -> let metasenv,term = disambiguate_term context metasenv term in metasenv,GrafiteAst.Inversion (loc, term) - | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> + | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) -> let f term to_what = let metasenv,term = disambiguate_term context metasenv term in term :: to_what in let to_what = List.fold_right f to_what [] in let metasenv,what = disambiguate_term context metasenv what in - metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident) + metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) | GrafiteAst.Left loc -> metasenv,GrafiteAst.Left loc | GrafiteAst.LetIn (loc, term, name) -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index e9f530f17..ccff1fab1 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -195,12 +195,14 @@ EXTEND | IDENT "inversion"; t = tactic_term -> GrafiteAst.Inversion (loc, t) | IDENT "lapply"; + linear = OPT [ IDENT "linear" ]; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; ident = OPT [ "as" ; ident = IDENT -> ident ] -> - let to_what = match to_what with None -> [] | Some to_what -> to_what in - GrafiteAst.LApply (loc, depth, to_what, what, ident) + let linear = match linear with None -> false | Some _ -> true in + let to_what = match to_what with None -> [] | Some to_what -> to_what in + GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) | IDENT "left" -> GrafiteAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> GrafiteAst.LetIn (loc, t, where) diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml index 22bdd0a4f..37a4f7136 100644 --- a/components/tactics/eliminationTactics.ml +++ b/components/tactics/eliminationTactics.ml @@ -35,12 +35,6 @@ module H = ProofEngineHelpers (* unexported tactics *******************************************************) -let get_name context index = - try match List.nth context (pred index) with - | Some (Cic.Name name, _) -> Some name - | _ -> None - with Invalid_argument "List.nth" -> None - let rec scan_tac ~old_context_length ~index ~tactic = let scan_tac status = let (proof, goal) = status in @@ -48,7 +42,7 @@ let rec scan_tac ~old_context_length ~index ~tactic = let _, context, _ = CicUtil.lookup_meta goal metasenv in let context_length = List.length context in let rec aux index = - match get_name context index with + match H.get_name context index with | _ when index <= 0 -> (proof, [goal]) | None -> aux (pred index) | Some what -> diff --git a/components/tactics/fwdSimplTactic.ml b/components/tactics/fwdSimplTactic.ml index 5d78a4ed6..ffc90c1cc 100644 --- a/components/tactics/fwdSimplTactic.ml +++ b/components/tactics/fwdSimplTactic.ml @@ -95,8 +95,16 @@ let strip_prods metasenv context ?how_many to_what term = | _, t -> metasenv, metas, conts in aux metasenv [] [] to_what (how_many, term) - -let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + +let get_clearables context terms = + let aux = function + | Cic.Rel i + | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i + | _ -> None + in + PEH.list_rev_map_filter aux terms + +let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) (* ?(substs = []) *) ?how_many ?(to_what = []) what = let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in let lapply_tac (proof, goal) = @@ -104,12 +112,13 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub let _, context, _ = CicUtil.lookup_meta goal metasenv in let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in let lemma = FNG.clean_dummy_dependent_types lemma in - let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in + let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in let conclusion = match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas) in - let tac = T.then_ ~start:(letin_tac conclusion) - ~continuation:(clearbody ~index:1) + let tac = + T.then_ ~start:(letin_tac conclusion) + ~continuation:(clearbody ~index:1) in let proof = (xuri, metasenv, u, t) in let aux (proof, goals) (tac, goal) = @@ -119,7 +128,26 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub List.fold_left aux (proof, []) ((tac, goal) :: conts) in PET.mk_tactic lapply_tac - + +let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what = + let lapply_tac status = + let proof, goal = status in + let _, metasenv, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in + let tac = + if linear then + let hyps = get_clearables context (what :: to_what) in + T.then_ ~start:lapply + ~continuation:(PESR.clear ~hyps) (* T.try_tactic ~tactic: *) + else + lapply + in + PET.apply_tactic tac status + in + PET.mk_tactic lapply_tac + (* fwd **********************************************************************) let fwd_simpl_tac diff --git a/components/tactics/fwdSimplTactic.mli b/components/tactics/fwdSimplTactic.mli index d75b83320..3dbcf6c9c 100644 --- a/components/tactics/fwdSimplTactic.mli +++ b/components/tactics/fwdSimplTactic.mli @@ -25,7 +25,8 @@ val lapply_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic + ?linear:bool -> ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> + ProofEngineTypes.tactic val fwd_simpl_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml index cf7df2d58..c3e6f04aa 100644 --- a/components/tactics/proofEngineHelpers.ml +++ b/components/tactics/proofEngineHelpers.ml @@ -686,3 +686,22 @@ let lookup_type metasenv context hyp = | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal")) in aux 1 context + +(* FG: **********************************************************************) + +let list_rev_map_filter f l = + let rec aux a = function + | [] -> a + | hd :: tl -> + begin match f hd with + | None -> aux a tl + | Some b -> aux (b :: a) tl + end + in + aux [] l + +let get_name context index = + try match List.nth context (pred index) with + | Some (Cic.Name name, _) -> Some name + | _ -> None + with Invalid_argument "List.nth" -> None diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli index a7c0e5b54..0b5db790d 100644 --- a/components/tactics/proofEngineHelpers.mli +++ b/components/tactics/proofEngineHelpers.mli @@ -116,3 +116,9 @@ val saturate_term: (* returns the index and the type of a premise in a context *) val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term +(* FG: some helper functions ************************************************) + +val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list + +val get_name: Cic.context -> int -> string option + diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 5bacca20c..73d864e1d 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Jun 27 17:58:26 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 28 17:27:38 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 @@ -55,6 +55,7 @@ val intros : val inversion : term:Cic.term -> ProofEngineTypes.tactic val lapply : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?linear:bool -> ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic val left : ProofEngineTypes.tactic diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma index 168cfbc2b..c630d3dfe 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 *) @@ -49,7 +49,7 @@ theorem add_gen_S_2: \forall p,q,r. add p (S q) r \to intros. inversion H; clear H; intros; [ lapply eq_gen_S_O to H as H0. apply H0 | clear H1 H3 r. - lapply eq_gen_S_S to H2 as H0. clear H2. + lapply linear eq_gen_S_S to H2 as H0. rewrite > H0. clear H0 q. apply ex_intro; [| auto ] (**) ]. @@ -70,7 +70,7 @@ theorem add_gen_S_3: \forall p,q,r. add p q (S r) \to intros. inversion H; clear H; intros; [ rewrite < H1. clear H1 p | clear H1. - lapply eq_gen_S_S to H3 as H0. clear H3. + lapply linear eq_gen_S_S to H3 as H0. rewrite > H0. clear H0 r. ]; apply ex_intro; [| auto || auto ] (**) qed. @@ -79,13 +79,13 @@ 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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p. auto | clear H. - lapply add_gen_S_2 to H1 as H0. clear H1. + lapply linear add_gen_S_2 to H1 as H0. decompose. - lapply eq_gen_O_S to H1 as H0. apply H0 + lapply linear eq_gen_O_S to H1 as H0. apply H0 ]. qed. @@ -93,12 +93,12 @@ variant add_gen_S_3_alt: \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 2. elim q; clear q; intros; - [ lapply add_gen_O_2 to H as H0. clear H. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p | clear H. - lapply add_gen_S_2 to H1 as H0. clear H1. + lapply linear add_gen_S_2 to H1 as H0. decompose. - lapply eq_gen_S_S to H1 as H0. clear H1. + lapply linear eq_gen_S_S to H1 as H0. rewrite > H0. clear H0 r. ]; apply ex_intro; [| auto || auto ]. (**) qed. @@ -107,22 +107,22 @@ 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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p - | lapply add_gen_S_2 to H1 as H0. clear H1. + | lapply linear add_gen_S_2 to H1 as H0. decompose. - lapply eq_gen_S_S to H2 as H0. clear H2. + lapply linear eq_gen_S_S to H2 as H0. 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. + [ lapply linear add_gen_O_1 to H as H0. rewrite > H0. clear H0 q - | lapply add_gen_S_1 to H1 as H0. clear H1. + | lapply linear add_gen_S_1 to H1 as H0. decompose. - lapply eq_gen_S_S to H2 as H0. clear H2. + lapply linear eq_gen_S_S to H2 as H0. 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 ab59c3a51..dd360676b 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma @@ -22,9 +22,9 @@ 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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p - | lapply add_gen_S_2 to H1 as H0. clear H1. + | lapply linear add_gen_S_2 to H1 as H0. decompose. rewrite > H2. clear H2 r ]; auto. @@ -32,9 +32,9 @@ 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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p - | lapply add_gen_S_2 to H1 as H0. clear H1. + | lapply linear add_gen_S_2 to H1 as H0. decompose. rewrite > H2. clear H2 r ]; auto. @@ -42,7 +42,7 @@ 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. + lapply linear add_gen_S_2 to H as H0. decompose. rewrite > H1. clear H1 r. auto. @@ -50,7 +50,7 @@ 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. + lapply linear add_gen_S_1 to H as H0. decompose. rewrite > H1. clear H1 r. auto. @@ -60,15 +60,15 @@ theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to \forall q2,r2. add r1 q2 r2 \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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p - | lapply add_gen_S_2 to H1 as H0. clear H1. + | lapply linear add_gen_S_2 to H1 as H0. decompose. rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply add_gen_S_1 to H2 as H0. clear H2. + lapply linear add_gen_S_1 to H2 as H0. decompose. rewrite > H2. clear H2 r2. - lapply H to H4, H3 as H0. clear H H4 H3. + lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto || auto ]. (**) qed. @@ -77,15 +77,15 @@ theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to \forall p2,r2. add p2 r1 r2 \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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0. clear H0 p1 - | lapply add_gen_S_2 to H1 as H0. clear H1. + | lapply linear add_gen_S_2 to H1 as H0. decompose. rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply add_gen_S_2 to H2 as H0. clear H2. + lapply linear add_gen_S_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. - lapply H to H4, H3 as H0. clear H H4 H3. + lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto || auto ]. (**) qed. @@ -93,12 +93,12 @@ qed. 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. + [ lapply linear add_gen_O_2 to H as H0. rewrite > H0 in H1. clear H0 p - | lapply add_gen_S_2 to H1 as H0. clear H1. + | lapply linear add_gen_S_2 to H1 as H0. decompose. rewrite > H3. clear H3 r1. - lapply add_gen_S_2 to H2 as H0. clear H2. + lapply linear add_gen_S_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. ]; auto. diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 56c2a6616..130c08e56 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -1061,7 +1061,7 @@ its constructor takes no arguments. lapply lapply - lapply depth=d t + lapply linear depth=d t to t1, ..., tn as H @@ -1071,6 +1071,7 @@ its constructor takes no arguments. lapply + [linear] [depth=&nat;] &sterm; [to @@ -1108,6 +1109,10 @@ its constructor takes no arguments. Usually the other ?'s preceding the n-th independent premise of t are istantiated as a consequence. + If the linear flag is specified and if + t, t1, ..., tn + are (applications of) premises in the current context, they are + cleared. diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index 45e097e1b..dd14d8a26 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -117,6 +117,7 @@ lapply + [linear] [depth=nat] sterm [to -- 2.39.2