14.6. 使用 `conv` 进行有针对性的重写🔗

conv 或转换策略允许在目标内进行有针对性的重写。 conv 的参数是用与主要策略语言互操作的单独语言编写的；它具有导航到目标内特定子项的命令以及允许重写这些子项的命令。当重写仅应用于目标的一部分（例如仅应用于等式的一侧）而不是全面应用时，或者当重写应用于阻止策略（如 rw）访问该术语的活页夹下方时，conv 非常有用。

转换策略语言与主要策略语言非常相似：它使用相同的证明状态，策略主要针对主要目标工作，并且可能会失败或成功执行一系列新目标，并且宏展开与策略交错执行。与主要的策略语言（其中策略旨在最终解决目标）不同，conv策略用于更改目标，以便它能够在主要的策略语言中进行进一步处理。打算用 conv 重写的目标用垂直条而不是十字转门显示。

tactic

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).

Navigation and Rewriting with conv

在此示例中，有多个加法实例，rw 默认情况下会重写它遇到的第一个实例。在重写之前使用 conv 导航到特定子术语使 rw 别无选择，只能重写正确的术语。

example (x y z : Nat) : x + (y + z) = (x + z) + y := byx:Naty:Natz:Nat⊢ x + (y + z) = x + z + y
  conv =>x:Naty:Natz:Nat| x + (y + z) = x + z + y
    lhsx:Naty:Natz:Nat| x + (y + z)
    arg 2x:Naty:Natz:Nat| y + z
    rw [Nat.add_comm]x:Naty:Natz:Nat| z + y
  rw [Nat.add_assocx:Naty:Natz:Nat⊢ x + (z + y) = x + (z + y)]All goals completed! 🐙

Live ↪

Rewriting Under Binders with conv

在此示例中，加法发生在活页夹下，因此无法使用 rw。然而，使用conv导航到函数体后，就成功了。 conv 的嵌套使用会导致在对其子项之一执行进一步转换后控制返回到项中的当前位置。由于目标是重写后的自反方程，因此 conv 自动将其关闭。

example :
    (fun (x y z : Nat) =>
      x + (y + z))
    =
    (fun x y z =>
      (z + x) + y)
  := by⊢ (fun x y z => x + (y + z)) = fun x y z => z + x + y
  conv =>| (fun x y z => x + (y + z)) = fun x y z => z + x + y
    lhs| fun x y z => x + (y + z)
    intro x y zx:Naty:Natz:Nat| x + (y + z)
    conv =>
      arg 2x:Naty:Natz:Nat| y + z
      rw [Nat.add_comm]x:Naty:Natz:Nat| z + y
    rw [← Nat.add_assoc]x:Naty:Natz:Nat| x + z + y
    arg 1x:Naty:Natz:Nat| x + z
    rw [Nat.add_comm]x:Naty:Natz:Nat| z + x

Live ↪

14.6.1. 控制结构🔗

conv tactic

first

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

conv tactic

try

try tac runs tac and succeeds even if tac failed.

conv tactic

<;>

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

conv tactic

repeat

repeat convs runs the sequence convs repeatedly until it fails to apply.

conv tactic

skip

skip does nothing.

conv tactic

{ ... }

{ convs } runs the list of convs on the current target, and any subgoals that remain are trivially closed by skip.

conv tactic

( ... )

(convs) runs the convs in sequence on the current list of targets. This is pure grouping with no added effects.

conv tactic

done

done succeeds iff there are no goals remaining.

14.6.2. 目标选择🔗

conv tactic

all_goals

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

conv tactic

any_goals

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

conv 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).

conv 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.

conv tactic

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.

conv 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.

conv tactic

· ...

· conv focuses on the main conv goal and tries to solve it using s.

conv tactic

fail_if_success

fail_if_success t fails if the tactic t succeeds.

14.6.3. 导航🔗

conv tactic

lhs

Traverses 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.

conv tactic

rhs

Traverses 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.

conv tactic

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.)

conv tactic

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.

conv tactic

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.

syntaxArguments to enter

enterArg ::= ...
    | num

enterArg ::= ...
    | @num

