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

user_10975520 0
Viewed 75

I'm not a mathematician, but I take interest in the topic and the use of proof assistants like Coq. I still need to learn a lot on how Coq works. As an exercise, I would like to proof that:

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

I failed to proof this directly and therefore thought of taking a roundtrip via the integers:

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.

I would now like to use this result to proof the initial theorem. Unfortunately, I get stuck in relating Nat.Odd to Z.Odd and the eventual application of 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.

I would like to know if I'm on the right track here. I'm also seeking for some hints on how to eventually proof T2 using the result T1 (assuming that this is actually a sensible approach to proving the initial goal using Coq).

Any help is appreciated.

coq
1 Answers

There is probably a way to prove this goal staying in Nat (by using a divisibility argument) but this approach is also feasible. The lemma L1 on which you got stuck can actually be solved in a similar fashion as the theorem T1, leveraging lia for finding the right lemmas. Then, the only thing in your way to apply T1 in the course of proving T2 is to show that Z.of_nat respects addition and multiplication: you can rely another time on lia. All together you obtain the following proof:

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.
user_78074380
Related