conv によるターゲットの書き換え（Targeted Rewriting with conv ）
conv 、もしくは変換タクティクはゴール内のターゲットを絞った書き換えを可能にします。 conv の引数はメインのタクティク言語と相互に連携する別の言語で記述されます；これはゴール内の特定の部分項に移動するコマンドと、これらの部分項を書き換えるコマンドを備えています。 conv は書き換えをゴール全体ではなく、ゴールの一部（例えば等式の片側のみ）にのみ適用する場合や、 rw のようなタクティクが項にアクセスするのを防いでしまう束縛子の中の書き換えを適用する場合に便利です。
変換タクティク言語はメインのタクティク言語に非常に似ています：同じ証明状態を使用し、タクティクは主にメインゴールに対して作用し、新しいゴールの列で失敗または成功する可能性があり、マクロ展開はタクティクの実行と交互に行われます。タクティクが最終的にゴールを解決するためのものであるメインのタクティク言語とは異なり、 conv はゴールを 変更 するために用いられます。これによってゴールはその後のメインのタクティク言語で容易に処理できるようになります。 conv で書き換えることを意図しているゴールはターンスタイルの代わりに縦棒で表示されます。
conv
conv => ... allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.
See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.
Basic forms:
conv => cs will rewrite the goal with conv tactics cs.
conv at h => cs will rewrite hypothesis h.
conv in pat => cs will rewrite the first subexpression matching pat (see pattern).
conv による移動と書き換え
この例では、加算のインスタンスが複数存在し、 rw はデフォルトで最初に出会ったインスタンスを書き換えてしまいます。書き換える前に特定の部分項へ移動するために conv を使用すると、 rw は正しい項を書き換える以外に選択肢がなくなります。
example (x y z : Nat) : x + (y + z) = (x + z) + y := x:Naty:Natz:Nat⊢ x + (y + z) = x + z + y
conv =>
x:Naty:Natz:Nat| x + (y + z)
x:Naty:Natz:Nat| y + z
rw [x:Naty:Natz:Nat| z + y]
All goals completed! 🐙
conv による束縛子の中の書き換え
この例では、加算は束縛子の中に存在するため、 rw は使えません。しかし、 conv を使用して関数本体に移動すると成功します。入れ子になった conv の使用は、その部分項の1つに対してさらなる変換を実行したのち、制御を項の中の現在の位置に戻します。ゴールは書き換え後の反射性の等式であるため、 conv は自動的にこれを閉じます。
example :
(fun (x y z : Nat) =>
x + (y + z))
=
(fun x y z =>
(z + x) + y)
:= ⊢ (fun x y z => x + (y + z)) = fun x y z => z + x + y
conv =>
| fun x y z => x + (y + z)
x:Naty:Natz:Nat| x + (y + z)
conv =>
x:Naty:Natz:Nat| y + z
rw [x:Naty:Natz:Nat| z + y]
rw [x:Naty:Natz:Nat| x + z + y]
x:Naty:Natz:Nat| x + z
rw [x:Naty:Natz:Nat| z + x]
first
first | conv | ... runs each conv until one succeeds, or else fails.
try
try tac runs tac and succeeds even if tac failed.
<;>
repeat
repeat convs runs the sequence convs repeatedly until it fails to apply.
{ ... }
{ convs } runs the list of convs on the current target, and any subgoals that
remain are trivially closed by skip.
( ... )
(convs) runs the convs in sequence on the current list of targets.
This is pure grouping with no added effects.
all_goals
all_goals tac runs tac on each goal, concatenating the resulting goals, if any.
any_goals
any_goals tac applies the tactic tac to every goal, and succeeds if at
least one application succeeds.
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).
case' ... => ...
next ... => ...
next => tac focuses on the next goal and solves it using tac, or else fails.
next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with
inaccessible names to the given names.
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.
. ...
· conv focuses on the main conv goal and tries to solve it using s.
· ...
· conv focuses on the main conv goal and tries to solve it using s.
fail_if_success
fail_if_success t fails if the tactic t succeeds.
lhsTraverses into the left subterm of a binary operator.
In general, for an n-ary operator, it traverses into the second to last argument.
It is a synonym for arg -2.
rhsTraverses into the right subterm of a binary operator.
In general, for an n-ary operator, it traverses into the last argument.
It is a synonym for arg -1.
fun
Traverses into the function of a (unary) function application.
For example, | f a b turns into | f a. (Use arg 0 to traverse into f.)
congr
Performs one step of "congruence", which takes a term and produces
subgoals for all the function arguments. For example, if the target is f x y then
congr produces two subgoals, one for x and one for y.
arg [@]i
arg i traverses into the i'th argument of the target. For example if the
target is f a b c d then arg 1 traverses to a and arg 3 traverses to c.
The index may be negative; arg -1 traverses into the last argument,
arg -2 into the second-to-last argument, and so on.
arg @i is the same as arg i but it counts all arguments instead of just the
explicit arguments.
arg 0 traverses into the function. If the target is f a b c d, arg 0 traverses into f.
enterArg ::= ... | num
enterArg ::= ... | @num
enterArg ::= ... | ident
enter
enter [arg, ...] is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:
enter [i] is equivalent to arg i.
enter [@i] is equivalent to arg @i.
enter [x] (where x is an identifier) is equivalent to ext x.
For example, given the target f (g a (fun x => x b)), enter [1, 2, x, 1]
will traverse to the subterm b.
pattern
pattern pat traverses to the first subterm of the target that matches pat.
pattern (occs := *) pat traverses to every subterm of the target that matches pat
which is not contained in another match of pat. It generates one subgoal for each matching
subterm.
pattern (occs := 1 2 4) pat matches occurrences 1, 2, 4 of pat and produces three subgoals.
Occurrences are numbered left to right from the outside in.
Note that skipping an occurrence of pat will traverse inside that subexpression, which means
it may find more matches and this can affect the numbering of subsequent pattern matches.
For example, if we are searching for f _ in f (f a) = f b:
occs := 1 2 (and occs := *) returns | f (f a) and | f b
occs := 2 returns | f a
occs := 2 3 returns | f a and | f b
occs := 1 3 is an error, because after skipping f b there is no third match.
ext
ext x traverses into a binder (a fun x => e or ∀ x, e expression)
to target e, introducing name x in the process.
args
args traverses into all arguments. Synonym for congr.
whnf
Reduces the target to Weak Head Normal Form. This reduces definitions
in "head position" until a constructor is exposed. For example, List.map f [a, b, c]
weak head normalizes to f a :: List.map f [b, c].
reducePuts term in normal form, this tactic is meant for debugging purposes only.
zetaExpands let-declarations and let-variables.
delta
unfold
unfold id unfolds all occurrences of definition id in the target.
unfold id1 id2 ... is equivalent to unfold id1; unfold id2; ....
Definitions can be either global or local definitions.
For non-recursive global definitions, this tactic is identical to delta.
For recursive global definitions, it uses the "unfolding lemma" id.eq_def,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to simp only [id], which unfolds definition id recursively.
This is the conv version of the unfold tactic.
simp
dsimp
change
change t' replaces the target t with t',
assuming t and t' are definitionally equal.
rw
erw
conv'
Executes the given conv block without converting regular goal into a conv goal.
tactic
Focuses, converts the conv goal ⊢ lhs into a regular goal ⊢ lhs = rhs, and then executes the given tactic block.
tactic'
Executes the given tactic block without converting conv goal into a regular goal.
conv'
Executes the given conv block without converting regular goal into a conv goal.
conv => ...
conv => cs runs cs in sequence on the target t,
resulting in t', which becomes the new target subgoal.
rfl
rfl closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).