X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FequalityTactics.ml;h=c697acaedaeeb79d08940d912abd3ced915b40d6;hb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;hp=29f0574794b649704f87959c4505f4c22b755b35;hpb=1beb5e1624ac1db045e36dff93d0cfafa6a70995;p=helm.git diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index 29f057479..c697acaed 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -24,16 +24,23 @@ *) (* $Id$ *) - + +module C = Cic +module U = UriManager +module PET = ProofEngineTypes +module PER = ProofEngineReduction +module PEH = ProofEngineHelpers +module PESR = ProofEngineStructuralRules +module P = PrimitiveTactics +module T = Tacticals +module R = CicReduction +module TC = CicTypeChecker +module LO = LibraryObjects +module DTI = DoubleTypeInference + let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality = let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status = - let module C = Cic in - let module U = UriManager in - let module PET = ProofEngineTypes in - let module PER = ProofEngineReduction in - let module PEH = ProofEngineHelpers in - let module PT = PrimitiveTactics in assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in let curi, metasenv, pbo, pty = proof in @@ -44,19 +51,21 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit (Tacticals.then_ (rewrite_tac ~direction ~pattern:(None,[he],None) equality) - (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality) + (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) + (CicSubstitution.lift 1 equality)) ) status | [_] as hyps_pat when concl_pat <> None -> PET.apply_tactic (Tacticals.then_ (rewrite_tac ~direction ~pattern:(None,hyps_pat,None) equality) - (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality) + (rewrite_tac ~direction ~pattern:(None,[],concl_pat) + (CicSubstitution.lift 1 equality)) ) status | _ -> let arg,dir2,tac,concl_pat,gty = match hyps_pat with - [] -> None,true,(fun ~term _ -> PT.exact_tac term),concl_pat,gty + [] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty | [name,pat] -> let rec find_hyp n = function @@ -73,10 +82,10 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit Tacticals.seq ~tactics: [ProofEngineStructuralRules.rename name dummy; - PT.letin_tac + P.letin_tac ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term; ProofEngineStructuralRules.clearbody name; - ReductionTactics.change_tac + ReductionTactics.change_tac ~pattern: (None,[name,Cic.Implicit (Some `Hole)], None) (ProofEngineTypes.const_lazy_term typ); @@ -95,7 +104,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit CicUniv.empty_ugraph in let (ty_eq,metasenv',arguments,fresh_meta) = ProofEngineHelpers.saturate_term - (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in let equality = if List.length arguments = 0 then equality @@ -135,7 +144,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit ProofEngineHelpers.select ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture ~pattern:lifted_pattern in - let metasenv' = CicMetaSubst.apply_subst_metasenv subst metasenv' in + let metasenv' = CicMetaSubst.apply_subst_metasenv subst metasenv' in let what,with_what = (* Note: Rel 1 does not live in the context context_of_t *) (* The replace_lifting_csc 0 function will take care of lifting it *) @@ -146,6 +155,8 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit let t1 = CicMetaSubst.apply_subst subst t1 in let t2 = CicMetaSubst.apply_subst subst t2 in let ty = CicMetaSubst.apply_subst subst ty in + let pbo = CicMetaSubst.apply_subst subst pbo in + let pty = CicMetaSubst.apply_subst subst pty in let equality = CicMetaSubst.apply_subst subst equality in let abstr_gty = ProofEngineReduction.replace_lifting_csc 0 @@ -169,15 +180,18 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit let exact_proof = C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality] in - let (proof',goals) = - PET.apply_tactic - (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal) - in - let goals = - goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:metasenv') - in - (proof',goals) + try + let (proof',goals) = + PET.apply_tactic + (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal) + in + let goals = + goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv + ~newmetasenv:metasenv') + in + (proof',goals) + with (* FG: this should be PET.Fail _ *) + TC.TypeCheckerFailure _ -> PET.apply_tactic (P.letout_tac ()) status in ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality) @@ -199,10 +213,6 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status = let _wanted, hyps_pat, concl_pat = pattern in let (proof, goal) = status in - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in let uri,metasenv,pbo,pty = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in assert (hyps_pat = []); (*CSC: not implemented yet *) @@ -316,9 +326,6 @@ let reflexivity_tac = let symmetry_tac = let symmetry_tac (proof, goal) = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with @@ -337,10 +344,6 @@ let symmetry_tac = let transitivity_tac ~term = let transitivity_tac ~term status = let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let module T = Tacticals in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with @@ -359,4 +362,43 @@ let transitivity_tac ~term = ProofEngineTypes.mk_tactic (transitivity_tac ~term) ;; +(* FG *) + +let msg0 = lazy "Subst: not found in context" +let msg1 = lazy "Subst: not a simple equality" +let msg2 = lazy "Subst: recursive equation" +let subst_tac ~hyp = + let hole = C.Implicit (Some `Hole) in + let map self = function + | Some (C.Name s, _) when s <> self -> Some (s, hole) + | _ -> None + in + let subst_tac status = + let (proof, goal) = status in + let (_, metasenv, _, _) = 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 direction, i, t = match ty with + | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) + when LO.is_eq_URI uri -> `LeftToRight, i, t + | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) + when LO.is_eq_URI uri -> `RightToLeft, i, t + | _ -> raise (PET.Fail msg1) + 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 pattern = None, PEH.list_rev_map_filter (map hyp) context, Some hole in + let start = rewrite_tac ~direction ~pattern what in + let continuation = PESR.clear ~hyps:[hyp; var] in + let tac = T.then_ ~start ~continuation in + PET.apply_tactic tac status + in + PET.mk_tactic subst_tac