coq - 当 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 :

Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by simpl. For instance a constant defined by plus' := plus is possibly unfolded and reused in the recursive calls, but a constant such as succ := plus (S O) is never unfolded.

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

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)。但是，如果我先展开 add_5，它就可以正常工作。我认为问题在于 plus_5 并不是直接的 Fixpoint。虽然 plus_5 (S n) 等同于 S (plus_5 n)，但这实际上并不是它的定义。所以 Coq 不认识到它的“名称可以在递归调用中重用”。 Nat.add(即“+”)直接定义为递归Fixpoint，因此simpl确实简化了它。

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

如果您不想处理这个问题，可以使用一个更简单的策略，那就是 cbn，它默认在此处工作，并且一般情况下效果更好。引用自the documentation :

The cbn tactic is claimed to be a more principled, faster and more predictable replacement for simpl.

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

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

使用上述任一策略实现 S (fold_length l) = S (length l) 的目标后，您可以使用 rewrite -> IHl。 就像你想要的那样。

---

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