Cleanest way to compose arbitrary number of functions

Stream: new members

[Nicolò Cavalleri]

Suppose n : ℕ and that I have f : (fin n) → (α → α) and a : α. What is the cleanest way to write $f_{n-1}(f_{n-2}(...(f_0 a)....))$ in Lean?

[Arthur Paulino]

I would write it like f $ g $ h x

[Kevin Buzzard]

That only works for n=3 though

[Arthur Paulino]

Ah, n is an input of f. I got confused because you wrote it subscripted in LaTeX (as if you had those functions at hand).

In Lean 4, I would foldl on List.range n

[Arthur Paulino]

How do you provide an element of fin 0 though?

[Henrik Böving]

I would write something along the lines of

def composeN (f : Fin n → (α → α)) : α → α := Id.run do
  match h1:n with
  | 0 => id
  | m + 1 =>
    let mut fn := f 0
    for h2:idx in [1:n] do
      fn := f ⟨idx, by simp_all[(· ∈ ·)]⟩ ∘ fn
    fn

the List.range approach is annoying to work with because you would have to prove the bounds on the values inside List.range and I don't know whether we have built in lemmata for that. This works with a default Lean 4 installation.

[Henrik Böving]

Based on how you are writing the Fin type here you are probably asking a Lean 3 quesiton though and I have no clue about that. There the List.range approachw ith something along the lines of

def composeN (f : Fin n → (α → α)) : α → α :=
  let range := List.range n
  range.foldl (init := id) (fun acc elem => f ⟨elem, sorry⟩ ∘ acc)

should work out but I have no clue about the things you have available.

[Arthur Paulino]

This question is related: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/iterating.20over.20.60Fin.20n.60/near/314789036

[Martin Dvořák]

The following code works in Lean 3.
Unfortunately, I don't know how to typecast (fin 5) → (ℤ → ℤ) to list (ℤ → ℤ).

import data.matrix.notation

def g : (fin 5) → (ℤ → ℤ) := ![(λ a, a - 1), (λ a, a * a), (λ a, a * a), (λ a, a / 2), (λ a, a + 1)]
def g' : list (ℤ → ℤ) :=      [(λ a, a - 1), (λ a, a * a), (λ a, a * a), (λ a, a / 2), (λ a, a + 1)]

def chain {α : Type*} (f : list (α → α)) : α → α := list.foldl (∘) id f

#eval (g 0) $ (g 1) $ (g 2) $ (g 3) $ (g 4) 9

#eval chain g' 9

Both #evals return 624.

[Henrik Böving]

def functions : Fin 3 → (Nat → Nat)
| 2 => h
| 1 => g
| 0 => f

example : composeN functions = h ∘ g ∘ f := by
  simp[composeN, forIn', Std.Range.forIn', Std.Range.forIn'.loop, functions, Id.run]

formally verified :tm:

[Eric Wieser]

Martin Dvořák said:

Unfortunately, I don't know how to typecast (fin 5) → (ℤ → ℤ) to list (ℤ → ℤ).

docs#list.of_fn

[Eric Wieser]

There might be a nice way to use docs#fin.cons_induction here

[Martin Dvořák]

I updates my solution above. Thanks!

[Nicolò Cavalleri]

Thanks to all

[Nicolò Cavalleri]

I am surprised this is not in mathlib yet though as I would have guessed somebody should have needed this at some point

[Nicolò Cavalleri]

I wonder if it should be pushed

[Eric Wieser]

@Martin Dvořák, why not list.foldr to avoid the need to reverse?

[Eric Wieser]

I doubt this is very useful to have in mathlib; if you're working frequently with functions from a type to itself, you can use docs#function.End

def comp_n (f : fin n → function.End α) := (list.of_fn f).prod

[Martin Dvořák]

Eric Wieser said:

Martin Dvořák, why not list.foldr to avoid the need to reverse?

I can do (list.of_fn f).reverse.foldr (∘) id instead. But you probably meant something different, didn't you?

[Martin Dvořák]

(list.of_fn f).foldr (λ x, λ y, y ∘ x) id

[Martin Dvořák]

(list.of_fn f).foldl (λ x, λ y, y ∘ x) id

[Martin Dvořák]

These four functions seem (but I haven't really checked it) to do the same.

[Martin Dvořák]

Either I reverse the list, or I reverse the sides of the composition.

[Martin Dvořák]

There doesn't seem to be a difference for our purpose between these two:

@[simp] def foldl (f : α → β → α) : α → list β → α
| a []       := a
| a (b :: l) := foldl (f a b) l

@[simp] def foldr (f : α → β → β) (b : β) : list α → β
| []       := b
| (a :: l) := f a (foldr l)

[Martin Dvořák]

Eric Wieser said:

I doubt this is very useful to have in mathlib; if you're working frequently with functions from a type to itself, you can use docs#function.End

def comp_n (f : fin n → function.End α) := (list.of_fn f).prod

Why is it named after endomorphisms and not just general unary operations?

[Martin Dvořák]

Martin Dvořák said:

(list.of_fn f).foldl (λ x, λ y, y ∘ x) id

(list.of_fn f).foldl (flip (∘)) id