Adventures in tacticSeqs

Stream: lean4

[Daniel Selsam]

It took me a while to diagnose some curious behavior involving tacticSeqs so I thought I would share in case others hit similar issues:

-- works
example (h : x) : y ∨ x := by
  first
  | apply Or.inl
    repeat assumption
    done
  | apply Or.inr
    repeat assumption
    done

-- fails: `repeat` claims `assumption; done`
example (h : x) : y ∨ x := by -- error: unsolved goals
  first
  | apply Or.inl; repeat assumption; done
  | apply Or.inr; repeat assumption; done

-- fails: `repeat` claims `assumption; done`
example (h : x) : y ∨ x := by -- error: unsolved goals
  first
  | (apply Or.inl; repeat assumption; done)
  | (apply Or.inr; repeat assumption; done)

-- works
example (h : x) : y ∨ x := by
  first
  | apply Or.inl; (repeat assumption); done
  | apply Or.inr; (repeat assumption); done

-- works: `{` indicates a tacticSeq, so `repeat` only claims `assumption`
example (h : x) : y ∨ x := by
  first
  | { apply Or.inl; repeat assumption; done }
  | { apply Or.inr; repeat assumption; done }

Takeaway: be very careful with tactic combinators, since they may take tacticSeqs and if so they won't play well with chains.