From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2005 16:15:29 +0000 (+0000) Subject: First draft implementation of rewriting in an hypothesis. X-Git-Tag: V_0_7_2_3~50 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dfbf84276e3183c190a6c7a59689324dccbaa6dc;p=helm.git First draft implementation of rewriting in an hypothesis. Highly incomplete. Fails randomly if the pattern is not one the tactic is able to cope with. --- diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index ebb54f126..194dbd17e 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -47,3 +47,10 @@ theorem foo: \forall n. n = n + 0. intros. rewrite < t; reflexivity. qed. + +theorem test_rewrite_in_hyp: \forall n,m. n + 0 = m \to m = n + 0 \to n=m \land m+0=n+0. + intros. + rewrite < plus_n_O in H. + rewrite > plus_n_O in H1. + split; [ exact H | exact H1]. +qed. diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 5a091b7ad..2b2afae67 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -33,15 +33,61 @@ let rewrite_tac ~direction ~pattern equality = let module PEH = ProofEngineHelpers in let module PT = PrimitiveTactics in assert (wanted = None); (* this should be checked syntactically *) - assert (hyps_pat = []); (*CSC: not implemented yet! *) + (*assert (hyps_pat = []); (*CSC: not implemented yet! *)*) let proof,goal = status in - let if_right_to_left a b = - match direction with - | `RightToLeft -> a - | `LeftToRight -> b - in let curi, metasenv, pbo, pty = proof in let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in + let arg,dir2,tac,concl_pat,gty = + match hyps_pat with + [] -> None,true,PT.exact_tac,concl_pat,gty + | [name,pat] -> + (*CSC: bug here; I am ignoring the concl_pat *) + let rec find_hyp n = + function + [] -> assert false + | Some (Cic.Name s,Cic.Decl ty)::_ when name = s -> + Cic.Rel n, CicSubstitution.lift n ty + | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet!*) + | _::tl -> find_hyp (n+1) tl + in + let arg,gty = find_hyp 1 context in + let last_hyp_name_of_status (proof,goal) = + let curi, metasenv, pbo, pty = proof in + let metano,context,gty = CicUtil.lookup_meta goal metasenv in + match context with + (Some (Cic.Name s,_))::_ -> s + | _ -> assert false + in + Some arg,false, + (fun ~term -> + Tacticals.seq + ~tactics: + [PT.letin_tac term; + PET.mk_tactic (fun status -> + PET.apply_tactic + (ProofEngineStructuralRules.clearbody + (last_hyp_name_of_status status)) status); + PET.mk_tactic (fun status -> + let hyp = last_hyp_name_of_status status in + PET.apply_tactic + (ReductionTactics.simpl_tac + ~pattern: + (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None)) + status); + ProofEngineStructuralRules.clear name; + PET.mk_tactic (fun status -> + let hyp = last_hyp_name_of_status status in + PET.apply_tactic + (ProofEngineStructuralRules.rename hyp name) status) + ]), + pat,gty + | _ -> assert false (*CSC: not implemented yet!*) + in + let if_right_to_left do_not_change a b = + match direction with + | `RightToLeft -> if do_not_change then a else b + | `LeftToRight -> if do_not_change then b else a + in let ty_eq,ugraph = CicTypeChecker.type_of_aux' metasenv context equality CicUniv.empty_ugraph in @@ -53,21 +99,26 @@ let rewrite_tac ~direction ~pattern equality = equality else C.Appl (equality :: arguments) in - let eq_ind, ty, t1, t2 = + (* t1x is t2 if we are rewriting in an hypothesis *) + let eq_ind, ty, t1, t2, t1x = match ty_eq with | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> let ind_uri = - if_right_to_left LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI + if_right_to_left dir2 + LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI in let eq_ind = C.Const (ind_uri uri,[]) in - if_right_to_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2) + if dir2 then + if_right_to_left true (eq_ind,ty,t2,t1,t2) (eq_ind,ty,t1,t2,t1) + else + if_right_to_left true (eq_ind,ty,t1,t2,t2) (eq_ind,ty,t2,t1,t1) | _ -> raise (PET.Fail (lazy "Rewrite: argument is not a proof of an equality")) in (* now we always do as if direction was `LeftToRight *) let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv' context C.Anonymous ~typ:ty in - let lifted_t1 = CicSubstitution.lift 1 t1 in + let lifted_t1 = CicSubstitution.lift 1 t1x in let lifted_gty = CicSubstitution.lift 1 gty in let lifted_conjecture = metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in @@ -81,33 +132,42 @@ let rewrite_tac ~direction ~pattern equality = 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 *) + (* The replace_lifting_csc 0 function will take care of lifting it *) (* to context_of_t *) List.fold_right (fun (context_of_t,t) (l1,l2) -> t::l1, Cic.Rel 1::l2) selected_terms_with_context ([],[]) in + let t1 = CicMetaSubst.apply_subst subst t1 in + let t2 = CicMetaSubst.apply_subst subst t2 in + let equality = CicMetaSubst.apply_subst subst equality in let abstr_gty = ProofEngineReduction.replace_lifting_csc 0 ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in - let t1 = CicMetaSubst.apply_subst subst t1 in - let t2 = CicMetaSubst.apply_subst subst t2 in - let equality = CicMetaSubst.apply_subst subst equality in - let gty' = CicSubstitution.subst t2 abstr_gty in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,gty')::metasenv' in let pred = C.Lambda (fresh_name, ty, abstr_gty) in + (* The argument is either a meta if we are rewriting in the conclusion + or the hypothesis if we are rewriting in an hypothesis *) + let metasenv',arg = + match arg with + None -> + let gty' = CicSubstitution.subst t2 abstr_gty in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,gty')::metasenv' in + metasenv', C.Meta (fresh_meta,irl) + | Some arg -> + metasenv,arg + in let exact_proof = - C.Appl [eq_ind ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality] + C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality] in let (proof',goals) = PET.apply_tactic - (PT.exact_tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal) + (tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal) in - assert (List.length goals = 0) ; let goals = - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:metasenv' + goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv + ~newmetasenv:metasenv') in (proof',goals) in