How to prove Chinese Remainder Theorem by Coq?

Question

I have already have the following definition and notation:

Definition modulo (a b n : Z) : Prop := (n | (a - b)) .

Notation "( a == b [ n ])" := (modulo a b n) .

And following lemmas(all of them are already proved, ends up with Qed .):

Lemma modulo_refl : forall a n : Z, (a == a [ n ]) .

Lemma modulo_symm : forall a b n : Z, (a == b [ n ]) -> (b == a [ n ]) .

Lemma modulo_tran : forall a b c n : Z, (a == b [ n ]) -> (b == c [ n ]) -> (a == c [ n ]) .

Lemma modulo_plus_comm : forall a b n : Z, (a + b == b + a [ n ]) .

Lemma modulo_plus_assoc : forall a b c n : Z, (a + b + c == a + (b + c) [ n ]) .

Lemma modulo_plus_subst : forall a b c n : Z, (a == b [ n ]) -> (a + c == b + c [ n ]) .

Now I want to prove the ChineseRemainderTheorem:

Hypothesis m n : Z .

Hypothesis co_prime : rel_prime m n .

Theorem modulo_inv : forall m n : Z, rel_prime m n -> exists x : Z, (m * x == 1 [ n ]) .

Theorem ChineseRemainderTheorem : forall a b : Z, exists x : Z, (x == a [ m ]) /\ (x == b [ n ]) .

How can I do this?

Answer 1

You already have those definitions in the standard library, file Require Import ZArith.Znumtheory.. Then we could prove the Chinese remainder theorem like this

Lemma ChineseRemainder : forall n p a b : Z,
    n <> 0 ->
    p <> 0 ->
    rel_prime n p ->
    exists x:Z, (x mod n = a mod n) /\ (x mod p = b mod p). 
Proof.
  intros n p a b npos ppos coprime. 
  destruct (rel_prime_bezout _ _ coprime) as [u v H0].
  exists (a*v*p+b*u*n). split.
  - rewrite Z.mod_add. 2: exact npos.
    rewrite <- Z.mul_assoc, <- Zdiv.Zmult_mod_idemp_r.
    assert ((u * n + v * p) mod n = 1 mod n) as H.
    rewrite H0. reflexivity.
    rewrite Z.add_comm, Z.mod_add in H. rewrite H.
    rewrite Zdiv.Zmult_mod_idemp_r, Z.mul_1_r.
    reflexivity. exact npos.
  - rewrite Z.add_comm, Z.mod_add. 2: exact ppos.
    rewrite <- Z.mul_assoc, <- Zdiv.Zmult_mod_idemp_r.
    assert ((u * n + v * p) mod p = 1 mod p) as H.
    rewrite H0. reflexivity.
    rewrite Z.mod_add in H. rewrite H.
    rewrite Zdiv.Zmult_mod_idemp_r, Z.mul_1_r.
    reflexivity. exact ppos.
Qed.