Omega: for non-arithmetical goals, try proving False from context (wish #2236)

 This way, no more error messages like "Unrecognized predicate".
 Some code simplification and reorganization on the way, in particular
 a few tests like "is_Prop ..." or "closed0 ..." were actually useless.
 Also add support for the situation H:~Zne x y for uniformity.

 Beware: scripts relying negatively on the strength of omega may have to
 be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails.").
 For instance, one line deletion in PermutSetoid.v
 Probably more cumbersome : "auto with *" becomes stronger since it
 may call omega. Todo : check the impact on contribs tomorrow.

 Btw, this commit seems to solve a bug where omega was to be guided
 by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 32faf5a95..a8cd69bb3 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -111,6 +111,12 @@ Proof.
   Z.swap_greater. apply Z.nle_gt.
 Qed.
 
+Lemma not_Zne n m : ~ Zne n m -> n = m.
+Proof.
+  intros H.
+  destruct (Z.eq_decidable n m); [assumption|now elim H].
+Qed.
+
 (** * Equivalence and order properties *)
 
 (** Reflexivity *)