0 
Theorem add_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m. induction m as [| m' IHn']. rewrite -> add_0_r. rewrite <- sum.

最后一个策略rewirte <- sum不起作用。这是目标：

n: ℕ
-------------
S(n) = n + 1

我不知道如何重写n+1为S(n). 我认为这n+1只是一个符号S(n)，对吧？

4

3 回答 3

1

如果你看+下面的定义，你可以看到它是通过对它的第一个参数进行归纳定义的：

Locate "+". (* to obtain the name Nat.add *)
Print Nat.add.
(*
Nat.add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat
*)

结果1 + n确实可以转换为S n（您可以看到 using Eval cbn in 1 + ?[n].）但不是n + 1（如果unfold Nat.add.您将获得卡在变量 上的模式匹配n）。

对于您的证明，该特定定义+意味着您可能会重新考虑您的方法并尝试通过归纳n而不是m（注意拥有正确的归纳假设）来进行证明。

于 2021-12-27T02:08:37.953 回答
0

能够证明以下几点：

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m. induction n as [| n' IHn']. 
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. reflexivity.
Qed.
于 2021-12-27T03:14:48.757 回答
0

如果您使用的nat是标准库中的类型，则n+1不是 的符号S n，而是函数的符号Nat.add。在那种情况下n+1显然不等于S n。你需要通过对 的归纳来证明它n。

顺便说一句，如果您使用Nat.nat，则需要使用归纳n而不是m。因为Nat.add是由match第一个参数上的 a 定义的。在这种情况下，归纳的第一个子目标可以简单地通过reflexivity.（Coq 能够简化S (0 + m)and 0 + S m，但不能简化S (n + 0)and n + 1）来证明。

于 2021-12-27T02:10:29.500 回答