Zulip Chat Archive

Stream: lean4

Topic: What does `repeat` mean?


Siddharth Bhat (Oct 14 2021 at 15:20):

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 (Oct 14 2021 at 15:22):

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 (Oct 14 2021 at 16:38):

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 (Oct 14 2021 at 19:38):

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 (Oct 14 2021 at 19:40):

(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 (Oct 14 2021 at 19:40):

*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 (Oct 14 2021 at 19:44):

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 (Oct 14 2021 at 19:52):

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

Gabriel Ebner (Oct 14 2021 at 20:00):

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 (Oct 14 2021 at 21:00):

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 (Oct 14 2021 at 21:15):

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.


Last updated: Dec 20 2023 at 11:08 UTC