enterArg ::= ...
    | `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident

conv tactic

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.
enter [in e] (where e is a term) is equivalent to pattern e. Occurrences can be specified with enter [in (occs := ...) e]. For example, given the target f (g a (fun x => x b)), enter [1, 2, x, 1] will traverse to the subterm b.

conv tactic

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.

conv tactic

ext

ext x traverses into a binder (a fun x => e or ∀ x, e expression) to target e, introducing name x in the process.

conv tactic

args

args traverses into all arguments. Synonym for congr.

conv tactic

left

left traverses into the left argument. Synonym for lhs.

conv tactic

right

right traverses into the right argument. Synonym for rhs.

conv tactic

intro

intro traverses into binders. Synonym for ext.

14.6.4. 改变目标🔗

14.6.4.1. 减少🔗

conv tactic

cbv

cbv performs simplification that closely mimics call-by-value evaluation. It reduces the target term by unfolding definitions using their defining equations and applying matcher equations. The unfolding is propositional, so cbv also works with functions defined via well-founded recursion or partial fixpoints.

The proofs produced by cbv only use the three standard axioms. In particular, they do not require trust in the correctness of the code generator.

The cbv Tactic

cbv策略可用于约简函数，包括通过良基递归定义的函数，否则这些函数是不可约的。通常，f 仅在命题上等于其展开，因此 rfl 无法证明等式 f 5 = 5：

def f (n : Nat) :=
  match n with
  | 0 => 0
  | n + 1 => f n + 1
termination_by (n,0)

example : f 5 = 5 := by⊢ f 5 = 5 Tactic `rfl` failed: The left-hand side
  f 5
is not definitionally equal to the right-hand side
  5

⊢ f 5 = 5rfl⊢ f 5 = 5

Tactic `rfl` failed: The left-hand side
  f 5
is not definitionally equal to the right-hand side
  5

⊢ f 5 = 5

在等式左侧使用 cbv，可以使该语句成立：

example : f 5 = 5 := by⊢ f 5 = 5
  conv =>| f 5 = 5
    lhs| f 5
    cbv| 5

Live ↪

conv tactic

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].

conv tactic

reduce

Puts term in normal form, this tactic is meant for debugging purposes only.

conv tactic

zeta

Expands let-declarations and let-variables.

conv tactic

delta

delta id1 id2 ... unfolds all occurrences of id1, id2, ... in the target. Like the delta tactic, this ignores any definitional equations and uses primitive delta-reduction instead, which may result in leaking implementation details. Users should prefer unfold for unfolding definitions.

conv tactic

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.

14.6.4.2. 简化🔗

conv tactic

simp

simp [thm] performs simplification using thm and marked @[simp] lemmas. See the simp tactic for more information.

conv tactic

dsimp

dsimp is the definitional simplifier in conv-mode. It differs from simp in that it only applies theorems that hold by reflexivity.

Examples:

example (a : Nat): (0 + 0) = a - a := bya:Nat⊢ 0 + 0 = a - a
  conv =>a:Nat| 0 + 0 = a - a
    lhsa:Nat| 0 + 0
    dsimpa:Nat| 0
    rw [← Nat.sub_self a]a:Nat| a - a

conv tactic

simp_match

simp_match simplifies match expressions. For example,

match [a, b] with
| [] => 0
| hd :: tl => hd

simplifies to a.

14.6.4.3. 重写🔗

conv tactic

change

change t' replaces the target t with t', assuming t and t' are definitionally equal.

conv tactic

rewrite

rw [thm] rewrites the target using thm. See the rw tactic for more information.

conv tactic

rw

rw [rules] applies the given list of rewrite rules to the target. See the rw tactic for more information.

conv tactic

erw

erw [rules] is a shorthand for rw (transparency := .default) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

conv tactic

apply

The apply thm conv tactic is the same as apply thm the tactic. There are no restrictions on thm, but strange results may occur if thm cannot be reasonably interpreted as proving one equality from a list of others.

14.6.5. 嵌套策略🔗

tactic

conv'

Executes the given conv block without converting regular goal into a conv goal.

conv tactic

tactic

Focuses, converts the conv goal ⊢ lhs into a regular goal ⊢ lhs = rhs, and then executes the given tactic block.

conv tactic

tactic'

Executes the given tactic block without converting conv goal into a regular goal.

tactic

conv'

Executes the given conv block without converting regular goal into a conv goal.

conv tactic

conv => ...

conv => cs runs cs in sequence on the target t, resulting in t', which becomes the new target subgoal.

14.6.6. 调试实用程序🔗

conv tactic

trace_state

trace_state prints the current goal state.

14.6.7. 其他🔗

conv tactic

rfl

rfl closes one conv goal "trivially", by using reflexivity (that is, no rewriting).

conv tactic

norm_cast

norm_cast tactic in conv mode.

14.1.	运行策略
14.2.	阅读校样状态
14.3.	策略语言
14.4.	选项
14.5.	策略参考
14.6.	使用 `conv` 进行有针对性的重写
14.7.	命名绑定变量
14.8.	定制策略

14.6. 使用 conv 进行有针对性的重写🔗

14.6.1. 控制结构🔗

14.6.2. 目标选择🔗

14.6.3. 导航🔗

14.6.4. 改变目标🔗

14.6.4.1. 减少🔗

14.6.4.2. 简化🔗

14.6.4.3. 重写🔗

14.6.5. 嵌套策略🔗

14.6.6. 调试实用程序🔗

14.6.7. 其他🔗

14.6. 使用 `conv` 进行有针对性的重写🔗