From 1a1895cd74de2b3272df34347fa37e69bea8d1b3 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 2 Jun 2022 21:38:24 +0000 Subject: [PATCH] feat(data/nat/basic): add lemmas about `nat.bit_cases_on` (#14481) Also drop `nat.bit_cases` (was the same definition with a different order of arguments). --- src/data/nat/basic.lean | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean index 1660691db8b9d..3f82c2c61fbbe 100644 --- a/src/data/nat/basic.lean +++ b/src/data/nat/basic.lean @@ -1526,10 +1526,29 @@ by { convert bit1_lt_bit0_iff, refl, } lemma pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n := by { cases n, cases h, apply succ_pos, } -/-- Define a function on `ℕ` depending on parity of the argument. -/ -@[elab_as_eliminator] -def bit_cases {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) : C n := -eq.rec_on n.bit_decomp (H (bodd n) (div2 n)) +@[simp] lemma bit_cases_on_bit {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (b : bool) (n : ℕ) : + bit_cases_on (bit b n) H = H b n := +eq_of_heq $ (eq_rec_heq _ _).trans $ by rw [bodd_bit, div2_bit] + +@[simp] lemma bit_cases_on_bit0 {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) : + bit_cases_on (bit0 n) H = H ff n := +bit_cases_on_bit H ff n + +@[simp] lemma bit_cases_on_bit1 {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) : + bit_cases_on (bit1 n) H = H tt n := +bit_cases_on_bit H tt n + +lemma bit_cases_on_injective {C : ℕ → Sort u} : + function.injective (λ H : Π b n, C (bit b n), λ n, bit_cases_on n H) := +begin + intros H₁ H₂ h, + ext b n, + simpa only [bit_cases_on_bit] using congr_fun h (bit b n) +end + +@[simp] lemma bit_cases_on_inj {C : ℕ → Sort u} (H₁ H₂ : Π b n, C (bit b n)) : + (λ n, bit_cases_on n H₁) = (λ n, bit_cases_on n H₂) ↔ H₁ = H₂ := +bit_cases_on_injective.eq_iff /-! ### decidability of predicates -/