coq - 在 coq 中应用原生归纳原理和几个参数

Question

我正在阅读《软件基础》一书。在“关于归纳的更多信息”一章中，作者讨论了在定义归纳类型时由 coq 生成的归纳原理。

下面是一个练习。在定义中封装“+”的关联概念，然后在其上应用 nat_ind。

我对定义的第一个猜测如下：

Definition P_plusassoc (n m o:nat) : Prop :=
  n + (m+ o) = (n+m) +o.

但是，当我想证明这一点时，我遇到了问题：

Theorem plus_assoct : forall o m n, P_plusassoc n m o.
Proof.
  apply nat_ind.

nat_ind不起作用。所以我认为这是因为P_plusassoc不依赖于一个整数而是三个。

所以我这样重写P_plusassoc：

Definition P_plusassoc (n:nat) : nat->nat->Prop :=
      fun (m o:nat) => n + (m+ o) = (n+m) +o.

但它仍然不起作用。问题出在哪里？我如何定义P_plusassoc使用nat_ind？

score 1 · Accepted Answer

书后给出了答案。定义可以是：

Definition P_plusassoc (n:nat) : Prop :=
      forall m o, n + (m+ o) = (n+m) +o.

score 0 · Accepted Answer

这个问题要你证明一个引理。但是，您正在定义一个函数。你应该做的是定义 Prop 类型的东西（比如Definition P_plusassoc (n:nat) : Prop := forall m o, n + (m+ o) = (n+m) +o.）。

就个人而言，我会定义一个Lemma : forall m n o :nat, n+(m+o)=(n+m)+o.Coq，然后你可以证明这个引理，你可以通过intros. apply (nat_ind n).

2 回答 2