theorem
proved
tactic proof
brgcPath_injective
show as:
view Lean formalization →
formal statement (Lean)
204theorem brgcPath_injective {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) : Function.Injective (brgcPath d) := by
proof body
Tactic-mode proof.
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
215 have hj0 : (natToGray j.val).testBit k = false :=
216 natToGray_testBit_false_of_ge (d := d) (n := j.val) (k := k) j.isLt hkge
217 simp [hi0, hj0]
218 have hgray : natToGray i.val = natToGray j.val := by
219 exact Nat.eq_of_testBit_eq hbits
220 -- show both indices are < 2^64
221 have hpow : 2 ^ d ≤ 2 ^ 64 := Nat.pow_le_pow_right (by decide : 0 < (2 : Nat)) hd
222 have hi64 : i.val < 2 ^ 64 := lt_of_lt_of_le i.isLt hpow
223 have hj64 : j.val < 2 ^ 64 := lt_of_lt_of_le j.isLt hpow
224 have hi_inv : GrayCodeAxioms.grayInverse (natToGray i.val) = i.val :=
225 GrayCodeFacts.grayToNat_inverts_natToGray (n := i.val) hi64
226 have hj_inv : GrayCodeAxioms.grayInverse (natToGray j.val) = j.val :=
227 GrayCodeFacts.grayToNat_inverts_natToGray (n := j.val) hj64
228 have : i.val = j.val := by
229 have := congrArg GrayCodeAxioms.grayInverse hgray
230 simpa [hi_inv, hj_inv] using this
231 exact Fin.ext this
232