在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第一次或第二次出现,进一步限制简化的结果.

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 节。