使用整数定理证明自然数定理答案

【问题标题】：Using a theorem on integer numbers for proving a theorem on natural numbers使用整数定理证明自然数定理
【发布时间】：2021-05-01 22:23:35
【问题描述】：

我不是数学家，但我对这个主题以及 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 证明初始目标的明智方法）。

感谢任何帮助。

【问题讨论】：

标签： coq

【解决方案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.

【讨论】：