feat(data/int/parity): update to match nat/parity (where applicable) (#…

…7155)

We had a number of lemmas for `nat` but not for `int`, so I add them. I also globalize variables in the file and add a module docstring.

src/data/int/parity.lean

@@ -2,73 +2,83 @@
 Copyright (c) 2019 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Benjamin Davidson
-
-The `even` and `odd` predicates on the integers.
 -/
 import data.int.modeq
 import data.nat.parity
 
+/-!
+# Parity of integers
+
+This file contains theorems about the `even` and `odd` predicates on the integers.
+
+## Tags
+
+even, odd
+-/
+
 namespace int
 
-@[simp] theorem mod_two_ne_one {n : ℤ} : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
+variables {m n : ℤ}
+
+@[simp] theorem mod_two_ne_one : ¬ 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 : ℤ} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
+theorem mod_two_ne_zero : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-@[simp] theorem even_coe_nat (n : nat) : even (n : ℤ) ↔ even n :=
+@[simp] theorem even_coe_nat (n : ℕ) : 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 : ℤ} : even n ↔ n % 2 = 0 :=
+theorem even_iff : 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 :=
+theorem odd_iff : 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 :=
+lemma not_even_iff : ¬ even n ↔ n % 2 = 1 :=
 by rw [even_iff, mod_two_ne_zero]
 
-lemma not_odd_iff {n : ℤ} : ¬ odd n ↔ n % 2 = 0 :=
+lemma not_odd_iff : ¬ odd n ↔ n % 2 = 0 :=
 by rw [odd_iff, mod_two_ne_one]
 
-lemma even_iff_not_odd {n : ℤ} : even n ↔ ¬ odd n :=
+lemma even_iff_not_odd : even n ↔ ¬ odd n :=
 by rw [not_odd_iff, even_iff]
 
-@[simp] lemma odd_iff_not_even {n : ℤ} : odd n ↔ ¬ even n :=
+@[simp] lemma odd_iff_not_even : odd n ↔ ¬ even n :=
 by rw [not_even_iff, odd_iff]
 
+lemma is_compl_even_odd : is_compl {n : ℕ | even n} {n | odd n} :=
+by simp [← set.compl_set_of, is_compl_compl]
+
 lemma even_or_odd (n : ℤ) : even n ∨ odd n :=
-or.imp_right (odd_iff_not_even.2) (em (even n))
+or.imp_right odd_iff_not_even.2 $ em $ even n
 
 lemma even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 :=
 by simpa only [exists_or_distrib, ← odd, ← even] using even_or_odd n
 
 lemma even_xor_odd (n : ℤ) : xor (even n) (odd n) :=
 begin
-  cases (even_or_odd n) with h,
-  { exact or.inl ⟨h, (even_iff_not_odd.mp h)⟩ },
-  { exact or.inr ⟨h, (odd_iff_not_even.mp h)⟩ },
+  cases even_or_odd n with h,
+  { exact or.inl ⟨h, even_iff_not_odd.mp h⟩ },
+  { exact or.inr ⟨h, odd_iff_not_even.mp h⟩ },
 end
 
 lemma even_xor_odd' (n : ℤ) : ∃ k, xor (n = 2 * k) (n = 2 * k + 1) :=
 begin
-  rcases (even_or_odd n) with ⟨k, h⟩ | ⟨k, h⟩;
+  rcases even_or_odd n with ⟨k, rfl⟩ | ⟨k, rfl⟩;
   use k,
