Can this be done without mutual recursion?

Stream: Is there code for X?

[Ching-Tsun Chou]

Is it possible to define the function oneStep below without using mutual recursion? Informally speaking, oneStep f (n+1) is the result of applying f to the concatenation of oneStep f 0, ..., oneStep f n. I can't figure out a way to produce that concatenation without mutual recursion.

variable {α : Type*}

mutual
  def oneStep (f : List α → List α) : ℕ → List α
    | 0 => f []
    | n + 1 => f (cumSteps f n)

  def cumSteps (f : List α → List α) : ℕ → List α
    | 0 => oneStep f 0
    | n + 1 => cumSteps f n ++ oneStep f (n + 1)
end

[Kenny Lau]

import Mathlib

variable {α : Type*}

def oneStep (f : List α → List α) : ℕ → List α
  | n => f (List.flatten <| (List.finRange n).map fun i : Fin n ↦ oneStep f i)

[Ching-Tsun Chou]

The same idea also occurred to me just after I posed the question. But your solution is more elegant.

def oneStep (f : List α → List α) : ℕ → List α
  | 0 => f []
  | n + 1 => f (List.ofFn (fun k : Fin (n + 1) ↦ oneStep f k)).flatten

[Aaron Liu]

I don't like these solutions because they don't reduce

[Ching-Tsun Chou]

Any better ideas?

[Ching-Tsun Chou]

BTW, I like @Kenny Lau's solution because it does not use recursion at all involve case split.

[Aaron Liu]

It definitely does use recursion

[Aaron Liu]

We call oneStep from inside itself

[Ching-Tsun Chou]

Sorry, I misspoke. I really meant to say that it does not involve a case split.

[Kenny Lau]

import Mathlib

variable {α : Type*}

def oneStep (f : List α → List α) : ℕ → List α :=
  fun n ↦ (aux n).2 where
  -- n ↦ (oneStep f 0 ++ oneStep f 1 ++ .. ++ oneStep f (n - 1), oneStep f n)
  aux : ℕ → List α × List α
  | 0 => ([], f [])
  | n+1 => match aux n with | (a, b) => (a ++ b, f (a ++ b))

variable (f : List α → List α)

example : oneStep f 3 = f (oneStep f 0 ++ oneStep f 1 ++ oneStep f 2) := rfl

[Ching-Tsun Chou]

In my real application, the function f involves a Classical.choose and Kenny's first solution turns out to be more convenient.

[Aaron Liu]

Kenny Lau said:

import Mathlib

variable {α : Type*}

def oneStep (f : List α → List α) : ℕ → List α
  | n => f (List.flatten <| (List.finRange n).map fun i : Fin n ↦ oneStep f i)

Instead of using List.flatten with List.map, does List.flatMap work?