English
In a monadic setting, an auxiliary map over an array corresponds to a monadic go operation, up to a unit.
Русский
В моноидном контексте вспомогательное отображение через массив эквивалентно моноидной операции go, с единицей в качестве дополнения.
LaTeX
$$$$ \\mathrm{mapIdxMAux'}\\ f\\ (arr.size)\\ as = \\mathrm{mapIdxM.go}\\ f\\ as\\ arr \\; *> \\; \\mathrm{pure}\\ PUnit.\\,unit. $$$$
Lean4
theorem mapIdxMAux'_eq_mapIdxMGo {α} (f : ℕ → α → m PUnit) (as : List α) (arr : Array PUnit) :
mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit := by
induction as generalizing arr with
| nil => simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
| cons head tail
ih =>
simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind, bind_pure_unit, LawfulMonad.bind_assoc,
pure_bind, mapIdxM.go]
generalize (f (Array.size arr) head) = head
have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
rw [← this, ih]
simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]
