有没有一种逐步简化的方法?
假设你有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
f (g x)
与simpl f.
一起使用时,也会使用g
的定义进行简化。在这个例子中,是否可能指示 Coq 只使用f
的定义进行简化,并保持g x
不变? - Waiting for Dev...