apply function n times

Stream: Is there code for X?

[Bernd Losert]

Is there a tactic that can take an n : ℕ, f : α → β, and x : α and produce f (f ... (f x)...), where f appears n times.

[Bernd Losert]

(deleted)

[Kevin Buzzard]

There's docs#nat.iterate (assuming you mean f : α → α) -- why do you need a tactic?

[Bernd Losert]

I can't use iterate because f is polymorphic and each application of f produce different types.

[Bernd Losert]

For example, suppose f is functor.map.

[Kevin Buzzard]

If the codomain and domain of f are different then I can make no sense of your question. What do the ... mean in your first post?

[Yaël Dillies]

How do you know that the n + 1-th application will be polymorphic enough to accept the n-th output?

[Bernd Losert]

A more concrete example:

constant xs : list (list (list nat))
constant f : nat → string

def ex : list (list (list string)) := list.map (list.map (list.map f)) xs

[Bernd Losert]

I want a tactic where I can write something like (iterate 3 list.map f) xs

[Mario Carneiro]

iterate 3 { apply list.map f }, exact xs?

[Bernd Losert]

What isiterate in that line of code?

[Yaël Dillies]

docs#tactic.interactive.iterate

[Bernd Losert]

Ah, OK. I tried

def ex : list (list (list string)) := begin
   iterate 3 { apply list.map f }, exact xs
end

but it complains about apply.

[Mario Carneiro]

actually you aren't applying directly to the goal in that example so you have to modify it a bit

def ex : list (list (list string)) := begin
  have := xs, revert this,
  iterate 3 { apply list.map }, exact f
end

[Bernd Losert]

Nice. I tried the following, but it does not work:

noncomputable def ex (n : ℕ) : nat.iterate list n string := begin
  have := xs, revert this,
  iterate n { apply list.map }, exact f
end

[Reid Barton]

what's the type of xs here?

[Bernd Losert]

Oops. I forgot to change that one.

[Reid Barton]

the way you're mixing the levels doesn't make sense here, you should just be able to use induction on n though

[Bernd Losert]

Let me try again.

[Reid Barton]

I feel like the answers involving the iterate tactic were possibly misleading, but then, it's also quite unclear what you want to do or why

[Bernd Losert]

Here you go:

def ex (n : ℕ) (f : nat → string) (xs : nat.iterate list n nat) : nat.iterate list n string := begin
  have := xs, revert this,
  iterate n { apply list.map }, exact f
end

[Reid Barton]

I guess you should move all arguments (except optionally f) to the right of the colon and use recursion

[Bernd Losert]

That's a good idea actually. But why does it not work with the iterate tactic. Does that tactic only work with hard-code n?

[Reid Barton]

Right, it just doesn't make sense

[Reid Barton]

iterate needs to know how many times to run the body, that number cannot be an internal variable

[Bernd Losert]

Bummer... Oh well.

[Reid Barton]

There is a phase distinction here

[Bernd Losert]

What do you mean by "phase"?

[Reid Barton]

e.g. compile-time vs run-time

[Reid Barton]

The tactic runs before the function itself (notionally) runs. So n doesn't refer to anything when the tactic executes, it's literally just the letter "n".

[Reid Barton]

It's like C macros, you cannot have a program expand a macro n times where n is a number the program read from stdin, because the macro expansion already had to be finished long ago

[Reid Barton]

In Lean it would make even less sense because the tactic block could be constructing a proof, and proofs don't even run at all.

[Bernd Losert]

Yes, that makes sense. For some reason, I thought I could get away with doing this sort of thing in Lean. I have come across this limitation with other macro systems. I guess this is a fundametal issue with macros in general.

[Bernd Losert]

So, I trying this, but I'm getting errors that I don't know how to fix:

def ex (f : nat → string) : ∀ n, (list^[n] nat) → (list^[n] string)
| (0) (n) := f n
| (n + 1) ([]) := []
| (n + 1) (list.cons m ms) := sorry,

[Reid Barton]

Hmm, I think nat.iterate is defined inconveniently for this purpose

[Reid Barton]

You would prefer to have list^[n+1] nat = list (list^[n] nat)

[Bernd Losert]

OK. Let me define my own nat.iterate then and see if that helps.

[Reid Barton]

Maybe you can also work with this definition by also generalizing over the types nat and string and the function f, and writing something like | (n + 1) f xs := ex n (list.map f) xs

[Reid Barton]

I feel like one of these is less efficient than the other, but I'm not sure which or whether that matters to you.

[Bernd Losert]

Progress!

def iter (f : α → α) : ∀ n : ℕ, α → α
| 0 := id
| (n + 1) := λ a, f (iter n a)

def ex (f : ℕ → string) : ∀ n : ℕ, (iter list n nat) → (iter list n string)
| (0) n := f n
| (n + 1) [] := []
| (n + 1) (m :: ms) := ex n m :: list.map (ex n) ms

[Reid Barton]

You should be able to use list.map in the (n + 1) case without doing a case split on the list as well.

[Bernd Losert]

Good catch. Thanks a lot.

[Bernd Losert]

If I have a proof of list^[n+1] nat = list (list^[n] nat), could I use that with the nat.iterate version somehow?

[Bernd Losert]

So I tried to generalize the ex example, but it doesn't work:

variables {α β : Type u}
variable {f : Type u → Type u}

def iter (f : α → α) : ∀ n : ℕ, α → α
| 0 := id
| (n + 1) := λ a, f (iter n a)

def map [functor f] (m : α → β) : ∀ n, iter f n α → iter f n β
| 0 val := m val
| (n + 1) val := functor.map (map n) val

[Reid Barton]

It's probably not obvious to Lean what functor you want to map until you unfold iter

[Bernd Losert]

Yes. Should I pass the functor f instance to functor.map?

[Bernd Losert]

Yeah, that works.