feat: port Data.Int.Parity (#1836)

Mathlib.lean

@@ -330,6 +330,7 @@ import Mathlib.Data.Int.NatPrime
 import Mathlib.Data.Int.Order.Basic
 import Mathlib.Data.Int.Order.Lemmas
 import Mathlib.Data.Int.Order.Units
+import Mathlib.Data.Int.Parity
 import Mathlib.Data.Int.Range
 import Mathlib.Data.Int.Sqrt
 import Mathlib.Data.Int.SuccPred

Mathlib/Data/Int/Parity.lean

@@ -0,0 +1,291 @@
+/-
+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
+
+! This file was ported from Lean 3 source module data.int.parity
+! leanprover-community/mathlib commit e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Nat.Parity
+import Mathlib.Tactic.Abel
+
+/-!
+# Parity of integers
+
+This file contains theorems about the `Even` and `Odd` predicates on the integers.
+
+## Tags
+
+even, odd
+-/
+
+namespace Int
+
+variable {m n : ℤ}
+
+@[simp]
+theorem emod_two_ne_one : ¬n % 2 = 1 ↔ n % 2 = 0 := by
+  cases' emod_two_eq_zero_or_one n with h h <;> simp [h]
+#align int.mod_two_ne_one Int.emod_two_ne_one
+
+-- Porting note: This comment from mathlib3 refers to a future file, revisit it once ported:
+-- euclidean_domain.mod_eq_zero uses (2 ∣ n) as normal form
+@[local simp]
+theorem emod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by
+  cases' emod_two_eq_zero_or_one n with h h <;> simp [h]
+#align int.mod_two_ne_zero Int.emod_two_ne_zero
+
+theorem even_iff : Even n ↔ n % 2 = 0 :=
+  ⟨fun ⟨m, hm⟩ => by simp [← two_mul, hm],
+    fun h => ⟨n / 2, (emod_add_ediv n 2).symm.trans (by simp [← two_mul, h])⟩⟩
+#align int.even_iff Int.even_iff
+
+theorem odd_iff : Odd n ↔ n % 2 = 1 :=
+  ⟨fun ⟨m, hm⟩ => (by rw [hm, add_emod]; norm_num),
+    fun h => ⟨n / 2, (emod_add_ediv n 2).symm.trans (by rw [h]; abel)⟩⟩
+#align int.odd_iff Int.odd_iff
+
+theorem not_even_iff : ¬Even n ↔ n % 2 = 1 := by rw [even_iff, emod_two_ne_zero]
+#align int.not_even_iff Int.not_even_iff
+
+theorem not_odd_iff : ¬Odd n ↔ n % 2 = 0 := by rw [odd_iff, emod_two_ne_one]
+#align int.not_odd_iff Int.not_odd_iff
+
+theorem even_iff_not_odd : Even n ↔ ¬Odd n := by rw [not_odd_iff, even_iff]
+#align int.even_iff_not_odd Int.even_iff_not_odd
+
+@[simp]
+theorem odd_iff_not_even : Odd n ↔ ¬Even n := by rw [not_even_iff, odd_iff]
+#align int.odd_iff_not_even Int.odd_iff_not_even
+
+theorem isCompl_even_odd : IsCompl { n : ℤ | Even n } { n | Odd n } := by
+  simp [← Set.compl_setOf, isCompl_compl]
+#align int.is_compl_even_odd Int.isCompl_even_odd
+
+theorem even_or_odd (n : ℤ) : Even n ∨ Odd n :=
+  Or.imp_right odd_iff_not_even.2 <| em <| Even n
+#align int.even_or_odd Int.even_or_odd
+
+-- Porting note: TODO. I'm struggling that `Even` uses `k + k` while Odd uses `2 * k`,
+-- does this proof need golfing?
+-- mathlib3 port: `simpa only [← two_mul, exists_or, ← Odd, ← Even] using even_or_odd n`
+theorem even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 := by
+  rw [exists_or]
+  convert even_or_odd n
+  funext i
+  rw [two_mul]
+#align int.even_or_odd' Int.even_or_odd'
+
+theorem even_xor'_odd (n : ℤ) : Xor' (Even n) (Odd n) := by
+  cases even_or_odd n with
+  | inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
+  | inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
+#align int.even_xor_odd Int.even_xor'_odd
+
+theorem even_xor'_odd' (n : ℤ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1) := by
+  rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;> use k
+  · simpa only [← two_mul, Xor', true_and_iff, eq_self_iff_true, not_true, or_false_iff,
+      and_false_iff] using (succ_ne_self (2 * k)).symm
+  · simp only [Xor', add_right_eq_self, false_or_iff, eq_self_iff_true, not_true, not_false_iff,
+      one_ne_zero, and_self_iff]
+#align int.even_xor_odd' Int.even_xor'_odd'
+
+@[simp]
+theorem two_dvd_ne_zero : ¬2 ∣ n ↔ n % 2 = 1 :=
+  even_iff_two_dvd.symm.not.trans not_even_iff
+#align int.two_dvd_ne_zero Int.two_dvd_ne_zero
+
+instance : DecidablePred (Even : ℤ → Prop) := fun _ => decidable_of_iff _ even_iff.symm
+
+instance : DecidablePred (Odd : ℤ → Prop) := fun _ => decidable_of_iff _ odd_iff_not_even.symm
+
+@[simp]
+theorem not_even_one : ¬Even (1 : ℤ) := by
+  rw [even_iff]
+  norm_num
+#align int.not_even_one Int.not_even_one
+
+@[parity_simps]
+theorem even_add : Even (m + n) ↔ (Even m ↔ Even n) := by
+  cases' emod_two_eq_zero_or_one m with h₁ h₁ <;>
+  cases' emod_two_eq_zero_or_one n with h₂ h₂ <;>
+  simp [even_iff, h₁, h₂, Int.add_emod]
+#align int.even_add Int.even_add
+
+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]
+#align int.even_add' Int.even_add'
+
+set_option linter.deprecated false in
+
+@[simp, deprecated]
+theorem not_even_bit1 (n : ℤ) : ¬Even (bit1 n) := by simp [bit1, parity_simps]
+#align int.not_even_bit1 Int.not_even_bit1
+
+theorem two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1 := by
+  simp [add_emod]
+#align int.two_not_dvd_two_mul_add_one Int.two_not_dvd_two_mul_add_one
+
+@[parity_simps]
+theorem even_sub : Even (m - n) ↔ (Even m ↔ Even n) := by
+  simp [sub_eq_add_neg, parity_simps]
+#align int.even_sub Int.even_sub
+
+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]
+#align int.even_sub' Int.even_sub'
+
+@[parity_simps]
+theorem even_add_one : Even (n + 1) ↔ ¬Even n := by
+  simp [even_add]
+#align int.even_add_one Int.even_add_one
+
+@[parity_simps]
+theorem even_mul : Even (m * n) ↔ Even m ∨ Even n := by
+  cases' emod_two_eq_zero_or_one m with h₁ h₁ <;>
+  cases' emod_two_eq_zero_or_one n with h₂ h₂ <;>
+  simp [even_iff, h₁, h₂, Int.mul_emod]
+#align int.even_mul Int.even_mul
+
+theorem odd_mul : Odd (m * n) ↔ Odd m ∧ Odd n := by simp [not_or, parity_simps]
+#align int.odd_mul Int.odd_mul
+
+theorem Odd.of_mul_left (h : Odd (m * n)) : Odd m :=
+  (odd_mul.mp h).1
+#align int.odd.of_mul_left Int.Odd.of_mul_left
+
+theorem Odd.of_mul_right (h : Odd (m * n)) : Odd n :=
+  (odd_mul.mp h).2
+#align int.odd.of_mul_right Int.Odd.of_mul_right
+
+@[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
+#align int.even_pow Int.even_pow
+
+theorem even_pow' {n : ℕ} (h : n ≠ 0) : Even (m ^ n) ↔ Even m :=
+  even_pow.trans <| and_iff_left h
+#align int.even_pow' Int.even_pow'
+
+@[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]
+#align int.odd_add Int.odd_add
+
+theorem odd_add' : Odd (m + n) ↔ (Odd n ↔ Even m) := by
+  rw [add_comm, odd_add]
+#align int.odd_add' Int.odd_add'
+
+theorem ne_of_odd_add (h : Odd (m + n)) : m ≠ n :=
+  fun hnot => by simp [hnot, parity_simps] at h
+#align int.ne_of_odd_add Int.ne_of_odd_add
+
+@[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]
+#align int.odd_sub Int.odd_sub
+
+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]
+#align int.odd_sub' Int.odd_sub'
+
+theorem even_mul_succ_self (n : ℤ) : Even (n * (n + 1)) := by
+  rw [even_mul]
+  convert n.even_or_odd
+  simp [parity_simps]
+#align int.even_mul_succ_self Int.even_mul_succ_self
+
+@[simp, norm_cast]
+theorem even_coe_nat (n : ℕ) : Even (n : ℤ) ↔ Even n := by
+  rw_mod_cast [even_iff, Nat.even_iff]
+#align int.even_coe_nat Int.even_coe_nat
+
+-- Porting note: was simp. simp can prove this.
+@[norm_cast]
+theorem odd_coe_nat (n : ℕ) : Odd (n : ℤ) ↔ Odd n := by
+  rw [odd_iff_not_even, Nat.odd_iff_not_even, even_coe_nat]
+#align int.odd_coe_nat Int.odd_coe_nat
+
+@[simp]
+theorem natAbs_even : Even n.natAbs ↔ Even n := by
+  simp [even_iff_two_dvd, dvd_natAbs, coe_nat_dvd_left.symm]
+#align int.nat_abs_even Int.natAbs_even
+
+-- Porting note: was simp. simp can prove this.
+--@[simp]
+theorem natAbs_odd : Odd n.natAbs ↔ Odd n := by
+  rw [odd_iff_not_even, Nat.odd_iff_not_even, natAbs_even]
+#align int.nat_abs_odd Int.natAbs_odd
+
+alias natAbs_even ↔ _ _root_.Even.natAbs
+#align even.nat_abs Even.natAbs
+
+alias natAbs_odd ↔ _ _root_.Odd.natAbs
+#align odd.nat_abs Odd.natAbs
+
+-- Porting note: "protected"-attribute not implemented yet.
+-- mathlib3 had:
+-- `attribute [protected] Even.natAbs Odd.natAbs`
+
+theorem four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
+    4 ∣ a + b ∨ 4 ∣ a - b := by
+  obtain ⟨m, rfl⟩ := ha
+  obtain ⟨n, rfl⟩ := hb
+  obtain h | h := Int.even_or_odd (m + n)
+  · right
+    rw [Int.even_add, ← Int.even_sub] at h
+    obtain ⟨k, hk⟩ := h
+    convert dvd_mul_right 4 k
+    rw [eq_add_of_sub_eq hk, mul_add, add_assoc, add_sub_cancel, ← two_mul, ← mul_assoc]
+    rfl
+  · left
+    obtain ⟨k, hk⟩ := h
+    convert dvd_mul_right 4 (k + 1)
+    rw [eq_sub_of_add_eq hk, add_right_comm, ← add_sub, mul_add, mul_sub, add_assoc, add_assoc,
+      sub_add, add_assoc, ← sub_sub (2 * n), sub_self, zero_sub, sub_neg_eq_add, ← mul_assoc,
+      mul_add]
+    rfl
+#align int.four_dvd_add_or_sub_of_odd Int.four_dvd_add_or_sub_of_odd
+
+theorem two_mul_ediv_two_of_even : Even n → 2 * (n / 2) = n :=
+  fun h => Int.mul_ediv_cancel' (even_iff_two_dvd.mp h)
+#align int.two_mul_div_two_of_even Int.two_mul_ediv_two_of_even
+
+theorem ediv_two_mul_two_of_even : Even n → n / 2 * 2 = n :=
+  fun h => Int.ediv_mul_cancel (even_iff_two_dvd.mp h)
+#align int.div_two_mul_two_of_even Int.ediv_two_mul_two_of_even
+
+theorem two_mul_ediv_two_add_one_of_odd : Odd n → 2 * (n / 2) + 1 = n := by
+  rintro ⟨c, rfl⟩
+  rw [mul_comm]
+  convert Int.ediv_add_emod' (2 * c + 1) 2
+  simp [Int.add_emod]
+#align int.two_mul_div_two_add_one_of_odd Int.two_mul_ediv_two_add_one_of_odd
+
+theorem ediv_two_mul_two_add_one_of_odd : Odd n → n / 2 * 2 + 1 = n := by
+  rintro ⟨c, rfl⟩
+  convert Int.ediv_add_emod' (2 * c + 1) 2
+  simp [Int.add_emod]
+#align int.div_two_mul_two_add_one_of_odd Int.ediv_two_mul_two_add_one_of_odd
+
+theorem add_one_ediv_two_mul_two_of_odd : Odd n → 1 + n / 2 * 2 = n := by
+  rintro ⟨c, rfl⟩
+  rw [add_comm]
+  convert Int.ediv_add_emod' (2 * c + 1) 2
+  simp [Int.add_emod]
+#align int.add_one_div_two_mul_two_of_odd Int.add_one_ediv_two_mul_two_of_odd
+
+theorem two_mul_ediv_two_of_odd (h : Odd n) : 2 * (n / 2) = n - 1 :=
+  eq_sub_of_add_eq (two_mul_ediv_two_add_one_of_odd h)
+#align int.two_mul_div_two_of_odd Int.two_mul_ediv_two_of_odd
+
+-- Here are examples of how `parity_simps` can be used with `int`.
+example (m n : ℤ) (h : Even m) : ¬Even (n + 3) ↔ Even (m ^ 2 + m + n) := by
+  simp [*, (by decide : ¬2 = 0), parity_simps]
+
+example : ¬Even (25394535 : ℤ) := by simp
+
+end Int