小编Ant*_*erM的帖子

假设我们有以下形式的结论：a + b + c + d + e。
我们还有一个引理：plus_assoc : forall n m p : nat, n + (m + p) = n + m + p。

将术语任意“插入一对括号”的惯用方法是什么？也就是说，如果有多个可用位置，我们如何轻松地选择重写位置。

我最终要做的事情如下：

replace (a + b + c + d + e)
with (a + b + c + (d + e))
by now rewrite <- ?plus_assoc

尽管此公式确实说明了我要执行的操作，但是对于比“ ab c ...”更复杂的公式而言，它变得非常漫长。

假设以下特定场景.

我们有一个平等的定义:

Inductive eqwal {A : Type} (x : A) : A -> Prop :=
    eqw_refl : eqwal x x.

和peano nats:

Inductive nawt : Prop :=
    | zewro : nawt
    | sawc  : nawt -> nawt.

我们在nat上定义了加法:

Fixpoint plaws (m n : nawt) : nawt :=
    match m with
      | zewro => n
      | sawc m' => sawc (plaws m' n)
    end.

现在我们想证明零从正确的wrt中立.总结:

Theorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n.

可悲的是,以下证明文件的最后一行说" 错误:n用于结论. ".

Proof. …