问题描述
是否可以一次简化一个步骤?
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 $ c的模式$ c>可以简化,您可以通过给出出现的位置(从左到右)来进一步限制简化的结果,例如第一次出现或第二次出现的
简单长度为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?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!