feat(algebra/parity): introduce is_square and, via to_additive, a…

…lso `even` (#13037)

This PR continues the refactor began in #12882.  Now that most of the the even/odd lemmas are in the same file, I changed the definition of `even` to become the `to_additive` version of `is_square`.

The reason for the large number of files touched is that the definition of `even` actually changed, from being of the form `2 * n` to being of the form `n + n`.  Thus, I inserted appropriate `two_mul`s and `even_iff_two_dvd`s in a few places where the defeq to the divisibility by 2 was exploited.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/even.2Fodd)

archive/100-theorems-list/45_partition.lean

@@ -412,6 +412,7 @@ begin
     rw nat.div_lt_iff_lt_mul _ _ zero_lt_two,
     exact lt_of_le_of_lt hin h },
   { rintro ⟨a, -, rfl⟩,
+    rw even_iff_two_dvd,
     apply nat.two_not_dvd_two_mul_add_one },
 end
 

archive/100-theorems-list/70_perfect_numbers.lean

@@ -84,6 +84,7 @@ begin
   have hpos := perf.2,
   rcases eq_two_pow_mul_odd hpos with ⟨k, m, rfl, hm⟩,
   use k,
+  rw even_iff_two_dvd at hm,
   rw [perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
     is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd hm).symm,
     sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf,
@@ -106,7 +107,7 @@ begin
       { apply hm,
         rw [← jcon2, pow_zero, one_mul, one_mul] at ev,
         rw [← jcon2, one_mul],
-        exact ev },
+        exact even_iff_two_dvd.mp ev },
       apply ne_of_lt _ jcon2,
       rw [mersenne, ← nat.pred_eq_sub_one, lt_pred_iff, ← pow_one (nat.succ 1)],
       apply pow_lt_pow (nat.lt_succ_self 1) (nat.succ_lt_succ (nat.succ_pos k)) },

archive/imo/imo2013_q1.lean

@@ -51,8 +51,9 @@ begin
   { intro n, use (λ_, 1), simp }, -- For the base case, any m works.
 
   intro n,
