用一个关于整数的定理来证明一个关于自然数的定理

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.