当 simpl 没有减少所有必要的步骤时应该怎么办？

Question

以下示例来自《软件基础》一书的 Poly 章节。

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
intros.
induction l.
- simpl. reflexivity.
- simpl.

1 subgoal
X : Type
x : X
l : list X
IHl : fold_length l = length l
______________________________________(1/1)
fold_length (x :: l) = S (length l)

我希望它能简化左侧的步骤。当然应该可以。

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
intros.
induction l.
- simpl. reflexivity.
- simpl. rewrite <- IHl. simpl.

1 subgoal
X : Type
x : X
l : list X
IHl : fold_length l = length l
______________________________________(1/1)
fold_length (x :: l) = S (fold_length l)

在运行测试期间，我遇到了一个问题，即simpl拒绝深入研究，但reflexivity成功了，所以我在这里尝试了同样的事情，并且证明成功了。

请注意，在给定目标状态的情况下，人们不会期望自反性会通过，但事实确实如此。在这个例子中它有效，但它确实迫使我以与最初意图相反的方向进行重写。

是否有可能有更多的控制权，simpl以便达到预期的减少量？

Answer 1

出于这个答案的目的，我假设 的定义fold类似于

Fixpoint fold {A B: Type} (f: A -> B -> B) (u: list A) (b: B): B :=
match u with
| [] => b
| x :: v => f x (fold f v b)
end.

（基本上fold_right来自标准库）。如果您的定义有很大不同，我推荐的策略可能行不通。

这里的问题是simpl常量的行为，在简化之前必须先展开常量。从文档中：

请注意，只有其名称可以在递归调用中重用的透明常量才可能由 simpl 展开。例如，由 plus' := plus 定义的常量可能会在递归调用中展开并重用，但像 succ := plus (SO) 这样的常量永远不会展开。

这有点难以理解，所以我们举个例子。

Definition add_5 (n: nat) := n + 5.

Goal forall n: nat, add_5 (S n) = S (add_5 n).
Proof.
  intro n.
  simpl.
  unfold add_5; simpl.
  exact eq_refl.
Qed.

您将看到第一次调用simpl没有执行任何操作，尽管add_5 (S n)可以简化为S (n + 5). 但是，如果我unfold add_5先这样做，它就会完美地工作。我认为问题在于这plus_5不是直接的Fixpoint. 虽然plus_5 (S n)相当于S (plus_5 n)，但这实际上并不是它的定义。所以 Coq 不认识到它的“名称可以在递归调用中重用”。Nat.add（即“+”）直接定义为递归Fixpoint，因此simpl也简化了它。

的行为simpl可以稍微改变一下（再次参见文档）。正如安东在评论中提到的，当尝试简化时，您可以使用Arguments白话命令进行更改。告诉 Coq如果至少提供了两个参数，则应该展开（斜杠分隔左侧必需的参数和右侧不必要的参数）。[sup]1[\sup]simplArguments fold_length _ _ /.fold_length

如果您不想处理这个问题，可以使用一个更简单的策略，即cbn默认情况下在此处有效并且通常效果更好。引用文档：

cbn 策略据称是 simpl 的更有原则、更快、更可预测的替代品。

既不要simpl使用Arguments斜线，也不cbn要将目标降低到您想要的情况，因为它会展开fold_length但不会重新折叠。您可以认识到对的调用fold是公正的fold_length l，并用 重新折叠它fold (fold_length l)。

您的情况的另一种可能性是使用该change策略。看起来您已经知道fold_length (a :: l)应该简化为S (fold_length l). 如果是这种情况，您可以使用change (fold_length (a :: l)) with (S (fold_length l)).，Coq 会尝试将一种转换为另一种（仅使用基本转换规则，而不是像那样的等式rewrite）。

S (fold_length l) = S (length l)当你达到使用上述任一策略的目标后，你就可以rewrite -> IHl.按照你想要的方式使用。

1. 我认为斜线只会让simpl事情变得更少，这就是为什么我之前没有提到它。我不确定默认值实际上是什么，因为将斜杠放在任何地方似乎都会simpl展开fold_length。