diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 53 | ||||
| -rw-r--r-- | tactics/equality.ml | 35 | ||||
| -rw-r--r-- | test-suite/output/subst.out | 97 | ||||
| -rw-r--r-- | test-suite/output/subst.v | 48 |
5 files changed, 198 insertions, 36 deletions
@@ -4,6 +4,7 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes - #4677: fix alpha-conversion in notations needing eta-expansion +- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. Changes from V8.5 to V8.5pl1 ============================ diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 903e2e19af..fa595d9159 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2854,42 +2854,57 @@ This tactic is deprecated. It can be replaced by {\tt enough} \tacindex{subst} \optindex{Regular Subst Tactic} -This tactic applies to a goal that has \ident\ in its context and -(at least) one hypothesis, say {\tt H}, of type {\tt - \ident=t} or {\tt t=\ident}. Then it replaces -\ident\ by {\tt t} everywhere in the goal (in the hypotheses -and in the conclusion) and clears \ident\ and {\tt H} from the context. +This tactic applies to a goal that has \ident\ in its context and (at +least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$ +{\tt = \ident} with {\ident} not occurring in $t$. Then it replaces +{\ident} by $t$ everywhere in the goal (in the hypotheses and in the +conclusion) and clears {\ident} and $H$ from the context. + +If {\ident} is a local definition of the form {\ident} := $t$, it is +also unfolded and cleared. + +\Rem +When several hypotheses have the form {\tt \ident} = $t$ or {\tt + $t$ = \ident}, the first one is used. \Rem -When several hypotheses have the form {\tt \ident=t} or {\tt - t=\ident}, the first one is used. +If $H$ is itself dependent in the goal, it is replaced by the +proof of reflexivity of equality. \begin{Variants} - \item {\tt subst \ident$_1$ \dots \ident$_n$} + \item {\tt subst \ident$_1$ {\dots} \ident$_n$} - Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. + This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. \item {\tt subst} - Applies {\tt subst} repeatedly to all identifiers from the context - for which an equality exists. + This applies {\tt subst} repeatedly from top to bottom to all + identifiers of the context for which an equality of the form {\tt + \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with + {\ident} not occurring in $t$. -\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set - Regular Subst Tactic}. When this option is activated, {\tt subst} - manages the following corner cases which otherwise it - does not: +\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled +using option {\tt Set Regular Subst Tactic}. When this option is +activated, {\tt subst} also deals with the following corner cases: \begin{itemize} \item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$} and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$} - or {\tt $u$ = \ident$_2$} + or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt + subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$ + respectively. + \item A context with cyclic dependencies as with hypotheses {\tt - \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} + \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which + without the option would be a cause of failure of {\tt subst}. \end{itemize} -Additionally, it prevents a local definition such as {\tt \ident := - $t$} to be unfolded which otherwise it would exceptionally unfold in +Additionally, it prevents a local definition such as {\tt \ident} := + $t$ to be unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form {\tt {\ident} = $u$}, or {\tt $u'$ = \ident} with $u'$ not a variable. +Finally, it preserves the initial order of hypotheses, which without +the option it may break. + The option is off by default. \end{Variants} diff --git a/tactics/equality.ml b/tactics/equality.ml index f72a72f46d..819a995db1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1595,6 +1595,17 @@ user = raise user error specific to rewrite (**********************************************************************) (* Substitutions tactics (JCF) *) +let regular_subst_tactic = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "more regular behavior of tactic subst"; + optkey = ["Regular";"Subst";"Tactic"]; + optread = (fun () -> !regular_subst_tactic); + optwrite = (:=) regular_subst_tactic } + let unfold_body x = Proofview.Goal.enter begin fun gl -> (** We normalize the given hypothesis immediately. *) @@ -1642,23 +1653,24 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) let dephyps = - List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) -> + List.rev (pi3 (List.fold_right (fun (id,b,_ as dcl) (dest,deps,allhyps) -> if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then - ((if b = None then deps else id::deps), id::allhyps) + let id_dest = if !regular_subst_tactic then dest else MoveLast in + (dest,(if b = None then deps else id::deps), (id_dest,id)::allhyps) else - (deps,allhyps)) + (MoveBefore id,deps,allhyps)) hyps - ([x],[]))) in + (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) let depconcl = occur_var env x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then - [revert dephyps; + [revert (List.map snd dephyps); general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); - (tclMAP intro_using dephyps)] + (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) @@ -1709,17 +1721,6 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } -let regular_subst_tactic = ref false - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "more regular behavior of tactic subst"; - optkey = ["Regular";"Subst";"Tactic"]; - optread = (fun () -> !regular_subst_tactic); - optwrite = (:=) regular_subst_tactic } - let subst_all ?(flags=default_subst_tactic_flags ()) () = if !regular_subst_tactic then diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out new file mode 100644 index 0000000000..f5768ba441 --- /dev/null +++ b/test-suite/output/subst.out @@ -0,0 +1,97 @@ +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : 0 = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + HA, HB : True + H4 : 0 = 4 + H3 : 0 = 3 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v new file mode 100644 index 0000000000..e48aa6bb28 --- /dev/null +++ b/test-suite/output/subst.v @@ -0,0 +1,48 @@ +(* Ensure order of hypotheses is respected after "subst" *) + +Set Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *) +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + +Unset Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + + |