From 0eea0d9fc53bd037da13abdf5d95a711cbd0c288 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 13 Jul 2019 12:25:07 -0400 Subject: [PATCH] feat(data/{nat,int}/parity): the 'even' predicate on nat and int (#1219) * feat(data/{nat,int}/parity): the 'even' predicate on nat and int * fix(data/{nat,int}/parity): shorten proof * delete extra comma --- src/data/int/parity.lean | 80 ++++++++++++++++++++++++++++++++++++++++ src/data/nat/parity.lean | 79 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 159 insertions(+) create mode 100644 src/data/int/parity.lean create mode 100644 src/data/nat/parity.lean diff --git a/src/data/int/parity.lean b/src/data/int/parity.lean new file mode 100644 index 0000000000000..a707802c183f8 --- /dev/null +++ b/src/data/int/parity.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2019 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Avigad + +The `even` predicate on the integers. +-/ +import .modeq data.nat.parity algebra.group_power + +namespace int + +@[simp] theorem mod_two_ne_one {n : int} : ¬ 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 : int} : ¬ n % 2 = 0 ↔ n % 2 = 1 := +by cases mod_two_eq_zero_or_one n with h h; simp [h] + +def even (n : int) : Prop := ∃ m, n = 2 * m + +@[simp] theorem even_coe_nat (n : nat) : even n ↔ nat.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 := +⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩ + +instance : decidable_pred even := +λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm + +@[simp] theorem even_zero : even (0 : int) := ⟨0, dec_trivial⟩ + +@[simp] theorem not_even_one : ¬ even (1 : int) := +by rw even_iff; apply one_ne_zero + +@[simp] theorem even_bit0 (n : int) : even (bit0 n) := +⟨n, by rw [bit0, two_mul]⟩ + +@[parity_simps] theorem even_add {m n : int} : 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₂], + { exact @modeq.modeq_add _ _ 0 _ 0 h₁ h₂ }, + { exact @modeq.modeq_add _ _ 0 _ 1 h₁ h₂ }, + { exact @modeq.modeq_add _ _ 1 _ 0 h₁ h₂ }, + exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂ +end + +@[simp] theorem not_even_bit1 (n : int) : ¬ even (bit1 n) := +by simp [bit1] with parity_simps + +@[parity_simps] theorem even_sub {m n : int} : even (m - n) ↔ (even m ↔ even n) := +begin + conv { to_rhs, rw [←sub_add_cancel m n, even_add] }, + by_cases h : even n; simp [h] +end + +@[parity_simps] theorem even_mul {m n : int} : 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₂], + { exact @modeq.modeq_mul _ _ 0 _ 0 h₁ h₂ }, + { exact @modeq.modeq_mul _ _ 0 _ 1 h₁ h₂ }, + { exact @modeq.modeq_mul _ _ 1 _ 0 h₁ h₂ }, + 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 := +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) := +by simp [*, (dec_trivial : ¬ 2 = 0)] with parity_simps + +example : ¬ even (25394535 : int) := +by simp + +end int diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean new file mode 100644 index 0000000000000..c352db450a261 --- /dev/null +++ b/src/data/nat/parity.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2019 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Avigad + +The `even` predicate on the natural numbers. +-/ +import .modeq + +namespace nat + +@[simp] theorem mod_two_ne_one {n : nat} : ¬ 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 := +by cases mod_two_eq_zero_or_one n with h h; simp [h] + +def even (n : nat) : Prop := ∃ m, n = 2 * m + +theorem even_iff {n : nat} : even n ↔ n % 2 = 0 := +⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩ + +instance : decidable_pred even := +λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm + +run_cmd mk_simp_attr `parity_simps + +@[simp] theorem even_zero : even 0 := ⟨0, dec_trivial⟩ + +@[simp] theorem not_even_one : ¬ even 1 := +by rw even_iff; apply one_ne_zero + +@[simp] theorem even_bit0 (n : nat) : even (bit0 n) := +⟨n, by rw [bit0, two_mul]⟩ + +@[parity_simps] theorem even_add {m n : nat} : 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₂], + { exact @modeq.modeq_add _ _ 0 _ 0 h₁ h₂ }, + { exact @modeq.modeq_add _ _ 0 _ 1 h₁ h₂ }, + { exact @modeq.modeq_add _ _ 1 _ 0 h₁ h₂ }, + exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂ +end + +@[simp] theorem not_even_bit1 (n : nat) : ¬ even (bit1 n) := +by simp [bit1] with parity_simps + +@[parity_simps] theorem even_sub {m n : nat} (h : m ≥ n) : 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 + +@[parity_simps] theorem even_succ {n : nat} : 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 := +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₂], + { exact @modeq.modeq_mul _ _ 0 _ 0 h₁ h₂ }, + { exact @modeq.modeq_mul _ _ 0 _ 1 h₁ h₂ }, + { exact @modeq.modeq_mul _ _ 1 _ 0 h₁ h₂ }, + exact @modeq.modeq_mul _ _ 1 _ 1 h₁ h₂ +end + +@[parity_simps] theorem even_pow {m n : nat} : even (m^n) ↔ even m ∧ n ≠ 0 := +by { induction n with n ih; simp [*, pow_succ, even_mul], tauto } + +-- 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) := +by simp [*, (dec_trivial : ¬ 2 = 0)] with parity_simps + +example : ¬ even 25394535 := +by simp + +end nat