Tactic Combinators: repeat (try ...), fails on trivial eg.

Stream: new members

[Jad Abou Hawili]

Been playing around with tactic combinators but I can't wrap my head around the following example I came up with:

example (p : Prop) (h : p) : p := by repeat (try assumption)

This returns a maximum recursion depth, why? Now, I know that repeat will keep going until the tactic it was given fails, and one of the form try ... never does. It seems like the repeat tactic doesn't stop when the goal is satisfied, which I guess matches the documentation 'repeat tac repeatedly applies tac so long as it succeeds.' Shouldn't it stop when the goal is proven? This really wrecked my understanding of how the repeat tactic works.
Does this mean that for this example:

example (p : Prop) (h : p) : p := by repeat (assumption)

assumption is ran once proving the goal, then it is run again which would fail because there is nothing to do, leading repeat to stop?
I have read the part where repeat first appears in chapter 5 in tpil4, but the book doesn't convey this. Should this be explicitly mentioned because it threw me off for a bit.

[Damiano Testa]

What is probably going on here is that, once no goals are left, you are not automatically "outside" of the proof. For instance, the tactic done is specifically designed to check that... you are done! So it lives exactly in the very small space between where there are no goals and where the next command starts.

[Damiano Testa]

Here, you are observing the same thing, I think: assumption fails in that narrow margin, since there are no goals, but try assumption succeeds, so repeat (try assumption) continues on indefinitely.

[Damiano Testa]

On the other hand, repeat assumption succeeds once, closing the goal, fails the second time around and reverts to the previous unfailing state, which is where the goal had been solved.

[Edward van de Meent]

not sure what the #xy is that made you run into this, but maybe any_goals assumption helps?

[Jad Abou Hawili]

@Damiano Testa Thanks for emphasizing the rolling back behavior and the done tactic. That helps.

Edward van de Meent said:

not sure what the #xy is that made you run into this, but maybe any_goals assumption helps?

I guess the 'root problem' would be that the automation is not transparent, i can't see what it's doing/trying and i don't know what algorithm it follows. Any pointers would help out alot. Maybe this should have been the question, how to see what proof automation is doing/trying. Can this be visualized as well, like a search tree or something?

[Jad Abou Hawili]

I am sure other people have asked a similar question but haven't found relevant channels yet.