Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: redefine Nat.bit Nat.div2 Nat.bodd #13649

Open
wants to merge 50 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
c047c64
chore: redefine `Nat.binaryRec` `Nat.div2` `Nat.bodd`
FR-vdash-bot Jun 9, 2024
5ccab29
Update Mathlib.lean
FR-vdash-bot Jun 9, 2024
9f429e9
fix
FR-vdash-bot Jun 9, 2024
7ffe999
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 13, 2024
584c3ce
fix
FR-vdash-bot Jul 13, 2024
fde50df
fix
FR-vdash-bot Jul 13, 2024
68a2c0b
fix
FR-vdash-bot Jul 13, 2024
ea3360b
shake
FR-vdash-bot Jul 13, 2024
6392674
fix
FR-vdash-bot Jul 13, 2024
77d68ab
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 15, 2024
bd0c24f
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 15, 2024
fd5c58d
fix merge
FR-vdash-bot Jul 15, 2024
049d442
fix
FR-vdash-bot Jul 15, 2024
16a10ce
fix
FR-vdash-bot Jul 15, 2024
7398e5b
fix
FR-vdash-bot Jul 15, 2024
4a9fd6e
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 17, 2024
ccb809c
fix
FR-vdash-bot Jul 17, 2024
38780b5
fix
FR-vdash-bot Jul 17, 2024
e056180
fix
FR-vdash-bot Jul 17, 2024
199117a
shake
FR-vdash-bot Jul 17, 2024
27734ef
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 17, 2024
84535ce
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 24, 2024
40ed248
shake
FR-vdash-bot Jul 24, 2024
80ce83e
fix
FR-vdash-bot Jul 24, 2024
e57a5d9
fix
FR-vdash-bot Jul 24, 2024
2046094
fix
FR-vdash-bot Jul 24, 2024
432eaec
fix
FR-vdash-bot Jul 24, 2024
9d9ccda
fix
FR-vdash-bot Jul 24, 2024
2097400
fix
FR-vdash-bot Jul 24, 2024
194bf44
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 27, 2024
d32d5c6
Merge branch 'master' into FR_binrec
FR-vdash-bot Jul 27, 2024
7a00093
Merge branch 'master' into FR_binrec
FR-vdash-bot Aug 2, 2024
7c3e5b3
Merge branch 'master' into FR_binrec
FR-vdash-bot Aug 6, 2024
6b19c7e
name
FR-vdash-bot Aug 6, 2024
871aa5f
golf
FR-vdash-bot Aug 6, 2024
19b05e0
golf
FR-vdash-bot Aug 6, 2024
3389c1d
Merge branch 'master' into FR_binrec
FR-vdash-bot Oct 22, 2024
8b6ae3b
split to #18039
FR-vdash-bot Oct 22, 2024
ccbbd75
fix merge
FR-vdash-bot Oct 22, 2024
4855c89
cleanup
FR-vdash-bot Oct 22, 2024
d1de536
cleanup
FR-vdash-bot Oct 22, 2024
c47385f
fix merge
FR-vdash-bot Oct 22, 2024
9bfda89
`Nat.bit`
FR-vdash-bot Oct 22, 2024
d569f2d
fix merge
FR-vdash-bot Oct 22, 2024
2983872
fix
FR-vdash-bot Oct 22, 2024
7e64fc8
fix merge
FR-vdash-bot Oct 22, 2024
4aab2a9
Merge branch 'master' into FR_binrec
FR-vdash-bot Oct 23, 2024
9662403
fix
FR-vdash-bot Oct 23, 2024
a884905
Merge branch 'master' into FR_binrec
FR-vdash-bot Nov 14, 2024
759d699
`csimp`
FR-vdash-bot Nov 14, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Computability/Primrec.lean
Original file line number Diff line number Diff line change
Expand Up @@ -796,7 +796,7 @@ instance sum : Primcodable (α ⊕ β) :=
to₂ <| nat_double.comp (Primrec.encode.comp snd)))).of_eq
fun n =>
show _ = encode (decodeSum n) by
simp only [decodeSum, Nat.boddDiv2_eq]
simp only [decodeSum]
cases Nat.bodd n <;> simp [decodeSum]
· cases @decode α _ n.div2 <;> rfl
· cases @decode β _ n.div2 <;> rfl⟩
Expand Down
4 changes: 1 addition & 3 deletions Mathlib/Data/Int/Bitwise.lean
Original file line number Diff line number Diff line change
Expand Up @@ -219,9 +219,7 @@ theorem bodd_bit (b n) : bodd (bit b n) = b := by
theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
| (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
| -[n+1] => by
rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero
cases b <;>
rfl
rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero, Bool.not_not]

@[simp]
theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
Expand Down
11 changes: 9 additions & 2 deletions Mathlib/Data/Nat/BinaryRec.lean
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,15 @@ universe u

