Proving Gauss' theorem for nat in Coq

Question

I'd like to prove Gauss' theorem for nat.

In plain (non-precise) language it says: if a divides b*c and none of a's factors are in b then they must all be in c.

Require Import NPeano. 
Theorem Gauss_nat: forall (a b c:nat), gcd a b = 1 -> (a | (b*c)) -> (a | c).

The theorem is already defined for integers Z, see here in the Coq manual. But I need it for nat. The recommendations I have gotten so far is to use Bezout's lemma which states that

Lemma Bezout: forall (a b c:Z), Z.gcd a b = c -> exists u v, u*a+v*b=c.

However, I can't use it directly for nats since the coefficients u and v might be negative and thus it doesn't hold for nat.

Is there another proof that does not use integers in the proof?

EDIT:

As was pointed out in a comment by Mark Dickinson, the theorem and lemma are already in Coq's library. They are in NPeano, named Nat.gcd_bezout and Nat.gauss.

You could prove and use a nat-based version of Bezout: forall (a b:nat), exists u v, u*a = gcd a b + v*b. — Mark Dickinson
That would be perfect! Could you give an "Answer" with a Coq prof of a nat-based Bezout and how Gauss_nat follows from it? — larsr
(Or at least bezout_nat, I was able to prove Gauss_nat by using it....) — larsr
It looks as though these results are already in the standard library: look for gcd_bezout_pos_pos, gcd_bezout, and gauss. — Mark Dickinson
Proof is here: github.com/coq/coq/blob/V8.4/theories/Numbers/Natural/Abstract/… — Mark Dickinson

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2015-11-21T08:41:52

If you just want to obtain the result for nat, and not really avoid the use of Z, you can just reuse the proof in the standard library. Here's a sketch of how you could proceed, relying on two auxiliary lemmas:

Require Import NPeano.
Require Import ZArith.
Require Import ZArith.Znumtheory.
Require Import Omega.

Close Scope Z_scope.

Lemma Zdiv_Ndiv a b : (a | b) <-> (Z.of_nat a | Z.of_nat b)%Z.
Proof. Admitted.

Lemma Zgcd_Ngcd a b : Z.of_nat (gcd a b) = Z.gcd (Z.of_nat a) (Z.of_nat b).
Proof. Admitted.

Theorem Gauss_nat a b c : gcd a b = 1 -> (a | (b*c)) -> (a | c).
Proof.
rewrite Zdiv_Ndiv, Zdiv_Ndiv, Nat2Z.inj_mul.
intros H1 H2.
assert (H3 : Z.of_nat (gcd a b) = 1%Z) by (rewrite H1; reflexivity).
rewrite Zgcd_Ngcd in H3.
apply (Gauss _ _ _ H2).
now rewrite <- Zgcd_1_rel_prime.
Qed.

Proving Gauss' theorem for nat in Coq

1 Answers