diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 14 | ||||
| -rw-r--r-- | tactics/inv.ml | 15 | ||||
| -rw-r--r-- | tactics/tactics.ml | 15 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 | ||||
| -rw-r--r-- | test-suite/success/Inversion.v | 20 |
6 files changed, 59 insertions, 7 deletions
@@ -189,6 +189,7 @@ Tactics swapped, as a more friendly replacement of "cut". - In destruct/induction, experimental modifier "!" prefixing the hypothesis name to tell not erasing the hypothesis. +- Bug fixes in "inversion as" may occasionally lead to incompatibilities. Program diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 90055ea837..e8ec731e61 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2272,7 +2272,7 @@ several times. See Section~\ref{Derive-Inversion}. \item \tacindex{inversion \dots\ as} \texttt{inversion {\ident} as \intropattern} - This behaves as \texttt{inversion} but using names in + This generally behaves as \texttt{inversion} but using names in {\intropattern} for naming hypotheses. The {\intropattern} must have the form {\tt [} $p_{11} \ldots p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1} \ldots p_{mn_m}$ {\tt ]} with $m$ being the number of @@ -2294,6 +2294,13 @@ several times. See Section~\ref{Derive-Inversion}. \dots, $p_{ijq}$)}) where $q$ is the number of subequalities obtained from splitting the original equation. Here is an example. + The \texttt{inversion \dots\ as} variant of \texttt{inversion} + generally behaves in a slightly more expectable way than + \texttt{inversion} (no artificial duplication of some hypotheses + referring to other hypotheses) To take benefit of these + improvements, it is enough to use \texttt{inversion \dots\ as []}, + letting the names being finally chosen by {\Coq}. + \begin{coq_eval} Require Import List. \end{coq_eval} @@ -2319,7 +2326,10 @@ Abort. {\ident} as \intropattern} This allows naming the hypotheses introduced by - \texttt{inversion\_clear} in the context. + \texttt{inversion\_clear} in the context. Notice that hypothesis + names can be provided as if \texttt{inversion} were called, even + though the \texttt{inversion\_clear} will eventually erase the + hypotheses. \item \tacindex{inversion \dots\ in} \texttt{inversion {\ident} in \ident$_1$ \dots\ \ident$_n$} diff --git a/tactics/inv.ml b/tactics/inv.ml index 5d49a90473..2efaa96b6d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -267,13 +267,14 @@ Summary: nine useless hypotheses! Nota: with Inversion_clear, only four useless hypotheses *) -let generalizeRewriteIntros tac depids id = +let generalizeRewriteIntros as_mode tac depids id = Proofview.Goal.nf_enter begin fun gl -> let dids = dependent_hyps id depids gl in + let reintros = if as_mode then intros_replacing else intros_possibly_replacing in (tclTHENLIST [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) - intros_replacing (ids_of_named_context dids)]) + reintros (ids_of_named_context dids)]) end let error_too_many_names pats = @@ -340,12 +341,13 @@ let projectAndApply as_mode thin id eqname names depids = let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in match (kind_of_term t1, kind_of_term t2) with - | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 - | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 + | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 + | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 | _ -> tac id end in - let deq_trailer id _ _ neqns = + let deq_trailer id clear_flag _ neqns = + assert (clear_flag == None); tclTHENLIST [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> @@ -356,6 +358,9 @@ let projectAndApply as_mode thin id eqname names depids = (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) names); (if as_mode then tclIDTAC else clear [id])] + (* Doing the above late breaks the computation of dids in + generalizeRewriteIntros, and hence breaks proper intros_replacing + but it is needed for compatibility *) in substHypIfVariable (* If no immediate variable in the equation, try to decompose it *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3cd6eb2881..83a8c2a49b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -596,6 +596,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false + let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false let intro = intro_gen (NamingAvoid []) MoveLast false false let introf = intro_gen (NamingAvoid []) MoveLast true false @@ -653,6 +654,20 @@ let intro_replacing id gl = reintroduce y, y,' y''. Note that we have to clear y, y' and y'' before introducing y because y' or y'' can e.g. depend on old y. *) +(* This version assumes that replacement is actually possible *) +let intros_possibly_replacing ids = + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let posl = List.fold_right (fun id posl -> + (id,get_next_hyp_position id posl hyps) :: posl) ids [] in + Tacticals.New.tclTHEN + (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id]))) ids) + (Tacticals.New.tclMAP (fun (id,pos) -> + Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) + posl) + end + +(* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 349e828a19..a9434d6ae7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -68,6 +68,7 @@ val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic +val intros_possibly_replacing : Id.t list -> unit Proofview.tactic val intros : unit Proofview.tactic diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index b068f7298c..892dd6d489 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -136,3 +136,23 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. + +(* Was failing at some time between 7 and 10 September 2014 *) +(* even though, it is not clear that the resulting context is interesting *) + +Parameter P:nat*nat->Prop. +Inductive IND : nat * nat -> { x : nat * nat | P x } * nat -> Prop := +CONSTR a b (H:P (a,b)) c : IND (a,b) (exist _ (a,b) H, c). + +Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z. +intros * Hyp. +inversion Hyp. + (* By the way, why is "H" removed even in non-clear mode ? *) +reflexivity. +Qed. + +Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z. +intros * Hyp. +inversion Hyp as (a,b,H,c,(H1_1,H1_2),(H2_1,H2_2,H2_3)). +reflexivity. +Qed. |