From cea3a50f515d1e39467073d2b447a9ddfa1a4852 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 21 Feb 2007 14:15:55 +0000 Subject: [PATCH] procedural : some improvements. decompose tactic: user provided premise and types removed. The decomposable types are now the non-recursive inductive types without right parameters and are auto-detected --- .../acic_procedural/acic2Procedural.ml | 31 +++-- .../acic_procedural/proceduralConversion.ml | 95 +++++++++++++- .../acic_procedural/proceduralConversion.mli | 5 + .../software/components/grafite/grafiteAst.ml | 6 +- .../components/grafite/grafiteAstPp.ml | 11 +- .../grafite_engine/grafiteEngine.ml | 10 +- .../grafite_parser/grafiteDisambiguate.ml | 20 +-- .../grafite_parser/grafiteParser.ml | 7 +- .../components/tactics/eliminationTactics.ml | 121 +++++++++--------- .../components/tactics/eliminationTactics.mli | 3 +- helm/software/components/tactics/tactics.mli | 5 +- helm/software/matita/help/C/sec_tactics.xml | 29 ++--- 12 files changed, 205 insertions(+), 138 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index b1cbc74ab..22936c1a4 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -228,7 +228,7 @@ and mk_fwd_rewrite st dtext name tl direction = [T.Branch (qs, ""); p2; p1] and mk_fwd_proof st dtext name = function - | C.AAppl (_, hd :: tl) as v -> + | C.AAppl (_, hd :: tl) as v -> if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in @@ -241,11 +241,16 @@ and mk_fwd_proof st dtext name = function let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in [T.LetIn (name, v, dtext ^ text)] end - | v -> - [T.LetIn (name, v, dtext)] + | C.AMutCase (id, uri, tyno, outty, arg, cases) as v -> + begin match Cn.mk_ind st.context id uri tyno outty arg cases with + | None -> [T.LetIn (name, v, dtext)] + | Some v -> mk_fwd_proof st dtext name v + end + | v -> + [T.LetIn (name, v, dtext)] and mk_proof st = function - | C.ALambda (_, name, v, t) as what -> + | C.ALambda (_, name, v, t) as what -> let entry = Some (name, C.Decl (cic v)) in let intro = get_intro name t in let ety = match get_inner_types st what with @@ -253,7 +258,7 @@ and mk_proof st = function | None -> None in mk_proof (add st entry intro ety) t - | C.ALetIn (_, name, v, t) as what -> + | C.ALetIn (_, name, v, t) as what -> let proceed, dtext = test_depth st in let script = if proceed then let entry = Some (name, C.Def (cic v, None)) in @@ -264,16 +269,16 @@ and mk_proof st = function [T.Apply (what, dtext)] in mk_intros st script - | C.ARel _ as what -> + | C.ARel _ as what -> let _, dtext = test_depth st in let text = "assumption" in let script = [T.Apply (what, dtext ^ text)] in mk_intros st script - | C.AMutConstruct _ as what -> + | C.AMutConstruct _ as what -> let _, dtext = test_depth st in let script = [T.Apply (what, dtext)] in mk_intros st script - | C.AAppl (_, hd :: tl) as t -> + | C.AAppl (_, hd :: tl) as t -> let proceed, dtext = test_depth st in let script = if proceed then let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in @@ -308,7 +313,15 @@ and mk_proof st = function [T.Apply (t, dtext)] in mk_intros st script - | t -> + | C.AMutCase (id, uri, tyno, outty, arg, cases) -> + begin match Cn.mk_ind st.context id uri tyno outty arg cases with + | None -> + let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in + let script = [T.Note text] in + mk_intros st script + | Some t -> mk_proof st t + end + | t -> let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in let script = [T.Note text] in mk_intros st script diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index abd6fd62a..555523a62 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -23,7 +23,40 @@ * http://cs.unibo.it/helm/. *) -module C = Cic +module C = Cic +module E = CicEnvironment +module Un = CicUniv +module TC = CicTypeChecker +module D = Deannotate +module UM = UriManager + +module T = ProceduralTypes + +(* helpers ******************************************************************) + +let cic = D.deannotate_term + +let get_ind_type uri tyno = + match E.get_obj Un.empty_ugraph uri with + | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno + | _ -> assert false + +let get_default_eliminator context uri tyno ty = + let _, (name, _, _, _) = get_ind_type uri tyno in + let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in + let ext = match sort with + | C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.CProp -> "_rec" + | C.Sort (C.Type _) -> "_rect" + | C.Meta (_,_) -> assert false + | _ -> assert false + in + let buri = UM.buri_of_uri uri in + let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in + C.Const (uri, []) + +(* proof construction *******************************************************) let rec need_whd i = function | C.ACast (_, t, _) -> need_whd i t @@ -59,3 +92,63 @@ let lift k n = | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) in lift_term k + +let fake_annotate c = + let get_binder c m = + try match List.nth c (pred m) with + | Some (C.Name s, _) -> s + | _ -> assert false + with + | Invalid_argument _ -> assert false + in + let mk_decl n v = Some (n, C.Decl v) in + let mk_def n v = Some (n, C.Def (v, None)) in + let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in + let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in + let rec ann_xns c (uri, t) = uri, ann_term c t + and ann_ms c = function + | None -> None + | Some t -> Some (ann_term c t) + and ann_fix newc c (name, i, ty, bo) = + "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo + and ann_cofix newc c (name, ty, bo) = + "", name, ann_term c ty, ann_term (List.rev_append newc c) bo + and ann_term c = function + | C.Sort sort -> C.ASort ("", sort) + | C.Implicit ann -> C.AImplicit ("", ann) + | C.Rel m -> C.ARel ("", "", m, get_binder c m) + | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss) + | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss) + | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss) + | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss) + | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss) + | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts) + | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty) + | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl) + | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t) + | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t) + | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t) + | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl) + | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl) + in + ann_term c + +let rec add_abst n t = + if n <= 0 then t else + let t = C.ALambda ("", C.Anonymous, C.AImplicit ("", None), lift 0 1 t) in + add_abst (pred n) t + +let mk_ind context id uri tyno outty arg cases = + let lpsno, (_, _, arity, constructors) = get_ind_type uri tyno in + let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in + let ps = match inty with + | C.MutInd _ -> [] + | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args + | _ -> assert false + in + let lps, rps = T.list_split lpsno ps in + let eliminator = get_default_eliminator context uri tyno inty in + let arg_ref = T.mk_arel 0 "" in + let body = C.AMutCase (id, uri, tyno, outty, arg_ref, cases) in + let predicate = add_abst (succ (List.length rps)) body in + None diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli index d5ad4fd1c..fef3ad07b 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.mli +++ b/helm/software/components/acic_procedural/proceduralConversion.mli @@ -26,3 +26,8 @@ val need_whd: int -> Cic.annterm -> bool val lift: int -> int -> Cic.annterm -> Cic.annterm + +val mk_ind: + Cic.context -> Cic.id -> UriManager.uri -> int -> + Cic.annterm -> Cic.annterm -> Cic.annterm list -> + Cic.annterm option diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 10d7b6bcc..24fb99d79 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -32,10 +32,6 @@ type loc = Token.flocation type ('term, 'lazy_term, 'ident) pattern = 'lazy_term option * ('ident * 'term) list * 'term option -type ('term, 'ident) type_spec = - | Ident of 'ident - | Type of UriManager.uri * int - type 'lazy_term reduction = [ `Normalize | `Reduce @@ -56,7 +52,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Constructor of loc * int | Contradiction of loc | Cut of loc * 'ident option * 'term - | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list + | Decompose of loc * 'ident list | Demodulate of loc | Destruct of loc * 'term | Elim of loc * 'term * 'term option * int option * 'ident list diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index d5fbf8034..423e68d4f 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -95,15 +95,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Cut (_, ident, term) -> "cut " ^ term_pp term ^ (match ident with None -> "" | Some id -> " as " ^ id) - | Decompose (_, [], what, 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) (opt_string_pp what) (pp_intros_specs (None, names)) + | Decompose (_, names) -> + sprintf "decompose%s" (pp_intros_specs (None, names)) | Demodulate _ -> "demodulate" | Destruct (_, term) -> "destruct " ^ term_pp term | Elim (_, term, using, num, idents) -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ab9813221..1714bf470 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -80,15 +80,9 @@ let tactic_of_ast status ast = | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | GrafiteAst.Decompose (_, types, what, names) -> - let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, Some typeno - | GrafiteAst.Ident _ -> assert false - in - let user_types = List.rev_map to_type types in - let dbd = LibraryDb.instance () in + | GrafiteAst.Decompose (_, names) -> 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 () | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 7d110e2df..0c64bbb07 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -148,24 +148,8 @@ let disambiguate_tactic | GrafiteAst.Cut (loc, ident, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.Decompose (loc, types, what, names) -> - let disambiguate (metasenv,types) = function - | GrafiteAst.Type _ -> assert false - | GrafiteAst.Ident id -> - (match - disambiguate_term context metasenv - (CicNotationPt.Ident(id, None)) - with - | metasenv,Cic.MutInd (uri, tyno, _) -> - metasenv,(GrafiteAst.Type (uri, tyno) :: types) - | _ -> - raise (GrafiteDisambiguator.DisambiguationError - (0,[[[],[],None,lazy "Decompose works only on inductive types",true]]))) - in - let metasenv,types = - List.fold_left disambiguate (metasenv,[]) types - in - metasenv,GrafiteAst.Decompose (loc, types, what, names) + | GrafiteAst.Decompose (loc, names) -> + metasenv,GrafiteAst.Decompose (loc, names) | GrafiteAst.Demodulate loc -> metasenv,GrafiteAst.Demodulate loc | GrafiteAst.Destruct (loc,term) -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 64c10b9b4..fd757d141 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -157,12 +157,9 @@ 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 = OPT IDENT; - idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> - let types = match types with None -> [] | Some types -> types in + | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> 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) + GrafiteAst.Decompose (loc, idents) | IDENT "demodulate" -> GrafiteAst.Demodulate loc | IDENT "destruct"; t = tactic_term -> GrafiteAst.Destruct (loc, t) diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index d05826ec0..c98f020d7 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -25,29 +25,30 @@ (* $Id$ *) -module C = Cic -module P = PrimitiveTactics -module T = Tacticals -module S = ProofEngineStructuralRules -module F = FreshNamesGenerator -module E = ProofEngineTypes -module H = ProofEngineHelpers -module R = ReductionTactics - -(* -(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) -let search_inductive_types ty = - let rec aux types = function - | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> - (uri, typeno) :: types - | C.Appl applist -> List.fold_left aux types applist - | _ -> types - in - aux [] ty -(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) -*) +module C = Cic +module P = PrimitiveTactics +module T = Tacticals +module S = ProofEngineStructuralRules +module F = FreshNamesGenerator +module PET = ProofEngineTypes +module H = ProofEngineHelpers +module RT = ReductionTactics +module E = CicEnvironment +module R = CicReduction +module Un = CicUniv + +(* from ProceduralClasify ***************************************************) + +let split c t = + let add s v c = Some (s, C.Decl v) :: c in + let rec aux whd a n c = function + | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t + | v when whd -> v :: a, n + | v -> aux true a n c (R.whd ~delta:true c v) + in + aux false [] 0 c t -(* unexported tactics *******************************************************) +(****************************************************************************) type type_class = Other | Ind @@ -55,6 +56,25 @@ type type_class = Other let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None +let get_inductive_type uri tyno = + match E.get_obj Un.empty_ugraph uri with + | C.InductiveDefinition (tys, _, lpsno, _), _ -> + let _, inductive, arity, _ = List.nth tys tyno in + lpsno, inductive, arity + | _ -> assert false + +let rec check_type = function + | C.MutInd (uri, tyno, _) -> + let lpsno, inductive, arity = get_inductive_type uri tyno in + let _, psno = split [] arity in + if lpsno <> psno && inductive then Other else Ind +(* | C.Const (uri, _) as t -> + if List.mem (uri, None) types then Con (PET.const_lazy_term t) else Other +*) | C.Appl (hd :: tl) -> check_type hd + | _ -> Other + +(* unexported tactics *******************************************************) + let rec scan_tac ~old_context_length ~index ~tactic = let scan_tac status = let (proof, goal) = status in @@ -69,39 +89,29 @@ let rec scan_tac ~old_context_length ~index ~tactic = let tac = T.then_ ~start:(tactic ~what) ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic) in - try E.apply_tactic tac status - with E.Fail _ -> aux (pred index) + try PET.apply_tactic tac status + with PET.Fail _ -> aux (pred index) in aux (index + context_length - old_context_length) in - E.mk_tactic scan_tac - -let rec check_types types = function - | C.MutInd (uri, typeno, _) -> - if List.mem (uri, Some typeno) types then Ind else Other - | C.Const (uri, _) as t -> - if List.mem (uri, None) types then Con (E.const_lazy_term t) else Other - | C.Appl (hd :: tl) -> check_types types hd - | _ -> Other + PET.mk_tactic scan_tac -let elim_clear_unfold_tac ~mk_fresh_name_callback ~types ~what = +let elim_clear_unfold_tac ~mk_fresh_name_callback ~what = let elim_clear_unfold_tac status = let (proof, goal) = status in let _, metasenv, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let index, ty = H.lookup_type metasenv context what in - match check_types types ty with - | Ind -> - let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) - ~continuation:(S.clear [what]) - in - E.apply_tactic tac status - | Con t -> - let tac = R.unfold_tac (Some t) ~pattern:(premise_pattern what) in - E.apply_tactic tac status + let tac = match check_type ty with + | Ind -> T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) + ~continuation:(S.clear [what]) + | Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what) | Other -> - raise (E.Fail (lazy "unexported elim_clear: not an eliminable type")) + let msg = "unexported elim_clear: not an decomposable type" in + raise (PET.Fail (lazy msg)) + in + PET.apply_tactic tac status in - E.mk_tactic elim_clear_unfold_tac + PET.mk_tactic elim_clear_unfold_tac (* elim type ****************************************************************) @@ -115,9 +125,9 @@ let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth let tac = T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac] in - E.apply_tactic tac status + PET.apply_tactic tac status in - E.mk_tactic elim_type_tac + PET.mk_tactic elim_type_tac (* decompose ****************************************************************) @@ -132,22 +142,15 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) (* roba seria ------------------------------------------------------------- *) -let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) - ?(user_types=[]) ?what ~dbd = +let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () = 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_unfold_tac ~mk_fresh_name_callback ~types in + let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback in 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 + let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic in - E.apply_tactic tac status + PET.apply_tactic tac status in - E.mk_tactic decompose_tac + PET.mk_tactic decompose_tac diff --git a/helm/software/components/tactics/eliminationTactics.mli b/helm/software/components/tactics/eliminationTactics.mli index 379166ac0..492566042 100644 --- a/helm/software/components/tactics/eliminationTactics.mli +++ b/helm/software/components/tactics/eliminationTactics.mli @@ -29,5 +29,4 @@ val elim_type_tac: val decompose_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?user_types:((UriManager.uri * int option) list) -> - ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic + unit -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index d821a3cb2..f0ac7adc8 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jan 24 20:31:34 CET 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Feb 21 14:36:23 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -25,8 +25,7 @@ val cut : Cic.term -> ProofEngineTypes.tactic val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?user_types:(UriManager.uri * int option) list -> - ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic + unit -> ProofEngineTypes.tactic val demodulate : dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic val destruct : term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index aa9610df0..cad04a53c 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -496,8 +496,7 @@ decompose decompose - decompose (T1 ... Tn) - H as H1 ... Hm + decompose as H1 ... Hm @@ -506,10 +505,6 @@ decompose - [( - &id;… - )] - [&id;] [as &id;…] @@ -517,26 +512,22 @@ Pre-conditions: - - H must inhabit one inductive type among - - T1 ... Tn - - and the types of a predefined list. - + None. Action: - Runs - elim H H1 ... Hm - , clears H and tries to run itself - recursively on each new identifier introduced by + For each each premise H + of type T in the current context + where T is a non-recursive inductive type + withour right parameters, the tactic runs + + elim H as H1 ... Hm + , clears H and runs itself + recursively on each new premise introduced by elim in the opened sequents. - If H is not provided tries this operation on - each premise in the current context. -- 2.39.2