逐步简化coq？

Question

有没有一种方法可以一次简化一个步骤？

假设你有 f1 (f2 x)，这两个都可以通过一个 simpl 依次简化，是否有可能简化 f2 x 作为第一步，检查中间结果和然后简化 f1?

以定理为例：

Theorem pred_length : forall n : nat, forall l : list nat,
  pred (length (n :: l)) = length l.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

simpl 策略将 Nat.pred (length (n :: l)) 简化为 length l。有没有办法将其分解为两步简化，即：

Nat.pred (length (n :: l)) --> Nat.pred (S (length l)) --> length l

Answer 1

我们可以关闭 pred 的简化，简化其参数，然后重新打开它：

Theorem pred_length : forall n : nat, forall l : list nat,
  pred (length (n :: l)) = length l.
Proof.
  intros.
  Arguments pred : simpl never.    (* do not unfold pred *)
  simpl.
  Arguments pred : simpl nomatch.  (* unfold if extra simplification is possible *)
  simpl.
  reflexivity.
Qed.

有关详细信息，请参阅参考手册的 §8.7.4。

Answer 2

您还可以对特定模式使用 simpl。

Theorem pred_length : forall n : nat, forall l : list nat,
  pred (length (n :: l)) = length l.
Proof.
 intros.
 simpl length.
 simpl pred.
 reflexivity.
Qed.

如果您多次出现类似 length 的可以简化的模式，您可以通过给出出现的位置（从左到右）来进一步限制简化的结果，例如simpl length at 1 或 simpl length at 2 表示第一次或第二次出现。

逐步简化coq？

Step by step simplification in coq?

coq