7.3. タクティク言語（The Tactic Language）🔗

タクティクのスクリプトはセミコロンか改行で区切られた一連のタクティクで構成されます。改行で区切る場合、タクティクは同じレベルにインデントされなければなりません。インデントの代わりに波括弧とセミコロンを使っても良いです。タクティクの列は括弧でグループ化することができます。こうすることで文法的には1つのタクティクが期待される位置で一連のタクティクを使うことができます。

一般的に、実行は上から下へと進み、各タクティクは前のタクティクが残した証明状態にて実行されます。タクティク言語には、このフローを変更できる制御構造が数多く含まれています。

各タクティクは tactic カテゴリの構文拡張です。つまり、タクティクは独自の具体的な構文やパース規則を自由に定義することができます。しかし、いくつかの例外を除いて、大部分のタクティクは先頭のキーワードで識別することができます；例外は典型的には <;> のようなよく使われる組み込みの制御構造です。

7.3.1. 制御構造（Control Structures）🔗

厳密に言えば、制御構造と他のタクティクの間に基礎的な区別はありません。どのようなタクティクであれ、他のものを引数として受け取り、適切と思われる文脈で実行できるようにアレンジすることは自由です。しかし、たとえこの区別が恣意的であったとしても、有用であることには変わりありません。この節のタクティクはプログラミングの伝統的な制御構造に似ているものや、それ自身が証明をすすめるのではなく、他のタクティクを再結合させる だけ などです。

7.3.1.1. 成功と失敗（Success and Failure）🔗

証明状態で実行すると、すべてのタクティクは成功するか失敗するかのどちらかです。タクティクの失敗は例外に似ています；失敗は通常、処理されるまで「沸き立ちます」。例外とは異なり、失敗の理由を区別する演算子はありません； first は単に成功した最初の分岐を取ります。

🔗tactic
fail

fail msg is a tactic that always fails, and produces an error using the given message.

🔗tactic
fail_if_success

fail_if_success t fails if the tactic t succeeds.

🔗tactic
try

try tac runs tac and succeeds even if tac failed.

🔗tactic
first

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

7.3.1.2. 分岐（Branching）🔗

タクティクの証明では、パターンマッチや条件式を使うことがあります。しかし、その意味は項においてのものと全く同じではありません。項では変数の値が分かってから実行されるのに対し、証明は変数が抽象的なまま実行され、同時に すべての ケースを考慮しなければなりません。したがって、if や match がタクティクで使われる場合、その意味は具体的な分岐の選択ではなく、ケースによる推論です。それらの分岐はすべて実行され、条件やパターンマッチは単一の分岐を選択するためではなく、各分岐でより多くの情報を使ってメインゴールを絞り込むために使われます。

🔗tactic
if ... then ... else ...

In tactic mode, if t then tac1 else tac2 is alternative syntax for:

by_cases t
· tac1
· tac2

It performs case distinction on h† : t or h† : ¬t, where h† is an anonymous hypothesis, and tac1 and tac2 are the subproofs. (It doesn't actually use nondependent if, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an ite application use refine if t then ?_ else ?_.)

🔗tactic
if h : ... then ... else ...

In tactic mode, if h : t then tac1 else tac2 can be used as alternative syntax for:

by_cases h : t
· tac1
· tac2

It performs case distinction on h : t or h : ¬t and tac1 and tac2 are the subproofs.

You can use ?_ or _ for either subproof to delay the goal to after the tactic, but if a tactic sequence is provided for tac1 or tac2 then it will require the goal to be closed by the end of the block.

if による場合分けの推論

Lean.Parser.Tactic.tacIfThenElse : tacticIn tactic mode, `if t then tac1 else tac2` is alternative syntax for: ``` by_cases t · tac1 · tac2 ``` It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an `ite` application use `refine if t then ?_ else ?_`.) if の各分岐では、n = 0 かどうかを反映する仮定が追加されます。

example (n : Nat) : if n = 0 then n < 1 else n > 0 := n:Nat⊢ if n = 0 then n < 1 else n > 0 if n = 0 n:Nath✝:n = 0⊢ if n = 0 then n < 1 else n > 0 All goals completed! 🐙 n:Nath✝:¬n = 0⊢ if n = 0 then n < 1 else n > 0 n:Nath✝:¬n = 0⊢ 0 < n All goals completed! 🐙
🔗tactic
match

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := by
  match n with
  | 0 => rfl
  | i+1 => simp

パターンマッチの場合、ゴールの中の被検査対象のインスタンスは各ブランチでそれにマッチするパターンに置き換えられます。その後、各ブランチは絞り込まれたゴールを証明しなければなりません。cases タクティクと比較すると、match を使用することで、実行するケース分析に柔軟性を持たせることができますが、各ブランチがゴールを完全に解決する必要があるため、大規模な自動化スクリプトに組み込むことが難しくなります。

