From 6eede071cb97e1e39772c2bdecb5189c4fa2adb0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 21 Jan 2016 23:28:40 +0100
Subject: Extending "contradiction" so that it recognizes statements such as
 "~x=x" or ~True.

Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.

New behavior deactivated when version is <= 8.5.
---
 CHANGES                               |  4 ++++
 doc/refman/RefMan-tac.tex             |  8 ++++----
 tactics/contradiction.ml              | 17 +++++++++++++++++
 theories/Numbers/Integer/BigZ/ZMake.v |  2 +-
 theories/Numbers/Natural/BigN/NMake.v |  2 +-
 theories/Structures/OrdersFacts.v     |  2 +-
 6 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/CHANGES b/CHANGES
index 594bbc831..f7e1dee4c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.
-- 
cgit v1.2.3