infinite loop

Stream: new members

[Raffaele Rossi]

Hi all, I'm new to Lean and I'm going through the Number Game. At level 6/13 of Advanced Addition World, I noticed that given the hypothesis h: t+a=t+b if you type repeat {rw add_comm at h} it gets stuck an infinite loop :) Is this "intended" or ideally lean should detect and abort with a failure?

[Kenny Lau]

do you have a solution to the halting problem?

[Raffaele Rossi]

this is not a halting problem, this is just detecting that you've come back to the current state.

[Kenny Lau]

that would make the tactic slower

[Kenny Lau]

tactics are tools, not magic algorithms that prove every theorem

[Raffaele Rossi]

only the repeat tactic, though

[Raffaele Rossi]

of course it's a tool, I did not ask for a magic wand. Just that if I say repeat {x} it could, conceptually, determine that it's going round an infinite loop

[Raffaele Rossi]

and it makes sense to slow down only the repeat tactic in this case

[Reid Barton]

That's not what repeat is defined to do, but also it's generally not that useful to detect loops anyways--what would it do if it detects one?

[Kenny Lau]

right, why not just use iterate n { rw foo } if you know it will be in a loop

[Raffaele Rossi]

I did not know about iterate

[Raffaele Rossi]

I'm literally just at level 6/13 of that world

[Reid Barton]

Oh, you said raise an error--but I think that's too expensive in the non-erroring case, and usually it's pretty obvious where the problem is if you just added repeat { foo } to your proof and Lean starts taking a long time

[Jalex Stark]

So to answer your original question, this is intended behavior

[Jalex Stark]

there are in fact smarter tactics that can figure out how to apply commutativity,

[Jalex Stark]

but the point of the natural number game is to learn how to do things without them :)

[Kenny Lau]

well I understand where you are coming from

[Kenny Lau]

the NNG is marketed as a game

[Reid Barton]

The original example isn't a good use of repeated rw anyways because the first rewrite will change t+a=t+b to a+t=t+b and the second one will change it back to t+a=t+b.

[Kenny Lau]

so in a game I would expect rw to have loop detection feature I guess

[Kevin Buzzard]

You mean repeat? I can just remove it if you like :-) Or replace with iterate 37, that should be enough for everyone

[Kevin Buzzard]

A few months ago the user would lose all their progress if they did this :-/

[Raffaele Rossi]

yeah so far the game did not mention iterate although even if it did I am sure I would have not used it :) was just food for thoughts and I understand this might have been a very trivial example that in real practice would not even actually happen

[Raffaele Rossi]

but I like that this community is very active

[Jalex Stark]

i would probably have had a better time with the nng my first time if repeat were a synonym for iterate 37 or maybe just iterate 3

[Jasmin Blanchette]

One can see that you guys aren't computer scientists. ;)

[Jalex Stark]

yes, the computer scientist's version of the nng might have ~none of the overrides that kevin made. thankfully the computer scientists have less trouble installing lean locally and playing more faithful tutorials

[Mario Carneiro]

I think repeat is actually defined as iterate 100000

[Yury G. Kudryashov]

I don't see 100000 in src#tactic.repeat

[Jalex Stark]

yeah it looks like it's a plain old infinite loop

[Mario Carneiro]

It appears that the definition of repeat has changed since my recollection. It has since been renamed to src#tactic.iterate, which differs from the current tactic.repeat only in the abnormally high limit

[Kevin Buzzard]

Yeah I think I even remember reading in some docs (maybe Programming in Lean?) that repeat was iterate 10^n for some n which should be enough for everyone