<;>

<;> は、直前のタクティクによって生成されたすべてのサブゴールに対して後続のタクティクを適用することを意味するタクティク結合子です。¹

variable (P Q : Prop)

example (hP : P) (hQ : Q) : P ∧ Q := by
  constructor <;> assumption

all_goals との違い

<;> は all_goals とよく似た挙動をします。しかし、<;> と all_goals は完全に同じではありません。 <;> が「直前のタクティクによって生成された全てのサブゴール」に対して後続のタクティクを実行するのに対して、all_goals は「すべての未解決のゴール」に対して後続のタクティクまたはタクティクブロックを実行します。

実際に以下のような例ではその違いが現れます。

variable (P Q R : Prop)

/-- <;> を使用したとき -/
example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
  constructor

  constructor <;> try assumption

  -- まだ示すべきことが残っている
  show R
  assumption

/-- all_goals を使用したとき -/
example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
  constructor

  constructor
  all_goals
    try assumption

  -- 証明完了
  done

ゴールが途中で閉じられたとき

tac1 <;> tac2 の実行において、tac1 の実行でゴールが閉じられた場合、tac2 は実行されずスキップされます。これは tac1; tac2 とは異なる挙動であることに注意してください。

example (hP : P) : P := by
  -- `assumption`の時点でゴールは閉じているが、エラーにならない
  -- `simp`の実行は単にスキップされる
  assumption <;> simp

example (hP : P) : P := by
  -- `tac1; tac2` では、`tac2` を実行しようとする
  -- そのため `tac2` が実行できないとエラーになることがある
  fail_if_success
    assumption; simp

  assumption

<;> の正式な呼び名はわかりません。linter.unnecessarySeqFocus というリンタが存在するので、ここでは seqFocus と仮に呼んでいます。 ↩

Lean by Example

<;>

all_goals との違い

ゴールが途中で閉じられたとき