用 Coq 编写简单算术证明

Question

我想证明一些简单的事情，例如对于每个自然数 n，都存在一个自然数 k 使得：

(2*n + 1)^2 = 8*k + 1

这样的证明是如何进行的呢？我想把它分成 n 是奇数或偶数的情况，但我不知道在 Coq 中如何做到这一点。另外，Coq 中是否有内置的幂（指数）运算符？

Answer 1

是的，有许多内置函数，您只需要正确的导入集或打开正确的符号范围。进行证明的一种简单方法是使用归纳法和一些自动化，如ring、 omega或lia策略。

From Coq Require Import Arith Psatz.

Goal forall n, exists k, (2*n + 1)^2 = 8*k + 1.
Proof.
  induction n as [| n [m IH]].
  - now exists 0.
  - exists (S n + m). rewrite Nat.pow_2_r in *. lia.
Qed.