From: Ferruccio Guidi Date: Tue, 6 Nov 2007 19:30:16 +0000 (+0000) Subject: new implementation of the destruct tactic, X-Git-Tag: make_still_working~5894 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c80e9d9409119febcab9c08d6e6cad702384169;p=helm.git new implementation of the destruct tactic, which includes the old subst tactic (now removed) --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index a0bb2e4f9..3e87ffba5 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/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/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index de7af8263..eb1a18e5a 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/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/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index f587d2def..0d2fb682e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/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/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index d4ab241cb..2fe6b9aae 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/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/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 081055ce8..83e9d10d8 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/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/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 964011bfd..579ab17cc 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/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/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index 964011bfd..579ab17cc 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/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/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index c4e020005..9a6c6d4d0 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/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/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml new file mode 100644 index 000000000..bbfee8041 --- /dev/null +++ b/helm/software/components/tactics/destructTactic.ml @@ -0,0 +1,677 @@ +(* 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/. + *) + +(* $Id$ *) + +module C = Cic +module U = UriManager +module P = PrimitiveTactics +module T = Tacticals +module CR = CicReduction +module PST = ProofEngineStructuralRules +module PET = ProofEngineTypes +module CTC = CicTypeChecker +module CU = CicUniv +module S = CicSubstitution +module RT = ReductionTactics +module PEH = ProofEngineHelpers +module ET = EqualityTactics +module DTI = DoubleTypeInference +module FNG = FreshNamesGenerator + +let debug = true +let debug_print = + if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) + +(* funzione generale di rilocazione dei riferimenti locali *) + +let relocate_term map t = + let rec map_xnss k xnss = + let imap (uri, t) = uri, map_term k t in + List.map imap xnss + and map_mss k mss = + let imap = function + | None -> None + | Some t -> Some (map_term k t) + in + List.map imap mss + and map_fs len k fs = + let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in + List.map imap fs + and map_cfs len k cfs = + let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in + List.map imap cfs + and map_term k = function + | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k)) + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss) + | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss) + | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss) + | C.MutConstruct (uri, tyno, consno, xnss) -> + C.MutConstruct (uri, tyno, consno, map_xnss k xnss) + | C.Meta (i, mss) -> C.Meta(i, map_mss k mss) + | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty) + | C.Appl ts -> C.Appl (List.map (map_term k) ts) + | C.MutCase (sp, i, outty, t, pl) -> + C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl) + | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t) + | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t) + | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t) + | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs) + | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs) + in + map_term 0 t + +let id n = n + +let after continuation aftermap beforemap = + continuation ~map:(fun n -> aftermap (beforemap n)) + +let after2 continuation aftermap beforemap ~map = + continuation ~map:(fun n -> map (aftermap (beforemap n))) + +(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori +diversi *) + +let discriminate_tac ~term = + let true_URI = + match LibraryObjects.true_URI () with + Some uri -> uri + | None -> raise (PET.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in + let false_URI = + match LibraryObjects.false_URI () with + Some uri -> uri + | None -> raise (PET.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in + let fail msg = raise (PET.Fail (lazy ("Discriminate: " ^ msg))) in + let find_discriminating_consno t1 t2 = + let rec aux t1 t2 = + match t1, t2 with + | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None + | C.Appl ((C.MutConstruct _ as constr1) :: args1), + C.Appl ((C.MutConstruct _ as constr2) :: args2) + when constr1 = constr2 -> + let rec aux_list l1 l2 = + match l1, l2 with + | [], [] -> None + | hd1 :: tl1, hd2 :: tl2 -> + (match aux hd1 hd2 with + | None -> aux_list tl1 tl2 + | Some _ as res -> res) + | _ -> (* same constructor applied to a different number of args *) + assert false + in + aux_list args1 args2 + | ((C.MutConstruct (_,_,consno1,subst1)), + (C.MutConstruct (_,_,consno2,subst2))) + | ((C.MutConstruct (_,_,consno1,subst1)), + (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _))) + | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)), + (C.MutConstruct (_,_,consno2,subst2))) + | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)), + (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _))) + when (consno1 <> consno2) || (subst1 <> subst2) -> + Some consno2 + | _ -> fail "not a discriminable equality" + in + aux t1 t2 + in + 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 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 + let branches = + List.map + (fun (id,cty) -> + (* dubbio: e' corretto ridurre in questo context ??? *) + let red_ty = CR.whd context cty in + let rec aux t k = + match t with + | C.Prod (_,_,target) when (k <= paramsno) -> + S.subst (List.nth args (k-1)) + (aux target (k+1)) + | C.Prod (binder,source,target) when (k > paramsno) -> + C.Lambda (binder, source, (aux target (k+1))) + | _ -> + if (id = false_constr_id) + then (C.MutInd(false_URI,0,[])) + else (C.MutInd(true_URI,0,[])) + in + (S.lift 1 (aux red_ty 1))) + constructor_list in + let outtype = + let seed = ref 0 in + let rec mk_lambdas rev_left_args = + function + 0, args, C.Prod (_,so,ta) -> + C.Lambda + (C.Name (incr seed; "x" ^ string_of_int !seed), + so, + mk_lambdas rev_left_args (0,args,ta)) + | 0, args, C.Sort _ -> + let rec mk_rels = + function + 0 -> [] + | n -> C.Rel n :: mk_rels (n - 1) in + let argsno = List.length args in + C.Lambda + (C.Name "x", + (if argsno + List.length rev_left_args > 0 then + C.Appl + (C.MutInd (turi, typeno, []) :: + (List.map + (S.lift (argsno + 1)) + (List.rev rev_left_args)) @ + mk_rels argsno) + else + C.MutInd (turi,typeno,[])), + C.Sort C.Prop) + | 0, _, _ -> assert false (* seriously screwed up *) + | n, he::tl, C.Prod (_,_,ta) -> + mk_lambdas (he::rev_left_args)(n-1,tl,S.subst he ta) + | n,_,_ -> + assert false (* we should probably reduce in some context *) + in + mk_lambdas [] (paramsno, args, rty) + in + branches, outtype + | _ -> assert false + in + let discriminate'_tac ~term status = + let (proof, goal) = status in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let termty,_ = + CTC.type_of_aux' metasenv context term CU.empty_ugraph + in + match termty with + | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] + when LibraryObjects.is_eq_URI equri -> + let turi,typeno,exp_named_subst,args = + match tty with + | (C.MutInd (turi,typeno,exp_named_subst)) -> + turi,typeno,exp_named_subst,[] + | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) -> + turi,typeno,exp_named_subst,args + | _ -> fail "not a discriminable equality" + in + let consno = + match find_discriminating_consno t1 t2 with + | Some consno -> consno + | None -> fail "discriminating terms are structurally equal" + in + let branches,outtype = + mk_branches_and_outtype turi typeno consno context args + in + PET.apply_tactic + (T.then_ + ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, []))) + ~continuation: + (T.then_ + ~start: + (RT.change_tac + ~pattern:(PET.conclusion_pattern None) + (fun _ m u -> + C.Appl [ + C.Lambda ( C.Name "x", tty, + C.MutCase (turi, typeno, outtype, (C.Rel 1), branches)); + t2 ], + m, u)) + ~continuation: + (T.then_ + ~start: + (ET.rewrite_simpl_tac + ~direction:`RightToLeft + ~pattern:(PET.conclusion_pattern None) + term []) + ~continuation: + (IntroductionTactics.constructor_tac ~n:1)))) status + | _ -> fail "not an equality" + in + PET.mk_tactic (discriminate'_tac ~term) + +let exn_noneq = + PET.Fail (lazy "Injection: not an equality") +let exn_nothingtodo = + PET.Fail (lazy "Nothing to do") +let exn_discrnonind = + PET.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible") +let exn_injwronggoal = + PET.Fail (lazy "Injection: goal after cut is not correct") +let exn_noneqind = + PET.Fail (lazy "Injection: not an equality over elements of an inductive type") + +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 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 -> + let name = match List.nth context (pred i) with + | Some (Cic.Name s, Cic.Def _) -> s + | Some (Cic.Name s, Cic.Decl _) -> s + | _ -> assert false + in + RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) + | _ -> T.id_tac + +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) + in + let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in + let injection_tac status = + let (proof, goal) = status in + (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma + * differiscono (o potrebbero differire?) nell'i-esimo parametro + * del costruttore *) + let _,metasenv,_subst,_,_, _ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + 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 *) + | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] + when LibraryObjects.is_eq_URI equri -> + let turi,typeno,ens,params = + match tty with (* some inductive type *) + | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[] + | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params + | _ -> raise exn_noneqind + in + let t1',t2',consno = (* sono i due sottotermini che differiscono *) + match t1,t2 with + | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1), + C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2) + when (uri1 = uri2) && (typeno1 = typeno2) && + (consno1 = consno2) && (ens1 = ens2) -> + (* controllo ridondante *) + List.nth applist1 (pred i),List.nth applist2 (pred i),consno2 + | _ -> assert false + in + let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in + let patterns,outtype = + 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 + let i_constr_id,_ = List.nth constructor_list (consno - 1) in + let patterns = + let seed = ref 0 in + List.map + (function (id,cty) -> + let reduced_cty = CR.whd context cty in + let rec aux k = function + | C.Prod (_,_,tgt) when k <= paramsno -> + let left = List.nth left_params (k-1) in + aux (k+1) (S.subst left tgt) + | C.Prod (binder,source,target) when k > paramsno -> + let binder' = give_name seed binder in + C.Lambda (binder',source,(aux (k+1) target)) + | _ -> + let nr_param_constr = k - paramsno - 1 in + if id = i_constr_id then C.Rel (k - i) + else S.lift nr_param_constr t1' + (* + 1 per liftare anche il lambda aggiunto + * esternamente al case *) + in S.lift 1 (aux 1 reduced_cty)) + constructor_list + in + (* this code should be taken from cases_tac *) + let outtype = + let seed = ref 0 in + let rec to_lambdas te head = + match CR.whd context te with + | C.Prod (binder,so,ta) -> + let binder' = give_name seed binder in + C.Lambda (binder',so,to_lambdas ta head) + | _ -> head + in + let rec skip_prods params te = + match params, CR.whd context te with + | [], _ -> te + | left::tl, C.Prod (_,_,ta) -> + skip_prods tl (S.subst left ta) + | _, _ -> assert false + in + let abstracted_tty = + let tty = + List.fold_left (fun x y -> S.subst y x) tty left_params + in + (* non lift, ma subst coi left! *) + match S.lift 1 tty with + | C.MutInd _ as tty' -> tty' + | C.Appl l -> + let keep,abstract = HExtlib.split_nth (paramsno +1) l in + let keep = List.map (S.lift paramsno) keep in + C.Appl (keep@mk_rels (List.length abstract)) + | _ -> assert false + in + match ind_type_list with + | [] -> assert false + | (_,_,ty,_)::_ -> + (* this is in general wrong, do as in cases_tac *) + to_lambdas (skip_prods left_params ty) + (C.Lambda + (C.Name "cased", abstracted_tty, + (* here we should capture right parameters *) + (* 1 for his Lambda, one for the Lambda outside the match + * and then one for each to_lambda *) + S.lift (2+List.length right_params) tty')) + in + patterns,outtype + | _ -> raise exn_discrnonind + in + let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in + let changed = + C.Appl [ C.Lambda (C.Name "x", tty, + C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1] + in + (* check if cutted and changed are well typed and if t1' ~ changed *) + let go_on = + try + let _,g = CTC.type_of_aux' metasenv context cutted + 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 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 + let _,context,gty = CicUtil.lookup_meta goal metasenv in + let gty = Unshare.unshare gty in + let new_t1' = match gty with + | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t + | _ -> raise exn_injwronggoal + in + debug_print (lazy ("metto: " ^ pp context changed)); + debug_print (lazy ("al posto di: " ^ pp context new_t1')); + debug_print (lazy ("nel goal: " ^ pp context gty)); + debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); + debug_print (lazy ("e poi rewrite con: "^pp context term)); + let tac = T.seq ~tactics:[ + RT.change_tac + ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1'])) + (fun _ m u -> changed,m,u); + ET.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(PET.conclusion_pattern None) + term []; + ET.reflexivity_tac + ] in + PET.apply_tactic tac status + in + PET.mk_tactic fill_cut + in + debug_print (lazy ("CUT: " ^ pp context 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:[ + 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 + +and subst_tac ~lterm ~direction ~where ~continuation = + let subst_tac 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 ("\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 + | 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 ok_tactic = + T.seq ~tactics:[continuation; recur_on_child_tac name] + in + debug_print (lazy ("figlio: " ^ name)); + T.if_ ~start ~continuation:ok_tactic ~fail:continuation + in + PET.apply_tactic tactic status + in + PET.mk_tactic subst_tac + +(* ~term vive nel contesto della tattica una volta ~mappato + * ~continuation riceve la mappa assoluta + *) +and destruct ~first_time ~term = + let are_convertible hd1 hd2 metasenv context = + 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 + 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 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 + let tac = match termty with + | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] + when LibraryObjects.is_eq_URI equri -> + begin match t1,t2 with +(* injection part *) + | C.MutConstruct _, + C.MutConstruct _ + 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 + | [], [] -> 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 ~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 +(* discriminate part *) + | C.MutConstruct (_,_,consno1,ens1), + C.MutConstruct (_,_,consno2,ens2) + | C.MutConstruct (_,_,consno1,ens1), + C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) + | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_), + C.MutConstruct (_,_,consno2,ens2) + | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_), + C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) + when (consno1 <> consno2) || (ens1 <> ens2) -> + discriminate_tac ~term +(* 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) + end + | _ 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 = 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/helm/software/components/tactics/destructTactic.mli b/helm/software/components/tactics/destructTactic.mli new file mode 100644 index 000000000..0ecccdab0 --- /dev/null +++ b/helm/software/components/tactics/destructTactic.mli @@ -0,0 +1,30 @@ +(* 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/. + *) + +(* Performs a recursive comparisons of the two sides of an equation + 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: Cic.term option -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml deleted file mode 100644 index 83f676ed3..000000000 --- a/helm/software/components/tactics/discriminationTactics.ml +++ /dev/null @@ -1,572 +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/. - *) - -(* $Id$ *) - -module C = Cic -module U = UriManager -module P = PrimitiveTactics -module T = Tacticals -module CR = CicReduction -module PST = ProofEngineStructuralRules -module PET = ProofEngineTypes -module CTC = CicTypeChecker -module CU = CicUniv -module S = CicSubstitution -module RT = ReductionTactics -module PEH = ProofEngineHelpers -module ET = EqualityTactics - -let debug = false -let debug_print = - if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) - -(* funzione generale di rilocazione dei riferimenti locali *) - -let relocate_term map t = - let rec map_xnss k xnss = - let imap (uri, t) = uri, map_term k t in - List.map imap xnss - and map_mss k mss = - let imap = function - | None -> None - | Some t -> Some (map_term k t) - in - List.map imap mss - and map_fs len k fs = - let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in - List.map imap fs - and map_cfs len k cfs = - let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in - List.map imap cfs - and map_term k = function - | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k)) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss) - | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss) - | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss) - | C.MutConstruct (uri, tyno, consno, xnss) -> - C.MutConstruct (uri, tyno, consno, map_xnss k xnss) - | C.Meta (i, mss) -> C.Meta(i, map_mss k mss) - | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty) - | C.Appl ts -> C.Appl (List.map (map_term k) ts) - | C.MutCase (sp, i, outty, t, pl) -> - C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl) - | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t) - | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t) - | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t) - | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs) - | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs) - in - map_term 0 t - -let id n = n - -let after continuation aftermap beforemap = - continuation ~map:(fun n -> aftermap (beforemap n)) - -let after2 continuation aftermap beforemap ~map = - continuation ~map:(fun n -> map (aftermap (beforemap n))) - -(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori -diversi *) - -let discriminate_tac ~term = - let true_URI = - match LibraryObjects.true_URI () with - Some uri -> uri - | None -> raise (PET.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in - let false_URI = - match LibraryObjects.false_URI () with - Some uri -> uri - | None -> raise (PET.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in - let fail msg = raise (PET.Fail (lazy ("Discriminate: " ^ msg))) in - let find_discriminating_consno t1 t2 = - let rec aux t1 t2 = - match t1, t2 with - | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None - | C.Appl ((C.MutConstruct _ as constr1) :: args1), - C.Appl ((C.MutConstruct _ as constr2) :: args2) - when constr1 = constr2 -> - let rec aux_list l1 l2 = - match l1, l2 with - | [], [] -> None - | hd1 :: tl1, hd2 :: tl2 -> - (match aux hd1 hd2 with - | None -> aux_list tl1 tl2 - | Some _ as res -> res) - | _ -> (* same constructor applied to a different number of args *) - assert false - in - aux_list args1 args2 - | ((C.MutConstruct (_,_,consno1,subst1)), - (C.MutConstruct (_,_,consno2,subst2))) - | ((C.MutConstruct (_,_,consno1,subst1)), - (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _))) - | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)), - (C.MutConstruct (_,_,consno2,subst2))) - | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)), - (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _))) - when (consno1 <> consno2) || (subst1 <> subst2) -> - Some consno2 - | _ -> fail "not a discriminable equality" - in - aux t1 t2 - in - 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 - | 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 - let branches = - List.map - (fun (id,cty) -> - (* dubbio: e' corretto ridurre in questo context ??? *) - let red_ty = CR.whd context cty in - let rec aux t k = - match t with - | C.Prod (_,_,target) when (k <= paramsno) -> - S.subst (List.nth args (k-1)) - (aux target (k+1)) - | C.Prod (binder,source,target) when (k > paramsno) -> - C.Lambda (binder, source, (aux target (k+1))) - | _ -> - if (id = false_constr_id) - then (C.MutInd(false_URI,0,[])) - else (C.MutInd(true_URI,0,[])) - in - (S.lift 1 (aux red_ty 1))) - constructor_list in - let outtype = - let seed = ref 0 in - let rec mk_lambdas rev_left_args = - function - 0, args, C.Prod (_,so,ta) -> - C.Lambda - (C.Name (incr seed; "x" ^ string_of_int !seed), - so, - mk_lambdas rev_left_args (0,args,ta)) - | 0, args, C.Sort _ -> - let rec mk_rels = - function - 0 -> [] - | n -> C.Rel n :: mk_rels (n - 1) in - let argsno = List.length args in - C.Lambda - (C.Name "x", - (if argsno + List.length rev_left_args > 0 then - C.Appl - (C.MutInd (turi, typeno, []) :: - (List.map - (S.lift (argsno + 1)) - (List.rev rev_left_args)) @ - mk_rels argsno) - else - C.MutInd (turi,typeno,[])), - C.Sort C.Prop) - | 0, _, _ -> assert false (* seriously screwed up *) - | n, he::tl, C.Prod (_,_,ta) -> - mk_lambdas (he::rev_left_args)(n-1,tl,S.subst he ta) - | n,_,_ -> - assert false (* we should probably reduce in some context *) - in - mk_lambdas [] (paramsno, args, rty) - in - branches, outtype - | _ -> assert false - in - let discriminate'_tac ~term status = - let (proof, goal) = status in - 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 - in - match termty with - | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] - when LibraryObjects.is_eq_URI equri -> - let turi,typeno,exp_named_subst,args = - match tty with - | (C.MutInd (turi,typeno,exp_named_subst)) -> - turi,typeno,exp_named_subst,[] - | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) -> - turi,typeno,exp_named_subst,args - | _ -> fail "not a discriminable equality" - in - let consno = - match find_discriminating_consno t1 t2 with - | Some consno -> consno - | None -> fail "discriminating terms are structurally equal" - in - let branches,outtype = - mk_branches_and_outtype turi typeno consno context args - in - PET.apply_tactic - (T.then_ - ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, []))) - ~continuation: - (T.then_ - ~start: - (RT.change_tac - ~pattern:(PET.conclusion_pattern None) - (fun _ m u -> - C.Appl [ - C.Lambda ( C.Name "x", tty, - C.MutCase (turi, typeno, outtype, (C.Rel 1), branches)); - t2 ], - m, u)) - ~continuation: - (T.then_ - ~start: - (ET.rewrite_simpl_tac - ~direction:`RightToLeft - ~pattern:(PET.conclusion_pattern None) - term []) - ~continuation: - (IntroductionTactics.constructor_tac ~n:1)))) status - | _ -> fail "not an equality" - 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 = - PET.Fail (lazy "Nothing to do") -let exn_discrnonind = - PET.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible") -let exn_injwronggoal = - PET.Fail (lazy "Injection: goal after cut is not correct") -let exn_noneqind = - PET.Fail (lazy "Injection: not an equality over elements of an inductive type") - -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 simpl_in_term context = function - | Cic.Rel i -> - let name = match List.nth context (pred i) with - | Some (Cic.Name s, Cic.Def _) -> s - | Some (Cic.Name s, Cic.Decl _) -> s - | _ -> assert false - in - RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) - | _ -> raise exn_nonproj - -(* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa assoluta - *) -let rec injection_tac ~map ~term ~i ~continuation = - let give_name seed = function - | C.Name _ as name -> name - | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed) - in - let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in - let injection_tac status = - let (proof, goal) = status in - (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma - * differiscono (o potrebbero differire?) nell'i-esimo parametro - * 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 - in - debug_print (lazy ("\ninjection su : " ^ pp context termty)); - match termty with (* an equality *) - | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] - when LibraryObjects.is_eq_URI equri -> - let turi,typeno,ens,params = - match tty with (* some inductive type *) - | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[] - | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params - | _ -> raise exn_noneqind - in - let t1',t2',consno = (* sono i due sottotermini che differiscono *) - match t1,t2 with - | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1), - C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2) - when (uri1 = uri2) && (typeno1 = typeno2) && - (consno1 = consno2) && (ens1 = ens2) -> - (* controllo ridondante *) - List.nth applist1 (pred i),List.nth applist2 (pred i),consno2 - | _ -> assert false - 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 - | 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 - let i_constr_id,_ = List.nth constructor_list (consno - 1) in - let patterns = - let seed = ref 0 in - List.map - (function (id,cty) -> - let reduced_cty = CR.whd context cty in - let rec aux k = function - | C.Prod (_,_,tgt) when k <= paramsno -> - let left = List.nth left_params (k-1) in - aux (k+1) (S.subst left tgt) - | C.Prod (binder,source,target) when k > paramsno -> - let binder' = give_name seed binder in - C.Lambda (binder',source,(aux (k+1) target)) - | _ -> - let nr_param_constr = k - paramsno - 1 in - if id = i_constr_id then C.Rel (k - i) - else S.lift nr_param_constr t1' - (* + 1 per liftare anche il lambda aggiunto - * esternamente al case *) - in S.lift 1 (aux 1 reduced_cty)) - constructor_list - in - (* this code should be taken from cases_tac *) - let outtype = - let seed = ref 0 in - let rec to_lambdas te head = - match CR.whd context te with - | C.Prod (binder,so,ta) -> - let binder' = give_name seed binder in - C.Lambda (binder',so,to_lambdas ta head) - | _ -> head - in - let rec skip_prods params te = - match params, CR.whd context te with - | [], _ -> te - | left::tl, C.Prod (_,_,ta) -> - skip_prods tl (S.subst left ta) - | _, _ -> assert false - in - let abstracted_tty = - let tty = - List.fold_left (fun x y -> S.subst y x) tty left_params - in - (* non lift, ma subst coi left! *) - match S.lift 1 tty with - | C.MutInd _ as tty' -> tty' - | C.Appl l -> - let keep,abstract = HExtlib.split_nth (paramsno +1) l in - let keep = List.map (S.lift paramsno) keep in - C.Appl (keep@mk_rels (List.length abstract)) - | _ -> assert false - in - match ind_type_list with - | [] -> assert false - | (_,_,ty,_)::_ -> - (* this is in general wrong, do as in cases_tac *) - to_lambdas (skip_prods left_params ty) - (C.Lambda - (C.Name "cased", abstracted_tty, - (* here we should capture right parameters *) - (* 1 for his Lambda, one for the Lambda outside the match - * and then one for each to_lambda *) - S.lift (2+List.length right_params) tty')) - in - patterns,outtype - | _ -> raise exn_discrnonind - in - let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in - let changed = - C.Appl [ C.Lambda (C.Name "x", tty, - C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1] - in - (* check if cutted and changed are well typed and if t1' ~ changed *) - let go_on = - try - let _,g = CTC.type_of_aux' metasenv context cutted - CicUniv.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 = - debug_print (lazy "riempio il cut"); - let (proof, goal) = status in - let _,metasenv,_subst,_,_, _ = proof in - let _,context,gty = CicUtil.lookup_meta goal metasenv in - let gty = Unshare.unshare gty in - let new_t1' = match gty with - | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t - | _ -> raise exn_injwronggoal - in - debug_print (lazy ("metto: " ^ pp context changed)); - debug_print (lazy ("al posto di: " ^ pp context new_t1')); - debug_print (lazy ("nel goal: " ^ pp context gty)); - debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); - debug_print (lazy ("e poi rewrite con: "^pp context term)); - let tac = T.seq ~tactics:[ - RT.change_tac - ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1'])) - (fun _ m u -> changed,m,u); - ET.rewrite_simpl_tac - ~direction:`LeftToRight - ~pattern:(PET.conclusion_pattern None) - term []; - ET.reflexivity_tac - ] in - PET.apply_tactic tac status - in - PET.mk_tactic tac - in - debug_print (lazy ("CUT: " ^ pp context cutted)); - PET.apply_tactic - (T.thens ~start: (P.cut_tac cutted) - ~continuations:[ - (destruct ~first_time:false ~term:(C.Rel 1) ~map:id - ~continuation:(after2 continuation succ map) - ); - tac term] - ) 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 - let subst_tac status = - let term = relocate_term map term in - let tactic = match where with - | None -> - 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 - 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) - in - T.if_ ~start ~continuation ~fail:fail_tactic - in - PET.apply_tactic tactic status - in - PET.mk_tactic subst_tac - -(* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa assoluta - *) -and destruct ~first_time ~map ~term ~continuation = - let are_convertible hd1 hd2 metasenv context = - fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.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 ("nel contesto:\n" ^ CicPp.ppcontext context)); - let termty,_ = - CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph - 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 _, - C.MutConstruct _ - when t1 = t2 -> - T.then_ ~start:(clear_term first_time context term) - ~continuation:(continuation ~map) - | 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) - | 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: - (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), - C.MutConstruct (_,_,consno2,ens2) - | C.MutConstruct (_,_,consno1,ens1), - C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) - | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_), - C.MutConstruct (_,_,consno2,ens2) - | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_), - C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) - when (consno1 <> consno2) || (ens1 <> ens2) -> - discriminate_tac ~term - | _ when not first_time -> continuation ~map - | _ (* when first_time *) -> - T.then_ ~start:(simpl_in_term context term) - ~continuation:(destruct ~first_time:false ~term ~map ~continuation) - end - | _ when not first_time -> continuation ~map - | _ (* when first_time *) -> raise exn_nonproj - end - | _ -> raise exn_nonproj - in - PET.apply_tactic tac status - in - PET.mk_tactic 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) diff --git a/helm/software/components/tactics/discriminationTactics.mli b/helm/software/components/tactics/discriminationTactics.mli deleted file mode 100644 index 3a74e3d7d..000000000 --- a/helm/software/components/tactics/discriminationTactics.mli +++ /dev/null @@ -1,30 +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/. - *) - -(* Performs a recursive comparisons of the two sides of an equation - 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 diff --git a/helm/software/components/tactics/substTactic.ml b/helm/software/components/tactics/substTactic.ml deleted file mode 100644 index feff68f3f..000000000 --- a/helm/software/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/helm/software/components/tactics/substTactic.mli b/helm/software/components/tactics/substTactic.mli deleted file mode 100644 index cce9d0fe9..000000000 --- a/helm/software/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/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index 67a607d1a..aa2e2bf4f 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/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/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index fb62b85fc..a58752461 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: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/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma index 177edbb45..2a5367834 100644 --- a/helm/software/matita/library/Fsub/defn.ma +++ b/helm/software/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/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma index 48543ce18..8558725cc 100644 --- a/helm/software/matita/library/Fsub/part1a.ma +++ b/helm/software/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/helm/software/matita/library/Fsub/part1a_inversion.ma b/helm/software/matita/library/Fsub/part1a_inversion.ma index 463ceca95..f96e07679 100644 --- a/helm/software/matita/library/Fsub/part1a_inversion.ma +++ b/helm/software/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/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/library/Fsub/util.ma index 41089172e..4f5e15422 100644 --- a/helm/software/matita/library/Fsub/util.ma +++ b/helm/software/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/helm/software/matita/library/Z/z.ma b/helm/software/matita/library/Z/z.ma index 64b608cb9..ac530c38f 100644 --- a/helm/software/matita/library/Z/z.ma +++ b/helm/software/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/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma index f4ba8abde..5b28071dc 100644 --- a/helm/software/matita/library/decidable_kit/fgraph.ma +++ b/helm/software/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/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index b68858d68..c1a03060b 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/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/helm/software/matita/tests/destruct.ma b/helm/software/matita/tests/destruct.ma index 1d6a51494..55275c480 100644 --- a/helm/software/matita/tests/destruct.ma +++ b/helm/software/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.