What does `repeat` mean?

Stream: lean4

[Siddharth Bhat]

I would expect that the repeattactic repeats a given tactic till it stops making progress. So consider the script:

inductive foo where
| done: foo
| kind?: (kind: String) -> foo -> foo

inductive foo_done : foo -> Prop where
| done: foo_done foo.done
| kind?_done:
  (s: String) -> (m: foo) -> (PRF: foo_done m) -> foo_done (foo.kind? s m)

def kind? (s: String)
  (m: foo)
  (PRF: foo_done (foo.kind? s m)): foo_done m :=
  match PRF with
  | foo_done.kind?_done s m prf => prf

def proof : ∃ m, foo_done m := by {
  apply Exists.intro;
  apply kind? "get"; apply kind? "set"; apply kind? "sub";
  -- repeat constructor; -- <== does not succeed!
  constructor; constructor; constructor; constructor;
}

See that calling constructor four times solves the goal. However, using repeat constructor does not work. I don't understand what happens, but repeat constructor leaves the proof unsolved at goal state:

case h.PRF.PRF.PRF.PRF
⊢ foo_done (foo.kind? "set" (foo.kind? "get" ?w))
case w
⊢ foo
case h.PRF.PRF.PRF.PRF.PRF
⊢ foo_done (foo.kind? "get" ?w)
case w
⊢ foo
case h.PRF.PRF.PRF.PRF.PRF.PRF
⊢ foo_done ?w
case w
⊢ foo

What's going on, and why doesn't repeat constructor solve this goal (which is solved by, well, repeated calls to constructor?

[Siddharth Bhat]

Oh, hm, wait a minute. it seems like repeat constructor _does work_, in that I can run lean on it with no errors.

So my new question is: Why doesn't the tactic state say goals accomplished when using repeat constructor? I find this very confusing!

[Tomas Skrivan]

I was confused about repeat too. It looks like that having cursor at the end of repeat <tactic> shows only one application of <tactic>.

[Eric Rodriguez]

oh, funny that this parser thing has carried on to lean4. this is a side-effect of how lean parses nested* tactics; if there's a skip tactic in lean4, you should be able to see the post-repeat state

[Eric Rodriguez]

(I'm still talking about lean3 here because it's what I'm familiar with but I'd be surprised if it's much different) this is fixable with some scanner finagling but it makes writing proofs in progress a lot harder, as it will give you a non-useful tactic state when the proof isn't done

[Eric Rodriguez]

*I reserve the right to be wrong about the name "nested", but I _think_ that's the lean3 internal name for tactics like repeat, all_goals, even conv, etc)

[Chris B]

There's also a done tactic:

def proof : ∃ m, foo_done m := by {
  apply Exists.intro;
  apply kind? "get"; apply kind? "set"; apply kind? "sub";
  repeat constructor
  done -- shows goals accomplished
}

[Siddharth Bhat]

Thanks, using skip and done will probably help a lot :)

[Gabriel Ebner]

I'm not too happy about the goal display at the end of proofs (or lack thereof) either. As a workaround I'm frequently putting skip everywhere to reliably get the tactic state.
We had a long discussion about the heuristic the last time: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/goal.20view/near/232498890 Maybe it's time to revisit it.

[Sebastian Ullrich]

This one doesn't look as much about cursor placement but about displaying overlapping goals. The current heuristic was mostly intended for tactics like cases x <;> |constructor where the overlapping goals are truly parallel, whereas in "serial" cases like inside repeat that doesn't make much sense.

[Sebastian Ullrich]

I don't remember if there was a case where we shouldn't simply use the outermost goal when placing the cursor strictly after all of them... but I'd also like to show sensible information when placing the cursor anywhere inside the tactic. Unless someone says they want to see all intermediate goals in that case.