aggCoeff_append

formal source

 365  simp only [h_filter_empty, List.filter_nil, List.map_nil, List.sum_nil]
 366
 367/-- Aggregation distributes over concatenation of move lists. -/
 368lemma aggCoeff_append (xs ys : List MicroMove) (pair : ℕ) (prim : Primitive) :
 369    aggCoeff (xs ++ ys) pair prim = aggCoeff xs pair prim + aggCoeff ys pair prim := by
 370  classical
 371  unfold aggCoeff
 372  simp only [List.filter_append, List.map_append, List.sum_append]
 373
 374/-- Aggregation over a flat-mapped list of row moves. -/
 375theorem aggCoeff_flatMap (nf : NormalForm) (pair : ℕ) (prim : Primitive)
 376    (l : List ℕ) (hl : l.Nodup) :
 377    aggCoeff (l.flatMap (rowMoves nf)) pair prim
 378      = if pair ∈ l then aggCoeff (rowMoves nf pair) pair prim else 0 := by
 379  induction l with
 380  | nil =>
 381    simp only [List.flatMap_nil, List.not_mem_nil, ↓reduceIte]
 382    unfold aggCoeff
 383    simp
 384  | cons h t ih =>
 385    simp only [List.flatMap_cons]
 386    rw [aggCoeff_append]
 387    have hnodup_t : t.Nodup := hl.of_cons
 388    have h_not_mem : h ∉ t := hl.not_mem
 389    by_cases hpair : pair = h
 390    · -- pair = h: contribution comes from rowMoves nf h, and pair ∉ t (since h ∉ t)
 391      subst hpair
 392      simp only [List.mem_cons, true_or, ↓reduceIte]
 393      have h_pair_not_in_t : pair ∉ t := h_not_mem
 394      rw [ih hnodup_t]
 395      simp only [h_pair_not_in_t, ↓reduceIte, add_zero]
 396    · -- pair ≠ h: contribution from rowMoves nf h is 0
 397      have h_ne : h ≠ pair := Ne.symm hpair
 398      rw [aggCoeff_rowMoves_of_ne nf h_ne]