逐步简化coq？ [英] Step by step simplification in coq?

问题描述

是否可以一次简化一个步骤？

Is there a way to simplify one step at a time?

假设您有 f1（f2 x）两者都可以通过单个 simpl 依次简化，是否有可能首先简化 f2 x 步骤，检查中间结果，然后简化 f1 ？

Say you have f1 (f2 x) both of which can be simplified in turn via a single simpl, is it possible to simplify f2 x as a first step, examine the intermediate result and then simplify 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（长度（n :: l））到长度l 。有没有办法将其分解为两步简化，即：

The simpl tactic simplifies Nat.pred (length (n :: l)) to length l. Is there a way to break that into a two step simplification i.e:

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

推荐答案

您也可以使用简单表示特定模式。

You can also use simpl for a specific pattern.

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 可以简化，您可以通过给出出现的位置（从左到右）来进一步限制简化的结果，例如第一次出现或第二次出现的简单长度为1 或简单长度为2 。

In case you have several occurrences of a pattern like length that could be simplified, you can further restrict the outcome of the simplification by giving a position of that occurrence (from left to right), e.g. simpl length at 1 or simpl length at 2 for the first or second occurrence.

这篇关于逐步简化coq？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！