chore(*/parity): Generalize lemmas and clarify names (#13268)

Generalizations

src/algebra/geom_sum.lean

@@ -148,8 +148,8 @@ begin
   { simp },
   { simp only [geom_sum_succ', nat.even_succ, hk],
     split_ifs,
-    { rw [nat.neg_one_pow_of_even h, add_zero] },
-    { rw [nat.neg_one_pow_of_odd (nat.odd_iff_not_even.mpr h), neg_add_self] } }
+    { rw [h.neg_one_pow, add_zero] },
+    { rw [(nat.odd_iff_not_even.2 h).neg_one_pow, neg_add_self] } }
 end
 
 theorem geom_sum₂_self {α : Type*} [comm_ring α] (x : α) (n : ℕ) :

src/algebra/group_power/basic.lean

@@ -385,10 +385,11 @@ by rw [pow_bit0', neg_mul_neg, pow_bit0']
 @[simp] theorem neg_pow_bit1 (a : R) (n : ℕ) : (- a) ^ (bit1 n) = - a ^ (bit1 n) :=
 by simp only [bit1, pow_succ, neg_pow_bit0, neg_mul_eq_neg_mul]
 
-@[simp] lemma neg_sq (a : R) : (-a)^2 = a^2 :=
-by simp [sq]
+@[simp] lemma neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
+@[simp] lemma neg_one_sq : (-1 : R) ^ 2 = 1 := by rw [neg_sq, one_pow]
 
 alias neg_sq ← neg_pow_two
+alias neg_one_sq ← neg_one_pow_two
 
 end has_distrib_neg
 

src/algebra/order/sub.lean

@@ -468,6 +468,10 @@ protected lemma tsub_tsub_assoc (hbc : add_le_cancellable (b - c)) (h₁ : b ≤
 by rw [hbc.tsub_eq_iff_eq_add_of_le (tsub_le_self.trans h₁), add_assoc,
   add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]
 
+protected lemma tsub_add_tsub_comm (hb : add_le_cancellable b) (hd : add_le_cancellable d)
+  (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d) :=
+by rw [hb.tsub_add_eq_add_tsub hba, ←hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]
+
 protected lemma le_tsub_iff_left (ha : add_le_cancellable a) (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c :=
 ⟨add_le_of_le_tsub_left_of_le h, ha.le_tsub_of_add_le_left⟩
 
@@ -589,6 +593,9 @@ contravariant.add_le_cancellable.tsub_add_eq_add_tsub h
 lemma tsub_tsub_assoc (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c :=
 contravariant.add_le_cancellable.tsub_tsub_assoc h₁ h₂
 
+lemma tsub_add_tsub_comm (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d) :=
+contravariant.add_le_cancellable.tsub_add_tsub_comm contravariant.add_le_cancellable hba hdc
+
 lemma le_tsub_iff_left (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c :=
 contravariant.add_le_cancellable.le_tsub_iff_left h
 

src/algebra/parity.lean

@@ -35,7 +35,7 @@ Odd elements are not unified with a multiplicative notion.
  -/
 
 open mul_opposite
-variables {α β : Type*}
+variables {F α β R : Type*}
 
 /--  An element `a` of a type `α` with multiplication satisfies `square a` if `a = r * r`,
 for some `r : α`. -/
@@ -61,20 +61,28 @@ attribute [to_additive even_of_exists_two_nsmul] is_square_of_exists_sq
 /-- Alias of the backwards direction of `even_iff_exists_two_nsmul`. -/
 add_decl_doc even_of_exists_two_nsmul
 
-@[simp, to_additive even_two_nsmul]
-lemma is_square_sq [monoid α] (a : α) : is_square (a ^ 2) := ⟨a, pow_two _⟩
-
 @[simp, to_additive]
 lemma is_square_one [mul_one_class α] : is_square (1 : α) := ⟨1, (mul_one _).symm⟩
 
 @[to_additive]
-lemma is_square.map {F : Type*} [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β]
-  {m : α} (f : F) (hm : is_square m) :
-  is_square (f m) :=
-begin
-  rcases hm with ⟨m, rfl⟩,
-  exact ⟨f m, by simp⟩
-end
+lemma is_square.map [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] {m : α} (f : F) :
+  is_square m → is_square (f m) :=
+by { rintro ⟨m, rfl⟩, exact ⟨f m, by simp⟩ }
+
+section monoid
+variables [monoid α]
+
+@[simp, to_additive even_two_nsmul]
+lemma is_square_sq (a : α) : is_square (a ^ 2) := ⟨a, pow_two _⟩
+
+variables [has_distrib_neg α] {n : ℕ}
+
+lemma even.neg_pow : even n → ∀ a : α, (-a) ^ n = a ^ n :=
+by { rintro ⟨c, rfl⟩ a, simp_rw [←two_mul, pow_mul, neg_sq] }
+
+lemma even.neg_one_pow (h : even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one_pow]
+
+end monoid
 
 @[to_additive]
 lemma is_square.mul_is_square [comm_monoid α] {m n : α} (hm : is_square m) (hn : is_square n) :
@@ -111,6 +119,22 @@ by { rw div_eq_mul_inv,  exact hm.mul_is_square ((is_square_inv n).mpr hn) }
 
 end comm_group
 
+-- `odd.tsub_odd` requires `canonically_linear_ordered_semiring`, which we don't have
+lemma  even.tsub_even [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α]
+  [contravariant_class α α (+) (≤)] {m n : α} (hm : even m) (hn : even n) : even (m - n) :=
+begin
+  obtain ⟨a, rfl⟩ := hm,
+  obtain ⟨b, rfl⟩ := hn,
+  refine ⟨a - b, _⟩,
+  obtain h | h := le_total a b,
+  { rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero] },
+  { exact (tsub_add_tsub_comm h h).symm }
+end
+
+lemma even_iff_exists_bit0 [has_add α] {a : α} : even a ↔ ∃ b, a = bit0 b := iff.rfl
+
+alias even_iff_exists_bit0 ↔ even.exists_bit0 _
+
 section semiring
 variables [semiring α] [semiring β] {m n : α}
 
@@ -145,8 +169,12 @@ section with_odd
 /-- 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
 
-@[simp] lemma odd_bit1 (a : α) : odd (bit1 a) :=
-⟨a, by rw [bit1, bit0, two_mul]⟩
+lemma odd_iff_exists_bit1 {a : α} : odd a ↔ ∃ b, a = bit1 b :=
+exists_congr $ λ b, by { rw two_mul, refl }
+
+alias odd_iff_exists_bit1 ↔ odd.exists_bit1 _
+
+@[simp] lemma odd_bit1 (a : α) : odd (bit1 a) := odd_iff_exists_bit1.2 ⟨a, rfl⟩
 
 @[simp] lemma range_two_mul_add_one (α : Type*) [semiring α] :
   set.range (λ x : α, 2 * x + 1) = {a | odd a} :=
@@ -197,11 +225,19 @@ lemma odd.pow (hm : odd m) : ∀ {a : ℕ}, odd (m ^ a)
 | (a + 1) := by { rw pow_succ, exact hm.mul_odd odd.pow }
 
 end with_odd
-
 end semiring
 
+section monoid
+variables [monoid α] [has_distrib_neg α] {a : α} {n : ℕ}
+
+lemma odd.neg_pow : odd n → ∀ a : α, (-a) ^ n = - a ^ n :=
+by { rintro ⟨c, rfl⟩ a, simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg] }
+lemma odd.neg_one_pow (h : odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_pow, one_pow]
+
+end monoid
+
 section ring
-variables [ring α] {m n : α}
+variables [ring α] {a b : α} {n : ℕ}
 
 @[simp] lemma even_neg_two : even (- 2 : α) := by simp only [even_neg, even_two]
 
@@ -211,7 +247,7 @@ begin
   exact even_neg a,
 end
 
-lemma odd.neg {a : α} (hp : odd a) : odd (-a) :=
+lemma odd.neg (hp : odd a) : odd (-a) :=
 begin
   obtain ⟨k, hk⟩ := hp,
   use -(k + 1),
@@ -224,23 +260,22 @@ end
 
 @[simp] lemma odd_neg_one : odd (- 1 : α) := by simp
 
-theorem odd.sub_even (hm : odd m) (hn : even n) : odd (m - n) :=
-by { rw sub_eq_add_neg, exact hm.add_even ((even_neg n).mpr hn) }
+lemma odd.sub_even (ha : odd a) (hb : even b) : odd (a - b) :=
+by { rw sub_eq_add_neg, exact ha.add_even ((even_neg _).mpr hb) }
 
-theorem even.sub_odd (hm : even m) (hn : odd n) : odd (m - n) :=
-by { rw sub_eq_add_neg, exact hm.add_odd ((odd_neg n).mpr hn) }
+lemma even.sub_odd (ha : even a) (hb : odd b) : odd (a - b) :=
+by { rw sub_eq_add_neg, exact ha.add_odd ((odd_neg _).mpr hb) }
 
-lemma odd.sub_odd (hm : odd m) (hn : odd n) : even (m - n) :=
-by { rw sub_eq_add_neg, exact hm.add_odd ((odd_neg n).mpr hn) }
+lemma odd.sub_odd (ha : odd a) (hb : odd b) : even (a - b) :=
+by { rw sub_eq_add_neg, exact ha.add_odd ((odd_neg _).mpr hb) }
 
 lemma odd_abs [linear_order α] {a : α} : odd (abs a) ↔ odd a :=
 by { cases abs_choice a with h h; simp only [h, odd_neg] }
 
 end ring
 
 section powers
-variables {R : Type*}
-  {a : R} {n : ℕ} [linear_ordered_ring R]
+variables [linear_ordered_ring R] {a : R} {n : ℕ}
 
 lemma even.pow_nonneg (hn : even n) (a : R) : 0 ≤ a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using pow_bit0_nonneg a k
@@ -290,27 +325,33 @@ lemma fintype.card_fin_even {k : ℕ} : fact (even (fintype.card (fin (bit0 k)))
 section field_power
 variable {K : Type*}
 
-lemma even.zpow_neg [division_ring K] {n : ℤ} (h : even n) (a : K) :
-  (-a) ^ n = a ^ n :=
-begin
-  obtain ⟨k, rfl⟩ := h,
-  rw [← two_mul, ←bit0_eq_two_mul, zpow_bit0_neg],
-end
+section division_ring
+variables [division_ring K] {n : ℤ}
+
+lemma even.neg_zpow (h : even n) (a : K) : (-a) ^ n = a ^ n :=
+by { obtain ⟨k, rfl⟩ := h, exact zpow_bit0_neg _ _ }
+
+lemma odd.neg_zpow (h : odd n) (a : K) : (-a) ^ n = - a ^ n :=
+by { obtain ⟨k, rfl⟩ := h.exists_bit1, exact zpow_bit1_neg _ _ }
+
+lemma even.neg_one_zpow (h : even n) : (-1 : K) ^ n = 1 := by rw [h.neg_zpow, one_zpow₀]
+lemma odd.neg_one_zpow (h : odd n) : (-1 : K) ^ n = -1 := by rw [h.neg_zpow, one_zpow₀]
+
+end division_ring
 
 variables [linear_ordered_field K] {n : ℤ} {a : K}
 
-lemma even.zpow_nonneg (hn : even n) (a : K) :
-  0 ≤ a ^ n :=
+protected lemma even.zpow_nonneg (hn : even n) (a : K) : 0 ≤ a ^ n :=
 begin
   cases le_or_lt 0 a with h h,
   { exact zpow_nonneg h _ },
-  { exact (hn.zpow_neg a).subst (zpow_nonneg (neg_nonneg_of_nonpos h.le) _) }
+  { exact (hn.neg_zpow a).subst (zpow_nonneg (neg_nonneg_of_nonpos h.le) _) }
 end
 
 theorem even.zpow_pos (hn : even n) (ha : a ≠ 0) : 0 < a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit0_pos ha k
 
-theorem odd.zpow_nonneg (hn : odd n) (ha : 0 ≤ a) : 0 ≤ a ^ n :=
+protected lemma odd.zpow_nonneg (hn : odd n) (ha : 0 ≤ a) : 0 ≤ a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit1_nonneg_iff.mpr ha
 
 theorem odd.zpow_pos (hn : odd n) (ha : 0 < a) : 0 < a ^ n :=
@@ -325,7 +366,7 @@ by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit1_neg_iff.mpr ha
 lemma even.zpow_abs {p : ℤ} (hp : even p) (a : K) : |a| ^ p = a ^ p :=
 begin
   cases abs_choice a with h h;
-  simp only [h, hp.zpow_neg _],
+  simp only [h, hp.neg_zpow _],
 end
 
 @[simp] lemma zpow_bit0_abs (a : K) (p : ℤ) : |a| ^ bit0 p = a ^ bit0 p :=

src/analysis/convex/specific_functions.lean

@@ -53,7 +53,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_even hn (even_bit0 1)).exists_two_nsmul _ with ⟨k, hk⟩,
+    obtain ⟨k, hk⟩ := (hn.tsub_even $ even_bit0 _).exists_two_nsmul _,
     rw [iter_deriv_pow, finset.prod_range_cast_nat_sub, hk, nsmul_eq_mul, pow_mul'],
     exact mul_nonneg (nat.cast_nonneg _) (pow_two_nonneg _) }
 end

src/data/int/parity.lean

@@ -75,11 +75,8 @@ end
 @[simp] theorem two_dvd_ne_zero : ¬ 2 ∣ n ↔ n % 2 = 1 :=
 even_iff_two_dvd.symm.not.trans not_even_iff
 
-instance : decidable_pred (even : ℤ → Prop) :=
-λ n, decidable_of_decidable_of_iff (by apply_instance) 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
+instance : decidable_pred (even : ℤ → Prop) := λ n, decidable_of_iff _ even_iff.symm
+instance : decidable_pred (odd : ℤ → Prop) := λ n, decidable_of_iff _ odd_iff_not_even.symm
 
 @[simp] theorem not_even_one : ¬ even (1 : ℤ) :=
 by rw even_iff; norm_num
@@ -163,6 +160,11 @@ by simp [even_iff_two_dvd, dvd_nat_abs, coe_nat_dvd_left.symm]
 @[simp] theorem nat_abs_odd : odd n.nat_abs ↔ odd n :=
 by rw [odd_iff_not_even, nat.odd_iff_not_even, nat_abs_even]
 
+alias nat_abs_even ↔ _ even.nat_abs
+alias nat_abs_odd ↔ _ odd.nat_abs
+
+attribute [protected] even.nat_abs odd.nat_abs
+
 lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : odd a) (hb : odd b) : 4 ∣ a + b ∨ 4 ∣ a - b :=
 begin
   obtain ⟨m, rfl⟩ := ha,

src/data/nat/digits.lean

@@ -602,7 +602,7 @@ begin
   replace h : even dig.length := by rwa list.length_map,
   refine eleven_dvd_iff.2 ⟨0, (_ : dig.alternating_sum = 0)⟩,
   have := dig.alternating_sum_reverse,
-  rw [(p.map _).reverse_eq, pow_succ, neg_one_pow_of_even h, mul_one, neg_one_zsmul] at this,
+  rw [(p.map _).reverse_eq, pow_succ, h.neg_one_pow, mul_one, neg_one_zsmul] at this,
   exact eq_zero_of_neg_eq this.symm,
 end
 

src/data/nat/parity.lean

@@ -78,11 +78,8 @@ by { obtain ⟨k, rfl⟩ := h, exact succ_pos' }
 @[simp] theorem two_dvd_ne_zero : ¬ 2 ∣ n ↔ n % 2 = 1 :=
 even_iff_two_dvd.symm.not.trans not_even_iff
 
-instance : decidable_pred (even : ℕ → Prop) :=
-λ n, decidable_of_decidable_of_iff (by apply_instance) 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
+instance : decidable_pred (even : ℕ → Prop) := λ n, decidable_of_iff _ even_iff.symm
+instance : decidable_pred (odd : ℕ → Prop) := λ n, decidable_of_iff _ odd_iff_not_even.symm
 
 mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`"
 
@@ -113,11 +110,6 @@ begin
   by_cases h : even n; simp [h]
 end
 
-theorem even.sub_even (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 [tsub_eq_zero_iff_le.mpr h, even_zero])
-
 theorem even_sub' (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]
 
@@ -194,20 +186,6 @@ 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)
 
-section distrib_neg_monoid
-
-variables {R : Type*} [monoid R] [has_distrib_neg R]
-
-@[simp] theorem neg_one_sq : (-1 : R) ^ 2 = 1 := by simp
-
-alias nat.neg_one_sq ← nat.neg_one_pow_two
-
-theorem neg_one_pow_of_even : even n → (-1 : R) ^ n = 1 :=
-by { rintro ⟨c, rfl⟩, simp [← two_mul, pow_mul] }
-
-theorem neg_one_pow_of_odd : odd n → (-1 : R) ^ n = -1 :=
-by { rintro ⟨c, rfl⟩, simp [pow_add, pow_mul] }
-
 lemma two_mul_div_two_of_even : even n → 2 * (n / 2) = n :=
  λ h, nat.mul_div_cancel_left' (even_iff_two_dvd.mp h)
 
@@ -223,15 +201,6 @@ 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) :=
@@ -241,3 +210,11 @@ example : ¬ even 25394535 :=
 by simp
 
 end nat
+
+open nat
+
+variables {R : Type*} [monoid R] [has_distrib_neg R] {n : ℕ}
+
+lemma neg_one_pow_eq_one_iff_even (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ even n :=
+⟨λ h', of_not_not $ λ hn, h $ (odd.neg_one_pow $ odd_iff_not_even.mpr hn).symm.trans h',
+  even.neg_one_pow⟩

src/group_theory/specific_groups/alternating.lean

@@ -64,7 +64,7 @@ lemma prod_list_swap_mem_alternating_group_iff_even_length {l : list (perm α)}
   l.prod ∈ alternating_group α ↔ even l.length :=
 begin
   rw [mem_alternating_group, sign_prod_list_swap hl, ← units.coe_eq_one, units.coe_pow,
-    units.coe_neg_one, nat.neg_one_pow_eq_one_iff_even],
+    units.coe_neg_one, neg_one_pow_eq_one_iff_even],
   dec_trivial
 end
 
@@ -267,7 +267,7 @@ begin
   norm_num at ha,
   rw [pow_add, pow_mul, int.units_pow_two,one_mul,
       units.ext_iff, units.coe_one, units.coe_pow, units.coe_neg_one,
-      nat.neg_one_pow_eq_one_iff_even _] at ha,
+      neg_one_pow_eq_one_iff_even _] at ha,
   swap, { dec_trivial },
   rw [is_conj_iff_cycle_type_eq, h2],
   interval_cases multiset.card g.cycle_type,

src/linear_algebra/general_linear_group.lean

@@ -151,7 +151,7 @@ each element. -/
 instance : has_neg (GL_pos n R) :=
 ⟨λ g, ⟨-g, begin
     rw [mem_GL_pos, general_linear_group.coe_det_apply, units.coe_neg, det_neg,
-      nat.neg_one_pow_of_even (fact.out (even (fintype.card n))), one_mul],
+      (fact.out $ even $ fintype.card n).neg_one_pow, one_mul],
     exact g.prop,
   end⟩⟩