NormalForm

formal source

  44namespace MicroMove
  45
  46/-- Canonical micro-move normal form: coefficient table with finite support. -/
  47@[ext]
  48structure NormalForm where
  49  supportPairs : Finset ℕ
  50  coeff : ℕ → Primitive → ℝ
  51  zero_outside : ∀ {pair prim}, pair ∉ supportPairs → coeff pair prim = 0
  52  nontrivial : ∀ {pair}, pair ∈ supportPairs → ∃ prim, coeff pair prim ≠ 0
  53
  54namespace NormalForm
  55
  56/-- Canonical ordered list of supported pairs (ascending). -/
  57noncomputable def pairList (nf : NormalForm) : List ℕ :=
  58  nf.supportPairs.sort (· ≤ ·)
  59
  60lemma pairList_mem {nf : NormalForm} {pair : ℕ} :
  61    pair ∈ pairList nf ↔ pair ∈ nf.supportPairs := by
  62  unfold pairList
  63  simp only [mem_sort]
  64
  65lemma pairList_nodup (nf : NormalForm) : (pairList nf).Nodup := by
  66  unfold pairList
  67  simp only [sort_nodup]
  68
  69/-- Micro-moves for a single pair. -/
  70noncomputable def rowMoves (nf : NormalForm) (pair : ℕ) : List MicroMove :=
  71  primitiveOrderList.filterMap (fun prim =>
  72    if nf.coeff pair prim = 0 then none
  73    else some ⟨pair, prim, nf.coeff pair prim⟩)
  74
  75/-- Canonical ordered list of micro-moves. -/
  76noncomputable def toMoves (nf : NormalForm) : List MicroMove :=
  77  (pairList nf).flatMap (rowMoves nf)