From ef870606391fff198f215127eb022eb3e41ab1d4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Nov 2007 19:30:16 +0000 Subject: [PATCH] new implementation of the destruct tactic, which includes the old subst tactic (now removed) --- components/grafite/grafiteAst.ml | 3 +- components/grafite/grafiteAstPp.ml | 4 +- components/grafite_engine/grafiteEngine.ml | 3 +- .../grafite_parser/grafiteDisambiguate.ml | 8 +- components/grafite_parser/grafiteParser.ml | 6 +- components/tactics/.depend | 49 ++-- components/tactics/.depend.opt | 49 ++-- components/tactics/Makefile | 2 +- ...riminationTactics.ml => destructTactic.ml} | 269 ++++++++++++------ ...minationTactics.mli => destructTactic.mli} | 2 +- components/tactics/substTactic.ml | 164 ----------- components/tactics/substTactic.mli | 27 -- components/tactics/tactics.ml | 3 +- components/tactics/tactics.mli | 5 +- matita/library/Fsub/defn.ma | 26 +- matita/library/Fsub/part1a.ma | 14 +- matita/library/Fsub/part1a_inversion.ma | 16 +- matita/library/Fsub/util.ma | 17 +- matita/library/Z/z.ma | 2 +- matita/library/decidable_kit/fgraph.ma | 2 +- matita/library/decidable_kit/list_aux.ma | 2 +- matita/tests/destruct.ma | 9 +- 22 files changed, 285 insertions(+), 397 deletions(-) rename components/tactics/{discriminationTactics.ml => destructTactic.ml} (72%) rename components/tactics/{discriminationTactics.mli => destructTactic.mli} (95%) delete mode 100644 components/tactics/substTactic.ml delete mode 100644 components/tactics/substTactic.mli diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index a0bb2e4f9..3e87ffba5 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -71,7 +71,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Cut of loc * 'ident option * 'term | Decompose of loc * 'ident option list | Demodulate of loc - | Destruct of loc * 'term + | Destruct of loc * 'term option | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern * 'ident intros_spec | ElimType of loc * 'term * 'term option * 'ident intros_spec @@ -96,7 +96,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Right of loc | Ring of loc | Split of loc - | Subst of loc | Symmetry of loc | Transitivity of loc * 'term (* Costruttori Aggiunti *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index de7af8263..eb1a18e5a 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -126,7 +126,8 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = Printf.sprintf "decompose%s" (pp_intros_specs "names " (None, names)) | Demodulate _ -> "demodulate" - | Destruct (_, term) -> "destruct " ^ term_pp term + | Destruct (_, None) -> "destruct" + | Destruct (_, Some term) -> "destruct " ^ term_pp term | Elim (_, what, using, pattern, specs) -> Printf.sprintf "elim %s%s %s%s" (term_pp what) @@ -177,7 +178,6 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | Right _ -> "right" | Ring _ -> "ring" | Split _ -> "split" - | Subst _ -> "subst" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ term_pp term (* Tattiche Aggiunte *) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index f587d2def..0d2fb682e 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -95,7 +95,7 @@ let rec tactic_of_ast status ast = | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe - | GrafiteAst.Destruct (_,term) -> Tactics.destruct term + | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names) ~pattern what @@ -160,7 +160,6 @@ let rec tactic_of_ast status ast = | GrafiteAst.Right _ -> Tactics.right | GrafiteAst.Ring _ -> Tactics.ring | GrafiteAst.Split _ -> Tactics.split - | GrafiteAst.Subst _ -> Tactics.subst | GrafiteAst.Symmetry _ -> Tactics.symmetry | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term (* Implementazioni Aggiunte *) diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index d4ab241cb..2fe6b9aae 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -216,9 +216,11 @@ let rec disambiguate_tactic metasenv,GrafiteAst.Decompose (loc, names) | GrafiteAst.Demodulate loc -> metasenv,GrafiteAst.Demodulate loc - | GrafiteAst.Destruct (loc,term) -> + | GrafiteAst.Destruct (loc, Some term) -> let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Destruct(loc,term) + metasenv,GrafiteAst.Destruct(loc, Some term) + | GrafiteAst.Destruct (loc, None) -> + metasenv,GrafiteAst.Destruct(loc,None) | GrafiteAst.Exact (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Exact (loc, cic) @@ -294,8 +296,6 @@ let rec disambiguate_tactic metasenv,GrafiteAst.Ring loc | GrafiteAst.Split loc -> metasenv,GrafiteAst.Split loc - | GrafiteAst.Subst loc -> - metasenv, GrafiteAst.Subst loc | GrafiteAst.Symmetry loc -> metasenv,GrafiteAst.Symmetry loc | GrafiteAst.Transitivity (loc, term) -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 081055ce8..83e9d10d8 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -170,8 +170,8 @@ EXTEND let idents = match idents with None -> [] | Some idents -> idents in GrafiteAst.Decompose (loc, idents) | IDENT "demodulate" -> GrafiteAst.Demodulate loc - | IDENT "destruct"; t = tactic_term -> - GrafiteAst.Destruct (loc, t) + | IDENT "destruct"; xt = OPT [ t = tactic_term -> t ] -> + GrafiteAst.Destruct (loc, xt) | IDENT "elim"; what = tactic_term; using = using; pattern = OPT pattern_spec; (num, idents) = intros_spec -> @@ -246,8 +246,6 @@ EXTEND GrafiteAst.Ring loc | IDENT "split" -> GrafiteAst.Split loc - | IDENT "subst" -> - GrafiteAst.Subst loc | IDENT "symmetry" -> GrafiteAst.Symmetry loc | IDENT "transitivity"; t = tactic_term -> diff --git a/components/tactics/.depend b/components/tactics/.depend index 964011bfd..579ab17cc 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -23,8 +23,7 @@ eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.cmi -discriminationTactics.cmi: proofEngineTypes.cmi -substTactic.cmi: proofEngineTypes.cmi +destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi @@ -147,20 +146,14 @@ auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \ paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi -discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ - proofEngineTypes.cmi proofEngineStructuralRules.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \ - equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi -discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ - proofEngineTypes.cmx proofEngineStructuralRules.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ - equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi -substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \ - discriminationTactics.cmi substTactic.cmi -substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \ - discriminationTactics.cmx substTactic.cmi +destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ + eliminationTactics.cmi destructTactic.cmi +destructTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmx \ + eliminationTactics.cmx destructTactic.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi @@ -199,18 +192,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \ - ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \ - primitiveTactics.cmi negationTactics.cmi inversion.cmi \ - introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ - equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi -tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ - ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \ - primitiveTactics.cmx negationTactics.cmx inversion.cmx \ - introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ - equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi +tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \ + reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ + negationTactics.cmi inversion.cmi introductionTactics.cmi \ + fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \ + eliminationTactics.cmi destructTactic.cmi compose.cmi \ + closeCoercionGraph.cmi auto.cmi tactics.cmi +tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \ + reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \ + negationTactics.cmx inversion.cmx introductionTactics.cmx \ + fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ + eliminationTactics.cmx destructTactic.cmx compose.cmx \ + closeCoercionGraph.cmx auto.cmx tactics.cmi declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/components/tactics/.depend.opt b/components/tactics/.depend.opt index 964011bfd..579ab17cc 100644 --- a/components/tactics/.depend.opt +++ b/components/tactics/.depend.opt @@ -23,8 +23,7 @@ eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.cmi -discriminationTactics.cmi: proofEngineTypes.cmi -substTactic.cmi: proofEngineTypes.cmi +destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi @@ -147,20 +146,14 @@ auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \ paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi -discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ - proofEngineTypes.cmi proofEngineStructuralRules.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \ - equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi -discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ - proofEngineTypes.cmx proofEngineStructuralRules.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ - equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi -substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \ - discriminationTactics.cmi substTactic.cmi -substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \ - discriminationTactics.cmx substTactic.cmi +destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ + eliminationTactics.cmi destructTactic.cmi +destructTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmx \ + eliminationTactics.cmx destructTactic.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi @@ -199,18 +192,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \ - ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \ - primitiveTactics.cmi negationTactics.cmi inversion.cmi \ - introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ - equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi -tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ - ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \ - primitiveTactics.cmx negationTactics.cmx inversion.cmx \ - introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ - equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi +tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \ + reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ + negationTactics.cmi inversion.cmi introductionTactics.cmi \ + fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \ + eliminationTactics.cmi destructTactic.cmi compose.cmi \ + closeCoercionGraph.cmi auto.cmi tactics.cmi +tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \ + reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \ + negationTactics.cmx inversion.cmx introductionTactics.cmx \ + fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ + eliminationTactics.cmx destructTactic.cmx compose.cmx \ + closeCoercionGraph.cmx auto.cmx tactics.cmi declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index c4e020005..9a6c6d4d0 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -22,7 +22,7 @@ INTERFACE_FILES = \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli \ auto.mli \ - discriminationTactics.mli substTactic.mli \ + destructTactic.mli \ inversion.mli inversion_principle.mli ring.mli setoids.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli declarative.mli diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/destructTactic.ml similarity index 72% rename from components/tactics/discriminationTactics.ml rename to components/tactics/destructTactic.ml index 83f676ed3..bbfee8041 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/destructTactic.ml @@ -38,8 +38,10 @@ module S = CicSubstitution module RT = ReductionTactics module PEH = ProofEngineHelpers module ET = EqualityTactics +module DTI = DoubleTypeInference +module FNG = FreshNamesGenerator -let debug = false +let debug = true let debug_print = if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) @@ -139,7 +141,7 @@ let discriminate_tac ~term = let mk_branches_and_outtype turi typeno consno context args = (* a list of "True" except for the element in position consno which * is "False" *) - match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with + match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with | C.InductiveDefinition (ind_type_list,_,paramsno,_) -> let _,_,rty,constructor_list = List.nth ind_type_list typeno in let false_constr_id,_ = List.nth constructor_list (consno - 1) in @@ -205,7 +207,7 @@ let discriminate_tac ~term = let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = - CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph + CTC.type_of_aux' metasenv context term CU.empty_ugraph in match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] @@ -253,8 +255,6 @@ let discriminate_tac ~term = in PET.mk_tactic (discriminate'_tac ~term) -let exn_nonproj = - PET.Fail (lazy "Injection: not a projectable equality") let exn_noneq = PET.Fail (lazy "Injection: not an equality") let exn_nothingtodo = @@ -270,15 +270,27 @@ let pp ctx t = let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in CicPp.pp t names -let clear_term first_time context term = - let g () = if first_time then raise exn_nothingtodo else T.id_tac in - match term with - | C.Rel n -> - begin match List.nth context (pred n) with - | Some (C.Name id, _) -> PST.clear ~hyps:[id] - | _ -> assert false - end - | _ -> g () +let clear_term first_time lterm = + let clear_term status = + let (proof, goal) = status in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + debug_print (lazy ("\nclear di: " ^ pp context term)); + debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); + let g () = if first_time then raise exn_nothingtodo else T.id_tac in + let tactic = match term with + | C.Rel n -> + begin match List.nth context (pred n) with + | Some (C.Name id, _) -> + T.if_ ~fail:(g ()) ~start:(PST.clear ~hyps:[id]) ~continuation:T.id_tac + | _ -> assert false + end + | _ -> g () + in + PET.apply_tactic tactic status + in + PET.mk_tactic clear_term let simpl_in_term context = function | Cic.Rel i -> @@ -288,12 +300,36 @@ let simpl_in_term context = function | _ -> assert false in RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) - | _ -> raise exn_nonproj + | _ -> T.id_tac -(* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa assoluta - *) -let rec injection_tac ~map ~term ~i ~continuation = +let mk_fresh_name metasenv context name typ = + let name = C.Name name in + match FNG.mk_fresh_name ~subst:[] metasenv context name ~typ with + | C.Name s -> s + | C.Anonymous -> assert false + +let exists context = function + | C.Rel i -> List.nth context (pred i) <> None + | _ -> true + +let rec recur_on_child_tac name = + let recur_on_child status = + let (proof, goal) = status in + let _, metasenv, _subst, _, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + debug_print (lazy ("\nrecur_on_child su: " ^ name)); + debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); + let rec search_name i = function + | [] -> T.id_tac + | Some (Cic.Name n, _) :: _ when n = name -> + destruct ~first_time:false ~term:(Cic.Rel i) + | _ :: tl -> search_name (succ i) tl + in + PET.apply_tactic (search_name 1 context) status + in + PET.mk_tactic recur_on_child + +and injection_tac ~lterm ~i ~continuation = let give_name seed = function | C.Name _ as name -> name | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed) @@ -306,9 +342,9 @@ let rec injection_tac ~map ~term ~i ~continuation = * del costruttore *) let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term = relocate_term map term in - let termty,_ = - CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph + let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + let termty,_ = + CTC.type_of_aux' metasenv context term CU.empty_ugraph in debug_print (lazy ("\ninjection su : " ^ pp context termty)); match termty with (* an equality *) @@ -332,7 +368,7 @@ let rec injection_tac ~map ~term ~i ~continuation = in let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in let patterns,outtype = - match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with + match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with | C.InductiveDefinition (ind_type_list,_,paramsno,_)-> let left_params, right_params = HExtlib.split_nth paramsno params in let _,_,_,constructor_list = List.nth ind_type_list typeno in @@ -412,18 +448,19 @@ let rec injection_tac ~map ~term ~i ~continuation = let go_on = try let _,g = CTC.type_of_aux' metasenv context cutted - CicUniv.empty_ugraph + CU.empty_ugraph in let _,g = CTC.type_of_aux' metasenv context changed g in fst (CR.are_convertible ~metasenv context t1' changed g) with | CTC.TypeCheckerFailure _ -> false in - if not go_on then - PET.apply_tactic (continuation ~map) status - else - let tac term = - let tac status = + if not go_on then begin + HLog.warn "destruct: injection failed"; + PET.apply_tactic continuation status + end else + let fill_cut_tac term = + let fill_cut status = debug_print (lazy "riempio il cut"); let (proof, goal) = status in let _,metasenv,_subst,_,_, _ = proof in @@ -450,42 +487,46 @@ let rec injection_tac ~map ~term ~i ~continuation = ] in PET.apply_tactic tac status in - PET.mk_tactic tac + PET.mk_tactic fill_cut in debug_print (lazy ("CUT: " ^ pp context cutted)); - PET.apply_tactic - (T.thens ~start: (P.cut_tac cutted) + let name = mk_fresh_name metasenv context "Hcut" cutted in + let mk_fresh_name_callback = PEH.namer_of [Some name] in + debug_print (lazy ("figlio: " ^ name)); + let tactic = + T.thens ~start: (P.cut_tac ~mk_fresh_name_callback cutted) ~continuations:[ - (destruct ~first_time:false ~term:(C.Rel 1) ~map:id - ~continuation:(after2 continuation succ map) - ); - tac term] - ) status + T.seq ~tactics:[continuation; recur_on_child_tac name]; + fill_cut_tac term + ] + in + PET.apply_tactic tactic status | _ -> raise exn_noneq in PET.mk_tactic injection_tac -(* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa assoluta - *) -and subst_tac ~map ~term ~direction ~where ~continuation = - let fail_tactic = continuation ~map in +and subst_tac ~lterm ~direction ~where ~continuation = let subst_tac status = - let term = relocate_term map term in + let (proof, goal) = status in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term)); let tactic = match where with | None -> + debug_print (lazy ("nella conclusione")); let pattern = PET.conclusion_pattern None in let tactic = ET.rewrite_tac ~direction ~pattern term [] in - T.then_ ~start:(T.try_tactic ~tactic) - ~continuation:fail_tactic - | Some name -> - let pattern = None, [name, PET.hole], None in + T.then_ ~start:(T.try_tactic ~tactic) ~continuation + | Some name -> + debug_print (lazy ("nella premessa: " ^ name)); + let pattern = None, [name, PET.hole], None in let start = ET.rewrite_tac ~direction ~pattern term [] in - let continuation = - destruct ~first_time:false ~term:(C.Rel 1) ~map:id - ~continuation:(after2 continuation succ map) + let ok_tactic = + T.seq ~tactics:[continuation; recur_on_child_tac name] in - T.if_ ~start ~continuation ~fail:fail_tactic + debug_print (lazy ("figlio: " ^ name)); + T.if_ ~start ~continuation:ok_tactic ~fail:continuation in PET.apply_tactic tactic status in @@ -494,54 +535,72 @@ and subst_tac ~map ~term ~direction ~where ~continuation = (* ~term vive nel contesto della tattica una volta ~mappato * ~continuation riceve la mappa assoluta *) -and destruct ~first_time ~map ~term ~continuation = +and destruct ~first_time ~term = let are_convertible hd1 hd2 metasenv context = - fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph) + fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph) in let destruct status = let (proof, goal) = status in let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term = relocate_term map term in - debug_print (lazy ("\nqnify di: " ^ pp context term)); + debug_print (lazy ("\ndestruct di: " ^ pp context term)); debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); let termty,_ = - CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph + CTC.type_of_aux' metasenv context term CU.empty_ugraph + in + debug_print (lazy ("\ndestruct su: " ^ pp context termty)); + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug + in + let lterm = mk_lterm term in + let mk_subst_chain direction index with_what what = + let k = match term with C.Rel i -> i | _ -> -1 in + let rec traverse_context first_time j = function + | [] -> + let continuation = + T.seq ~tactics:[ + clear_term first_time lterm; + clear_term false (mk_lterm what); + clear_term false (mk_lterm with_what) + ] + in + subst_tac ~direction ~lterm ~where:None ~continuation + | Some (C.Name name, _) :: tl when j < index && j <> k -> + debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j)); + subst_tac ~direction ~lterm ~where:(Some name) + ~continuation:(traverse_context false (succ j) tl) + | _ :: tl -> traverse_context first_time (succ j) tl + in + traverse_context first_time 1 context in - debug_print (lazy ("\nqnify su: " ^ pp context termty)); let tac = match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] - when LibraryObjects.is_eq_URI equri -> begin - match (CR.whd ~delta:true context tty) with - | C.MutInd _ - | C.Appl (C.MutInd _ :: _) -> - begin match t1,t2 with - | C.MutConstruct _, + when LibraryObjects.is_eq_URI equri -> + begin match t1,t2 with +(* injection part *) + | C.MutConstruct _, C.MutConstruct _ - when t1 = t2 -> - T.then_ ~start:(clear_term first_time context term) - ~continuation:(continuation ~map) + when t1 = t2 -> clear_term first_time lterm | C.Appl (C.MutConstruct _ as mc1 :: applist1), C.Appl (C.MutConstruct _ as mc2 :: applist2) when mc1 = mc2 -> let rec traverse_list first_time i l1 l2 = match l1, l2 with - | [], [] -> - fun ~map:aftermap -> - T.then_ ~start:(clear_term first_time context term) - ~continuation:(after continuation aftermap map) + | [], [] -> clear_term first_time lterm | hd1 :: tl1, hd2 :: tl2 -> if are_convertible hd1 hd2 metasenv context then traverse_list first_time (succ i) tl1 tl2 else - injection_tac ~i ~term ~continuation: + injection_tac ~i ~lterm ~continuation: (traverse_list false (succ i) tl1 tl2) | _ -> assert false (* i 2 termini hanno in testa lo stesso costruttore, * ma applicato a un numero diverso di termini *) in - traverse_list first_time 1 applist1 applist2 ~map:id - | C.MutConstruct (_,_,consno1,ens1), + traverse_list first_time 1 applist1 applist2 +(* discriminate part *) + | C.MutConstruct (_,_,consno1,ens1), C.MutConstruct (_,_,consno2,ens2) | C.MutConstruct (_,_,consno1,ens1), C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) @@ -551,22 +610,68 @@ and destruct ~first_time ~map ~term ~continuation = C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) when (consno1 <> consno2) || (ens1 <> ens2) -> discriminate_tac ~term - | _ when not first_time -> continuation ~map +(* subst part *) + | C.Rel _, C.Rel _ when t1 = t2 -> + T.seq ~tactics:[ + clear_term first_time lterm; + clear_term false (mk_lterm t1) + ] + | C.Rel i1, C.Rel i2 when i1 < i2 -> + mk_subst_chain `LeftToRight i1 t2 t1 + | C.Rel i1, C.Rel i2 when i1 > i2 -> + mk_subst_chain `RightToLeft i2 t1 t2 + | C.Rel i1, _ when DTI.does_not_occur i1 t2 -> + mk_subst_chain `LeftToRight i1 t2 t1 + | _, C.Rel i2 when DTI.does_not_occur i2 t1 -> + mk_subst_chain `RightToLeft i2 t1 t2 +(* else part *) + | _ when not first_time -> T.id_tac | _ (* when first_time *) -> T.then_ ~start:(simpl_in_term context term) - ~continuation:(destruct ~first_time:false ~term ~map ~continuation) + ~continuation:(destruct ~first_time:false ~term) end - | _ when not first_time -> continuation ~map - | _ (* when first_time *) -> raise exn_nonproj - end - | _ -> raise exn_nonproj + | _ when not first_time -> T.id_tac + | _ (* when first_time *) -> raise exn_nothingtodo in PET.apply_tactic tac status in PET.mk_tactic destruct +let lazy_destruct_tac ~first_time ~lterm = + let lazy_destruct status = + let (proof, goal) = status in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let term, _, _ = lterm context metasenv CU.empty_ugraph in + let tactic = + if exists context term then destruct ~first_time ~term else T.id_tac + in + PET.apply_tactic tactic status + in + PET.mk_tactic lazy_destruct + (* destruct performs either injection or discriminate *) (* equivalent to Coq's "analyze equality" *) -let destruct_tac = - destruct - ~first_time:true ~map:id ~continuation:(fun ~map -> T.id_tac) +let destruct_tac = function + | Some term -> destruct ~first_time:true ~term + | None -> + let destruct_all status = + let (proof, goal) = status in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug + in + let rec mk_tactics first_time i tacs = function + | [] -> List.rev tacs + | Some _ :: tl -> + let lterm = mk_lterm (C.Rel i) in + let tacs = lazy_destruct_tac ~first_time ~lterm :: tacs in + mk_tactics false (succ i) tacs tl + | _ :: tl -> mk_tactics first_time (succ i) tacs tl + in + let tactics = mk_tactics false 1 [] context in + PET.apply_tactic (T.seq ~tactics) status + in + PET.mk_tactic destruct_all diff --git a/components/tactics/discriminationTactics.mli b/components/tactics/destructTactic.mli similarity index 95% rename from components/tactics/discriminationTactics.mli rename to components/tactics/destructTactic.mli index 3a74e3d7d..0ecccdab0 100644 --- a/components/tactics/discriminationTactics.mli +++ b/components/tactics/destructTactic.mli @@ -27,4 +27,4 @@ looking for constructors. If the two sides differ on two constructors, it closes the current goal. If they differ by other two terms it introduces an equality. *) -val destruct_tac: term:Cic.term -> ProofEngineTypes.tactic +val destruct_tac: Cic.term option -> ProofEngineTypes.tactic diff --git a/components/tactics/substTactic.ml b/components/tactics/substTactic.ml deleted file mode 100644 index feff68f3f..000000000 --- a/components/tactics/substTactic.ml +++ /dev/null @@ -1,164 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -module C = Cic -module DT = DiscriminationTactics -module DTI = DoubleTypeInference -module ET = EqualityTactics -module HEL = HExtlib -module LO = LibraryObjects -module PEH = ProofEngineHelpers -module PESR = ProofEngineStructuralRules -module PET = ProofEngineTypes -module RT = ReductionTactics -module S = CicSubstitution -module T = Tacticals -module TC = CicTypeChecker - -let lift_rewrite_tac ~context ~direction ~pattern equality = - let lift_rewrite_tac status = - let (proof, goal) = status in - let (_, metasenv, _subst, _, _, _) = proof in - let _, new_context, _ = CicUtil.lookup_meta goal metasenv in - let n = List.length new_context - List.length context in - let equality = S.lift n equality in - PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status - in - PET.mk_tactic lift_rewrite_tac - -let lift_destruct_tac ~context ~what = - let lift_destruct_tac status = - let (proof, goal) = status in - let (_, metasenv, _subst, _, _, _) = proof in - let _, new_context, _ = CicUtil.lookup_meta goal metasenv in - let n = List.length new_context - List.length context in - let what = S.lift n what in - PET.apply_tactic (DT.destruct_tac ~term:what) status - in - PET.mk_tactic lift_destruct_tac - -let msg0 = lazy "Subst: not found in context" -let msg1 = lazy "Subst: not an erasable equation" -let msg2 = lazy "Subst: recursive equation" -let msg3 = lazy "Subst: no progress" - -let rec subst_tac ~try_tactic ~hyp = - let hole = C.Implicit (Some `Hole) in - let meta = C.Implicit None in - let rec ind = function - | C.MutInd _ -> true - | C.Appl (t :: tl) -> ind t - | _ -> false - in - let rec constr = function - | C.MutConstruct _ -> true - | C.Appl (t :: tl) -> constr t - | _ -> false - in - let subst_tac status = - let (proof, goal) = status in - let (_, metasenv, _subst, _, _, _) = proof in - let _, context, _ = CicUtil.lookup_meta goal metasenv in - let what = match PEH.get_rel context hyp with - | Some t -> t - | None -> raise (PET.Fail msg0) - in - let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in - let subst_g direction i t = - let rewrite pattern = - let tactic = lift_rewrite_tac ~context ~direction ~pattern what in - try_tactic ~tactic - in - let var = match PEH.get_name context i with - | Some name -> name - | None -> raise (PET.Fail msg0) - in - if DTI.does_not_occur i t then () else raise (PET.Fail msg2); - let map self = function - | Some (C.Name s, _) when s <> self -> - Some (rewrite (None, [(s, hole)], None)) - | _ -> None - in - let rew_hips = HEL.list_rev_map_filter (map hyp) context in - let rew_concl = rewrite (None, [], Some hole) in - let clear = PESR.clear ~hyps:[hyp; var] in - List.rev_append (rew_concl :: rew_hips) [clear] - in - let destruct_g () = - [lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]] - in - let whd_g () = - let whd_pattern = C.Appl [meta; hole; hole; hole] in - let pattern = None, [hyp, whd_pattern], None in - [RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp] - in - let tactics = match ty with - | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) - when LO.is_eq_URI uri -> subst_g `LeftToRight i t - | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) - when LO.is_eq_URI uri -> subst_g `RightToLeft i t - | (C.Appl [(C.MutInd (uri, 0, [])); t; t1; t2]) - when LO.is_eq_URI uri && ind t && constr t1 && constr t2 -> destruct_g () - | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) - when LO.is_eq_URI uri -> whd_g () - | _ -> raise (PET.Fail msg1) - in - PET.apply_tactic (T.seq ~tactics) status - in - PET.mk_tactic subst_tac - -let subst_tac = - let subst_tac status = - let progress = ref false in - let try_tactic ~tactic = - let try_tactic status = - try - let result = PET.apply_tactic tactic status in - progress := true; result - with - | PET.Fail _ -> PET.apply_tactic T.id_tac status - in - PET.mk_tactic try_tactic - in - let subst hyp = try_tactic ~tactic:(subst_tac ~try_tactic ~hyp) in - let map = function - | Some (C.Name s, _) -> Some (subst s) - | _ -> None - in - let (proof, goal) = status in - let (_, metasenv, _subst, _, _, _) = proof in - let _, context, _ = CicUtil.lookup_meta goal metasenv in - let tactics = HEL.list_rev_map_filter map context in - let result = PET.apply_tactic (T.seq ~tactics) status in - if !progress then result else raise (PET.Fail msg3) - in - PET.mk_tactic subst_tac - - let try_tac tactic = T.try_tactic ~tactic - let then_tac start continuation = T.then_ ~start ~continuation - -let subst_tac = - let tactic = T.repeat_tactic ~tactic:subst_tac in - T.try_tactic ~tactic diff --git a/components/tactics/substTactic.mli b/components/tactics/substTactic.mli deleted file mode 100644 index cce9d0fe9..000000000 --- a/components/tactics/substTactic.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* rewrites and clears all simple equalities in the context *) -val subst_tac: ProofEngineTypes.tactic diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index 67a607d1a..aa2e2bf4f 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -39,7 +39,7 @@ let contradiction = NegationTactics.contradiction_tac let cut = PrimitiveTactics.cut_tac let decompose = EliminationTactics.decompose_tac let demodulate = Auto.demodulate_tac -let destruct = DiscriminationTactics.destruct_tac +let destruct = DestructTactic.destruct_tac let elim_intros = PrimitiveTactics.elim_intros_tac let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac let elim_type = EliminationTactics.elim_type_tac @@ -67,7 +67,6 @@ let ring = Ring.ring_tac let simpl = ReductionTactics.simpl_tac let solve_rewrite = Auto.solve_rewrite_tac let split = IntroductionTactics.split_tac -let subst = SubstTactic.subst_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let unfold = ReductionTactics.unfold_tac diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index fb62b85fc..a58752461 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jul 6 11:03:35 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov 6 16:23:06 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -32,7 +32,7 @@ val decompose : unit -> ProofEngineTypes.tactic val demodulate : dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic -val destruct : term:Cic.term -> ProofEngineTypes.tactic +val destruct : Cic.term option -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> @@ -98,7 +98,6 @@ val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val solve_rewrite : universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic -val subst : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val unfold : diff --git a/matita/library/Fsub/defn.ma b/matita/library/Fsub/defn.ma index 177edbb45..2a5367834 100644 --- a/matita/library/Fsub/defn.ma +++ b/matita/library/Fsub/defn.ma @@ -224,7 +224,7 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))). intros 10;elim H [simplify in H1;elim (in_cons_case ? ? ? ? H1) - [destruct H3;elim (H2 Hcut1) + [destruct H3;elim (H2);reflexivity |simplify;apply (in_Skip ? ? ? ? H3);] |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2) [rewrite > H4;apply in_Base @@ -323,18 +323,16 @@ lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G. intros 7;elim H 0 [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4) - |destruct H8;rewrite < Hcut2 in H6;rewrite < Hcut in H4; - rewrite < Hcut in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)] + |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)] |intros;simplify;generalize in match H2;elim t;simplify in H4; inversion H4;intros [destruct H5 |destruct H9;apply WFE_cons - [rewrite < Hcut in H5;apply (H1 H5 H3) - |rewrite < (fv_env_extends ? x B C T U);rewrite > Hcut;rewrite > Hcut2; - assumption - |rewrite < Hcut3 in H8;rewrite > Hcut1;apply (WFT_env_incl ? ? H8); + [apply (H1 H5 H3) + |rewrite < (fv_env_extends ? x B C T U); assumption + |apply (WFT_env_incl ? ? H8); rewrite < (fv_env_extends ? x B C T U);unfold;intros; - rewrite > Hcut;assumption]]] + assumption]]] qed. lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to @@ -343,13 +341,13 @@ lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to intros 6;elim H [lapply (in_list_nil ? ? H1);elim Hletin |elim (in_cons_case ? ? ? ? H6) - [destruct H7;subst;elim (in_cons_case ? ? ? ? H5) - [destruct H7;assumption - |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? b); + [destruct H7;destruct;elim (in_cons_case ? ? ? ? H5) + [destruct H7;reflexivity + |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); apply (ex_intro ? ? T);assumption] |elim (in_cons_case ? ? ? ? H5) [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); - apply (ex_intro ? ? U);rewrite < Hcut1;assumption + apply (ex_intro ? ? U);assumption |apply (H2 H8 H7)]]] qed. @@ -360,8 +358,8 @@ lemma WFT_to_incl: ∀G,T,U. intros.elim (fresh_name ((fv_type U)@(fv_env G))).lapply(H a) [unfold;intros;lapply (fv_WFT ? x ? Hletin) [simplify in Hletin1;inversion Hletin1;intros - [destruct H4;elim H1;rewrite > Hcut;rewrite < H3.autobatch - |destruct H6;rewrite > Hcut1;assumption] + [destruct H4;elim H1;autobatch + |destruct H6;assumption] |apply in_FV_subst;assumption] |*:intro;apply H1;autobatch] qed. diff --git a/matita/library/Fsub/part1a.ma b/matita/library/Fsub/part1a.ma index 48543ce18..8558725cc 100644 --- a/matita/library/Fsub/part1a.ma +++ b/matita/library/Fsub/part1a.ma @@ -43,8 +43,8 @@ intros 4;elim H [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) |apply (WFE_cons ? ? ? ? H6 H8);autobatch |unfold;intros;inversion H9;intros - [destruct H11;rewrite > Hcut;apply in_Base - |destruct H13;rewrite < Hcut1 in H10;apply in_Skip;apply (H7 ? H10)]]] + [destruct H11;apply in_Base + |destruct H13;apply in_Skip;apply (H7 ? H10)]]] qed. theorem narrowing:∀X,G,G1,U,P,M,N. @@ -87,15 +87,15 @@ intros 3;elim H;clear H; try autobatch; |generalize in match H7;generalize in match H4;generalize in match H2; generalize in match H5;clear H7 H4 H2 H5; generalize in match (refl_eq ? (Arrow t t1)); - elim H6 in ⊢ (? ? ? %→%); clear H6; intros; subst; + elim H6 in ⊢ (? ? ? %→%); clear H6; intros; destruct; [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? ? H8 H9);autobatch - |inversion H11;intros; subst; autobatch depth=4 width=4 size=9; + |inversion H11;intros; destruct; autobatch depth=4 width=4 size=9; ] |generalize in match H7;generalize in match H4;generalize in match H2; generalize in match H5;clear H7 H4 H2 H5; - generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);subst + generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);destruct; [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? H7 H8 H9 H10);reflexivity - |inversion H11;intros;subst + |inversion H11;intros;destruct; [apply SA_Top [autobatch |apply WFT_Forall @@ -108,7 +108,7 @@ intros 3;elim H;clear H; try autobatch; |intro;apply H15;apply H8;apply (WFT_to_incl ? ? ? H3); assumption |simplify;autobatch - |apply (narrowing X (mk_bound true X t::l2) + |apply (narrowing X (mk_bound true X t::l1) ? ? ? ? ? H7 ? ? []) [intros;apply H9 [unfold;intros;lapply (H8 ? H17);rewrite > fv_append; diff --git a/matita/library/Fsub/part1a_inversion.ma b/matita/library/Fsub/part1a_inversion.ma index 463ceca95..f96e07679 100644 --- a/matita/library/Fsub/part1a_inversion.ma +++ b/matita/library/Fsub/part1a_inversion.ma @@ -43,8 +43,8 @@ intros 4;elim H [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) |apply (WFE_cons ? ? ? ? H6 H8);autobatch |unfold;intros;inversion H9;intros - [destruct H11;rewrite > Hcut;apply in_Base - |destruct H13;rewrite < Hcut1 in H10;apply in_Skip;apply (H7 ? H10)]]] + [destruct H11;apply in_Base + |destruct H13;apply in_Skip;apply (H7 ? H10)]]] qed. theorem narrowing:∀X,G,G1,U,P,M,N. @@ -95,10 +95,10 @@ lemma JSubtype_Arrow_inv: elim H2 in ⊢ (? ? ? % → ? ? ? % → %); [1,2: destruct H6 |5: destruct H8 - | lapply (H5 H6 H7); subst; clear H5; + | lapply (H5 H6 H7); destruct; clear H5; apply H; assumption - | subst; + | destruct; clear H4 H6; apply H1; assumption @@ -111,13 +111,13 @@ intros 3;elim H;clear H; try autobatch; [rewrite > (JSubtype_Top ? ? H3);autobatch |apply (JSubtype_Arrow_inv ? ? ? ? ? ? ? H6); intros; [ autobatch - | inversion H7;intros; subst; autobatch depth=4 width=4 size=9 + | inversion H7;intros; destruct; autobatch depth=4 width=4 size=9 ] |generalize in match H7;generalize in match H4;generalize in match H2; generalize in match H5;clear H7 H4 H2 H5; - generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);subst + generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);destruct; [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? H7 H8 H9 H10);reflexivity - |inversion H11;intros;subst + |inversion H11;intros;destruct; [apply SA_Top [autobatch |apply WFT_Forall @@ -130,7 +130,7 @@ intros 3;elim H;clear H; try autobatch; |intro;apply H15;apply H8;apply (WFT_to_incl ? ? ? H3); assumption |simplify;autobatch - |apply (narrowing X (mk_bound true X t::l2) + |apply (narrowing X (mk_bound true X t::l1) ? ? ? ? ? H7 ? ? []) [intros;apply H9 [unfold;intros;lapply (H8 ? H17);rewrite > fv_append; diff --git a/matita/library/Fsub/util.ma b/matita/library/Fsub/util.ma index 41089172e..4f5e15422 100644 --- a/matita/library/Fsub/util.ma +++ b/matita/library/Fsub/util.ma @@ -73,7 +73,7 @@ qed. lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t). intros;inversion H;intros - [destruct H2;left;symmetry;assumption + [destruct H2;left;symmetry;reflexivity |destruct H4;right;applyS H1] qed. @@ -112,15 +112,12 @@ theorem append_to_or_in_list: \forall A:Type.\forall x:A. intros 3. elim l [right.apply H - |simplify in H1.inversion H1;intros - [destruct H3.left.rewrite < Hcut. - apply in_Base - |destruct H5. - elim (H l2) - [left.apply in_Skip. - rewrite < H4.assumption - |right.rewrite < H4.assumption - |rewrite > Hcut1.rewrite > H4.assumption + |simplify in H1.inversion H1;intros; destruct; + [left.apply in_Base + | elim (H l2) + [left.apply in_Skip. assumption + |right.assumption + |assumption ] ] ] diff --git a/matita/library/Z/z.ma b/matita/library/Z/z.ma index 64b608cb9..ac530c38f 100644 --- a/matita/library/Z/z.ma +++ b/matita/library/Z/z.ma @@ -122,7 +122,7 @@ elim x. (* goal: x=pos y=pos *) elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))). left.apply eq_f.assumption. - right.unfold Not.intros (H_inj).apply H. destruct H_inj. assumption. + right.unfold Not.intros (H_inj).apply H. destruct H_inj. reflexivity. (* goal: x=pos y=neg *) right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption. (* goal: x=neg *) diff --git a/matita/library/decidable_kit/fgraph.ma b/matita/library/decidable_kit/fgraph.ma index f4ba8abde..5b28071dc 100644 --- a/matita/library/decidable_kit/fgraph.ma +++ b/matita/library/decidable_kit/fgraph.ma @@ -35,7 +35,7 @@ apply prove_reflect; intros; [1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2); intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType)); reflexivity - |2: unfold Not; intros (H3); destruct H3; rewrite > Hcut in H2; + |2: unfold Not; intros (H3); destruct H3; rewrite > (cmp_refl (list_eqType d2)) in H2; destruct H2;] qed. diff --git a/matita/library/decidable_kit/list_aux.ma b/matita/library/decidable_kit/list_aux.ma index b68858d68..c1a03060b 100644 --- a/matita/library/decidable_kit/list_aux.ma +++ b/matita/library/decidable_kit/list_aux.ma @@ -98,7 +98,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ] [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1; destruct H; rewrite > Hcut in H'; apply H'; reflexivity; | intros; lapply (IH ? H1) as H'; destruct H; - rewrite > Hcut1 in H'; apply H'; reflexivity;]]]] + apply H'; reflexivity;]]]] qed. definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d). diff --git a/matita/tests/destruct.ma b/matita/tests/destruct.ma index 1d6a51494..55275c480 100644 --- a/matita/tests/destruct.ma +++ b/matita/tests/destruct.ma @@ -64,29 +64,28 @@ inductive complex (A,B : Type) : B → A → Type ≝ | C1 : ∀x:nat.∀a:A.∀b:B. complex A B b a | C2 : ∀a,a1:A.∀b,b1:B.∀x:nat. complex A B b1 a1 → complex A B b a. - theorem recursive1: ∀ x,y : nat. (C1 ? ? O (Some ? x) y) = (C1 ? ? (S O) (Some ? x) y) → False. -intros; destruct H; +intros; destruct H. qed. theorem recursive2: ∀ x,y,z,t : nat. (C1 ? ? t (Some ? x) y) = (C1 ? ? z (Some ? x) y) → t=z. -intros; destruct H;assumption. +intros; destruct H; reflexivity. qed. theorem recursive3: ∀ x,y,z,t : nat. C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) = C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t. -intros; destruct H;assumption. +intros; destruct H; reflexivity. qed. theorem recursive4: ∀ x,y,z,t : nat. C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) = C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t. -intros; destruct H;assumption. +intros; destruct H; reflexivity. qed. theorem recursive2: ∀ x,y : nat. -- 2.39.2