grayCycle3_oneBit_step

formal source

 154theorem grayCycle3_surjective : Function.Surjective grayCycle3Path :=
 155  (grayCycle3_bijective).2
 156
 157theorem grayCycle3_oneBit_step : ∀ i : Fin 8, OneBitDiff (grayCycle3Path i) (grayCycle3Path (i + 1)) := by
 158  intro i
 159  -- 8 explicit cases; each step flips exactly one of the three bits.
 160  fin_cases i
 161  · -- 0 -> 1 (flip bit 0)
 162    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 163    · simp [grayCycle3Path, gray8At, pattern3]
 164    · intro k hk
 165      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 166  · -- 1 -> 3 (flip bit 1)
 167    refine ⟨⟨1, by decide⟩, ?_, ?_⟩
 168    · simp [grayCycle3Path, gray8At, pattern3]
 169    · intro k hk
 170      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 171  · -- 2 -> 3?  (i=2 means gray8At 2 = 3, next is gray8At 3 = 2; flip bit 0)
 172    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 173    · simp [grayCycle3Path, gray8At, pattern3]
 174    · intro k hk
 175      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 176  · -- i=3: 2 -> 6 (flip bit 2)
 177    refine ⟨⟨2, by decide⟩, ?_, ?_⟩
 178    · simp [grayCycle3Path, gray8At, pattern3]
 179    · intro k hk
 180      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 181  · -- i=4: 6 -> 7 (flip bit 0)
 182    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 183    · simp [grayCycle3Path, gray8At, pattern3]
 184    · intro k hk
 185      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 186  · -- i=5: 7 -> 5 (flip bit 1)
 187    refine ⟨⟨1, by decide⟩, ?_, ?_⟩