From 99e308d3ff7de07b6c278cc9c9e87b37575de728 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Tue, 6 Oct 2020 12:41:47 +0000 Subject: [PATCH] chore(parity): even and odd in semiring (#4473) Replaces the ad-hoc `nat.even`, `nat.odd`, `int.even` and `int.odd` by definitions that make sense in semirings and get that `odd` can be `rintros`/`rcases`'ed. This requires almost no change except that `even` is not longer usable as a dot notation (which I see as a feature since I find `even n` to be more readable than `n.even`). Co-authored-by: Scott Morrison --- src/algebra/ring/basic.lean | 8 +++ src/analysis/convex/specific_functions.lean | 8 +-- src/analysis/mean_inequalities.lean | 2 +- src/data/int/parity.lean | 57 +++++++++------------ src/data/nat/parity.lean | 55 +++++++++----------- src/number_theory/sum_four_squares.lean | 6 +-- 6 files changed, 65 insertions(+), 71 deletions(-) diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index 32dafd649ba52..7d531e6a5b953 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -171,6 +171,14 @@ lemma ite_mul_zero_right {α : Type*} [mul_zero_class α] (P : Prop) [decidable ite P (a * b) 0 = a * ite P b 0 := by { by_cases h : P; simp [h], } +/-- An element `a` of a semiring is even if there exists `k` such `a = 2*k`. -/ +def even (a : α) : Prop := ∃ k, a = 2*k + +lemma even_iff_two_dvd {a : α} : even a ↔ 2 ∣ a := iff.rfl + +/-- 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 + end semiring namespace add_monoid_hom diff --git a/src/analysis/convex/specific_functions.lean b/src/analysis/convex/specific_functions.lean index b82bfb81e4374..4b313f5542c3e 100644 --- a/src/analysis/convex/specific_functions.lean +++ b/src/analysis/convex/specific_functions.lean @@ -29,12 +29,12 @@ convex_on_univ_of_deriv2_nonneg differentiable_exp (by simp) (assume x, (iter_deriv_exp 2).symm ▸ le_of_lt (exp_pos x)) /-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even -/ -lemma convex_on_pow_of_even {n : ℕ} (hn : n.even) : convex_on set.univ (λ x : ℝ, x^n) := +lemma convex_on_pow_of_even {n : ℕ} (hn : even n) : convex_on set.univ (λ x : ℝ, x^n) := begin apply convex_on_univ_of_deriv2_nonneg differentiable_pow, { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] }, { intro x, - rcases hn.sub (nat.even_bit0 1) with ⟨k, hk⟩, + rcases nat.even.sub 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 _) } @@ -53,7 +53,7 @@ end lemma finset.prod_nonneg_of_card_nonpos_even {α β : Type*} [linear_ordered_comm_ring β] {f : α → β} [decidable_pred (λ x, f x ≤ 0)] - {s : finset α} (h0 : (s.filter (λ x, f x ≤ 0)).card.even) : + {s : finset α} (h0 : even (s.filter (λ x, f x ≤ 0)).card) : 0 ≤ ∏ x in s, f x := calc 0 ≤ (∏ x in s, ((if f x ≤ 0 then (-1:β) else 1) * f x)) : finset.prod_nonneg (λ x _, by @@ -61,7 +61,7 @@ calc 0 ≤ (∏ x in s, ((if f x ≤ 0 then (-1:β) else 1) * f x)) : ... = _ : by rw [finset.prod_mul_distrib, finset.prod_ite, finset.prod_const_one, mul_one, finset.prod_const, neg_one_pow_eq_pow_mod_two, nat.even_iff.1 h0, pow_zero, one_mul] -lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : n.even) : +lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : even n) : 0 ≤ ∏ k in finset.range n, (m - k) := begin cases (le_or_lt ↑n m) with hnm hmn, diff --git a/src/analysis/mean_inequalities.lean b/src/analysis/mean_inequalities.lean index 2b3097964f715..924f8a8ea3726 100644 --- a/src/analysis/mean_inequalities.lean +++ b/src/analysis/mean_inequalities.lean @@ -145,7 +145,7 @@ theorem pow_arith_mean_le_arith_mean_pow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 (convex_on_pow n).map_sum_le hw hw' hz theorem pow_arith_mean_le_arith_mean_pow_of_even (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) - (hw' : ∑ i in s, w i = 1) {n : ℕ} (hn : n.even) : + (hw' : ∑ i in s, w i = 1) {n : ℕ} (hn : even n) : (∑ i in s, w i * z i) ^ n ≤ ∑ i in s, (w i * z i ^ n) := (convex_on_pow_of_even hn).map_sum_le hw hw' (λ _ _, trivial) diff --git a/src/data/int/parity.lean b/src/data/int/parity.lean index 1ed8b18a9cf2b..7594bf594b2b7 100644 --- a/src/data/int/parity.lean +++ b/src/data/int/parity.lean @@ -10,57 +10,50 @@ import data.nat.parity namespace int -@[simp] theorem mod_two_ne_one {n : int} : ¬ n % 2 = 1 ↔ n % 2 = 0 := +@[simp] theorem mod_two_ne_one {n : ℤ} : ¬ 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 : int} : ¬ n % 2 = 0 ↔ n % 2 = 1 := +theorem mod_two_ne_zero {n : ℤ} : ¬ n % 2 = 0 ↔ n % 2 = 1 := by cases mod_two_eq_zero_or_one n with h h; simp [h] -/-- An integer `n` is `even` if `2 | n`. -/ -def even (n : int) : Prop := 2 ∣ n - -@[simp] theorem even_coe_nat (n : nat) : even n ↔ nat.even n := +@[simp] theorem even_coe_nat (n : nat) : 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 : int} : even n ↔ n % 2 = 0 := +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 })⟩⟩ + lemma not_even_iff {n : ℤ} : ¬ even n ↔ n % 2 = 1 := by rw [even_iff, mod_two_ne_zero] -/-- An integer `n` is `odd` if it is not even. The mathlib API -for parity is developed in terms of `even`; to avoid duplication, -results should not be stated in terms of `odd`. The purpose of this -definition is for code outside mathlib that wishes to have a formal -statement that is as literal a translation as possible of the -corresponding informal statement, where that informal statement refers -to odd numbers. -/ -def odd (n : ℤ) : Prop := ¬ even n - -@[simp] lemma odd_def (n : ℤ) : odd n ↔ ¬ even n := iff.rfl +@[simp] lemma odd_iff_not_even {n : ℤ} : odd n ↔ ¬ even n := +by rw [not_even_iff, odd_iff] -@[simp] theorem two_dvd_ne_zero {n : int} : ¬ 2 ∣ n ↔ n % 2 = 1 := +@[simp] theorem two_dvd_ne_zero {n : ℤ} : ¬ 2 ∣ n ↔ n % 2 = 1 := not_even_iff -instance : decidable_pred even := +instance : decidable_pred (even : ℤ → Prop) := λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm -instance decidable_pred_odd : decidable_pred odd := -λ n, decidable_of_decidable_of_iff (by apply_instance) not_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 -@[simp] theorem even_zero : even (0 : int) := ⟨0, dec_trivial⟩ +@[simp] theorem even_zero : even (0 : ℤ) := ⟨0, dec_trivial⟩ -@[simp] theorem not_even_one : ¬ even (1 : int) := +@[simp] theorem not_even_one : ¬ even (1 : ℤ) := by rw even_iff; apply one_ne_zero -@[simp] theorem even_bit0 (n : int) : even (bit0 n) := +@[simp] theorem even_bit0 (n : ℤ) : even (bit0 n) := ⟨n, by rw [bit0, two_mul]⟩ -@[parity_simps] theorem even_add {m n : int} : even (m + n) ↔ (even m ↔ even n) := +@[parity_simps] theorem even_add {m n : ℤ} : 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], @@ -70,15 +63,15 @@ begin exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂ end -@[parity_simps] theorem even_neg {n : ℤ} : even (-n) ↔ even n := by simp [even] +@[parity_simps] theorem even_neg {n : ℤ} : even (-n) ↔ even n := by simp [even_iff] -@[simp] theorem not_even_bit1 (n : int) : ¬ even (bit1 n) := +@[simp] theorem not_even_bit1 (n : ℤ) : ¬ even (bit1 n) := by simp [bit1] with parity_simps -@[parity_simps] theorem even_sub {m n : int} : even (m - n) ↔ (even m ↔ even n) := +@[parity_simps] theorem even_sub {m n : ℤ} : even (m - n) ↔ (even m ↔ even n) := by simp [sub_eq_add_neg] with parity_simps -@[parity_simps] theorem even_mul {m n : int} : even (m * n) ↔ even m ∨ even n := +@[parity_simps] theorem even_mul {m n : ℤ} : 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], @@ -88,15 +81,15 @@ begin exact @modeq.modeq_mul _ _ 1 _ 1 h₁ h₂ end -@[parity_simps] theorem even_pow {m : int} {n : nat} : even (m^n) ↔ even m ∧ n ≠ 0 := +@[parity_simps] theorem even_pow {m : ℤ} {n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 := by { induction n with n ih; simp [*, even_mul, pow_succ], tauto } -- Here are examples of how `parity_simps` can be used with `int`. -example (m n : int) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) := +example (m n : ℤ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) := by simp [*, (dec_trivial : ¬ 2 = 0)] with parity_simps -example : ¬ even (25394535 : int) := +example : ¬ even (25394535 : ℤ) := by simp end int diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean index d82c8bbc70828..52f5df61c8e61 100644 --- a/src/data/nat/parity.lean +++ b/src/data/nat/parity.lean @@ -9,37 +9,30 @@ import data.nat.modeq namespace nat -@[simp] theorem mod_two_ne_one {n : nat} : ¬ n % 2 = 1 ↔ n % 2 = 0 := +@[simp] theorem mod_two_ne_one {n : ℕ} : ¬ n % 2 = 1 ↔ n % 2 = 0 := by cases mod_two_eq_zero_or_one n with h h; simp [h] -@[simp] theorem mod_two_ne_zero {n : nat} : ¬ n % 2 = 0 ↔ n % 2 = 1 := +@[simp] theorem mod_two_ne_zero {n : ℕ} : ¬ n % 2 = 0 ↔ n % 2 = 1 := by cases mod_two_eq_zero_or_one n with h h; simp [h] -/-- A natural number `n` is `even` if `2 | n`. -/ -def even (n : nat) : Prop := 2 ∣ n - -theorem even_iff {n : nat} : even n ↔ n % 2 = 0 := +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 })⟩⟩ + lemma not_even_iff {n : ℕ} : ¬ even n ↔ n % 2 = 1 := by rw [even_iff, mod_two_ne_zero] -/-- A natural number `n` is `odd` if it is not even. The mathlib API -for parity is developed in terms of `even`; to avoid duplication, -results should not be stated in terms of `odd`. The purpose of this -definition is for code outside mathlib that wishes to have a formal -statement that is as literal a translation as possible of the -corresponding informal statement, where that informal statement refers -to odd numbers. -/ -def odd (n : ℕ) : Prop := ¬ even n - -@[simp] lemma odd_def (n : ℕ) : odd n ↔ ¬ even n := iff.rfl +@[simp] lemma odd_iff_not_even {n : ℕ} : odd n ↔ ¬ even n := +by rw [not_even_iff, odd_iff] -instance : decidable_pred even := +instance : decidable_pred (even : ℕ → Prop) := λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm -instance decidable_pred_odd : decidable_pred odd := -λ n, decidable_of_decidable_of_iff (by apply_instance) not_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 mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`" @@ -48,10 +41,10 @@ mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`" @[simp] theorem not_even_one : ¬ even 1 := by rw even_iff; apply one_ne_zero -@[simp] theorem even_bit0 (n : nat) : even (bit0 n) := +@[simp] theorem even_bit0 (n : ℕ) : even (bit0 n) := ⟨n, by rw [bit0, two_mul]⟩ -@[parity_simps] theorem even_add {m n : nat} : even (m + n) ↔ (even m ↔ even n) := +@[parity_simps] theorem even_add {m n : ℕ} : 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₂], @@ -61,10 +54,10 @@ begin exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂ end -theorem even.add {m n : ℕ} (hm : m.even) (hn : n.even) : (m + n).even := +theorem even.add {m n : ℕ} (hm : even m) (hn : even n) : even (m + n) := even_add.2 $ by simp only [*] -@[simp] theorem not_even_bit1 (n : nat) : ¬ even (bit1 n) := +@[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) := @@ -76,21 +69,21 @@ 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 -@[parity_simps] theorem even_sub {m n : nat} (h : n ≤ m) : even (m - n) ↔ (even m ↔ even 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 : m.even) (hn : n.even) : (m - n).even := +theorem even.sub {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]) -@[parity_simps] theorem even_succ {n : nat} : even (succ n) ↔ ¬ even n := +@[parity_simps] theorem even_succ {n : ℕ} : even (succ n) ↔ ¬ even n := by rw [succ_eq_add_one, even_add]; simp [not_even_one] -@[parity_simps] theorem even_mul {m n : nat} : even (m * n) ↔ even m ∨ even n := +@[parity_simps] theorem even_mul {m n : ℕ} : 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₂], @@ -100,13 +93,13 @@ begin exact @modeq.modeq_mul _ _ 1 _ 1 h₁ h₂ end -/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even +/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even if and only if `m` is even and `n` is positive. -/ -@[parity_simps] theorem even_pow {m n : nat} : even (m^n) ↔ even m ∧ n ≠ 0 := +@[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 := -by rw [even, dvd_iff_mod_eq_zero, nat.div_mod_eq_mod_mul_div, mul_comm] +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): (-1 : α) ^ n = 1 ↔ even n := @@ -116,7 +109,7 @@ theorem neg_one_pow_eq_one_iff_even {α : Type*} [ring α] {n : ℕ} (h1 : (-1 : -- Here are examples of how `parity_simps` can be used with `nat`. -example (m n : nat) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) := +example (m n : ℕ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) := by simp [*, (dec_trivial : ¬ 2 = 0)] with parity_simps example : ¬ even 25394535 := diff --git a/src/number_theory/sum_four_squares.lean b/src/number_theory/sum_four_squares.lean index 15efa2640fb15..48994897e3bc3 100644 --- a/src/number_theory/sum_four_squares.lean +++ b/src/number_theory/sum_four_squares.lean @@ -25,9 +25,9 @@ namespace int lemma sum_two_squares_of_two_mul_sum_two_squares {m x y : ℤ} (h : 2 * m = x^2 + y^2) : m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 := -have (x^2 + y^2).even, by simp [h.symm, even_mul], -have hxaddy : (x + y).even, by simpa [pow_two] with parity_simps, -have hxsuby : (x - y).even, by simpa [pow_two] with parity_simps, +have even (x^2 + y^2), by simp [h.symm, even_mul], +have hxaddy : even (x + y), by simpa [pow_two] with parity_simps, +have hxsuby : even (x - y), by simpa [pow_two] with parity_simps, have (x^2 + y^2) % 2 = 0, by simp [h.symm], (mul_right_inj' (show (2*2 : ℤ) ≠ 0, from dec_trivial)).1 $ calc 2 * 2 * m = (x - y)^2 + (x + y)^2 : by rw [mul_assoc, h]; ring