Semantics of repeat

Stream: lean4

[Jannis Limperg]

The semantics of repeat have changed between Lean 3 and Lean 4. In Lean 3, repeat t applies t to the initial goals, then to the subgoals produced by each invocation of t, etc., until t fails. In Lean 4, repeat t applies t to the first goal, then to the first goal again, etc., until t fails. This is similar to (the same as?) Lean 3 iterate.

Was this change intentional? Imo Lean 3 repeat is the much more useful combinator and the subtle change of semantics will likely be confusing for people coming from Lean 3. (Also, the docstring for Lean 4 repeat seems to be describing the Lean 3 behaviour.)

To get the Lean 3 behaviour back, I believe repeat should be defined like this:

syntax "repeat " tacticSeq : tactic
macro_rules
  | `(tactic| repeat $seq) => `(tactic| all_goals first | ($seq) <;> repeat $seq | skip)

[Alex J. Best]

I also hit this today, +1 for copying the lean 3 version

[Sebastian Ullrich]

So what's an example where the semantics differ?

[Mario Carneiro]

The alternative behavior is available in std as repeat'

[Alex J. Best]

The example I hit is

theorem mul_eq_zero (a b) (h : a ≠ 0) (h : b ≠ 0) : a * b ≠ 0 :=
sorry

theorem a (a b c) : a * (b * c) ≠ 0 :=
by
  repeat apply mul_eq_zero -- add curly braces for lean 3

[Alex J. Best]

In lean 4 we get two goals a nonzero and b * c nonzero, in lean 3 we get 3 goals

[Mario Carneiro]

see https://github.com/leanprover-community/mathport/blob/170c9451a829ac0225ac31d3dcb31fba82097e5e/Mathport/Syntax/Translate/Tactic/Lean3.lean#L201-L208

[Mario Carneiro]

• iterate { tac } -> repeat tac or iterate tac
• iterate n { tac } -> iterate n tac
• repeat { tac } -> repeat' tac

[Jannis Limperg]

We hit this issue with some teaching code for the Hitchhiker's Guide (which was specifically about repeat, so a synthetic example).