相关疑难解决方法(0)

有没有办法一次简化一步？

假设您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

这种simpl策略展现出像2 + a"匹配树"这样的表达方式,这些表达方式看起来并不简单.例如:

Goal forall i:Z, ((fun x => x + i) 3 = i + 3).
simpl.

导致:

forall i : Z,
match i with
| 0 => 3
| Z.pos y' =>
    Z.pos
      match y' with
      | q~1 =>
          match q with
          | q0~1 => (Pos.succ q0)~1
          | q0~0 => (Pos.succ q0)~0
          | 1 => 3
          end~0
      | q~0 =>
          match q with
          | q0~1 => (Pos.succ q0)~0
          | q0~0 => q0~1
          | 1 …