Make [nsatz_contradict] better at inequalities

2 files changed, 38 insertions, 15 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index baa676b64..d7b684760 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -225,7 +225,21 @@ Module Group.
       intros ? Hx Ho.
       assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity).
       rewrite Ho, right_identity in Hxo. intuition.
-   Qed.
+    Qed.
+
+    Lemma neq_inv_nonzero : forall x, x <> inv x -> x <> id.
+    Proof.
+      intros ? Hx Hi; apply Hx.
+      rewrite Hi.
+      symmetry; apply inv_id.
+    Qed.
+
+    Lemma inv_neq_nonzero : forall x, inv x <> x -> x <> id.
+    Proof.
+      intros ? Hx Hi; apply Hx.
+      rewrite Hi.
+      apply inv_id.
+    Qed.
 
     Section ZeroNeqOne.
       Context {one} `{is_zero_neq_one T eq id one}.
@@ -613,13 +627,7 @@ Ltac field_algebra :=
   try solve
       [neq01
       |trivial
-      |apply Ring.opp_nonzero_nonzero;trivial
-      |match goal with
-       | [ H : not (?eq ?zero (?opp ?zero)) |- _ ]
-         => exfalso; apply H; nsatz
-       | [ H : not (?eq (?opp ?zero) ?zero) |- _ ]
-         => exfalso; apply H; nsatz
-       end].
+      |apply Ring.opp_nonzero_nonzero;trivial].
 
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v
index dc7bd25aa..97b9da1ad 100644
--- a/src/Tactics/Nsatz.v
+++ b/src/Tactics/Nsatz.v
@@ -126,13 +126,28 @@ Tactic Notation "nsatz" constr(n) :=
 
 Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.
 
-Ltac nsatz_contradict :=
-  unfold not;
-  intros;
-  let domain := nsatz_guess_domain in
+(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y]
+    contradicts any hypothesis of the form [?x' <> ?y'], we turn this
+    problem about inequalities into one about equalities and give it
+    to [nsatz]. *)
+Ltac nsatz_contradict_single_hypothesis domain :=
   lazymatch type of domain with
   | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    assert (eq one zero) as Hbad;
-    [nsatz; nsatz_nonzero
-    |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
+    unfold not in *;
+    match goal with
+    | [ H : eq _ _ -> False |- eq _ _ -> False ]
+      => intro; apply H; nsatz
+    end
   end.
+
+Ltac nsatz_contradict :=
+  let domain := nsatz_guess_domain in
+  nsatz_contradict_single_hypothesis domain
+  || (unfold not;
+      intros;
+      lazymatch type of domain with
+      | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+        assert (eq one zero) as Hbad;
+        [nsatz; nsatz_nonzero
+        |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
+      end).