when does a branch in the first combinator change the goal?

Stream: lean4

[Bulhwi Cha]

Consider the following example from Section Tactic Combinators of #tpil:

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

The compound tactic first tries to solve the left disjunct, p, immediately by assumption. That attempt fails, and the goal remains the same. It then tries to focus on the right disjunct, q ∨ r. That attempt also fails; however, the goal changes from p ∨ q ∨ r to q ∨ r.

When exactly does a subtactic in the first combinator change the goal?

[Jovan Gerbscheid]

Did you mean to write
repeat (first | apply Or.inl; assumption | apply Or.inr; assumption)

[Bulhwi Cha]

No, that doesn't work.

[Jovan Gerbscheid]

It seems to match what you were describing. You say that the attempt to focus on the right goal fails. But the focussing on the right goal of course doesn't fail.

[Jovan Gerbscheid]

As in, apply Or.inr is successful, so that is were the first combinator stops

[Bulhwi Cha]

I'm not sure what the word "fail" really means in this context.

[Jovan Gerbscheid]

fail means that the tactic throws an error

[Jovan Gerbscheid]

apply Or.inl; assumption throws an error because assumption does. apply Or.inr doesn't throw an error

[Bulhwi Cha]

From docs#Lean.Parser.Tactic.first:

def Lean.Parser.Tactic.first : ParserDescr

first | tac | ... runs each tac until one succeeds, or else fails.

[Jovan Gerbscheid]

Oh, is the "runs each tac" confusing? It doesn't actually run each tactic: it stops when one succeeds.

[Bulhwi Cha]

Jovan Gerbscheid said:

As in, apply Or.inr is successful, so that is were the first combinator stops

Does apply Or.inr succeed in the following example?

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  apply Or.inr

[Bulhwi Cha]

What exactly is the meaning of the word "succeed" in this context?

[Jovan Gerbscheid]

Yes, it succeeds because the tactic doesn't throw an error

[Jovan Gerbscheid]

Here is an example of a tactic that doesn't succeed:

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  apply trivial

[Bulhwi Cha]

I do get an error message from the first line of my example:

Messages here:
1:47:
unsolved goals
case h
p q r : Prop
hr : r
⊢ q ∨ r

[Jovan Gerbscheid]

This error message is not thrown by the apply tactic. The apply tactic successfully applies, and then there are no more tactics left, so lean checks if all goals have been closed. That is what throws this error.

For example:

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  apply Or.inr
  repeat sorry

doesn't throw an error (just a warning), while

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  apply trivial
  repeat sorry

throws an error, because apply trivial failed. So Lean doesn't even try to repeat sorry.

[Bulhwi Cha]

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  first | apply Or.inr | exact Or.inr (Or.inr hr) -- unsolved goals

You're right. If apply Or.inr in the above first combinator failed, it'd run exact Or.inr (Or.inr hr), but it doesn't.

[Bulhwi Cha]

Bulhwi Cha said:

Consider the following example from Section Tactic Combinators of #tpil:

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

The compound tactic first tries to solve the left disjunct, p, immediately by assumption. That attempt fails, and the goal remains the same. It then tries to focus on the right disjunct, q ∨ r. That attempt also fails; however, the goal changes from p ∨ q ∨ r to q ∨ r.

I should fix the above explanation as follows:

The first combinator tries to solve the left disjunct, p, immediately by assumption. That attempt fails, and the goal remains the same. It then tries to focus on the right disjunct, q ∨ r. That attempt succeeds, so the goal changes from p ∨ q ∨ r to q ∨ r.

The repeat combinator applies the first combinator again. The second subtactic in the first combinator succeeds, so the goal changes from q ∨ r to r.

The repeat combinator applies the first combinator once again. The last subtactic in first combinator, assumption, succeeds and closes the goal.

Therefore, the compound tactic is equivalent to the following sequence of the same first combinators:

example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by
  first | apply Or.inl; assumption | apply Or.inr | assumption -- runs `apply Or.inr`
  first | apply Or.inl; assumption | apply Or.inr | assumption -- runs `apply Or.inr`
  first | apply Or.inl; assumption | apply Or.inr | assumption -- runs `assumption`

[Bulhwi Cha]

I'm glad that I asked about the first combinator. Thanks for your answer!

[Bulhwi Cha]

From docs#Lean.Parser.Tactic.first:

def Lean.Parser.Tactic.first : ParserDescr

first | tac | ... runs each tac until one succeeds, or else fails.

Should we change the description of the first combinator as follows?

first | tac | ... runs only the first tac that succeeds; it fails if none of them succeeds.

[Bulhwi Cha]

Jovan Gerbscheid said:

Oh, is the "runs each tac" confusing? It doesn't actually run each tactic: it stops when one succeeds.

To put it another way, first | tac | ... tries to run each tac until one succeeds, or else fails. I think we should change the description of it.

[Jovan Gerbscheid]

Yes, I think both of these options are a better description.

[Kevin Buzzard]

I don't think "runs only the first tac that succeeds" is better than "runs each tac until one succeeds"; in fact I think it's strictly worse. What first does is exactly the latter thing (i.e. what it already says it does), not the former thing. I agree that the second clause is better though.