feat(data/nat/parity): addition/subtraction of even/odd nats (#5934)

 Added various theorems pertaining to the addition and subtraction of even and odd natural numbers.

Author: benjamindavidson

src/analysis/convex/specific_functions.lean

@@ -35,7 +35,7 @@ begin
   apply convex_on_univ_of_deriv2_nonneg differentiable_pow,
   { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] },
   { intro x,
-    rcases nat.even.sub hn (nat.even_bit0 1) with ⟨k, hk⟩,
+    rcases nat.even.sub_even 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 _) }

src/data/nat/parity.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad
+Authors: Jeremy Avigad, Benjamin Davidson
 
 The `even` and `odd` predicates on the natural numbers.
 -/
@@ -19,8 +19,8 @@ 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 })⟩⟩
+⟨λ ⟨m, hm⟩, by norm_num [hm, add_mod],
+ λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by rw [h, add_comm])⟩⟩
 
 lemma not_even_iff {n : ℕ} : ¬ even n ↔ n % 2 = 1 :=
 by rw [even_iff, mod_two_ne_zero]
@@ -86,32 +86,46 @@ begin
   exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂
 end
 
-theorem even.add {m n : ℕ} (hm : even m) (hn : even n) : even (m + n) :=
+theorem even.add_even {m n : ℕ} (hm : even m) (hn : even n) : even (m + n) :=
 even_add.2 $ by simp only [*]
 
+theorem even_add' {m n : ℕ} : even (m + n) ↔ (odd m ↔ odd n) :=
+by rw [even_add, even_iff_not_odd, even_iff_not_odd, not_iff_not]
+
+theorem odd.add_odd {m n : ℕ} (hm : odd m) (hn : odd n) : even (m + n) :=
+even_add'.2 $ by simp only [*]
+
 @[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) :=
+lemma two_not_dvd_two_mul_add_one (n : ℕ) : ¬(2 ∣ 2 * n + 1) :=
 begin
-  convert not_even_bit1 a,
-  exact two_mul a,
+  convert not_even_bit1 n,
+  exact two_mul n,
 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
+lemma two_not_dvd_two_mul_sub_one : Π {n : ℕ} (w : 0 < n), ¬(2 ∣ 2 * n - 1) | (n + 1) _ :=
+two_not_dvd_two_mul_add_one 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 : even m) (hn : even n) : even (m - n) :=
+theorem even.sub_even {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])
 
+theorem even_sub' {m n : ℕ} (h : n ≤ m) : even (m - n) ↔ (odd m ↔ odd n) :=
+by rw [even_sub h, even_iff_not_odd, even_iff_not_odd, not_iff_not]
+
+theorem odd.sub_odd {m n : ℕ} (hm : odd m) (hn : odd 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 : ℕ} : even (succ n) ↔ ¬ even n :=
 by rw [succ_eq_add_one, even_add]; simp [not_even_one]
 
@@ -130,10 +144,47 @@ if and only if `m` is even and `n` is positive. -/
 @[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 :=
+lemma even_div {m n : ℕ} : even (m / n) ↔ m % (2 * n) / n = 0 :=
 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):
+@[parity_simps] theorem odd_add {m n : ℕ} : odd (m + n) ↔ (odd m ↔ even n) :=
+begin
+  by_contra hnot,
+  rw [not_iff, ← even_iff_not_odd, even_add, odd_iff_not_even, ← not_iff] at hnot,
+  exact (iff_not_self _).mp hnot,
+end
+
+theorem odd.add_even {m n : ℕ} (hm : odd m) (hn : even n) : odd (m + n) :=
+odd_add.2 $ by simp only [*]
+
+theorem odd_add' {m n : ℕ} : odd (m + n) ↔ (odd n ↔ even m) :=
+by rw [add_comm, odd_add]
+
+theorem even.add_odd {m n : ℕ} (hm : even m) (hn : odd n) : odd (m + n) :=
+odd_add'.2 $ by simp only [*]
+
+@[parity_simps] theorem odd_sub {m n : ℕ} (h : n ≤ m) : odd (m - n) ↔ (odd m ↔ even n) :=
+begin
+  by_contra hnot,
+  rw [not_iff, ← even_iff_not_odd, even_sub h, odd_iff_not_even, ← not_iff] at hnot,
+  exact (iff_not_self _).mp hnot,
+end
+
+theorem odd.sub_even {m n : ℕ} (h : n ≤ m) (hm : odd m) (hn : even n) : odd (m - n) :=
+(odd_sub h).mpr (iff_of_true hm hn)
+
+theorem odd_sub' {m n : ℕ} (h : n ≤ m) : odd (m - n) ↔ (odd n ↔ even m) :=
+begin
+  by_contra hnot,
+  rw [not_iff, ← even_iff_not_odd, even_sub h, odd_iff_not_even, ← not_iff,
+      @iff.comm _ (even n)] at hnot,
+  exact (iff_not_self _).mp hnot,
+end
+
+theorem even.sub_odd {m n : ℕ} (h : n ≤ m) (hm : even m) (hn : odd n) : odd (m - n) :=
+(odd_sub' h).mpr (iff_of_true hn hm)
+
+theorem neg_one_pow_eq_one_iff_even {α : Type*} [ring α] {n : ℕ} (h1 : (-1 : α) ≠ 1) :
   (-1 : α) ^ n = 1 ↔ even n :=
 ⟨λ h, n.mod_two_eq_zero_or_one.elim (dvd_iff_mod_eq_zero _ _).2
   (λ hn, by rw [neg_one_pow_eq_pow_mod_two, hn, pow_one] at h; exact (h1 h).elim),