allOnes_testBit_lt

formal source

  84          simpa using hR.symm
  85  exact Nat.add_right_cancel h
  86
  87private lemma allOnes_testBit_lt : ∀ {t k : Nat}, k < t → (allOnes t).testBit k = true
  88  | 0, _, hk => (Nat.not_lt_zero _ hk).elim
  89  | (t + 1), 0, _ => by
  90      -- `allOnes (t+1) = bit true (allOnes t)`
  91      have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
  92      simpa [hrepr] using (Nat.testBit_bit_zero true (allOnes t))
  93  | (t + 1), (k + 1), hk => by
  94      have hk' : k < t := Nat.lt_of_succ_lt_succ hk
  95      have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
  96      -- shift the bit index down one using `testBit_bit_succ`
  97      have hshift :
  98          (allOnes (t + 1)).testBit (k + 1) = (allOnes t).testBit k := by
  99        simpa [hrepr] using (Nat.testBit_bit_succ (b := true) (n := allOnes t) (m := k))
 100      -- now finish by IH
 101      simpa [hshift] using (allOnes_testBit_lt (t := t) (k := k) hk')
 102
 103private lemma allOnes_testBit_eq_false_at (t : Nat) : (allOnes t).testBit t = false := by
 104  -- `allOnes t < 2^t`
 105  have hlt : allOnes t < 2 ^ t := by
 106    -- `2^t - 1 < 2^t` since `2^t > 0`
 107    simpa [allOnes] using Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) t) (by decide : 0 < 1)
 108  exact Nat.testBit_eq_false_of_lt hlt
 109
 110theorem brgc_wrap_oneBitDiff {d : Nat} (hdpos : 0 < d) :
 111    OneBitDiff (brgcPath d ⟨2 ^ d - 1, by
 112      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩) (brgcPath d 0) := by
 113  classical
 114  rcases Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hdpos) with ⟨t, rfl⟩
 115  -- d = t+1, unique differing bit is the last one (value t)
 116  let iLast : Fin (2 ^ (t + 1)) :=
 117    ⟨2 ^ (t + 1) - 1, by