namespace Nat

/-- `bit b` appends the digit `b` to the binary representation of its natural number input. -/
def bit (b : Bool) : Nat → Nat := cond b (2 * · + 1) (2 * ·)
/-- `bit b` appends the digit `b` to the little end of the binary representation of
its natural number input. -/
def bit (b : Bool) (n : Nat) : Nat :=
cond b (2 * n + 1) (2 * n)

private def bitImpl (b : Bool) (n : Nat) : Nat :=
cond b (n <<< 1 + 1) (n <<< 1)
FR-vdash-bot marked this conversation as resolved.
Show resolved Hide resolved

@[csimp] theorem bit_eq_bitImpl : bit = bitImpl := rfl

theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl

Expand Down
90 changes: 36 additions & 54 deletions Mathlib/Data/Nat/Bits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ Authors: Praneeth Kolichala
-/
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Nat
import Mathlib.Data.Nat.Defs
import Mathlib.Data.Nat.BinaryRec
import Mathlib.Data.Nat.Defs
import Mathlib.Data.List.Defs
import Mathlib.Tactic.Convert
import Mathlib.Tactic.GeneralizeProofs
Expand Down Expand Up @@ -34,18 +34,20 @@ variable {m n : ℕ}

/-- `boddDiv2 n` returns a 2-tuple of type `(Bool, Nat)` where the `Bool` value indicates whether
`n` is odd or not and the `Nat` value returns `⌊n/2⌋` -/
def boddDiv2 : ℕ → Bool × ℕ
@[deprecated (since := "2024-06-09")] def boddDiv2 : ℕ → Bool × ℕ
| 0 => (false, 0)
| succ n =>
match boddDiv2 n with
| (false, m) => (true, m)
| (true, m) => (false, succ m)

/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
def div2 (n : ℕ) : ℕ := (boddDiv2 n).2
def div2 (n : ℕ) : ℕ := n >>> 1

theorem div2_val (n) : div2 n = n / 2 := rfl

/-- `bodd n` returns `true` if `n` is odd -/
def bodd (n : ℕ) : Bool := (boddDiv2 n).1
def bodd (n : ℕ) : Bool := 1 &&& n != 0

@[simp] lemma bodd_zero : bodd 0 = false := rfl

Expand All @@ -55,9 +57,8 @@ lemma bodd_two : bodd 2 = false := rfl

@[simp]
lemma bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
simp only [bodd, boddDiv2]
let ⟨b,m⟩ := boddDiv2 n
cases b <;> rfl
simp only [bodd, succ_eq_add_one, one_and_eq_mod_two]
cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]

@[simp]
lemma bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by
Expand All @@ -73,19 +74,13 @@ lemma bodd_mul (m n : ℕ) : bodd (m * n) = (bodd m && bodd n) := by
simp only [mul_succ, bodd_add, IH, bodd_succ]
cases bodd m <;> cases bodd n <;> rfl

lemma mod_two_of_bodd (n : ℕ) : n % 2 = (bodd n).toNat := by
have := congr_arg bodd (mod_add_div n 2)
simp? [not] at this says
simp only [bodd_add, bodd_mul, bodd_succ, not, bodd_zero, Bool.false_and, Bool.bne_false]
at this
have _ : ∀ b, and false b = false := by
intro b
cases b <;> rfl
have _ : ∀ b, bxor b false = b := by
intro b
cases b <;> rfl
rw [← this]
rcases mod_two_eq_zero_or_one n with h | h <;> rw [h] <;> rfl
@[simp]
lemma bodd_bit (b n) : bodd (bit b n) = b := by
simp [bodd]

lemma mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
cases n using bitCasesOn with
| h b n => cases b <;> simp

@[simp] lemma div2_zero : div2 0 = 0 := rfl

Expand All @@ -95,24 +90,18 @@ lemma div2_two : div2 2 = 1 := rfl

@[simp]
lemma div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n) := by
simp only [bodd, boddDiv2, div2]
rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp
cases n using bitCasesOn with
| h b n => cases b <;> simp [bit_val, div2_val, succ_div]

@[simp]
lemma div2_bit (b n) : div2 (bit b n) = n := by
rw [div2_val, bit_div_two]

attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc

lemma bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
| 0 => rfl
| succ n => by
simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]
refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))
cases bodd n
· simp
· simp; omega

lemma div2_val (n) : div2 n = n / 2 := by
refine Nat.eq_of_mul_eq_mul_left (by decide)
(Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))
rw [mod_two_of_bodd, bodd_add_div2]
lemma bodd_add_div2 (n : ℕ) : cond (bodd n) 1 0 + 2 * div2 n = n := by
cases n using bitCasesOn with
| h b n => simpa using (bit_val b n).symm

lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
(bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
Expand All @@ -139,12 +128,10 @@ lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
@[simp] lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl
@[simp] lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl

lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
rw [div2_val]
apply (div_lt_iff_lt_mul <| succ_pos 1).2
have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
(lt_of_le_of_ne n.zero_le h.symm)
rwa [Nat.mul_one] at this
lemma div2_lt_self (h : n ≠ 0) : div2 n < n :=
div_lt_self (Nat.pos_iff_ne_zero.mpr h) Nat.one_lt_two

@[deprecated (since := "2024-10-22")] alias binaryRec_decreasing := div2_lt_self

/-- `size n` : Returns the size of a natural number in
bits i.e. the length of its binary representation -/
Expand All @@ -164,17 +151,6 @@ def ldiff : ℕ → ℕ → ℕ :=

/-! bitwise ops -/

lemma bodd_bit (b n) : bodd (bit b n) = b := by
rw [bit_val]
simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false,
Bool.not_true, Bool.and_false, Bool.xor_false]
cases b <;> cases bodd n <;> rfl

lemma div2_bit (b n) : div2 (bit b n) = n := by
rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
<;> cases b
<;> decide

lemma shiftLeft'_add (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k
| 0 => rfl
| k + 1 => congr_arg (bit b) (shiftLeft'_add b m n k)
Expand Down Expand Up @@ -205,8 +181,14 @@ lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
/-! ### `boddDiv2_eq` and `bodd` -/


@[simp]
theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := rfl
set_option linter.deprecated false in
@[deprecated (since := "2024-10-22")]
theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := by
induction n with
| zero => rfl
| succ n ih =>
rw [boddDiv2, ih]
cases hn : n.bodd <;> simp [hn]

@[simp]
theorem div2_bit0 (n) : div2 (2 * n) = n :=
Expand Down
32 changes: 11 additions & 21 deletions Mathlib/Data/Nat/Bitwise.lean
Original file line number Diff line number Diff line change
Expand Up @@ -59,30 +59,24 @@ lemma bitwise_zero : bitwise f 0 0 = 0 := by
simp only [bitwise_zero_right, ite_self]

lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2)) := by
bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f n.div2 m.div2) := by
conv_lhs => unfold bitwise
have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
simp only [mod_two_of_bodd, cond]; cases bodd x <;> rfl
simp only [hn, hm, mod_two_iff_bod, ite_false, bit, two_mul, Bool.cond_eq_ite]
split_ifs <;> rfl
simp [hn, hm, mod_two_iff_bod, bit, div2_val, Nat.shiftLeft_succ, two_mul]

theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
(h : n ≠ 0) :
binaryRec z f n = bit_decomp n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n)) := by
cases n using bitCasesOn with
| h b n =>
rw [binaryRec_eq _ _ (by right; simpa [bit_eq_zero_iff] using h)]
generalize_proofs h; revert h
rw [bodd_bit, div2_bit]
simp
binaryRec z f n = n.bit_decomp ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]; rfl

@[simp]
lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by
conv_lhs => unfold bitwise
#adaptation_note /-- nightly-2024-03-16: simp was
-- simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, Bool.cond_eq_ite] -/
simp only [bit, ite_apply, Bool.cond_eq_ite]
simp only [bit_val, ite_apply, Bool.cond_eq_ite]
have h2 x : (x + x + 1) % 2 = 1 := by rw [← two_mul, add_comm]; apply add_mul_mod_self_left
have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
cases a <;> cases b <;> simp [h2, h4] <;> split_ifs
Expand Down Expand Up @@ -151,8 +145,7 @@ lemma bitwise_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool)
rw [← bit_ne_zero_iff] at ham hbn
simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit, ne_eq,
ite_false]
conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]
split_ifs with hf <;> rfl
conv_rhs => simp [bit, Bool.cond_eq_ite, Nat.shiftLeft_succ, two_mul]

lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
bitwise f =
Expand All @@ -168,8 +161,8 @@ lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
| z => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
| f yb y hyb =>
rw [← bit_ne_zero_iff] at hyb
simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, ← div2_val,
div2_bit, eq_rec_constant, ih]
simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
eq_rec_constant, ih]

theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n = 0 := by
induction' n using Nat.binaryRec with b n hn
Expand Down Expand Up @@ -241,12 +234,9 @@ theorem bitwise_swap {f : Bool → Bool → Bool} :
bitwise (Function.swap f) = Function.swap (bitwise f) := by
funext m n
simp only [Function.swap]
induction' m using Nat.strongRecOn with m ih generalizing n
cases' m with m
<;> cases' n with n
<;> try rw [bitwise_zero_left, bitwise_zero_right]
· specialize ih ((m+1) / 2) (div_lt_self' ..)
simp [bitwise_of_ne_zero, ih]
induction' m using Nat.binaryRec' with bm m hm ihm generalizing n; · simp
induction' n using Nat.binaryRec' with bn n hn; · simp
rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]

