当 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 的行为，在简化之前必须展开常量。来自the documentation：

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

这个有点难理解，举个例子吧。

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 的行为可以稍作更改（再次参见文档）。正如 Anton 在 cmets 中提到的，当simpl 尝试简化时，您可以使用Arguments 白话命令进行更改。 Arguments fold_length _ _ /. 告诉 Coq，如果至少提供了两个参数，则应该展开 fold_length（斜线分隔左侧的必需参数和右侧的不必要参数）。[sup]1[\sup]

如果您不想处理这个问题，可以使用更简单的策略cbn，它默认在这里有效，并且总体上效果更好。引用the documentation:

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。