-  obtain ⟨t, ht : ↑n = 2 * t⟩ | ⟨t, ht : ↑n = 2 * t + 1⟩ := (n : ℕ).even_or_odd,
+  obtain ⟨t, ht : ↑n = t + t⟩ | ⟨t, ht : ↑n = 2 * t + 1⟩ := (n : ℕ).even_or_odd,
   { -- even case
+    rw ← two_mul at ht,
     cases t, -- Eliminate the zero case to simplify later calculations.
     { exfalso, rw mul_zero at ht, exact pnat.ne_zero n ht },
 

src/algebra/parity.lean

@@ -8,50 +8,133 @@ import algebra.ring.basic
 import algebra.algebra.basic
 import algebra.group_power.basic
 import algebra.field_power
+import algebra.opposites
 
-/-!  This file proves some general facts about even and odd elements of semirings. -/
+/-!  # Squares, even and odd elements
 
+This file proves some general facts about squares, even and odd elements of semirings.
+
+In the implementation, we define `is_square` and we let `even` be the notion transported by
+`to_additive`.  The definition are therefore as follows:
+```lean
+is_square a ↔ ∃ r, a = r * r
+even a ↔ ∃ r, a = r + r
+```
+
+Odd elements are not unified with a multiplicative notion.
+
+## Future work
+
+* TODO: Try to generalize further the typeclass assumptions on `is_square/even`.
+  For instance, in some cases, there are `semiring` assumptions that I (DT) am not convinced are
+  necessary.
+* TODO: Consider moving the definition and lemmas about `odd` to a separate file.
+* TODO: The "old" definition of `even a` asked for the existence of an element `c` such that
+  `a = 2 * c`.  For this reason, several fixes introduce an extra `two_mul` or `← two_mul`.
+  It might be the case that by making a careful choice of `simp` lemma, this can be avoided.
+ -/
+
+open mul_opposite
 variables {α β : Type*}
 
-section semiring
-variables [semiring α] [semiring β] {m n : α}
+/--  An element `a` of a type `α` with multiplication satisfies `square a` if `a = r * r`,
+for some `r : α`. -/
+@[to_additive
+"An element `a` of a type `α` with addition satisfies `even a` if `a = r + r`,
+for some `r : α`."]
+def is_square [has_mul α] (a : α) : Prop := ∃ r, a = r * r
+
+@[simp, to_additive]
+lemma is_square_mul_self [has_mul α] (m : α) : is_square (m * m) := ⟨m, rfl⟩
+
+@[to_additive even_iff_exists_two_nsmul]
+lemma is_square_iff_exists_sq [monoid α] (m : α) : is_square m ↔ ∃ c, m = c ^ 2 :=
+by simp [is_square, pow_two]
+
+alias is_square_iff_exists_sq ↔ is_square.exists_sq is_square_of_exists_sq
+
+attribute [to_additive even.exists_two_nsmul] is_square.exists_sq
+/-- Alias of the forwards direction of `even_iff_exists_two_nsmul`. -/
+add_decl_doc even.exists_two_nsmul
 
-/-- An element `a` of a semiring is even if there exists `k` such `a = 2*k`. -/
-def even (a : α) : Prop := ∃ k, a = 2*k
+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] lemma even_zero : even (0 : α) := ⟨0, (mul_zero _).symm⟩
+@[simp, to_additive even_two_nsmul]
+lemma is_square_sq [monoid α] (a : α) : is_square (a ^ 2) := ⟨a, pow_two _⟩
 
-lemma even_two_mul (m : α) : even (2 * m) := ⟨m, rfl⟩
+@[simp, to_additive]
+lemma is_square_one [mul_one_class α] : is_square (1 : α) := ⟨1, (mul_one _).symm⟩
 
-lemma add_monoid_hom.even (f : α →+ β) (hm : even m) : even (f m) :=
+@[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 [two_mul]⟩
+  exact ⟨f m, by simp⟩
+end
+
+@[to_additive]
+lemma is_square.mul_is_square [comm_monoid α] {m n : α} (hm : is_square m) (hn : is_square n) :
+  is_square (m * n) :=
+begin
+  rcases hm with ⟨m, rfl⟩,
+  rcases hn with ⟨n, rfl⟩,
+  refine ⟨m * n, mul_mul_mul_comm m m n n⟩,
+end
+
+section group
+variable [group α]
+
+@[to_additive]
+lemma is_square_op_iff (a : α) : is_square (op a) ↔ is_square a :=
+⟨λ ⟨c, hc⟩, ⟨unop c, by rw [← unop_mul, ← hc, unop_op]⟩, λ ⟨c, hc⟩, by simp [hc]⟩
+
+@[simp, to_additive] lemma is_square_inv (a : α) : is_square a⁻¹ ↔ is_square a :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { rw [← is_square_op_iff, ← inv_inv a],
+    exact h.map (mul_equiv.inv' α) },
+  { exact ((is_square_op_iff a).mpr h).map (mul_equiv.inv' α).symm }
 end
 
-lemma even_iff_two_dvd {a : α} : even a ↔ 2 ∣ a := iff.rfl
+end group
+
+section comm_group
+variable [comm_group α]
+
+@[to_additive]
+lemma is_square.div_is_square {m n : α} (hm : is_square m) (hn : is_square n) : is_square (m / n) :=
+by { rw div_eq_mul_inv,  exact hm.mul_is_square ((is_square_inv n).mpr hn) }
+
+end comm_group
+
+section semiring
+variables [semiring α] [semiring β] {m n : α}
+
+lemma even_iff_exists_two_mul (m : α) : even m ↔ ∃ c, m = 2 * c :=
+by simp [even_iff_exists_two_nsmul]
+
+lemma even_iff_two_dvd {a : α} : even a ↔ 2 ∣ a := by simp [even, has_dvd.dvd, two_mul]
 
 @[simp] lemma range_two_mul (α : Type*) [semiring α] :
   set.range (λ x : α, 2 * x) = {a | even a} :=
-by { ext x, simp [even, eq_comm] }
+by { ext x, simp [eq_comm, two_mul, even] }
 
 @[simp] lemma even_bit0 (a : α) : even (bit0 a) :=
-⟨a, by rw [bit0, two_mul]⟩
+⟨a, rfl⟩
 
-lemma even.add_even (hm : even m) (hn : even n) : even (m + n) :=
-begin
-  rcases hm with ⟨m, rfl⟩,
-  rcases hn with ⟨n, rfl⟩,
-  exact ⟨m + n, (mul_add _ _ _).symm⟩
-end
+@[simp] lemma even_two : even (2 : α) := ⟨1, rfl⟩
 
-@[simp] lemma even_two : even (2 : α) := ⟨1, (mul_one _).symm⟩
+@[simp] lemma even.mul_left (hm : even m) (n) : even (n * m) :=
+hm.map (add_monoid_hom.mul_left n)
 
 @[simp] lemma even.mul_right (hm : even m) (n) : even (m * n) :=
-(add_monoid_hom.mul_right n).even hm
+hm.map (add_monoid_hom.mul_right n)
 
-@[simp] lemma even.mul_left (hm : even m) (n) : even (n * m) :=
-(add_monoid_hom.mul_left n).even hm
+lemma even_two_mul (m : α) : even (2 * m) := ⟨m, two_mul _⟩
 
 lemma even.pow_of_ne_zero (hm : even m) : ∀ {a : ℕ}, a ≠ 0 → even (m ^ a)
 | 0       a0 := (a0 rfl).elim
@@ -73,7 +156,7 @@ lemma even.add_odd (hm : even m) (hn : odd n) : odd (m + n) :=
 begin
   rcases hm with ⟨m, rfl⟩,
   rcases hn with ⟨n, rfl⟩,
-  exact ⟨m + n, by rw [mul_add, add_assoc]⟩
+  exact ⟨m + n, by rw [mul_add, ← two_mul, add_assoc]⟩
 end
 
 lemma odd.add_even (hm : odd m) (hn : even n) : odd (m + n) :=
@@ -84,7 +167,8 @@ begin
   rcases hm with ⟨m, rfl⟩,
   rcases hn with ⟨n, rfl⟩,
   refine ⟨n + m + 1, _⟩,
-  rw [←add_assoc, add_comm _ (2 * n), ←add_assoc, ←mul_add, add_assoc, mul_add _ (n + m), mul_one],
+  rw [← two_mul, ←add_assoc, add_comm _ (2 * n), ←add_assoc, ←mul_add, add_assoc, mul_add _ (n + m),
+    mul_one],
   refl
 end
 
@@ -119,13 +203,13 @@ end semiring
 section ring
 variables [ring α] {m n : α}
 
-@[simp] theorem even_neg (a : α) : even (-a) ↔ even a :=
-dvd_neg _ _
-
-@[simp] lemma even_neg_two : even (- 2 : α) := by simp
+@[simp] lemma even_neg_two : even (- 2 : α) := by simp only [even_neg, even_two]
 
-lemma even.sub_even (hm : even m) (hn : even n) : even (m - n) :=
-by { rw sub_eq_add_neg, exact hm.add_even ((even_neg n).mpr hn) }
+lemma even_abs [linear_order α] {a : α} : even (|a|) ↔ even a :=
+begin
+  rcases abs_choice a with h | h; rw h,
+  exact even_neg a,
+end
 
 lemma odd.neg {a : α} (hp : odd a) : odd (-a) :=
 begin
@@ -149,19 +233,11 @@ by { rw sub_eq_add_neg, exact hm.add_odd ((odd_neg n).mpr hn) }
 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) }
 
--- from src/algebra/order/ring.lean
-variables [linear_order α]
-lemma even_abs {a : α} : even (|a|) ↔ even a :=
-dvd_abs _ _
-
--- from src/algebra/order/ring.lean
-lemma odd_abs {a : α} : odd (abs a) ↔ odd a :=
+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
 
-
--- from src/algebra/group_power/lemmas.lean
 section powers
 variables {R : Type*}
   {a : R} {n : ℕ} [linear_ordered_ring R]
@@ -206,21 +282,19 @@ by cases hn with k hk; simpa only [hk, two_mul] using strict_mono_pow_bit1 _
 
 end powers
 
--- from src/data/fintype/basic.lean
 /-- The cardinality of `fin (bit0 k)` is even, `fact` version.
 This `fact` is needed as an instance by `matrix.special_linear_group.has_neg`. -/
 lemma fintype.card_fin_even {k : ℕ} : fact (even (fintype.card (fin (bit0 k)))) :=
 ⟨by { rw [fintype.card_fin], exact even_bit0 k }⟩
 
--- from src/algebra/field_power.lean
 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 [←bit0_eq_two_mul, zpow_bit0_neg],
+  rw [← two_mul, ←bit0_eq_two_mul, zpow_bit0_neg],
 end
 
 variables [linear_ordered_field K] {n : ℤ} {a : K}

src/algebra/periodic.lean

@@ -357,7 +357,7 @@ lemma antiperiodic.nat_mul_eq_of_eq_zero [comm_semiring α] [add_group β]
 begin
   rcases nat.even_or_odd n with ⟨k, rfl⟩ | ⟨k, rfl⟩;
   have hk : (k : α) * (2 * c) = 2 * k * c := by rw [mul_left_comm, ← mul_assoc],
-  { simpa [hk, hi] using (h.nat_even_mul_periodic k).eq },
+  { simpa [← two_mul, hk, hi] using (h.nat_even_mul_periodic k).eq },
   { simpa [add_mul, hk, hi] using (h.nat_odd_mul_antiperiodic k).eq },
 end
 
@@ -367,7 +367,7 @@ lemma antiperiodic.int_mul_eq_of_eq_zero [comm_ring α] [add_group β]
 begin
   rcases int.even_or_odd n with ⟨k, rfl⟩ | ⟨k, rfl⟩;
   have hk : (k : α) * (2 * c) = 2 * k * c := by rw [mul_left_comm, ← mul_assoc],
-  { simpa [hk, hi] using (h.int_even_mul_periodic k).eq },
+  { simpa [← two_mul, hk, hi] using (h.int_even_mul_periodic k).eq },
   { simpa [add_mul, hk, hi] using (h.int_odd_mul_antiperiodic k).eq },
 end
 

src/analysis/convex/specific_functions.lean

@@ -53,8 +53,8 @@ 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) with ⟨k, hk⟩,
-    rw [iter_deriv_pow, finset.prod_range_cast_nat_sub, hk, pow_mul'],
+    rcases (nat.even.sub_even hn (even_bit0 1)).exists_two_nsmul _ with ⟨k, hk⟩,
+    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
 
@@ -106,7 +106,8 @@ lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : even n) :
 begin
   rcases hn with ⟨n, rfl⟩,
   induction n with n ihn, { simp },
-  rw [nat.succ_eq_add_one, mul_add, mul_one, bit0, ← add_assoc, finset.prod_range_succ,
+  rw ← two_mul at ihn,
+  rw [← two_mul, nat.succ_eq_add_one, mul_add, mul_one, bit0, ← add_assoc, finset.prod_range_succ,
     finset.prod_range_succ, mul_assoc],
   refine mul_nonneg ihn _, generalize : (1 + 1) * n = k,
   cases le_or_lt m k with hmk hmk,

src/combinatorics/simple_graph/degree_sum.lean

@@ -137,15 +137,15 @@ begin
     { use v,
       simp only [true_and, mem_filter, mem_univ],
       use h, },
-    rwa [←card_pos, hg, zero_lt_mul_left] at hh,
+    rwa [←card_pos, hg, ← two_mul, zero_lt_mul_left] at hh,
     exact zero_lt_two, },
   have hc : (λ (w : V), w ≠ v ∧ odd (G.degree w)) = (λ (w : V), odd (G.degree w) ∧ w ≠ v),
   { ext w,
     rw and_comm, },
   simp only [hc, filter_congr_decidable],
   rw [←filter_filter, filter_ne', card_erase_of_mem],
   { refine ⟨k - 1, tsub_eq_of_eq_add $ hg.trans _⟩,
-    rw [add_assoc, one_add_one_eq_two,  ←nat.mul_succ],
+    rw [add_assoc, one_add_one_eq_two, ←nat.mul_succ, ← two_mul],
     congr,
     exact (tsub_add_cancel_of_le $ nat.succ_le_iff.2 hk).symm },
   { simpa only [true_and, mem_filter, mem_univ] },

src/combinatorics/simple_graph/matching.lean

@@ -100,7 +100,7 @@ begin
   classical,
   rw is_matching_iff_forall_degree at h,
   use M.coe.edge_finset.card,
-  rw ← M.coe.sum_degrees_eq_twice_card_edges,
+  rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges],
   simp [h, finset.card_univ],
 end