Repeat N times

Stream: new members

[Marcus Rossel]

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]

The better way is to write a calc block!

[Scott Morrison]

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.

[Marcus Rossel]

(deleted)

[Marcus Rossel]

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]

You're probably looking for tactic#iterate

[Anne Baanen]

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]

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

[Scott Morrison]

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]

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