gray8At_injective

formal source

 106def grayCycle3Path : Fin 8 → Pattern 3 :=
 107  fun i => pattern3 (gray8At i)
 108
 109theorem gray8At_injective : Function.Injective gray8At := by
 110  intro i j h
 111  -- brute-force on the 8 cases
 112  fin_cases i <;> fin_cases j <;> cases h <;> rfl
 113
 114/-! ## A small helper: 3-bit patterns can be re-encoded as a Nat in [0,8) -/
 115
 116/-- Convert a 3-bit pattern to a Nat by the usual binary expansion. -/
 117def toNat3 (p : Pattern 3) : ℕ :=
 118  (if p ⟨0, by decide⟩ then 1 else 0) +
 119  (if p ⟨1, by decide⟩ then 2 else 0) +
 120  (if p ⟨2, by decide⟩ then 4 else 0)
 121
 122lemma toNat3_pattern3 (w : Fin 8) : toNat3 (pattern3 w) = w.val := by
 123  -- Only 8 cases; compute directly.
 124  fin_cases w <;> decide
 125
 126theorem pattern3_injective : Function.Injective pattern3 := by
 127  intro a b hab
 128  apply Fin.ext
 129  have hNat : toNat3 (pattern3 a) = toNat3 (pattern3 b) := congrArg toNat3 hab
 130  simpa [toNat3_pattern3] using hNat
 131
 132theorem grayCycle3_injective : Function.Injective grayCycle3Path := by
 133  intro i j hij
 134  have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij)
 135  exact gray8At_injective h0
 136
 137theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by
 138  classical
 139  -- card(Fin 8) = 8