chore(parity): even and odd in semiring (#4473)

Replaces the ad-hoc `nat.even`, `nat.odd`, `int.even` and `int.odd` by definitions that make sense in semirings and get that `odd` can be `rintros`/`rcases`'ed. This requires almost no change except that `even` is not longer usable as a dot notation (which I see as a feature since I find `even n` to be more readable than `n.even`).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/ring/basic.lean

@@ -171,6 +171,14 @@ lemma ite_mul_zero_right {α : Type*} [mul_zero_class α] (P : Prop) [decidable
   ite P (a * b) 0 = a * ite P b 0 :=
 by { by_cases h : P; simp [h], }
 
+/-- An element `a` of a semiring is even if there exists `k` such `a = 2*k`. -/
+def even (a : α) : Prop := ∃ k, a = 2*k
+
+lemma even_iff_two_dvd {a : α} : even a ↔ 2 ∣ a := iff.rfl
+
+/-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`. -/
+def odd (a : α) : Prop := ∃ k, a = 2*k + 1
+
 end semiring
 
 namespace add_monoid_hom

src/analysis/convex/specific_functions.lean

@@ -29,12 +29,12 @@ convex_on_univ_of_deriv2_nonneg differentiable_exp (by simp)
   (assume x, (iter_deriv_exp 2).symm ▸ le_of_lt (exp_pos x))
 
 /-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even -/
-lemma convex_on_pow_of_even {n : ℕ} (hn : n.even) : convex_on set.univ (λ x : ℝ, x^n) :=
+lemma convex_on_pow_of_even {n : ℕ} (hn : even n) : convex_on set.univ (λ x : ℝ, x^n) :=
 begin
   apply convex_on_univ_of_deriv2_nonneg differentiable_pow,
   { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] },
   { intro x,
-    rcases hn.sub (nat.even_bit0 1) with ⟨k, hk⟩,
+    rcases nat.even.sub hn (nat.even_bit0 1) with ⟨k, hk⟩,
     simp only [iter_deriv_pow, finset.prod_range_succ, finset.prod_range_zero, nat.sub_zero,
       mul_one, hk, pow_mul', pow_two],
     exact mul_nonneg (nat.cast_nonneg _) (mul_self_nonneg _) }
@@ -53,15 +53,15 @@ end
 lemma finset.prod_nonneg_of_card_nonpos_even
   {α β : Type*} [linear_ordered_comm_ring β]
   {f : α → β} [decidable_pred (λ x, f x ≤ 0)]
-  {s : finset α} (h0 : (s.filter (λ x, f x ≤ 0)).card.even) :
+  {s : finset α} (h0 : even (s.filter (λ x, f x ≤ 0)).card) :
   0 ≤ ∏ x in s, f x :=
 calc 0 ≤ (∏ x in s, ((if f x ≤ 0 then (-1:β) else 1) * f x)) :
   finset.prod_nonneg (λ x _, by
     { split_ifs with hx hx, by simp [hx], simp at hx ⊢, exact le_of_lt hx })
 ... = _ : by rw [finset.prod_mul_distrib, finset.prod_ite, finset.prod_const_one,
   mul_one, finset.prod_const, neg_one_pow_eq_pow_mod_two, nat.even_iff.1 h0, pow_zero, one_mul]
 
-lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : n.even) :
+lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : even n) :
   0 ≤ ∏ k in finset.range n, (m - k) :=
 begin
   cases (le_or_lt ↑n m) with hnm hmn,

src/analysis/mean_inequalities.lean

@@ -145,7 +145,7 @@ theorem pow_arith_mean_le_arith_mean_pow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0
 (convex_on_pow n).map_sum_le hw hw' hz
 
 theorem pow_arith_mean_le_arith_mean_pow_of_even (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
-  (hw' : ∑ i in s, w i = 1) {n : ℕ} (hn : n.even) :
+  (hw' : ∑ i in s, w i = 1) {n : ℕ} (hn : even n) :
   (∑ i in s, w i * z i) ^ n ≤ ∑ i in s, (w i * z i ^ n) :=
 (convex_on_pow_of_even hn).map_sum_le hw hw' (λ _ _, trivial)
 

src/data/int/parity.lean

@@ -10,57 +10,50 @@ import data.nat.parity
 
 namespace int
 
-@[simp] theorem mod_two_ne_one {n : int} : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
+@[simp] theorem mod_two_ne_one {n : ℤ} : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
 local attribute [simp] -- euclidean_domain.mod_eq_zero uses (2 ∣ n) as normal form
-theorem mod_two_ne_zero {n : int} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
+theorem mod_two_ne_zero {n : ℤ} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-/-- An integer `n` is `even` if `2 | n`. -/
-def even (n : int) : Prop := 2 ∣ n
-
-@[simp] theorem even_coe_nat (n : nat) : even n ↔ nat.even n :=
+@[simp] theorem even_coe_nat (n : nat) : even (n : ℤ) ↔ even n :=
 have ∀ m, 2 * to_nat m = to_nat (2 * m),
  from λ m, by cases m; refl,
 ⟨λ ⟨m, hm⟩, ⟨to_nat m, by rw [this, ←to_nat_coe_nat n, hm]⟩,
  λ ⟨m, hm⟩, ⟨m, by simp [hm]⟩⟩
 
-theorem even_iff {n : int} : even n ↔ n % 2 = 0 :=
+theorem even_iff {n : ℤ} : even n ↔ n % 2 = 0 :=
 ⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩
 
+theorem odd_iff {n : ℤ} : odd n ↔ n % 2 = 1 :=
+⟨λ ⟨m, hm⟩, by { rw [hm, add_mod], norm_num },
+ λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by { rw h, abel })⟩⟩
+
 lemma not_even_iff {n : ℤ} : ¬ even n ↔ n % 2 = 1 :=
 by rw [even_iff, mod_two_ne_zero]
 
-/-- An integer `n` is `odd` if it is not even.  The mathlib API
-for parity is developed in terms of `even`; to avoid duplication,
-results should not be stated in terms of `odd`.  The purpose of this
-definition is for code outside mathlib that wishes to have a formal
-statement that is as literal a translation as possible of the
-corresponding informal statement, where that informal statement refers
-to odd numbers. -/
-def odd (n : ℤ) : Prop := ¬ even n
-
-@[simp] lemma odd_def (n : ℤ) : odd n ↔ ¬ even n := iff.rfl
+@[simp] lemma odd_iff_not_even {n : ℤ} : odd n ↔ ¬ even n :=
+by rw [not_even_iff, odd_iff]
 
-@[simp] theorem two_dvd_ne_zero {n : int} : ¬ 2 ∣ n ↔ n % 2 = 1 :=
+@[simp] theorem two_dvd_ne_zero {n : ℤ} : ¬ 2 ∣ n ↔ n % 2 = 1 :=
 not_even_iff
 
-instance : decidable_pred even :=
+instance : decidable_pred (even : ℤ → Prop) :=
 λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm
 
-instance decidable_pred_odd : decidable_pred odd :=
-λ n, decidable_of_decidable_of_iff (by apply_instance) not_even_iff.symm
+instance decidable_pred_odd : decidable_pred (odd : ℤ → Prop) :=
+λ n, decidable_of_decidable_of_iff (by apply_instance) odd_iff_not_even.symm
 
-@[simp] theorem even_zero : even (0 : int) := ⟨0, dec_trivial⟩
+@[simp] theorem even_zero : even (0 : ℤ) := ⟨0, dec_trivial⟩
 
-@[simp] theorem not_even_one : ¬ even (1 : int) :=
+@[simp] theorem not_even_one : ¬ even (1 : ℤ) :=
 by rw even_iff; apply one_ne_zero
 
-@[simp] theorem even_bit0 (n : int) : even (bit0 n) :=
+@[simp] theorem even_bit0 (n : ℤ) : even (bit0 n) :=
 ⟨n, by rw [bit0, two_mul]⟩
 
-@[parity_simps] theorem even_add {m n : int} : even (m + n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_add {m n : ℤ} : even (m + n) ↔ (even m ↔ even n) :=
 begin
   cases mod_two_eq_zero_or_one m with h₁ h₁; cases mod_two_eq_zero_or_one n with h₂ h₂;
     simp [even_iff, h₁, h₂, -euclidean_domain.mod_eq_zero],
@@ -70,15 +63,15 @@ begin
   exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂
 end
 
-@[parity_simps] theorem even_neg {n : ℤ} : even (-n) ↔ even n := by simp [even]
+@[parity_simps] theorem even_neg {n : ℤ} : even (-n) ↔ even n := by simp [even_iff]
 
-@[simp] theorem not_even_bit1 (n : int) : ¬ even (bit1 n) :=
+@[simp] theorem not_even_bit1 (n : ℤ) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps
 
-@[parity_simps] theorem even_sub {m n : int} : even (m - n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_sub {m n : ℤ} : even (m - n) ↔ (even m ↔ even n) :=
 by simp [sub_eq_add_neg] with parity_simps
 
-@[parity_simps] theorem even_mul {m n : int} : even (m * n) ↔ even m ∨ even n :=
+@[parity_simps] theorem even_mul {m n : ℤ} : even (m * n) ↔ even m ∨ even n :=
 begin
   cases mod_two_eq_zero_or_one m with h₁ h₁; cases mod_two_eq_zero_or_one n with h₂ h₂;
     simp [even_iff, h₁, h₂, -euclidean_domain.mod_eq_zero],
@@ -88,15 +81,15 @@ begin
   exact @modeq.modeq_mul _ _ 1 _ 1 h₁ h₂
 end
 
-@[parity_simps] theorem even_pow {m : int} {n : nat} : even (m^n) ↔ even m ∧ n ≠ 0 :=
+@[parity_simps] theorem even_pow {m : ℤ} {n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 :=
 by { induction n with n ih; simp [*, even_mul, pow_succ], tauto }
 
 -- Here are examples of how `parity_simps` can be used with `int`.
 
-example (m n : int) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=
+example (m n : ℤ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=
 by simp [*, (dec_trivial : ¬ 2 = 0)] with parity_simps
 
-example : ¬ even (25394535 : int) :=
+example : ¬ even (25394535 : ℤ) :=
 by simp
 
 end int

src/data/nat/parity.lean

@@ -9,37 +9,30 @@ import data.nat.modeq
 
 namespace nat
 
-@[simp] theorem mod_two_ne_one {n : nat} : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
+@[simp] theorem mod_two_ne_one {n : ℕ} : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-@[simp] theorem mod_two_ne_zero {n : nat} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
+@[simp] theorem mod_two_ne_zero {n : ℕ} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-/-- A natural number `n` is `even` if `2 | n`. -/
-def even (n : nat) : Prop := 2 ∣ n
-
-theorem even_iff {n : nat} : even n ↔ n % 2 = 0 :=
+theorem even_iff {n : ℕ} : even n ↔ n % 2 = 0 :=
 ⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩
 
+theorem odd_iff {n : ℕ} : odd n ↔ n % 2 = 1 :=
+⟨λ ⟨m, hm⟩, by { rw [hm, add_mod], norm_num },
+ λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by { rw h, abel })⟩⟩
+
 lemma not_even_iff {n : ℕ} : ¬ even n ↔ n % 2 = 1 :=
 by rw [even_iff, mod_two_ne_zero]
 
-/-- A natural number `n` is `odd` if it is not even.  The mathlib API
-for parity is developed in terms of `even`; to avoid duplication,
-results should not be stated in terms of `odd`.  The purpose of this
-definition is for code outside mathlib that wishes to have a formal
-statement that is as literal a translation as possible of the
-corresponding informal statement, where that informal statement refers
-to odd numbers. -/
-def odd (n : ℕ) : Prop := ¬ even n
-
-@[simp] lemma odd_def (n : ℕ) : odd n ↔ ¬ even n := iff.rfl
+@[simp] lemma odd_iff_not_even {n : ℕ} : odd n ↔ ¬ even n :=
+by rw [not_even_iff, odd_iff]
 
-instance : decidable_pred even :=
+instance : decidable_pred (even : ℕ → Prop) :=
 λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm
 
-instance decidable_pred_odd : decidable_pred odd :=
-λ n, decidable_of_decidable_of_iff (by apply_instance) not_even_iff.symm
+instance decidable_pred_odd : decidable_pred (odd : ℕ → Prop) :=
+λ n, decidable_of_decidable_of_iff (by apply_instance) odd_iff_not_even.symm
 
 mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`"
 
@@ -48,10 +41,10 @@ mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`"
 @[simp] theorem not_even_one : ¬ even 1 :=
 by rw even_iff; apply one_ne_zero
 
-@[simp] theorem even_bit0 (n : nat) : even (bit0 n) :=
+@[simp] theorem even_bit0 (n : ℕ) : even (bit0 n) :=
 ⟨n, by rw [bit0, two_mul]⟩
 
-@[parity_simps] theorem even_add {m n : nat} : even (m + n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_add {m n : ℕ} : even (m + n) ↔ (even m ↔ even n) :=
 begin
   cases mod_two_eq_zero_or_one m with h₁ h₁; cases mod_two_eq_zero_or_one n with h₂ h₂;
     simp [even_iff, h₁, h₂],
@@ -61,10 +54,10 @@ begin
   exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂
 end
 
-theorem even.add {m n : ℕ} (hm : m.even) (hn : n.even) : (m + n).even :=
+theorem even.add {m n : ℕ} (hm : even m) (hn : even n) : even (m + n) :=
 even_add.2 $ by simp only [*]
 
-@[simp] theorem not_even_bit1 (n : nat) : ¬ even (bit1 n) :=
+@[simp] theorem not_even_bit1 (n : ℕ) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps
 
 lemma two_not_dvd_two_mul_add_one (a : ℕ) : ¬(2 ∣ 2 * a + 1) :=
@@ -76,21 +69,21 @@ end
 lemma two_not_dvd_two_mul_sub_one : Π {a : ℕ} (w : 0 < a), ¬(2 ∣ 2 * a - 1)
 | (a+1) _ := two_not_dvd_two_mul_add_one a
 
-@[parity_simps] theorem even_sub {m n : nat} (h : n ≤ m) : even (m - n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_sub {m n : ℕ} (h : n ≤ m) : even (m - n) ↔ (even m ↔ even n) :=
 begin
   conv { to_rhs, rw [←nat.sub_add_cancel h, even_add] },
   by_cases h : even n; simp [h]
 end
 
-theorem even.sub {m n : ℕ} (hm : m.even) (hn : n.even) : (m - n).even :=
+theorem even.sub {m n : ℕ} (hm : even m) (hn : even n) : even (m - n) :=
 (le_total n m).elim
   (λ h, by simp only [even_sub h, *])
   (λ h, by simp only [sub_eq_zero_of_le h, even_zero])
 
-@[parity_simps] theorem even_succ {n : nat} : even (succ n) ↔ ¬ even n :=
+@[parity_simps] theorem even_succ {n : ℕ} : even (succ n) ↔ ¬ even n :=
 by rw [succ_eq_add_one, even_add]; simp [not_even_one]
 
-@[parity_simps] theorem even_mul {m n : nat} : even (m * n) ↔ even m ∨ even n :=
+@[parity_simps] theorem even_mul {m n : ℕ} : even (m * n) ↔ even m ∨ even n :=
 begin
   cases mod_two_eq_zero_or_one m with h₁ h₁; cases mod_two_eq_zero_or_one n with h₂ h₂;
     simp [even_iff, h₁, h₂],
@@ -100,13 +93,13 @@ begin
   exact @modeq.modeq_mul _ _ 1 _ 1 h₁ h₂
 end
 
-/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even 
+/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
 if and only if `m` is even and `n` is positive. -/
-@[parity_simps] theorem even_pow {m n : nat} : even (m^n) ↔ even m ∧ n ≠ 0 :=
+@[parity_simps] theorem even_pow {m n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 :=
 by { induction n with n ih; simp [*, pow_succ', even_mul], tauto }
 
 lemma even_div {a b : ℕ} : even (a / b) ↔ a % (2 * b) / b = 0 :=
-by rw [even, dvd_iff_mod_eq_zero, nat.div_mod_eq_mod_mul_div, mul_comm]
+by rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, nat.div_mod_eq_mod_mul_div, mul_comm]
 
 theorem neg_one_pow_eq_one_iff_even {α : Type*} [ring α] {n : ℕ} (h1 : (-1 : α) ≠ 1):
   (-1 : α) ^ n = 1 ↔ even n :=
@@ -116,7 +109,7 @@ theorem neg_one_pow_eq_one_iff_even {α : Type*} [ring α] {n : ℕ} (h1 : (-1 :
 
 -- Here are examples of how `parity_simps` can be used with `nat`.
 
-example (m n : nat) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=
+example (m n : ℕ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=
 by simp [*, (dec_trivial : ¬ 2 = 0)] with parity_simps
 
 example : ¬ even 25394535 :=

src/number_theory/sum_four_squares.lean

@@ -25,9 +25,9 @@ namespace int
 
 lemma sum_two_squares_of_two_mul_sum_two_squares {m x y : ℤ} (h : 2 * m =  x^2 + y^2) :
   m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 :=
-have (x^2 + y^2).even, by simp [h.symm, even_mul],
-have hxaddy : (x + y).even, by simpa [pow_two] with parity_simps,
-have hxsuby : (x - y).even, by simpa [pow_two] with parity_simps,
+have even (x^2 + y^2), by simp [h.symm, even_mul],
+have hxaddy : even (x + y), by simpa [pow_two] with parity_simps,
+have hxsuby : even (x - y), by simpa [pow_two] with parity_simps,
 have (x^2 + y^2) % 2 = 0, by simp [h.symm],
 (mul_right_inj' (show (2*2 : ℤ) ≠ 0, from dec_trivial)).1 $
 calc 2 * 2 * m = (x - y)^2 + (x + y)^2 : by rw [mul_assoc, h]; ring