From 016e4c6fc449b50ac19e73eb952cfb2dc64f4398 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Jul 2005 10:21:29 +0000 Subject: [PATCH] Bug fixed: metavariables generated by the saturation in the rewrite tactic were not declared as new goals in the output of the tactic. --- helm/matita/tests/rewrite.ma | 13 ++++++++++++- helm/ocaml/tactics/equalityTactics.ml | 21 ++++++++++++++------- 2 files changed, 26 insertions(+), 8 deletions(-) diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index 3941ab0cb..aa4fa1f32 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -4,7 +4,7 @@ alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "leibnitz's equality". alias symbol "plus" (instance 0) = "natural plus". - +alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". theorem a: \forall a,b:nat. @@ -21,3 +21,14 @@ simplify. reflexivity. qed. +theorem t: \forall n. 0=0 \to n = n + 0. + intros. + apply plus_n_O. +qed. + +(* In this test "rewrite < t" should open a new goal 0=0 and put it in *) +(* the goallist so that the THEN tactical closes it using reflexivity. *) +theorem foo: \forall n. n = n + 0. + intros. + rewrite < t; reflexivity. +qed. \ No newline at end of file diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 4a6c445e6..7eae7fb5c 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -45,7 +45,7 @@ let rewrite_tac ~direction ~pattern equality = let ty_eq,ugraph = CicTypeChecker.type_of_aux' metasenv context equality CicUniv.empty_ugraph in - let (ty_eq,metasenv,arguments,fresh_meta) = + let (ty_eq,metasenv',arguments,fresh_meta) = ProofEngineHelpers.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq in let equality = @@ -66,16 +66,17 @@ let rewrite_tac ~direction ~pattern equality = (* now we always do as if direction was `LeftToRight *) let fresh_name = FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv context C.Anonymous ~typ:ty in + ~subst:[] metasenv' context C.Anonymous ~typ:ty in let lifted_t1 = CicSubstitution.lift 1 t1 in let lifted_gty = CicSubstitution.lift 1 gty in let lifted_conjecture = metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in - let subst,metasenv,ugraph,_,selected_terms_with_context = + let subst,metasenv',ugraph,_,selected_terms_with_context = ProofEngineHelpers.select - ~metasenv ~ugraph ~conjecture:lifted_conjecture ~pattern:lifted_pattern in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture + ~pattern:lifted_pattern 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 *) @@ -92,7 +93,7 @@ let rewrite_tac ~direction ~pattern equality = 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 metasenv' = (fresh_meta,context,gty')::metasenv' in let pred = C.Lambda (fresh_name, ty, abstr_gty) in let exact_proof = C.Appl [eq_ind ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality] @@ -102,7 +103,13 @@ let rewrite_tac ~direction ~pattern equality = (PT.exact_tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal) in assert (List.length goals = 0) ; - (proof',[fresh_meta]) + let goals = List.map (fun (i,_,_) -> i) metasenv' in + let goals = + List.filter + (fun i -> + not (List.exists (fun (j,_,_) -> i=j) metasenv)) goals + in + (proof',goals) in ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality) -- 2.39.2