用整数定理证明自然数定理

Question

我不是数学家，但我对这个话题和 Coq 等证明助手的使用很感兴趣。关于 Coq 的工作原理，我仍然需要学习很多。作为练习，我想证明：

forall n : nat, n > 0 -> Nat.Odd n <-> Nat.Odd (5 * n + 6).

我未能直接证明这一点，因此想到通过整数进行往返：

Require Import ZArith.
Require Import Lia.

Theorem T1 : forall n : Z,
  Z.Odd n <-> Z.Odd (5 * n + 6).
Proof.
  unfold Z.Odd.
  intros. split.
  - intros. destruct H as [x G]. rewrite G. exists ((5 * x + 5)%Z). lia.
  - intros. destruct H as [x G]. exists ((-2 * n - 3 + x)%Z). lia.
Qed.

我现在想用这个结果来证明初定理。不幸的是，我陷入了 Nat.Odd 与 Z.Odd 的关联以及 T1:

的最终应用

Lemma L1 : forall n : nat,
  Z.Odd (Z.of_nat n) <-> Nat.Odd n.
Proof.
  intros.
  Admitted.

Theorem T2 : forall n : nat,
  n > 0 -> Nat.Odd n <-> Nat.Odd (5 * n + 6).
Proof.
  intros.
  pose proof T1 as G.
  rewrite <- L1.
  rewrite <- L1.
  Admitted.

我想知道我是否在正确的轨道上。我也在寻求一些关于如何使用结果 T1 最终证明 T2 的提示（假设这实际上是使用 Coq 证明初始目标的明智方法）。

感谢任何帮助。

Answer 1

可能有一种方法可以证明这个目标留在 Nat 中（通过使用可分性论证），但这种方法也是可行的。您卡住的引理 L1 实际上可以用与定理 T1 类似的方式求解，利用 lia 找到正确的引理。然后，在证明 T2 的过程中应用 T1 的唯一方法是证明 Z.of_nat 遵守加法和乘法：您可以再次依赖 lia .综上所述，您将获得以下证明：

From Coq Require Import ZArith Arith.PeanoNat Psatz.

Theorem T1 : forall n : Z, Z.Odd n <-> Z.Odd (5 * n + 6).
Admitted.

Lemma L1 (n : nat) : Z.Odd (Z.of_nat n) <-> Nat.Odd n.
Proof.
  split.
  - intros [x?]. exists (Z.to_nat x). lia.
  - intros [x?]. exists (Z.of_nat x). lia.
Qed.

Theorem T2 (n : nat) : Nat.Odd n <-> Nat.Odd (5 * n + 6).
Proof.
  do 2 rewrite <- L1.
  (* We need to massage slightly the goal to apply T1 *)
  assert (Z.of_nat (5*n + 6) = (5*(Z.of_nat n)+6)%Z) as -> by lia.
  apply T1.
Qed.

用整数定理证明自然数定理

Using a theorem on integer numbers for proving a theorem on natural numbers

coq