match による場合分けの推論

Lean.Parser.Tactic.match : tactic`match` performs case analysis on one or more expressions. See [Induction and Recursion][tpil4]. The syntax for the `match` tactic is the same as term-mode `match`, except that the match arms are tactics instead of expressions. ``` example (n : Nat) : n = n := by match n with | 0 => rfl | i+1 => simp ``` [tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html match の各ブランチでは、被検査対象 n が 0 または k + 1 に置き換えられています。

example (n : Nat) : if n = 0 then n < 1 else n > 0 := n:Nat⊢ if n = 0 then n < 1 else n > 0 match n with | 0 => All goals completed! 🐙 | k + 1 => All goals completed! 🐙

7.3.1.3. ゴールの選択（Goal Selection）🔗

ほとんどのタクティクは メインゴール に影響を与えます。ゴール選択タクティクは異なるゴールをメインゴールとして扱う方法を提供し、証明状態のゴールの順序を並べ替えます。

🔗tactic
case

  • case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.

  • case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

  • case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).

🔗tactic
case'

case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

🔗tactic
rotate_left

rotate_left n rotates goals to the left by n. That is, rotate_left 1 takes the main goal and puts it to the back of the subgoal list. If n is omitted, it defaults to 1.

🔗tactic
rotate_right

Rotate the goals to the right by n. That is, take the goal at the back and push it to the front n times. If n is omitted, it defaults to 1.

7.3.1.3.1. 順序実行（Sequencing）🔗

タクティク言語では、タクティクを次々に実行し、それぞれがメインゴールを解決するために使用されることに加え、目標の生成方法に従ってタクティクを順番に実行することもサポートしています。 <;> タクティクコンビネータは、他のタクティクによって生成された すべての サブゴール ごとにタクティクを適用することを可能にします。新しいゴールが生成されなければ、2番目のタクティクは実行されません。

🔗tactic
<;>

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

タクティクが サブゴール のいずれかで失敗した場合、 <;> タクティク全体が失敗します。

サブゴールの順序実行

この証明状態において：

x:Nath:x = 1 ∨ x = 2⊢ x < 3

タクティク x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 は以下の2つのゴールを生成します：

x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3

x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 ; x:Nath✝:x = 2⊢ x < 3 を実行することで、 simp が最初のゴールを解決し、2つ目が残ります：

x:Nath✝:x = 2⊢ x < 3

; を <;> で置き換え、 x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 All goals completed! 🐙 を実行すると simp によって新しいゴールが 両方とも 解決されます：

All goals completed! 🐙

7.3.1.3.2. 複数のゴールに作用する（Working on Multiple Goals）🔗

タクティク all_goals と any_goals は証明状態のすべてのゴールにタクティクを適用できます。両者の違いは、タクティクがいずれかのゴールで失敗した場合、 all_goals はそれ自体が失敗する一方、 any_goals はタクティクがすべてのゴールで失敗した場合のみに失敗します。

🔗tactic
all_goals

all_goals tac runs tac on each goal, concatenating the resulting goals, if any.

🔗tactic
any_goals

any_goals tac applies the tactic tac to every goal, and succeeds if at least one application succeeds.

7.3.1.4. 焦点をあてる（Focusing）🔗

焦点をあてるタクティクは証明ゴールのサブセット（通常はメインゴールのみを残します）をそれ以降のタクティクの検討対象から外します。ここで説明するタクティクに加えて、 case と case' は選択されたゴールに焦点を当てます。

🔗tactic
·

· tac focuses on the main goal and tries to solve it using tac, or else fails.

一般に、1つのタクティク行から複数の新しいサブゴールが生成される場合、ブレットを使用することが良い Lean 流と考えられています。こうすることで、推論のステップ間の繋がりがより明確になり、証明の編集中にサブゴールの数を変更しても局所的な効果しかないため、証明を読みやすく、維持しやすくなります。

🔗tactic
focus

focus tac focuses on the main goal, suppressing all other goals, and runs tac on it. Usually · tac, which enforces that the goal is closed by tac, should be preferred.

7.3.1.5. 繰り返しと反復（Repetition and Iteration）🔗

🔗tactic
iterate

iterate n tac runs tac exactly n times. iterate tac runs tac repeatedly until failure.

iterate's argument is a tactic sequence, so multiple tactics can be run using iterate n (tac₁; tac₂; ⋯) or

iterate n
  tac₁
  tac₂
  ⋯
🔗tactic
repeat

