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 ebb54f126588f9dd5abb4895a40d6286a155ddc3..194dbd17ecedafbf35a4fbf83f973224a2d6a2e8 100644 (file)
--- 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 5a091b7ad895cb196243c9d96c0394e8330fe1f3..2b2afae67772bc73fd657288691e046ea97bc1dd 100644 (file)
--- 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