/-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
is also commutative. -/
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Data/Nat/Digits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -572,9 +572,9 @@ theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1
rw [bits_append_bit _ _ fun hn => absurd hn h]
cases b
· rw [digits_def' one_lt_two]
· simpa [Nat.bit]
· simpa [Nat.bit, pos_iff_ne_zero]
· simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
· simpa [bit_val]
· simpa [pos_iff_ne_zero, bit_eq_zero_iff]
· simpa [bit_val, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

/-! ### Modular Arithmetic -/

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/Nat/Fib/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1)) := by
· rintro (_|_) n' ih <;>
simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih,
congr_arg Prod.snd ih, Prod.mk.inj_iff] <;>
simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]
simp [bit_val, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]

theorem fast_fib_eq (n : ℕ) : fastFib n = fib n := by rw [fastFib, fast_fib_aux_eq]

Expand Down
6 changes: 2 additions & 4 deletions Mathlib/Data/Num/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ theorem ofNat'_succ : ∀ {n}, ofNat' (n + 1) = ofNat' n + 1 :=
cases b
· erw [ofNat'_bit true n, ofNat'_bit]
simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]
· rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
· rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit_val, mul_add],
ofNat'_bit, ofNat'_bit, ih]
simp only [cond, add_one, bit1_succ])

Expand Down Expand Up @@ -663,9 +663,7 @@ theorem ofNat'_eq : ∀ n, Num.ofNat' n = n :=
rw [ofNat'] at IH ⊢
rw [Nat.binaryRec_eq _ _ (.inl rfl), IH]
-- Porting note: `Nat.cast_bit0` & `Nat.cast_bit1` are not `simp` theorems anymore.
cases b <;> simp only [cond_false, cond_true, Nat.bit, two_mul, Nat.cast_add, Nat.cast_one]
· rw [bit0_of_bit0]
· rw [bit1_of_bit1]
cases b <;> simp [Nat.bit_val, two_mul, ← bit0_of_bit0, ← bit1_of_bit1]

theorem zneg_toZNum (n : Num) : -n.toZNum = n.toZNumNeg := by cases n <;> rfl

Expand Down
5 changes: 2 additions & 3 deletions Mathlib/Logic/Denumerable.lean
Original file line number Diff line number Diff line change
Expand Up @@ -126,9 +126,8 @@ set_option linter.deprecated false in
instance sum : Denumerable (α ⊕ β) :=
⟨fun n => by
suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some',
Option.mem_def, Sum.exists]
cases bodd n <;> simp [decodeSum, bit, encodeSum, Nat.two_mul]⟩
simp only [decodeSum, decode_eq_ofNat, Option.map_some', Option.mem_def, Sum.exists]
cases bodd n <;> simp [bit_val, encodeSum]⟩

section Sigma

Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Logic/Encodable/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -232,9 +232,9 @@ def encodeSum : α ⊕ β → ℕ

/-- Explicit decoding function for the sum of two encodable types. -/
def decodeSum (n : ℕ) : Option (α ⊕ β) :=
match boddDiv2 n with
| (false, m) => (decode m : Option α).map Sum.inl
| (_, m) => (decode m : Option β).map Sum.inr
match bodd n, div2 n with
| false, m => (decode m : Option α).map Sum.inl
| _, m => (decode m : Option β).map Sum.inr

/-- If `α` and `β` are encodable, then so is their sum. -/
instance _root_.Sum.encodable : Encodable (α ⊕ β) :=
Expand Down Expand Up @@ -284,7 +284,7 @@ theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none := by
rw [Nat.le_div_iff_mul_le]
exacts [h, by decide]
cases' exists_eq_succ_of_ne_zero (_root_.ne_of_gt this) with m e
simp only [decodeSum, boddDiv2_eq, div2_val]; cases bodd n <;> simp [e]
simp only [decodeSum, div2_val]; cases bodd n <;> simp [e]

noncomputable instance _root_.Prop.encodable : Encodable Prop :=
ofEquiv Bool Equiv.propEquivBool
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Logic/Equiv/Nat.lean
Original file line number Diff line number Diff line change
Expand Up @@ -25,9 +25,9 @@ variable {α : Type*}
@[simps]
def boolProdNatEquivNat : Bool × ℕ ≃ ℕ where
toFun := uncurry bit
invFun := boddDiv2
left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair, boddDiv2_eq]
right_inv n := by simp only [bit_decomp, boddDiv2_eq, uncurry_apply_pair]
invFun n := ⟨n.bodd, n.div2⟩
left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair]
right_inv n := by simp only [bit_decomp, uncurry_apply_pair]

/-- An equivalence between `ℕ ⊕ ℕ` and `ℕ`, by mapping `(Sum.inl x)` to `2 * x` and `(Sum.inr x)` to
`2 * x + 1`.
Expand Down