natToGray_testBit_false_of_ge

formal source

 181
 182/-! ## Injectivity of the BRGC path (no extra axioms) -/
 183
 184private lemma natToGray_testBit_false_of_ge {d n k : Nat} (hn : n < 2 ^ d) (hk : d ≤ k) :
 185    (natToGray n).testBit k = false := by
 186  -- natToGray n = n XOR (n >>> 1)
 187  have hn_lt : n < 2 ^ k := by
 188    have hpow : 2 ^ d ≤ 2 ^ k := by
 189      rcases lt_or_eq_of_le hk with hlt | rfl
 190      · exact le_of_lt (Nat.pow_lt_pow_right (by decide : 1 < (2 : Nat)) hlt)
 191      · rfl
 192    exact lt_of_lt_of_le hn hpow
 193  have hn_bit : n.testBit k = false := Nat.testBit_eq_false_of_lt hn_lt
 194  have hdiv_le : (n >>> 1) ≤ n := by
 195    -- shiftRight_eq_div_pow: n >>> 1 = n / 2
 196    simp [Nat.shiftRight_eq_div_pow, Nat.div_le_self]
 197  have hdiv_lt : (n >>> 1) < 2 ^ k := lt_of_le_of_lt hdiv_le hn_lt
 198  have hdiv_bit : (n >>> 1).testBit k = false := Nat.testBit_eq_false_of_lt hdiv_lt
 199  -- combine
 200  simp [natToGray, hn_bit, hdiv_bit]
 201
 202variable [GrayCodeFacts]
 203
 204theorem brgcPath_injective {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) : Function.Injective (brgcPath d) := by
 205  intro i j hij
 206  -- reduce to equality of the Nat Gray codes, then invert using `GrayCodeFacts.grayToNat_inverts_natToGray`.
 207  have hbits : ∀ k : Nat, (natToGray i.val).testBit k = (natToGray j.val).testBit k := by
 208    intro k
 209    by_cases hk : k < d
 210    · have := congrArg (fun p : Pattern d => p ⟨k, hk⟩) hij
 211      simpa [brgcPath, binaryReflectedGray, natToGray] using this
 212    · have hkge : d ≤ k := le_of_not_gt hk
 213      have hi0 : (natToGray i.val).testBit k = false :=
 214        natToGray_testBit_false_of_ge (d := d) (n := i.val) (k := k) i.isLt hkge