Zulip Chat Archive

Stream: general

Topic: is it possible to "loop" the same thing?


view this post on Zulip eax (Feb 28 2021 at 01:58):

for example if I'm trying to prove lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b :=

rw zero_mul,
rw zero_mul,
rw zero_mul,
refl,```
gets the base case; but I'd really just like to say `apply zero_mul repeatedly until you can't` ?

view this post on Zulip Bryan Gin-ge Chen (Feb 28 2021 at 02:01):

There's tactic#repeat, (I think it may be covered later in the Natural Number Game).

view this post on Zulip Bryan Gin-ge Chen (Feb 28 2021 at 02:01):

I also often use simp only [zero_mul] for a bunch of repeated rewrites.

view this post on Zulip eax (Feb 28 2021 at 02:03):

thanks! the whole tactic library is generally useful (I was looking for it); that said if the game teaches it I'll just wait until I get there too

view this post on Zulip eax (Feb 28 2021 at 02:03):

in the meantime its hard enough to re-learn the basics of proofs using peano axioms while also learning lean :-p


Last updated: May 18 2021 at 16:25 UTC