coq - 在 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

您也可以使用 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对于第一次或第二次出现。