repeat tac repeatedly applies tac so long as it succeeds. The tactic tac may be a tactic sequence, and if tac fails at any point in its execution, repeat will revert any partial changes that tac made to the tactic state.

The tactic tac should eventually fail, otherwise repeat tac will run indefinitely.

See also:

  • try tac is like repeat tac but will apply tac at most once.

  • repeat' tac recursively applies tac to each goal.

  • first | tac1 | tac2 implements the backtracking used by repeat

🔗tactic
repeat'

repeat' tac recursively applies tac on all of the goals so long as it succeeds. That is to say, if tac produces multiple subgoals, then repeat' tac is applied to each of them.

See also:

  • repeat tac simply repeatedly applies tac.

  • repeat1' tac is repeat' tac but requires that tac succeed for some goal at least once.

🔗tactic
repeat1'

repeat1' tac recursively applies to tac on all of the goals so long as it succeeds, but repeat1' tac fails if tac succeeds on none of the initial goals.

See also:

  • repeat tac simply applies tac repeatedly.

  • repeat' tac is like repeat1' tac but it does not require that tac succeed at least once.

7.3.2. 名前と健全性（Names and Hygiene）🔗

裏側では、タクティクは証明項を生成しています。これらの証明項はローカルコンテキストに存在します。なぜなら証明状態の仮定は項のローカルの束縛子に対応するからです。仮定の使用は変数の参照に対応します。仮定の名前付けは予測可能であることが非常に重要です；そうでなければ、タクティクの内部実装に小さな変更を加えると、変数がキャプチャされたり、異なる名前が選択されると参照が壊れたりする可能性があります。

Lean のタクティク言語は 健全 （hygienic）です。これはタクティク言語が字句スコープを尊重することを意味します：タクティク内で出現する名前は生成されたコードによって決定されるのではなく、ソースコードの束縛を参照しており、タクティクフレームワークはこのプロパティを維持する責任があります。タクティクスクリプトの変数参照は裏側で証明項で使うために選ばれた名前ではなく、スクリプトの最初にスコープにあった名前か、タクティクの一部として明示的に導入された束縛を参照します。

健全なタクティクの結果として、仮定を参照する唯一の方法は、その仮定に明示的に名前をつけることです。タクティクは自分で仮定に名前を付けることができず、むしろユーザからの名前を受け入れなければなりません；これに応じてユーザは参照したい仮定の名前を提供する義務があります。ユーザが仮定に名前を提供しない場合、その仮定は短剣（'†'、DAGGER 0x2020）と共に証明状態に表示されます。この短剣はその名前が アクセス不能 （inaccessible）であり、明示的に参照できないことを示します。

オプション tactic.hygienic を false に設定することで、健全性を無効にすることができます。多くのタクティクはキャプチャを防ぐために健全性システムに依存しており、注意深く手動で名前を選択するオーバーヘッドが発生しないため、これは推奨されません。

🔗option
tactic.hygienic

Default value: true

make sure tactics are hygienic

タクティクの健全さ：アクセス不能な仮定

∀ (n : Nat), 0 + n = n を証明する場合、最初の証明状態は次のようになります：

⊢ ∀ (n : Nat), 0 + n = n

タクティク n✝:Nat⊢ 0 + n✝ = n✝ によってアクセス不能な仮定を持つ証明状態になります：

n✝:Nat⊢ 0 + n✝ = n✝
タクティクの健全さ：アクセス可能な仮定

∀ (n : Nat), 0 + n = n を証明する場合、最初の証明状態は次のようになります：

⊢ ∀ (n : Nat), 0 + n = n

明示的な名前 n を伴ったタクティク n:Nat⊢ 0 + n = n はアクセス可能な名前の仮定を持つ証明状態になります：

n:Nat⊢ 0 + n = n

7.3.2.1. 仮定へのアクセス（Accessing Assumptions）🔗

多くのタクティクは、導入する仮定の名前を指定する手段を提供します。例えば、 intro と intros は引数として仮定の名前を取り、 induction の Lean.Parser.Tactic.induction : tacticAssuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well. For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `induction n` produces one goal with hypothesis `h : P 0` and target `Q 0`, and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`. Here the names `a` and `ih₁` are chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor. - `induction e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then performs induction on the resulting variable. - `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a term whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables - `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. - Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case. with による形式はケース選択・仮定の名前付け・焦点当てを同時に行うことができます。仮定に名前がない場合、 next ・ case ・ rename_i などを使用して名前を割り当てることができます。

🔗tactic
rename_i

rename_i x_1 ... x_n renames the last n inaccessible names using the given names.

7.3.3. 仮定の管理（Assumption Management）🔗

