English
If there exist codes cf and cg realizing f and g respectively for all inputs, then there exists a code c realizing the composition of g and f: c.eval on v equals the monadic pure of the concatenation of the outputs obtained by first applying g to v for all i and then applying f to the resulting data.
Русский
Если существуют коды cf и cg, реализующие f и g соответственно на входах, то существует код c, реализующий композицию g ∘ f: c.eval(v) = pure((List.Vector.mOfFn i => g i v) >>= f).
LaTeX
$$$\\exists c. \\forall v. c.eval(v) = \\operatorname{pure}\\big((\\mathrm{List}.Vector.mOfFn(\\lambda i. g\\ i\\ v)) \\\\bind f\\big)$$$
Lean4
theorem comp {m n} {f : List.Vector ℕ n →. ℕ} {g : Fin n → List.Vector ℕ m →. ℕ}
(hf : ∃ c : Code, ∀ v : List.Vector ℕ n, c.eval v.1 = pure <$> f v)
(hg : ∀ i, ∃ c : Code, ∀ v : List.Vector ℕ m, c.eval v.1 = pure <$> g i v) :
∃ c : Code, ∀ v : List.Vector ℕ m, c.eval v.1 = pure <$> ((List.Vector.mOfFn fun i => g i v) >>= f) :=
by
rsuffices ⟨cg, hg⟩ : ∃ c : Code, ∀ v : List.Vector ℕ m, c.eval v.1 = Subtype.val <$> List.Vector.mOfFn fun i => g i v
· obtain ⟨cf, hf⟩ := hf
exact
⟨cf.comp cg, fun v => by
simp [hg, hf, map_bind]
rfl⟩
clear hf f
induction n with
| zero => exact ⟨nil, fun v => by simp [Vector.mOfFn]; rfl⟩
| succ n IH =>
obtain ⟨cg, hg₁⟩ := hg 0
obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
exact
⟨cons cg cl, fun v => by
simp [Vector.mOfFn, hg₁, map_bind, hl]
rfl⟩
