From 6397e144f310c3202a1bd70f0d4f658816bc9d3f Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Wed, 13 Jan 2021 21:36:28 +0000 Subject: [PATCH] feat(data/nat/cast): add nat.bin_cast for faster casting (#5664) [As suggested](https://github.com/leanprover-community/mathlib/pull/5462#discussion_r553226279) by @gebner. Co-authored-by: Yakov Pechersky --- src/data/nat/cast.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean index b10551a4d43e3..6d247d82f9d03 100644 --- a/src/data/nat/cast.lean +++ b/src/data/nat/cast.lean @@ -19,6 +19,10 @@ protected def cast : ℕ → α | 0 := 0 | (n+1) := cast n + 1 +/-- Computationally friendlier cast than `nat.cast`, using binary representation. -/ +protected def bin_cast (n : ℕ) : α := +@nat.binary_rec (λ _, α) 0 (λ odd k a, cond odd (a + a + 1) (a + a)) n + /-- Coercions such as `nat.cast_coe` that go from a concrete structure such as `ℕ` to an arbitrary ring `α` should be set up as follows: @@ -59,6 +63,7 @@ theorem cast_succ (n : ℕ) : ((succ n : ℕ) : α) = n + 1 := rfl @[simp, norm_cast] theorem cast_ite (P : Prop) [decidable P] (m n : ℕ) : (((ite P m n) : ℕ) : α) = ite P (m : α) (n : α) := by { split_ifs; refl, } + end @[simp, norm_cast] theorem cast_one [add_monoid α] [has_one α] : ((1 : ℕ) : α) = 1 := zero_add _ @@ -67,6 +72,18 @@ end | 0 := (add_zero _).symm | (n+1) := show ((m + n : ℕ) : α) + 1 = m + (n + 1), by rw [cast_add n, add_assoc] +@[simp] lemma bin_cast_eq [add_monoid α] [has_one α] (n : ℕ) : + (nat.bin_cast n : α) = ((n : ℕ) : α) := +begin + rw nat.bin_cast, + apply binary_rec _ _ n, + { rw [binary_rec_zero, cast_zero] }, + { intros b k h, + rw [binary_rec_eq, h], + { cases b; simp [bit, bit0, bit1] }, + { simp } }, +end + /-- `coe : ℕ → α` as an `add_monoid_hom`. -/ def cast_add_monoid_hom (α : Type*) [add_monoid α] [has_one α] : ℕ →+ α := { to_fun := coe,