Z is integral domain

2 files changed, 35 insertions, 4 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 43aac8e4a..b5eb4a7f5 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -527,7 +527,8 @@ Ltac nsatz_rewrite_and_revert domain :=
 Ltac nsatz_nonzero := 
   try solve [apply Integral_domain.integral_domain_one_zero
             |apply Integral_domain.integral_domain_minus_one_zero
-            |trivial].
+            |trivial
+            |apply Ring.opp_nonzero_nonzero;trivial].
 
 Ltac nsatz_domain_sugar_power domain sugar power := 
   let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
@@ -585,8 +586,8 @@ Ltac field_algebra :=
   try (nsatz; dropRingSyntax);
   repeat (apply conj);
   try solve
-      [unfold not; intro; nsatz_contradict
-      |nsatz_nonzero].
+      [nsatz_nonzero
+      |unfold not; intro; nsatz_contradict].
 
 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}.
@@ -603,4 +604,24 @@ Section Example.
 
   Example _example_nonzero_nsatz_contradict x y : x * y = 1 -> not (x = 0).
   Proof. intros. intro. nsatz_contradict. Qed.
-End Example.
\ No newline at end of file
+End Example.
+
+Section Z.
+  Require Import ZArith.
+  Global Instance ring_Z : @ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof. repeat split; auto using Z.eq_dec with zarith typeclass_instances. Qed.
+
+  Global Instance commutative_ring_Z : @commutative_ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof. eauto using @commutative_ring, @is_commutative, ring_Z with zarith. Qed.
+
+  Global Instance integral_domain_Z : @integral_domain Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof.
+    split.
+    { apply commutative_ring_Z. }
+    { constructor. intros. apply Z.neq_mul_0; auto. }
+    { constructor. discriminate. }
+  Qed.
+
+  Example _example_nonzero_nsatz_contradict_Z x y : Z.mul x y = (Zpos xH) -> not (x = Z0).
+  Proof. intros. intro. nsatz_contradict. Qed.
+End Z.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index dabfcf883..fe7600784 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -149,6 +149,16 @@ Section FandZ.
     intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition.
   Qed.
 
+  Require Crypto.Algebra.
+  Global Instance ring_modulo : @Algebra.ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul.
+  Proof.
+    repeat split; Fdefn.
+    { rewrite Z.add_0_r. auto. }
+    { rewrite <-Z.add_sub_swap, <-Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. apply Z_mod_same_full. }
+    { apply F_eq_dec. }
+    { rewrite Z.mul_1_r. auto. }
+  Qed.
+
   Lemma ZToField_0 : @ZToField m 0 = 0.
   Proof.
     Fdefn.