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

- savx2

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表示第一次或第二次出现。

- ichistmeinname

---

非常有用！但我发现这简化了模式中的所有内容。例如 f (g x) 与 simpl f. 一起使用时，也会使用 g 的定义进行简化。在这个例子中，是否可能指示 Coq 只使用 f 的定义进行简化，并保持 g x 不变？ - Waiting for Dev...

Answer 2

我们可以关闭对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了解更多详情。

- Anton Trunov

---

@Savvas Savvides 谢谢您接受我的答案，但我想恭敬地建议您不要太早接受答案，因为这可能会阻止一些用户提供他们自己的高质量答案，而我们都对此感兴趣。最好等待至少24小时。祝您愉快并祝您好运 :) - Anton Trunov