From 309f44c8c35f0d67b50cf9bd37aba51126b8630b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 26 Apr 2007 13:05:48 +0000 Subject: [PATCH] bug fix in subst tactic --- helm/software/components/tactics/.depend | 36 ++--- helm/software/components/tactics/.depend.opt | 36 ++--- .../components/tactics/substTactic.ml | 129 ++++++++++++------ helm/software/components/tactics/tactics.mli | 2 +- 4 files changed, 126 insertions(+), 77 deletions(-) diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index bac580671..6908172de 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,6 +1,6 @@ proofEngineHelpers.cmi: proofEngineTypes.cmi continuationals.cmi: proofEngineTypes.cmi -tacticals.cmi: proofEngineTypes.cmi continuationals.cmi +tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi @@ -31,7 +31,7 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi -tactics.cmi: universe.cmi proofEngineTypes.cmi +tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -155,12 +155,12 @@ 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 proofEngineTypes.cmi \ +substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \ - substTactic.cmi -substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ + discriminationTactics.cmi substTactic.cmi +substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \ - substTactic.cmi + discriminationTactics.cmx substTactic.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi @@ -199,18 +199,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.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 discriminationTactics.cmi autoTactic.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 discriminationTactics.cmx autoTactic.cmx auto.cmx \ - tactics.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 \ + autoTactic.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 \ + autoTactic.cmx auto.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index bac580671..6908172de 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -1,6 +1,6 @@ proofEngineHelpers.cmi: proofEngineTypes.cmi continuationals.cmi: proofEngineTypes.cmi -tacticals.cmi: proofEngineTypes.cmi continuationals.cmi +tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi @@ -31,7 +31,7 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi -tactics.cmi: universe.cmi proofEngineTypes.cmi +tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -155,12 +155,12 @@ 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 proofEngineTypes.cmi \ +substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \ - substTactic.cmi -substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ + discriminationTactics.cmi substTactic.cmi +substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \ - substTactic.cmi + discriminationTactics.cmx substTactic.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi @@ -199,18 +199,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.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 discriminationTactics.cmi autoTactic.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 discriminationTactics.cmx autoTactic.cmx auto.cmx \ - tactics.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 \ + autoTactic.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 \ + autoTactic.cmx auto.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/helm/software/components/tactics/substTactic.ml b/helm/software/components/tactics/substTactic.ml index 1c0124648..fd11631ac 100644 --- a/helm/software/components/tactics/substTactic.ml +++ b/helm/software/components/tactics/substTactic.ml @@ -24,6 +24,7 @@ *) module C = Cic +module DT = DiscriminationTactics module DTI = DoubleTypeInference module ET = EqualityTactics module HEL = HExtlib @@ -31,36 +32,46 @@ module LO = LibraryObjects module PEH = ProofEngineHelpers module PESR = ProofEngineStructuralRules module PET = ProofEngineTypes +module RT = ReductionTactics module S = CicSubstitution module T = Tacticals module TC = CicTypeChecker -(* FG: This should be replaced by T.try_tactic *) -let try_tactic ~tactic = - let try_tactic status = - try PET.apply_tactic tactic status with - | PET.Fail _ -> PET.apply_tactic T.id_tac status - in - PET.mk_tactic try_tactic - -let rec lift_rewrite_tac ~context ~direction ~pattern equality = +let lift_rewrite_tac ~context ~direction ~pattern equality = let lift_rewrite_tac status = let (proof, goal) = status in let (_, metasenv, _, _, _) = proof in let _, new_context, _ = CicUtil.lookup_meta goal metasenv in let n = List.length new_context - List.length context in - let equality = if n > 0 then S.lift n equality else equality 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, _, _, _) = 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 a simple equality" +let msg1 = lazy "Subst: not an erasable equation" let msg2 = lazy "Subst: recursive equation" +let msg3 = lazy "Subst: no progress" -let subst_tac ~hyp = +let rec subst_tac ~try_tactic ~hyp = let hole = C.Implicit (Some `Hole) in + let meta = C.Implicit None 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, _, _, _) = proof in @@ -70,46 +81,84 @@ let subst_tac ~hyp = | None -> raise (PET.Fail msg0) in let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in - let direction, i, t = match ty with + 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; meta; 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 -> `LeftToRight, 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 -> `RightToLeft, i, t + when LO.is_eq_URI uri -> subst_g `RightToLeft i t + | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) + when LO.is_eq_URI uri && 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 - 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 - let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in PET.apply_tactic (T.seq ~tactics) status in PET.mk_tactic subst_tac let subst_tac = - let subst hyp = try_tactic ~tactic:(subst_tac hyp) in - let map = function - | Some (C.Name s, _) -> Some (subst s) - | _ -> None - in 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, _, _, _) = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let tactics = HEL.list_rev_map_filter map context in - PET.apply_tactic (T.seq ~tactics) status + 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 rec repeat_tactic ~tactic = + try_tac (then_tac tactic (repeat_tactic ~tactic)) + +let subst_tac = + let subst_tac status = + PET.apply_tactic (repeat_tactic ~tactic:subst_tac) status + in + PET.mk_tactic subst_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 34bc2d4f3..81e19bcec 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 Apr 20 17:07:53 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 26 15:04:41 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : -- 2.39.2