より大きな証明では証明状態の管理による恩恵が大きく、無関係な仮定を削除し、それらの名前を理解しやすくします。ここまでの演算子に加え、 rename_i はアクセス不能な仮定の名前を付けなおし、 intro ・ intros ・ rintro は含意または全称量化されたゴールを追加の仮定を持つゴールに変換します。

🔗tactic
rename

rename t => x renames the most recent hypothesis whose type matches t (which may contain placeholders) to x, or fails if no such hypothesis could be found.

🔗tactic
revert

revert x... is the inverse of intro x...: it moves the given hypotheses into the main goal's target type.

🔗tactic
clear

clear x... removes the given hypotheses, or fails if there are remaining references to a hypothesis.

7.3.4. ローカル定義と証明（Local Definitions and Proofs）🔗

have と let はどちらもローカルの仮定を作ります。一般的に言って、中間的な補題を証明する時には have を使うべきです； let はローカル定義の保存に使うべきです。

🔗tactic
have

The have tactic is for adding hypotheses to the local context of the main goal.

  • have h : t := e adds the hypothesis h : t if e is a term of type t.

  • have h := e uses the type of e for t.

  • have : t := e and have := e use this for the name of the hypothesis.

  • have pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.

🔗tactic
haveI

haveI behaves like have, but inlines the value instead of producing a let_fun term.

🔗tactic
have'

Similar to have, but using refine'

🔗tactic
let

The let tactic is for adding definitions to the local context of the main goal.

  • let x : t := e adds the definition x : t := e if e is a term of type t.

  • let x := e uses the type of e for t.

  • let : t := e and let := e use this for the name of the hypothesis.

  • let pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that let only one applicable constructor. For example, given p : α × β × γ, let ⟨x, y, z⟩ := p produces the local variables x : α, y : β, and z : γ.

🔗tactic
let rec

let rec f : t := e adds a recursive definition f to the current goal. The syntax is the same as term-mode let rec.

🔗tactic
letI

letI behaves like let, but inlines the value instead of producing a let_fun term.

🔗tactic
let'

Similar to let, but using refine'

7.3.5. 設定（Configuration）🔗

多くのタクティクは設定変更が可能です。 慣例的に、タクティクは設定の構文を共有しており、 optConfig を使って記述します。各タクティクで利用可能なオプションはタクティクのドキュメントに記述されています。

syntax

タクティクの設定は0個以上の 設定項目 （configuration item）から構成されます：

Configuration options for tactics. optConfig ::=
    Configuration options for tactics. A configuration item for a tactic configuration. configItem*
syntax

各設定項目は、タクティクのオプションに対応する名前を持ちます。真偽値のオプションは、接頭辞 + と - を使って有効・無効に設定できます：

A configuration item for a tactic configuration. configItem ::=
    A configuration item for a tactic configuration. `+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
+ident
A configuration item for a tactic configuration. configItem ::= ...
    | A configuration item for a tactic configuration. `-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
-ident

オプションは、名前付き関数の引数の構文に似た構文を使って特定の値を割り当てることができます：

A configuration item for a tactic configuration. configItem ::= ...
    | A configuration item for a tactic configuration. `(opt := val)` sets the `opt` configuration option to `val`.

As a special case, `(config := ...)` sets the entire configuration.
(ident := term)

最後に、config という名前が予約されています；これはオプションのセット全体をデータ構造として渡すために使われます。期待される具体的な型はタクティクによって異なります。

A configuration item for a tactic configuration. configItem ::= ...
    | A configuration item for a tactic configuration. `(opt := val)` sets the `opt` configuration option to `val`.

As a special case, `(config := ...)` sets the entire configuration.
(config := term)

7.3.6. 名前空間とオプション管理（Namespace and Option Management）🔗

名前空間とオプションは項と同じ構文を使ってタクティクスクリプトで調整できます。

🔗tactic
set_option

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

🔗tactic
open

open Foo in tacs (the tactic) acts like open Foo at command level, but it opens a namespace only within the tactics tacs.

7.3.6.1. 展開のコントロール（Controlling Unfolding）🔗

デフォルトでは、定義上の等価性をチェックする時を除いて、reducible とマークされた定義だけが展開されます。これらの演算子により、タクティクスクリプトの一部でこのデフォルトを調整することができます。

🔗tactic
with_reducible_and_instances

with_reducible_and_instances tacs executes tacs using the .instances transparency setting. In this setting only definitions tagged as [reducible] or type class instances are unfolded.

🔗tactic
with_reducible

with_reducible tacs executes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

🔗tactic
with_unfolding_all

with_unfolding_all tacs executes tacs using the .all transparency setting. In this setting all definitions that are not opaque are unfolded.