aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-tac.tex30
-rw-r--r--proofs/refiner.ml2
-rw-r--r--proofs/refiner.mli6
-rw-r--r--tactics/equality.ml61
-rw-r--r--tactics/tacticals.ml1
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--theories/Init/Tactics.v23
7 files changed, 65 insertions, 60 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b491cc3d4..315286571 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1584,20 +1584,30 @@ This happens if \term$_1$ does not occur in the goal.
\item {\tt rewrite {\term} in \textit{clause}}
\tacindex{rewrite \dots\ in}\\
Analogous to {\tt rewrite {\term}} but rewriting is done following
- \textit{clause} (similarly to \ref{Conversion-tactics}). For instance:
- \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1;
- rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do
- \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <>
- H}.
-
-\item {\tt rewrite -> {\term} in {\ident}}
+ \textit{clause} (similarly to \ref{Conversion-tactics}). For
+ instance:
+ \begin{itemize}
+ \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis
+ \texttt{H1} instead of the current goal.
+ \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1;
+ rewrite H in H2}. In particular a failure will happen if any of
+ these three simplier tactics fails.
+ \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
+ H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+ as soon as at least one of these simplier tactics succeeds.
+ \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H}
+ and \texttt{rewrite H in * |-} that succeeds if at
+ least one of these two tactics succeeds.
+ \end{itemize}
+
+\item {\tt rewrite -> {\term} in \textit{clause}}
\tacindex{rewrite -> \dots\ in}\\
- Behaves as {\tt rewrite {\term} in {\ident}}.
+ Behaves as {\tt rewrite {\term} in \textit{clause}}.
-\item {\tt rewrite <- {\term} in {\ident}}\\
+\item {\tt rewrite <- {\term} in \textit{clause}}\\
\tacindex{rewrite <- \dots\ in}
Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
- rewrite in the hypothesis named {\ident}.
+ rewrite in \textit{clause} as explained above.
\end{Variants}
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9d5fb3151..3d65406b8 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -540,6 +540,8 @@ let tclIFTHENSELSE=ite_gen tclTHENS
let tclIFTHENSVELSE=ite_gen tclTHENSV
+let tclIFTHENTRYELSEMUST tac1 tac2 gl =
+ tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
(* Fails if a tactic did not solve the goal *)
let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 72afde93e..0225e6443 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -144,6 +144,12 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
+(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
+ has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
+ Equivalent to [(tac1;try tac2)||tac2] *)
+
+val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
+
(*s Tactics handling a list of goals. *)
type validation_list = proof_tree list -> proof_tree list
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 72a1267c3..b1f0360c4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -119,36 +119,39 @@ let general_rewrite_bindings_in l2r id =
let general_rewrite_in l2r id c =
general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
-
let general_multi_rewrite l2r c cl =
- let rec do_hyps = function
- | [] -> tclIDTAC
- | ((_,id),_) :: l ->
- tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
- in
- let rec try_do_hyps = function
- | [] -> tclIDTAC
- | id :: l ->
- tclTHENFIRST
- (tclTRY (general_rewrite_bindings_in l2r id c))
- (try_do_hyps l)
- in
- if cl.concl_occs <> [] then
- error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
- else
- tclTHENFIRST
- (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
- (match cl.onhyps with
- | Some l -> do_hyps l
- | None ->
- fun gl ->
- (* try to rewrite in all hypothesis
- (except maybe the rewritten one) *)
- let ids = match kind_of_term (fst c) with
- | Var id -> list_remove id (pf_ids_of_hyps gl)
- | _ -> pf_ids_of_hyps gl
- in try_do_hyps ids gl)
-
+ if cl.concl_occs <> [] then
+ error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+ else match cl.onhyps with
+ | Some l ->
+ (* If a precise list of locations is given, success is mandatory for
+ each of these locations. *)
+ let rec do_hyps = function
+ | [] -> tclIDTAC
+ | ((_,id),_) :: l ->
+ tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+ in
+ if not cl.onconcl then do_hyps l
+ else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l)
+ | None ->
+ (* Otherwise, if we are told to rewrite in all hypothesis via the
+ syntax "* |-", we fail iff all the different rewrites fail *)
+ let rec do_hyps_atleastonce = function
+ | [] -> (fun gl -> error "Nothing to rewrite.")
+ | id :: l ->
+ tclIFTHENTRYELSEMUST
+ (general_rewrite_bindings_in l2r id c)
+ (do_hyps_atleastonce l)
+ in
+ let do_hyps gl =
+ (* If the term to rewrite is an hypothesis, don't rewrite in itself *)
+ let ids = match kind_of_term (fst c) with
+ | Var id -> list_remove id (pf_ids_of_hyps gl)
+ | _ -> pf_ids_of_hyps gl
+ in do_hyps_atleastonce ids gl
+ in
+ if not cl.onconcl then do_hyps
+ else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps
(* Conditional rewriting, the success of a rewriting is related
to the resolution of the conditions by a given tactic *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c5cf54d47..4aad135c6 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -68,6 +68,7 @@ let tclTHENTRY = tclTHENTRY
let tclIFTHENELSE = tclIFTHENELSE
let tclIFTHENSELSE = tclIFTHENSELSE
let tclIFTHENSVELSE = tclIFTHENSVELSE
+let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST
let unTAC = unTAC
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4b0e39e78..de6ce5964 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -64,7 +64,7 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic
val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic
-
+val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
val unTAC : tactic -> goal sigma -> proof_tree sigma
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9750be0df..7b03a56c5 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -49,24 +49,7 @@ Ltac f_equal :=
| _ => idtac
end.
-(* Rewriting in all hypothesis. *)
+(* Rewriting in all hypothesis several times everywhere *)
-Ltac rewrite_all Eq := match type of Eq with
- ?a = ?b =>
- generalize Eq; clear Eq;
- match goal with
- | H : context [a] |- _ => intro Eq; rewrite Eq in H; rewrite_all Eq
- | _ => intro Eq; try rewrite Eq
- end
- end.
-
-Ltac rewrite_all_rev Eq := match type of Eq with
- ?a = ?b =>
- generalize Eq; clear Eq;
- match goal with
- | H : context [b] |- _ => intro Eq; rewrite <- Eq in H; rewrite_all_rev Eq
- | _ => intro Eq; try rewrite <- Eq
- end
- end.
-
-Tactic Notation "rewrite_all" "<-" constr(H) := rewrite_all_rev H.
+Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
+Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 14:22:49 +0000