allOnes

formal source

  47
  48/-! ### Wrap-around step (last → 0) is one-bit adjacent (axiom-free) -/
  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