-  { simpa only [xor, h, true_and, eq_self_iff_true, not_true, or_false, and_false]
+  { simpa only [xor, true_and, eq_self_iff_true, not_true, or_false, and_false]
       using (succ_ne_self (2*k)).symm },
-  { simp only [xor, h, add_right_eq_self, false_or, eq_self_iff_true, not_true, not_false_iff,
+  { simp only [xor, add_right_eq_self, false_or, eq_self_iff_true, not_true, not_false_iff,
                one_ne_zero, and_self] },
 end
 
-lemma ne_of_odd_sum {x y : ℤ} (h : odd (x + y)) : x ≠ y :=
-by { rw odd_iff_not_even at h, intros contra, apply h, exact ⟨x, by rw [contra, two_mul]⟩, }
-
-@[simp] theorem two_dvd_ne_zero {n : ℤ} : ¬ 2 ∣ n ↔ n % 2 = 1 :=
+@[simp] theorem two_dvd_ne_zero : ¬ 2 ∣ n ↔ n % 2 = 1 :=
 not_even_iff
 
 instance : decidable_pred (even : ℤ → Prop) :=
@@ -85,7 +95,7 @@ by rw even_iff; apply one_ne_zero
 @[simp] theorem even_bit0 (n : ℤ) : even (bit0 n) :=
 ⟨n, by rw [bit0, two_mul]⟩
 
-@[parity_simps] theorem even_add {m n : ℤ} : even (m + n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_add : 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],
@@ -95,15 +105,40 @@ begin
   exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂
 end
 
-@[parity_simps] theorem even_neg {n : ℤ} : even (-n) ↔ even n := by simp [even_iff]
+theorem even.add_even (hm : even m) (hn : even n) : even (m + n) :=
+even_add.2 $ iff_of_true hm hn
+
+theorem even_add' : 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 (hm : odd m) (hn : odd n) : even (m + n) :=
+even_add'.2 $ iff_of_true hm hn
+
+@[parity_simps] theorem even_neg : even (-n) ↔ even n :=
+by simp [even_iff]
 
 @[simp] theorem not_even_bit1 (n : ℤ) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps
 
-@[parity_simps] theorem even_sub {m n : ℤ} : even (m - n) ↔ (even m ↔ even n) :=
+lemma two_not_dvd_two_mul_add_one (n : ℤ) : ¬(2 ∣ 2 * n + 1) :=
+by convert not_even_bit1 n; exact two_mul n
+
+@[parity_simps] theorem even_sub : even (m - n) ↔ (even m ↔ even n) :=
 by simp [sub_eq_add_neg] with parity_simps
 
-@[parity_simps] theorem even_mul {m n : ℤ} : even (m * n) ↔ even m ∨ even n :=
+theorem even.sub_even (hm : even m) (hn : even n) : even (m - n) :=
+even_sub.2 $ iff_of_true hm hn
+
+theorem even_sub' : even (m - n) ↔ (odd m ↔ odd n) :=
+by rw [even_sub, even_iff_not_odd, even_iff_not_odd, not_iff_not]
+
+theorem odd.sub_odd (hm : odd m) (hn : odd n) : even (m - n) :=
+even_sub'.2 $ iff_of_true hm hn
+
+@[parity_simps] theorem even_add_one : even (n + 1) ↔ ¬ even n :=
+by simp [even_add]
+
+@[parity_simps] theorem even_mul : 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],
@@ -113,9 +148,54 @@ begin
   exact @modeq.modeq_mul _ _ 1 _ 1 h₁ h₂
 end
 
-@[parity_simps] theorem even_pow {m : ℤ} {n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 :=
+theorem odd_mul : odd (m * n) ↔ odd m ∧ odd n :=
+by simp [not_or_distrib] with parity_simps
+
+theorem even.mul_left (hm : even m) (n : ℤ) : even (m * n) :=
+even_mul.mpr $ or.inl hm
+
+theorem even.mul_right (m : ℤ) (hn : even n) : even (m * n) :=
+even_mul.mpr $ or.inr hn
+
+theorem odd.mul (hm : odd m) (hn : odd n) : odd (m * n) :=
+odd_mul.mpr ⟨hm, hn⟩
+
+theorem odd.of_mul_left (h : odd (m * n)) : odd m :=
+(odd_mul.mp h).1
+
+theorem odd.of_mul_right (h : odd (m * n)) : odd n :=
+(odd_mul.mp h).2
+
+@[parity_simps] theorem even_pow {n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 :=
 by { induction n with n ih; simp [*, even_mul, pow_succ], tauto }
 
+@[parity_simps] theorem odd_add : odd (m + n) ↔ (odd m ↔ even n) :=
+by rw [odd_iff_not_even, even_add, not_iff, odd_iff_not_even]
+
+theorem odd.add_even (hm : odd m) (hn : even n) : odd (m + n) :=
+odd_add.2 $ iff_of_true hm hn
+
+theorem odd_add' : odd (m + n) ↔ (odd n ↔ even m) :=
+by rw [add_comm, odd_add]
+
+theorem even.add_odd (hm : even m) (hn : odd n) : odd (m + n) :=
+odd_add'.2 $ iff_of_true hn hm
+
+lemma ne_of_odd_sum (h : odd (m + n)) : m ≠ n :=
+λ hnot, by simpa [hnot] with parity_simps using h
+
+@[parity_simps] theorem odd_sub : odd (m - n) ↔ (odd m ↔ even n) :=
+by rw [odd_iff_not_even, even_sub, not_iff, odd_iff_not_even]
+
+theorem odd.sub_even (hm : odd m) (hn : even n) : odd (m - n) :=
+odd_sub.2 $ iff_of_true hm hn
+
+theorem odd_sub' : odd (m - n) ↔ (odd n ↔ even m) :=
+by rw [odd_iff_not_even, even_sub, not_iff, not_iff_comm, odd_iff_not_even]
+
+theorem even.sub_odd (hm : even m) (hn : odd n) : odd (m - n) :=
+odd_sub'.2 $ iff_of_true hn hm
+
 lemma even_mul_succ_self (n : ℤ) : even (n * (n + 1)) :=
 begin
   rw even_mul,