allOnes_testBit_eq_false_at

formal source

 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
 118      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1)) (by decide)⟩
 119  have hw : OneBitDiff (brgcPath (t + 1) iLast) (brgcPath (t + 1) 0) := by
 120    refine ⟨Fin.last t, ?_, ?_⟩
 121    · -- show the last bit differs (it is true at iLast, false at 0)
 122      have ht_true : (natToGray iLast.val).testBit t = true := by
 123        -- compute `natToGray (allOnes (t+1))` at bit t: true XOR false = true
 124        have hn : iLast.val = allOnes (t + 1) := rfl
 125        have hshift : (iLast.val >>> 1) = allOnes t := by
 126          -- `allOnes (t+1) = bit true (allOnes t)` ⇒ shiftRight 1 yields `allOnes t`
 127          have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
 128          -- use `bit_shiftRight_one`
 129          have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
 130          simpa [hn, hrepr] using this
 131        -- now compute testBit of xor
 132        -- n.testBit t = true (all ones), (n>>>1).testBit t = false
 133        have hnbit : (iLast.val).testBit t = true := by