using repeat and all_goals to prove theorems

Stream: lean4

[Bulhwi Cha]

Unlike the first proof of the example below, the second one gives the message, "maximum recursion depth has been reached." I'm not sure why this happens.

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (all_goals (first | constructor | assumption))

[Aaron Liu]

all_goals succeeds on no goals, so repeat is repeatedly applying it to no goals

[Bulhwi Cha]

Aaron Liu said:

all_goals succeeds on no goals

Can you elaborate on this? Shouldn't all_goals succeed on the goal p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p)?

[Aaron Liu]

All the goals are solved, but repeat is supposed to keep going until the tactic fails, so it keeps running it on no goals, and it keeps succeeding

[Bulhwi Cha]

Then why does the repeat tactic succeed in the following example?

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (any_goals (first | constructor | assumption))

[Aaron Liu]

Clearly, my diagnosis was wrong, and the recursion limit is a lot closer than I thought

[Bulhwi Cha]

I think I know why:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption)

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  any_goals (first | constructor | assumption)
  any_goals (first | constructor | assumption)
  any_goals (first | constructor | assumption)
  any_goals (first | constructor | assumption)
  any_goals (first | constructor | assumption)
  any_goals (first | constructor | assumption) -- failed on all goals

[Bulhwi Cha]

I think this behavior of all_goals is inconsistent with that of any_goals, but perhaps there's a reason for it. If not, I suggest making all_goals fail to run when there's no goal to solve.

[Yaël Dillies]

Is it inconsistent? ∀ goal : Goal, Solved goal implies ∃ goal : Goal, Solved goal only if Goal is nonempty, after all...

[Bulhwi Cha]

I think the meanings of "any" and "exists" are slightly different here. any_goals applies its tactic argument to as many goals as possible.

[Yaël Dillies]

Yes, so does all_goals. Then any_goals fails if no goal has progressed, all_goals fails if not all goals have progressed. That feels pretty consistent to me.

[Bulhwi Cha]

Yaël Dillies said:

Yes, so does all_goals.

No, it doesn't. Unlike any_goals, all_goals tries to apply its tactic argument to all open goals even if it will fail on some goals.

[Bulhwi Cha]

example (p q r s : Prop) (hp : p) (hq : q) (hr : r) : s ∧ p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  all_goals (first | constructor | assumption)
  all_goals (first | constructor | assumption) -- tactic 'assumption' failed
  sorry

example (p q r s : Prop) (hp : p) (hq : q) (hr : r) : s ∧ p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  any_goals (first | constructor | assumption)
  any_goals (first | constructor | assumption)
  sorry

[Jovan Gerbscheid]

I agree with @Yaël Dillies that the behaviour is technically consistent with the tactic name: all_goals tac fails if and only if tac fails on one of the goals. (so if there are no goals, all_goals tac succeeds)

[Jovan Gerbscheid]

However, it is common for tactics to check that there are no goals left, and for good reason, because it doesn't make much sense to run a tactic when there are no goals left. So there is still an argument for changing the behaviour.

[Yaël Dillies]

There's a linter to catch tactics that do nothing. Why not rely on that instead?

[Bulhwi Cha]

Jovan Gerbscheid said:

all_goals tac fails if and only if tac fails on one of the goals.

@Jovan Gerbscheid @Yaël Dillies Do you think the second assumption tactic fails in the following proof? You might say, "It's vacuously true that the second tactic succeeds on all goals since there's no goal to solve." Still, we get an error message.

example (p : Prop) (hp : p) : p := by
  assumption
  assumption -- no goals to be solved

[Jovan Gerbscheid]

Bulhwi Cha said:

Do you think the second assumption tactic fails in the following proof?

example (p : Prop) (hp : p) : p := by
  assumption
  assumption -- no goals to be solved

Yes, as indicated by the red squiggly line under assumption

[Jovan Gerbscheid]

Yaël Dillies said:

There's a linter to catch tactics that do nothing. Why not rely on that instead?

Because of the original example:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (all_goals (first | constructor | assumption))

[Jovan Gerbscheid]

Actually, there is a better solution:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat' (first | constructor | assumption)

[Jovan Gerbscheid]

Well, actually in your example

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (first | constructor | assumption)

also works.

But you can see the difference between repeat and repeat' if the tactic is non-finishing:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat' (first | constructor)

[Bulhwi Cha]

Huh, I didn't know repeat' exists.

[Jovan Gerbscheid]

I forgot about it as well, it's not named amazingly. It does the same as repeat, but goes into all newly created subgoals.

[Bulhwi Cha]

I'm puzzled by the two examples below:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (all_goals (first | constructor | assumption)) -- maximum recursion depth has been reached

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat' (all_goals (first | constructor | assumption))

[Jovan Gerbscheid]

Neither repeat nor repeat' should be used in combination with all_goals. But if you want to know the details:

• repeat (all_goals tac) loops here because after all goals are solved, all_goals tac keeps on succeeding
• repeat' (all_goals tac) doesn't loop, because repeat' only runs all_goals tac on newly created goals. And at some point no new goal are created.

[Bulhwi Cha]

From https://lean-lang.org/theorem_proving_in_lean4/tactics.html:

In fact, we can compress the full tactic down to one line:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
      p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat (any_goals (first | constructor | assumption))

#tpil has an example of using repeat and any_goals, so I thought I could replace any_goals with all_goals in that example.

[Jovan Gerbscheid]

In fact, repeat' (all_goals tac) is equivalent to repeat' tac, because repeat' tac only runs tac on sinlge-goal tactic states.

[Jovan Gerbscheid]

I think repeat (any_goals tac) is a less perfomant version of repeat' tac (but more conceptual, so it works great in the #tpil book)

[Jovan Gerbscheid]

Bulhwi Cha said:

#tpil has an example of using repeat and any_goals, so I thought I could replace any_goals with all_goals in that example.

I don't know why you would want to do that.

[Bulhwi Cha]

I'm recording videos of me reading the textbook in Korean and commenting on it. I only wanted to say that you could use all_goals instead of any_goals in that example, but it turned out I was wrong.