feat(data/nat/*): generalize typeclass assumptions (#13260)

Author: ericrbg

src/data/nat/cast.lean

@@ -264,7 +264,7 @@ end prod
 
 section add_monoid_hom_class
 
-variables {A B F : Type*} [add_monoid A] [add_monoid B] [has_one B]
+variables {A B F : Type*} [add_zero_class A] [add_monoid B] [has_one B]
 
 lemma ext_nat' [add_monoid_hom_class F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
 fun_like.ext f g $ begin
@@ -283,15 +283,16 @@ lemma eq_nat_cast' [add_monoid_hom_class F ℕ A] (f : F) (h1 : f 1 = 1) :
 | 0     := by simp
 | (n+1) := by rw [map_add, h1, eq_nat_cast' n, nat.cast_add_one]
 
-lemma map_nat_cast' [add_monoid_hom_class F A B] (f : F) (h : f 1 = 1) : ∀ (n : ℕ), f n = n
+lemma map_nat_cast' {A} [add_monoid A] [has_one A] [add_monoid_hom_class F A B]
+                    (f : F) (h : f 1 = 1) : ∀ (n : ℕ), f n = n
 | 0     := by simp
 | (n+1) := by rw [nat.cast_add, map_add, nat.cast_add, map_nat_cast', nat.cast_one, h, nat.cast_one]
 
 end add_monoid_hom_class
 
 section monoid_with_zero_hom_class
 
-variables {A F : Type*} [monoid_with_zero A]
+variables {A F : Type*} [mul_zero_one_class A]
 
 /-- If two `monoid_with_zero_hom`s agree on the positive naturals they are equal. -/
 theorem ext_nat'' [monoid_with_zero_hom_class F ℕ A] (f g : F)

src/data/nat/parity.lean

@@ -194,15 +194,9 @@ end
 lemma even_sub_one_of_prime_ne_two {p : ℕ} (hp : prime p) (hodd : p ≠ 2) : even (p - 1) :=
 odd.sub_odd (odd_iff.2 $ hp.eq_two_or_odd.resolve_left hodd) (odd_iff.2 rfl)
 
-variables {R : Type*} [ring R]
+section distrib_neg_monoid
 
-theorem neg_one_pow_eq_one_iff_even (h1 : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ even n :=
-begin
-  rcases n.even_or_odd' with ⟨n, rfl | rfl⟩,
-  { simp [neg_one_pow_eq_pow_mod_two, pow_zero] },
-  { rw [← not_iff_not, neg_one_pow_eq_pow_mod_two, not_even_iff, add_mod],
-    simp only [h1, mul_mod_right, one_mod, pow_one, not_false_iff, eq_self_iff_true] }
-end
+variables {R : Type*} [monoid R] [has_distrib_neg R]
 
 @[simp] theorem neg_one_sq : (-1 : R) ^ 2 = 1 := by simp
 
@@ -229,6 +223,15 @@ by { convert nat.div_add_mod' n 2, rw odd_iff.mp h }
 lemma one_add_div_two_mul_two_of_odd (h : odd n) : 1 + n / 2 * 2 = n :=
 by { rw add_comm, convert nat.div_add_mod' n 2, rw odd_iff.mp h }
 
+theorem neg_one_pow_eq_one_iff_even (h1 : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ even n :=
+begin
+  refine ⟨λ h, _, neg_one_pow_of_even⟩,
+  contrapose! h1,
+  exact (neg_one_pow_of_odd $ odd_iff_not_even.mpr h1).symm.trans h
+end
+
+end distrib_neg_monoid
+
 -- Here are examples of how `parity_simps` can be used with `nat`.
 
 example (m n : ℕ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=