theorem
proved
tactic proof
brgc_wrap_oneBitDiff
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
134 -- t < t+1
135 have : t < t + 1 := Nat.lt_succ_self t
136 simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := t) this
137 have hmbit : (iLast.val >>> 1).testBit t = false := by
138 -- iLast>>>1 = allOnes t, and that has bit t = false
139 simpa [hshift] using allOnes_testBit_eq_false_at t
140 -- combine via xor
141 simp [natToGray, hnbit, hmbit]
142 -- translate to the Pattern statement
143 have : brgcPath (t + 1) iLast (Fin.last t) ≠ brgcPath (t + 1) 0 (Fin.last t) := by
144 -- right side is false, left side is true
145 have h0 : brgcPath (t + 1) 0 (Fin.last t) = false := by
146 simp [brgcPath, binaryReflectedGray, natToGray]
147 have h1 : brgcPath (t + 1) iLast (Fin.last t) = true := by
148 simpa [brgcPath, binaryReflectedGray] using ht_true
149 simpa [h0, h1]
150 simpa using this
151 · intro j hj
152 -- any differing index must be the last one (all other bits are equal/false)
153 induction j using Fin.lastCases with
154 | last => rfl
155 | cast j =>
156 -- show contradiction: at castSucc j, both patterns are false
157 have hjlt : (j.val : Nat) < t := j.isLt
158 -- compute natToGray at bit j.val: true XOR true = false (since both allOnes have ones there)
159 have hfalse : brgcPath (t + 1) iLast j.castSucc = false := by
160 -- n = allOnes(t+1), m = n>>>1 = allOnes t
161 have hn : iLast.val = allOnes (t + 1) := rfl
162 have hnbit : (iLast.val).testBit j.val = true := by
163 have : j.val < t + 1 := Nat.lt_succ_of_lt hjlt
164 simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := j.val) this
165 have hshift : (iLast.val >>> 1) = allOnes t := by
166 have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
167 have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
168 simpa [hn, hrepr] using this
169 have hmbit : (iLast.val >>> 1).testBit j.val = true := by
170 simpa [hshift, allOnes] using allOnes_testBit_lt (t := t) (k := j.val) hjlt
171 have : (natToGray iLast.val).testBit j.val = false := by
172 simp [natToGray, hnbit, hmbit]
173 simpa [brgcPath, binaryReflectedGray] using this
174 have h0 : brgcPath (t + 1) 0 j.castSucc = false := by
175 simp [brgcPath, binaryReflectedGray, natToGray]
176 have : False := by
177 -- hj says they differ, but both patterns are false
178 simpa [hfalse, h0] using hj
179 exact this.elim
180 simpa [iLast] using hw
181
182/-! ## Injectivity of the BRGC path (no extra axioms) -/
183