From e7244db8006e890bc89309466e16e90e575eb65f Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Sat, 15 Jul 2023 18:06:24 +0100 Subject: [PATCH 1/3] Add Nat.evenOddStrongRec --- Mathlib/Data/Nat/EvenOddRec.lean | 36 ++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean index acdd96f9462a1..99569570e37a4 100644 --- a/Mathlib/Data/Nat/EvenOddRec.lean +++ b/Mathlib/Data/Nat/EvenOddRec.lean @@ -8,7 +8,7 @@ Authors: Stuart Presnell ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathlib.Data.Nat.Basic +import Mathlib.Data.Nat.Parity import Mathlib.Init.Data.Nat.Bitwise /-! # A recursion principle based on even and odd numbers. -/ @@ -22,7 +22,6 @@ namespace Nat extend from `P i` to both `P (2 * i)` and `P (2 * i + 1)`, then we have `P n` for all `n : ℕ`. This is nothing more than a wrapper around `Nat.binaryRec`, to avoid having to switch to dealing with `bit0` and `bit1`. -/ - @[elab_as_elim] def evenOddRec {P : ℕ → Sort _} (h0 : P 0) (h_even : ∀ (n) (_ : P n), P (2 * n)) (h_odd : ∀ (n) (_ : P n), P (2 * n + 1)) (n : ℕ) : P n := @@ -57,4 +56,37 @@ theorem evenOddRec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i eq_of_heq (this _ (bit1_val _)) #align nat.even_odd_rec_odd Nat.evenOddRec_odd +/-- Strong recursion principle on even and odd numbers: if for all `i : ℕ` we can prove `P (2 * i)` +from `P j` for all `j < 2 * i` and we can prove `P (2 * i + 1)` from `P j` for all `j < 2 * i + 1`, +then we have `P n` for all `n : ℕ`. -/ +noncomputable +def evenOddStrongRec {p : Sort _} (n : ℕ) + (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p) → p) + (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p) → p) : p := +n.strongRecOn' <| fun m ih => m.even_or_odd'.choose_spec.by_cases + (fun hm => peven m.even_or_odd'.choose <| fun k hk => ih k <| hm.symm ▸ hk) + (fun hm => podd m.even_or_odd'.choose <| fun k hk => ih k <| hm.symm ▸ hk) + +@[simp] +lemma evenOddStrongRec_even {p : Sort _} (m : ℕ) + (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p) → p) + (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p) → p) : + (2 * m).evenOddStrongRec peven podd = + peven m (fun k _ => k.evenOddStrongRec peven podd) := by + rcases (2 * m).even_or_odd'.choose_spec with h | h + · rw [evenOddStrongRec, strongRecOn'_beta, Or.by_cases, dif_pos h] + conv_rhs => rw [mul_left_cancel₀ two_ne_zero h] + · exact (two_mul_ne_two_mul_add_one h).elim + +@[simp] +lemma evenOddStrongRec_odd {p : Sort _} (m : ℕ) + (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p) → p) + (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p) → p) : + (2 * m + 1).evenOddStrongRec peven podd = + podd m (fun k _ => k.evenOddStrongRec peven podd) := by + rcases (2 * m + 1).even_or_odd'.choose_spec with h | h + · exact (two_mul_ne_two_mul_add_one h.symm).elim + · rw [evenOddStrongRec, strongRecOn'_beta, Or.by_cases, dif_neg two_mul_ne_two_mul_add_one.symm] + conv_rhs => rw [mul_left_cancel₀ two_ne_zero <| succ_injective h] + end Nat From 9a0d9e59228df53319bcf67e64829049dd19f806 Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Fri, 21 Jul 2023 18:00:53 +0100 Subject: [PATCH 2/3] Change type --- Mathlib/Data/Nat/EvenOddRec.lean | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean index 99569570e37a4..a7b8b84c2100d 100644 --- a/Mathlib/Data/Nat/EvenOddRec.lean +++ b/Mathlib/Data/Nat/EvenOddRec.lean @@ -59,18 +59,17 @@ theorem evenOddRec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i /-- Strong recursion principle on even and odd numbers: if for all `i : ℕ` we can prove `P (2 * i)` from `P j` for all `j < 2 * i` and we can prove `P (2 * i + 1)` from `P j` for all `j < 2 * i + 1`, then we have `P n` for all `n : ℕ`. -/ -noncomputable -def evenOddStrongRec {p : Sort _} (n : ℕ) - (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p) → p) - (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p) → p) : p := +noncomputable def evenOddStrongRec {p : ℕ → Sort _} (n : ℕ) + (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p k) → p (2 * m)) + (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p k) → p (2 * m + 1)) : p n := n.strongRecOn' <| fun m ih => m.even_or_odd'.choose_spec.by_cases - (fun hm => peven m.even_or_odd'.choose <| fun k hk => ih k <| hm.symm ▸ hk) - (fun hm => podd m.even_or_odd'.choose <| fun k hk => ih k <| hm.symm ▸ hk) + (fun hm => hm.symm ▸ peven m.even_or_odd'.choose <| hm ▸ ih) + (fun hm => hm.symm ▸ podd m.even_or_odd'.choose <| hm ▸ ih) @[simp] -lemma evenOddStrongRec_even {p : Sort _} (m : ℕ) - (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p) → p) - (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p) → p) : +lemma evenOddStrongRec_even {p : ℕ → Sort _} (m : ℕ) + (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p k) → p (2 * m)) + (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p k) → p (2 * m + 1)) : (2 * m).evenOddStrongRec peven podd = peven m (fun k _ => k.evenOddStrongRec peven podd) := by rcases (2 * m).even_or_odd'.choose_spec with h | h @@ -79,9 +78,9 @@ lemma evenOddStrongRec_even {p : Sort _} (m : ℕ) · exact (two_mul_ne_two_mul_add_one h).elim @[simp] -lemma evenOddStrongRec_odd {p : Sort _} (m : ℕ) - (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p) → p) - (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p) → p) : +lemma evenOddStrongRec_odd {p : ℕ → Sort _} (m : ℕ) + (peven : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m → p k) → p (2 * m)) + (podd : ∀ m : ℕ, (∀ k : ℕ, k < 2 * m + 1 → p k) → p (2 * m + 1)) : (2 * m + 1).evenOddStrongRec peven podd = podd m (fun k _ => k.evenOddStrongRec peven podd) := by rcases (2 * m + 1).even_or_odd'.choose_spec with h | h From f6ca18ab58a2833ddc14e592661b5cc5fb0d528d Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Tue, 20 Feb 2024 17:26:33 +0000 Subject: [PATCH 3/3] Golf Co-authored-by: Oliver Nash --- Mathlib/Data/Nat/EvenOddRec.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean index 09716994ffa70..085c3ed55f705 100644 --- a/Mathlib/Data/Nat/EvenOddRec.lean +++ b/Mathlib/Data/Nat/EvenOddRec.lean @@ -57,8 +57,8 @@ from `P j` for all `j < 2 * i` and we can prove `P (2 * i + 1)` from `P j` for a then we have `P n` for all `n : ℕ`. -/ @[elab_as_elim] noncomputable def evenOddStrongRec {P : ℕ → Sort*} (n : ℕ) - (h_even : ∀ n : ℕ, (∀ k : ℕ, k < 2 * n → P k) → P (2 * n)) - (h_odd : ∀ n : ℕ, (∀ k : ℕ, k < 2 * n + 1 → P k) → P (2 * n + 1)) : P n := + (h_even : ∀ n : ℕ, (∀ k < 2 * n, P k) → P (2 * n)) + (h_odd : ∀ n : ℕ, (∀ k < 2 * n + 1, P k) → P (2 * n + 1)) : P n := n.strongRecOn fun m ih => m.even_or_odd'.choose_spec.by_cases (fun h => h.symm ▸ h_even m.even_or_odd'.choose <| h ▸ ih) (fun h => h.symm ▸ h_odd m.even_or_odd'.choose <| h ▸ ih)