From 249d79bebff886846fbab65cc079623d90684baf Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 5 Jul 2005 15:49:26 +0000 Subject: [PATCH] name specifications added for elim_intros, elim_intros_simpl and elim_type --- helm/coq-contribs/LAMBDA-TYPES/pr3_props.v | 3 +- helm/matita/matita.lang | 1 + helm/matita/matitaEngine.ml | 31 +++++++++++-------- helm/matita/matitaGui.ml | 4 +-- helm/matita/tests/fguidi.ma | 9 +++++- .../cic_disambiguation/cicTextualLexer2.ml | 2 +- .../cic_disambiguation/cicTextualParser2.ml | 15 ++++++--- helm/ocaml/cic_transformations/tacticAst.ml | 4 +-- helm/ocaml/cic_transformations/tacticAstPp.ml | 14 +++++++-- helm/ocaml/tactics/discriminationTactics.ml | 3 +- helm/ocaml/tactics/eliminationTactics.ml | 15 ++++----- helm/ocaml/tactics/eliminationTactics.mli | 4 ++- helm/ocaml/tactics/negationTactics.ml | 4 +-- helm/ocaml/tactics/primitiveTactics.ml | 14 +++++---- helm/ocaml/tactics/primitiveTactics.mli | 6 ++-- helm/ocaml/tactics/ring.ml | 3 +- helm/ocaml/tactics/tactics.mli | 12 +++++-- 17 files changed, 94 insertions(+), 50 deletions(-) diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v index dfdc49c50..106bfe66c 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v @@ -35,7 +35,7 @@ Require pr3_defs. (* case 2.1 : i0 = 0 *) DropGenBase; Inversion H2; Clear H2. Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0. - Subst0Subst0; Arith9'In H4 i; XDEAuto 7. + Subst0Subst0; Arith9'In H4 i. (*; XDEAuto 7. (* case 2.2 : i0 > 0 *) Clear IHi0; NewInduction k; DropGenBase; XEAuto. Qed. @@ -111,3 +111,4 @@ Require pr3_defs. Hints Resolve pr3_lift : ltlc. +*) diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index 5941b1126..67f724ce0 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -42,6 +42,7 @@ to as using + names diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 0e46c34d2..7f70736ab 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -40,9 +40,10 @@ let tactic_of_ast = function | TacticAst.DecideEquality _ -> Tactics.decide_equality | TacticAst.Decompose (_,term) -> Tactics.decompose term | TacticAst.Discriminate (_,term) -> Tactics.discriminate term - | TacticAst.Elim (_, term, _) -> - Tactics.elim_intros term - | TacticAst.ElimType (_, term) -> Tactics.elim_type term + | TacticAst.Elim (_, what, using, depth, names) -> + Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what + | TacticAst.ElimType (_, what, using, depth, names) -> + Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what | TacticAst.Exact (_, term) -> Tactics.exact term | TacticAst.Exists _ -> Tactics.exists | TacticAst.Fail _ -> Tactics.fail @@ -447,16 +448,20 @@ let disambiguate_tactic status = function | TacticAst.Exact (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Exact (loc, cic) - | TacticAst.Elim (loc, term, Some term') -> - let status, cic1 = disambiguate_term status term in - let status, cic2 = disambiguate_term status term' in - status, TacticAst.Elim (loc, cic1, Some cic2) - | TacticAst.Elim (loc, term, None) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Elim (loc, cic, None) - | TacticAst.ElimType (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.ElimType (loc, cic) + | TacticAst.Elim (loc, what, Some using, depth, idents) -> + let status, what = disambiguate_term status what in + let status, using = disambiguate_term status using in + status, TacticAst.Elim (loc, what, Some using, depth, idents) + | TacticAst.Elim (loc, what, None, depth, idents) -> + let status, what = disambiguate_term status what in + status, TacticAst.Elim (loc, what, None, depth, idents) + | TacticAst.ElimType (loc, what, Some using, depth, idents) -> + let status, what = disambiguate_term status what in + let status, using = disambiguate_term status using in + status, TacticAst.ElimType (loc, what, Some using, depth, idents) + | TacticAst.ElimType (loc, what, None, depth, idents) -> + let status, what = disambiguate_term status what in + status, TacticAst.ElimType (loc, what, None, depth, idents) | TacticAst.Exists loc -> status, TacticAst.Exists loc | TacticAst.Fail loc -> status,TacticAst.Fail loc | TacticAst.Fold (loc,reduction_kind, term, pattern) -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index c9b387178..5ac24f8f6 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -156,8 +156,8 @@ class gui () = connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); - connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None))); - connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole))); + connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, []))); + connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, []))); connect_button tbar#splitButton (tac (A.Split loc)); connect_button tbar#leftButton (tac (A.Left loc)); connect_button tbar#rightButton (tac (A.Right loc)); diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index e42de00b5..141e29776 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -94,5 +94,12 @@ qed. theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). intros 1. elim x. auto. -fwd H1 []. +fwd H1 [H0]. +elim H0 names [pippo; pappo]. + +decompose H0 + + +elim H0. clear H0. elim H1. clear H1. + *) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 32d8ae54d..92a24ec82 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -66,7 +66,7 @@ let keywords = Hashtbl.create 17 let _ = List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with"; - "in"; "and"; "to"; "as"; "on"] + "in"; "and"; "to"; "as"; "on"; "names"] let error lexbuf msg = raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg)) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 59bb1bc81..9ce70062f 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -398,11 +398,16 @@ EXTEND TacticAst.Decompose (loc, where) | IDENT "discriminate"; t = tactic_term -> TacticAst.Discriminate (loc, t) - | IDENT "elim"; t1 = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ] -> - TacticAst.Elim (loc, t1, using) - | IDENT "elimType"; t = tactic_term -> - TacticAst.ElimType (loc, t) + | IDENT "elim"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.Elim (loc, what, using, num, idents) + | IDENT "elimType"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.ElimType (loc, what, using, num, idents) | IDENT "exact"; t = tactic_term -> TacticAst.Exact (loc, t) | IDENT "exists" -> diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 0dfb48aed..581b44698 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -45,8 +45,8 @@ type ('term, 'ident) tactic = | DecideEquality of loc | Decompose of loc * 'term | Discriminate of loc * 'term - | Elim of loc * 'term * 'term option (* what to elim, which principle to use *) - | ElimType of loc * 'term + | Elim of loc * 'term * 'term option * int option * 'ident list + | ElimType of loc * 'term * 'term option * int option * 'ident list | Exact of loc * 'term | Exists of loc | Fail of loc diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 21bf33a0a..327595365 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -57,6 +57,12 @@ let pp_pattern (t, hyp, goal) = in pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal +let pp_intros_specs = function + | None, [] -> "" + | Some num, [] -> Printf.sprintf " names %i" num + | None, idents -> Printf.sprintf " names %s" (pp_idents idents) + | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents) + let rec pp_tactic = function | Absurd (_, term) -> "absurd" ^ pp_term_ast term | Apply (_, term) -> "apply " ^ pp_term_ast term @@ -76,10 +82,14 @@ let rec pp_tactic = function | Decompose (_, term) -> sprintf "decompose %s" (pp_term_ast term) | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term - | Elim (_, term, using) -> + | Elim (_, term, using, num, idents) -> sprintf "elim " ^ pp_term_ast term ^ (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) - | ElimType (_, term) -> "elim type " ^ pp_term_ast term + ^ pp_intros_specs (num, idents) + | ElimType (_, term, using, num, idents) -> + sprintf "elim type " ^ pp_term_ast term ^ + (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + ^ pp_intros_specs (num, idents) | Exact (_, term) -> "exact " ^ pp_term_ast term | Exists _ -> "exists" | Fold (_, kind, term, pattern) -> diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 0f06351b4..76b733734 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -204,6 +204,7 @@ exception TwoDifferentSubtermsFound of int (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) +(* FG: METTERE I NOMI ANCHE QUI? *) let discriminate'_tac ~term = let discriminate'_tac ~term status = let (proof, goal) = status in @@ -287,7 +288,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - ~term:(C.MutInd(LibraryObjects.false_URI (),0,[]))) + (C.MutInd(LibraryObjects.false_URI (),0,[]))) status in (match goals' with diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 4f840764a..e52fff6e4 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -57,18 +57,19 @@ let induction_tac ~term status = ;; *) -let elim_type_tac ~term = - let elim_type_tac ~term status = +let elim_type_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ?depth ?using what = + let elim_type_tac status = let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in ProofEngineTypes.apply_tactic (T.thens - ~start: (P.cut_tac term) - ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]) + ~start: (P.cut_tac what) + ~continuations:[ P.elim_intros_simpl_tac ?depth ?using ~mk_fresh_name_callback (C.Rel 1) ; T.id_tac ]) status in - ProofEngineTypes.mk_tactic (elim_type_tac ~term) + ProofEngineTypes.mk_tactic elim_type_tac ;; @@ -107,7 +108,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) | _ -> urilist - (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *) + (* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) in let rec purge_duplicates urilist = let rec aux triple urilist = @@ -148,7 +149,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = warn ("elim " ^ CicPp.ppterm termty); ProofEngineTypes.apply_tactic (T.then_ - ~start:(P.elim_intros_simpl_tac ~term:term') + ~start:(P.elim_intros_simpl_tac term') ~continuation:( (* clear the hyp that has just been eliminated *) ProofEngineTypes.mk_tactic (fun status -> diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli index 92d9eee01..111bc5747 100644 --- a/helm/ocaml/tactics/eliminationTactics.mli +++ b/helm/ocaml/tactics/eliminationTactics.mli @@ -23,7 +23,9 @@ * http://cs.unibo.it/helm/. *) -val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic +val elim_type_tac: + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic (* The default callback always decomposes the term as much as possible *) val decompose_tac: diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index ee76921b2..0e3c0c142 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -46,6 +46,7 @@ let absurd_tac ~term = ProofEngineTypes.mk_tactic (absurd_tac ~term) ;; +(* FG: METTERE I NOMI ANCHE QUI? *) let contradiction_tac = let contradiction_tac status = let module C = Cic in @@ -60,8 +61,7 @@ let contradiction_tac = T.then_ ~start: (EliminationTactics.elim_type_tac - ~term: - (C.MutInd (LibraryObjects.false_URI (), 0, []))) + (C.MutInd (LibraryObjects.false_URI (), 0, []))) ~continuation: VariousTactics.assumption_tac)) status with diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 3fefc662a..06e83a125 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -574,17 +574,19 @@ let elim_tac ~term = mk_tactic (elim_tac ~term) ;; -let elim_intros_tac ~term = - Tacticals.then_ ~start:(elim_tac ~term) - ~continuation:(intros_tac ()) +let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ?depth ?using what = + Tacticals.then_ ~start:(elim_tac ~term:what) + ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ()) ;; (* The simplification is performed only on the conclusion *) -let elim_intros_simpl_tac ~term = - Tacticals.then_ ~start:(elim_tac ~term) +let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ?depth ?using what = + Tacticals.then_ ~start:(elim_tac ~term:what) ~continuation: (Tacticals.thens - ~start:(intros_tac ()) + ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ()) ~continuations: [ReductionTactics.simpl_tac ~pattern:(ProofEngineTypes.conclusion_pattern None)]) diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli index 2e35f4250..6dac98724 100644 --- a/helm/ocaml/tactics/primitiveTactics.mli +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -52,6 +52,8 @@ val letin_tac: ProofEngineTypes.tactic val elim_intros_simpl_tac: - term: Cic.term -> ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic val elim_intros_tac: - term: Cic.term -> ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index 298a87f3c..1d5fd903d 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -388,12 +388,13 @@ let elim_type_tac ~term status = @param term term to cut @param proof term used to prove second subgoal generated by elim_type *) +(* FG: METTERE I NOMI ANCHE QUI? *) let elim_type2_tac ~term ~proof = let elim_type2_tac ~term ~proof status = let module E = EliminationTactics in warn "in Ring.elim_type2"; ProofEngineTypes.apply_tactic - (Tacticals.thens ~start:(E.elim_type_tac ~term) + (Tacticals.thens ~start:(E.elim_type_tac term) ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status in ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof) diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 32bbf2c6a..ff888d78b 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -25,9 +25,15 @@ val decompose : list) -> Cic.term -> ProofEngineTypes.tactic val discriminate : term:Cic.term -> ProofEngineTypes.tactic -val elim_intros : term:Cic.term -> ProofEngineTypes.tactic -val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic -val elim_type : term:Cic.term -> ProofEngineTypes.tactic +val elim_intros : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic +val elim_intros_simpl : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic +val elim_type : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic val exact : term:Cic.term -> ProofEngineTypes.tactic val exists : ProofEngineTypes.tactic val fail : ProofEngineTypes.tactic -- 2.39.2