lemma
proved
allOnes_succ_eq_bit
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Patterns.GrayCycleGeneral on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
49
50private def allOnes (d : Nat) : Nat := 2 ^ d - 1
51
52private lemma allOnes_succ_eq_bit (t : Nat) :
53 allOnes (t + 1) = Nat.bit true (allOnes t) := by
54 have hpos1 : 1 ≤ 2 ^ (t + 1) := Nat.succ_le_of_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1))
55 have hpos0 : 1 ≤ 2 ^ t := Nat.succ_le_of_lt (pow_pos (by decide : 0 < (2 : Nat)) t)
56 -- LHS + 1
57 have hL : allOnes (t + 1) + 1 = 2 ^ (t + 1) := by
58 simp [allOnes, Nat.sub_add_cancel hpos1]
59 -- RHS + 1
60 have hR : Nat.bit true (allOnes t) + 1 = 2 ^ (t + 1) := by
61 have hge : 2 ≤ 2 * (2 ^ t) := by
62 have h1 : 1 ≤ 2 ^ t := Nat.one_le_pow t 2 (by decide : 0 < (2 : Nat))
63 -- multiply the inequality by 2
64 simpa using (Nat.mul_le_mul_left 2 h1)
65 calc
66 Nat.bit true (allOnes t) + 1
67 = (2 * (allOnes t) + 1) + 1 := by simp [Nat.bit_val, Nat.add_assoc]
68 _ = 2 * (allOnes t) + 2 := by
69 simp [Nat.add_assoc]
70 _ = 2 * (2 ^ t - 1) + 2 := by
71 simp [allOnes]
72 _ = (2 * (2 ^ t) - 2) + 2 := by
73 -- distribute `2 * (a - 1)` and simplify
74 simp [Nat.mul_sub_left_distrib, Nat.mul_one, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm,
75 Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
76 _ = 2 * (2 ^ t) := Nat.sub_add_cancel hge
77 _ = 2 ^ (t + 1) := by
78 -- `2^(t+1) = 2^t * 2`
79 simp [pow_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
80 have h : allOnes (t + 1) + 1 = Nat.bit true (allOnes t) + 1 := by
81 calc
82 allOnes (t + 1) + 1 = 2 ^ (t + 1) := hL