## Stream: new members

### Topic: Repeat N times

#### Marcus Rossel (Mar 11 2021 at 12:02):

Is there a way to repeat a tactic N times? I need to prove a chain of transitivity with 6 steps, and currently have:

begin
transitivity, exact step_1,
transitivity, exact step_2,
...
transitivity, exact step_6
end


I would like to write something like:

begin
repeat 6 { transitivity },
exact step_1, exact step_2, ... exact step_6,
end


Or is there some better way to do this?

#### Scott Morrison (Mar 11 2021 at 12:09):

The better way is to write a calc block!

#### Scott Morrison (Mar 11 2021 at 12:09):

I don't think there is such a repeat_at_most tactic at the moment, although if there isn't it would be easy (and helpful) to add.

(deleted)

#### Marcus Rossel (Mar 11 2021 at 12:18):

Is there a way to keep the intermediate terms implicit?
So for:

calc a = b : H1
...    = c : H2
...    = d : H3


... is there a way I can only write H1, H2, H3 and have Lean infer b, c, d?

#### Anne Baanen (Mar 11 2021 at 12:28):

You're probably looking for tactic#iterate

#### Anne Baanen (Mar 11 2021 at 12:30):

Or to apply it up to 6 times, rather than exactly, you can do iterate 6 { try { ... } }:

import tactic

example (f : ℕ →+ ℕ) : f (f (f 0)) = 0 :=
by iterate 2 { rw f.map_zero } -- unsolved goal: f 0 = 0

example (f : ℕ →+ ℕ) : f (f (f 0)) = 0 :=
by iterate 3 { rw f.map_zero } -- works

example (f : ℕ →+ ℕ) : f (f (f 0)) = 0 :=
by iterate 4 { rw f.map_zero } -- match failed

example (f : ℕ →+ ℕ) : f (f (f 0)) = 0 :=
by iterate 4 { try { rw f.map_zero } } -- works


#### Marcus Rossel (Mar 11 2021 at 12:37):

Yes! This is exactly what I need. Thanks :)

#### Scott Morrison (Mar 11 2021 at 12:42):

In a calc block you can write _ in places (e.g. instead of the b, c, d), but it does lessen the readability.

#### Mario Carneiro (Mar 11 2021 at 16:33):

There is docs#tactic.iterate_at_most, but it's not exposed as an interactive tactic

Last updated: Dec 20 2023 at 11:08 UTC