def
definition
pattern3
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Patterns.GrayCycle on GitHub at line 82.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
79-/
80
81/-- Convert a `Fin 8` codeword into a 3-bit pattern via `testBit`. -/
82def pattern3 : Fin 8 → Pattern 3
83| ⟨0, _⟩ => fun _ => false
84| ⟨1, _⟩ => fun j => decide (j.val = 0)
85| ⟨2, _⟩ => fun j => decide (j.val = 1)
86| ⟨3, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 1)
87| ⟨4, _⟩ => fun j => decide (j.val = 2)
88| ⟨5, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 2)
89| ⟨6, _⟩ => fun j => decide (j.val = 1 ∨ j.val = 2)
90| ⟨7, _⟩ => fun _ => true
91
92/-- Canonical 3-bit Gray order as a function `Fin 8 → Fin 8`.
93
94Sequence: [0,1,3,2,6,7,5,4]. -/
95def gray8At : Fin 8 → Fin 8
96| ⟨0, _⟩ => 0
97| ⟨1, _⟩ => 1
98| ⟨2, _⟩ => 3
99| ⟨3, _⟩ => 2
100| ⟨4, _⟩ => 6
101| ⟨5, _⟩ => 7
102| ⟨6, _⟩ => 5
103| ⟨7, _⟩ => 4
104
105/-- The 3-bit Gray-cycle path (period 8). -/
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