Zulip Chat Archive

Stream: new members

Topic: Repeat N times


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Mar 11 2021 at 12:09):

The better way is to write a calc block!

view this post on Zulip 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.

view this post on Zulip Marcus Rossel (Mar 11 2021 at 12:14):

(deleted)

view this post on Zulip 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?

view this post on Zulip Anne Baanen (Mar 11 2021 at 12:28):

You're probably looking for tactic#iterate

view this post on Zulip 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

view this post on Zulip Marcus Rossel (Mar 11 2021 at 12:37):

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

view this post on Zulip 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.

view this post on Zulip 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: May 17 2021 at 23:14 UTC