diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 8 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 17 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 | ||||
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 2 |
6 files changed, 28 insertions, 7 deletions
@@ -61,6 +61,10 @@ Tactics "Structural Injection". In this case, hypotheses are also put in the context in the natural left-to-right order and the hypothesis on which injection applies is cleared. +- Tactic "contradiction" (hence "easy") now also solve goals with + hypotheses of the form "~True" or "t<>t" (possible source of + incompatibilities because of more successes in automation, but + generally a more intuitive strategy). Hints diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8172b5771..65b49893b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1491,10 +1491,10 @@ the local context. \tacindex{contradiction} This tactic applies to any goal. The {\tt contradiction} tactic -attempts to find in the current context (after all {\tt intros}) one -hypothesis that is equivalent to {\tt False}. It permits to prune -irrelevant cases. This tactic is a macro for the tactics sequence -{\tt intros; elimtype False; assumption}. +attempts to find in the current context (after all {\tt intros}) an +hypothesis that is equivalent to an empty inductive type (e.g. {\tt + False}), to the negation of a singleton inductive type (e.g. {\tt + True} or {\tt x=x}), or two contradictory hypotheses. \begin{ErrMsgs} \item \errindex{No such assumption} diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c3796b484..445a104d6 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -42,6 +42,8 @@ let absurd c = absurd c (* Contradiction *) +let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 + (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function @@ -67,6 +69,21 @@ let contradiction_context = simplest_elim (mkVar id) else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> + let is_unit_or_eq = + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t + else None in + Tacticals.New.tclORELSE + (match is_unit_or_eq with + | Some _ -> + let hd,args = decompose_app t in + let (ind,_ as indu) = destInd hd in + let nparams = Inductiveops.inductive_nparams_env env ind in + let params = Util.List.firstn nparams args in + let p = applist ((mkConstructUi (indu,1)), params) in + (* Checking on the fly that it type-checks *) + simplest_elim (mkApp (mkVar id,[|p|])) + | None -> + Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) (Proofview.tclORELSE (Proofview.Goal.enter { enter = begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 63fb5800c..fec6e0683 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType. Proof. apply Bool.eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min n m := match compare n m with Gt => m | _ => n end. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 98949736c..1425041a1 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType. Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 954d3df20..b059173cb 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -448,7 +448,7 @@ Lemma leb_compare x y : (x <=? y) = match compare x y with Gt => false | _ => true end. Proof. apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff. -destruct compare; split; try easy. now destruct 1. +now destruct compare; split. Qed. End BoolOrderFacts. |