diff options
-rw-r--r-- | CHANGES | 7 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 16 | ||||
-rw-r--r-- | tactics/equality.ml | 40 | ||||
-rw-r--r-- | tactics/equality.mli | 4 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 24 | ||||
-rw-r--r-- | theories/Sorting/Permutation.v | 2 | ||||
-rw-r--r-- | toplevel/auto_ind_decl.ml | 2 |
7 files changed, 72 insertions, 23 deletions
@@ -50,7 +50,12 @@ Tactics "context" can be retrieved at parse time by setting the "Tactic Compat Context" flag. (possible source of incompatibilities). - Introduction patterns of the form [x1 .. xn] or (x1,..,xn) now apply - injection when used on an equality statement ("ssreflect" style) + "injection" when used on an equality statement ("ssreflect" style). +- Tactic "injection c as ipats" now clears c if c refers to an + hypothesis and moves the resulting equations in the hypotheses + independently of the number of ipats, which has itself to be less + than the number of new hypotheses (possible source of incompatibilities; + former behavior obtainable by "Unset Injection L2R Pattern Order"). Program diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 432ff5279..238217560 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -822,6 +822,14 @@ introduction pattern~$p$: of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots}, $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots} $p_n$]}); +\item as a special case, if the product is over an equality type, then + a pattern of the form {\tt [$p_{1}$ \dots\ $p_n$]} or of the form + {\tt ($p_1$, \ldots, $p_n$)} applies {\tt injection} instead of {\tt + destruct} on the hypothesis and use the patterns $p_1$, \ldots, + $p_n$ on the hypotheses generated by {\tt injection} (see + Section~\ref{injection}); if the number of patterns is smaller than + the number of hypotheses generated, the pattern \texttt{?} is used + to complete the list; \item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)} is a shortcut for introduction via {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the @@ -2118,7 +2126,13 @@ introduced hypothesis. \tacindex{injection \dots\ as} These variants apply \texttt{intros} \nelistnosep{\intropattern} after -the call to \texttt{injection} or \texttt{einjection}. +the call to \texttt{injection} or \texttt{einjection} so that all +equalities generated are moved in the context of hypotheses. The +number of {\intropattern} must not exceed the number of equalities +newly generated. If it is smaller, fresh names are automatically +generated to adjust the list of {\intropattern} to the number of new +equalities. The original equality is erased if it corresponds to an +hypothesis. \end{Variants} diff --git a/tactics/equality.ml b/tactics/equality.ml index 16ab1ee5b..842ce67a0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -60,6 +60,21 @@ let _ = optread = (fun () -> !discriminate_introduction); optwrite = (:=) discriminate_introduction } +let injection_pattern_l2r_order = ref true + +let use_injection_pattern_l2r_order () = + !injection_pattern_l2r_order + && Flags.version_strictly_greater Flags.V8_4 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "injection left-to-right pattern order"; + optkey = ["Injection";"L2R";"Pattern";"Order"]; + optread = (fun () -> !injection_pattern_l2r_order) ; + optwrite = (fun b -> injection_pattern_l2r_order := b) } + (* Rewriting tactics *) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) @@ -1171,10 +1186,25 @@ let injEq_then tac l2r (eq,_,(t,t1,t2) as u) eq_clause = (tac (clenv_value eq_clause)) let injEq ipats = + let l2r = + if use_injection_pattern_l2r_order () & ipats <> None then true else false + in injEq_then - (fun c _ -> - tclTHEN (clear_if_overwritten c ipats) (intros_pattern MoveLast ipats)) - false + (fun c n -> match ipats with + | Some ipats -> + let clear_tac = + if use_injection_pattern_l2r_order () && isVar c + then tclTRY (clear [destVar c]) + else tclIDTAC in + let ipats = + if use_injection_pattern_l2r_order () + then adjust_intro_patterns n ipats + else ipats in + tclTHEN + (clear_tac) + (intros_pattern MoveLast ipats) + | None -> tclIDTAC) + l2r let inj ipats with_evars = onEquality with_evars (injEq ipats) @@ -1182,8 +1212,8 @@ let injClause ipats with_evars = function | None -> onNegatedEquality with_evars (injEq ipats) | Some c -> onInductionArg (inj ipats with_evars) c -let injConcl gls = injClause [] false None gls -let injHyp id gls = injClause [] false (Some (ElimOnIdent (Loc.ghost,id))) gls +let injConcl gls = injClause None false None gls +let injHyp id gls = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) gls let _ = declare_injector (fun tac -> injEq_then (fun _ -> tac) true) diff --git a/tactics/equality.mli b/tactics/equality.mli index 147218efd..1413c1b70 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -91,9 +91,9 @@ val discrHyp : Id.t -> tactic val discrEverywhere : evars_flag -> tactic val discr_tac : evars_flag -> constr with_bindings induction_arg option -> tactic -val inj : intro_pattern_expr Loc.located list -> evars_flag -> +val inj : intro_pattern_expr Loc.located list option -> evars_flag -> constr with_bindings -> tactic -val injClause : intro_pattern_expr Loc.located list -> evars_flag -> +val injClause : intro_pattern_expr Loc.located list option -> evars_flag -> constr with_bindings induction_arg option -> tactic val injHyp : Id.t -> tactic val injConcl : tactic diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 5a8fc3bbb..75fedc598 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -118,44 +118,44 @@ let discrHyp id gl = discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl let injection_main c = - elimOnConstrWithHoles (injClause []) false c + elimOnConstrWithHoles (injClause None) false c TACTIC EXTEND injection_main | [ "injection" constr_with_bindings(c) ] -> [ injection_main c ] END TACTIC EXTEND injection -| [ "injection" ] -> [ injClause [] false None ] +| [ "injection" ] -> [ injClause None false None ] | [ "injection" quantified_hypothesis(h) ] -> - [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ] + [ injClause None false (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND einjection_main | [ "einjection" constr_with_bindings(c) ] -> - [ elimOnConstrWithHoles (injClause []) true c ] + [ elimOnConstrWithHoles (injClause None) true c ] END TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause [] true None ] -| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ] +| [ "einjection" ] -> [ injClause None true None ] +| [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND injection_as_main | [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ elimOnConstrWithHoles (injClause ipat) false c ] + [ elimOnConstrWithHoles (injClause (Some ipat)) false c ] END TACTIC EXTEND injection_as | [ "injection" "as" simple_intropattern_list(ipat)] -> - [ injClause ipat false None ] + [ injClause (Some ipat) false None ] | [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> - [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ] + [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND einjection_as_main | [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ elimOnConstrWithHoles (injClause ipat) true c ] + [ elimOnConstrWithHoles (injClause (Some ipat)) true c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" simple_intropattern_list(ipat)] -> - [ injClause ipat true None ] + [ injClause (Some ipat) true None ] | [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> - [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ] + [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ] END let injHyp id gl = diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 65bf17ef0..cf9f8ee42 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -313,7 +313,7 @@ Qed. Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. Proof. intros a l H; remember [a] as m in H. - induction H; try (injection Heqm as -> ->; clear Heqm); + induction H; try (injection Heqm as -> ->); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 56bdc810d..82445a0fd 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -666,7 +666,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); - Equality.inj [] false (mkVar freshz,NoBindings); + Equality.inj None false (mkVar freshz,NoBindings); intros; simpl_in_concl; Auto.default_auto; tclREPEAT ( |