How do I prove the simplified Chinese Remainder Th

Question

I've managed to prove

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

My question is how to finish the following proof (maybe using the modulo_inv theorem?):

Variables m n : Z.
Hypothesis co_prime : rel_prime m n.

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

Here is what I tried, but I don't know whether it is correct or not.

Proof.
    intros a b.
    exists ((a * n) * (n ^ (-1) mod m) + (b * m) * (m ^ (-1) mod n)).
    refine (conj _ _).
        (* case : ((a * n) * (n ^ (-1) mod m) + (b * m) * (m ^ (-1) mod n) == a [m]) *)
        red.
        rewrite Z.add_sub_swap.
        apply Z.divide_add_r.

        (* case : ((a * n) * (n ^ (-1) mod m) + (b * m) * (m ^ (-1) mod n) == b [n]) *)

Can anybody provide any suggestions?

Answer 1

Reusing the proof from Wikipedia which is based on Bézout's lemma, we get the following:

From Coq Require Import ZArith Znumtheory.
Import Z.

Definition modulo (a b n : Z) : Prop := (n | (a - b)).
Notation "a == b [ n ]" := (modulo a b n) (at level 50).

Section SimpleChineseRemainder.
Variables m n : Z.
Hypothesis co_prime : rel_prime m n.

Theorem SimpleChineseRemainder a b :  exists x : Z, (x == a [[m]]) /\ (x == b [[n]]).
Proof.
  destruct (rel_prime_bezout _ _ co_prime) as [u v Eq].
  exists (a * v * n + b * u * m); split; [| rewrite add_comm in *];
  match goal with |- _ == ?c [_] => replace c with (c * 1) at 2 by apply mul_1_r end;
  rewrite <-Eq, mul_add_distr_l, !mul_assoc;
  now eexists; rewrite add_add_simpl_l_r, <-mul_sub_distr_r.
Qed.
End SimpleChineseRemainder.

Answer 2

Code-golfing Anton's answer, I was hoping that ring would be clever enough to use the Eq information, and that the proof would simply be

Theorem SimpleChineseRemainder' a b :  exists x : Z, (x == a [m]) /\ (x == b [n]).
Proof.
  destruct (rel_prime_bezout _ _ co_prime) as [u v Eq];
  exists (a * v * n + b * u * m); split ; [ exists ((b-a)*u) | exists ((a-b)*v)]; ring.
Qed.

Unfortunately it didn't automatically exploit that u * m + v * n = 1 -> u * m = 1 - v * n. So until we have a stronger tactic, I guess that has to be added manually, like so:

Theorem SimpleChineseRemainder' a b : exists x : Z, (x == a [m]) /\ (x == b [n]).
Proof.
  destruct (rel_prime_bezout _ _ co_prime) as [u v Eq].
  exists (a * (v * n) + b * (u * m)); split ; [ exists ((b-a)*u) | exists ((a-b)*v)].
  - replace (v*n) with (1-u*m) by (rewrite <- Eq; ring); ring.
  - replace (u*m) with (1-v*n) by (rewrite <- Eq; ring); ring.
Qed.

EDIT: The nsatz tactic is able to solve the equation system. However, it introduces a notation for [ ... ] that conflicts with the notation introduced above, and I don't know how to handle that. However, by changing the notation to i.e. [[ ... ]], the proof becomes just two lines:

Require Import Nsatz.
Theorem SimpleChineseRemainder' a b :
  exists x : Z, (x == a [[m]]) /\ (x == b [[n]]).
Proof.
  destruct (rel_prime_bezout _ _ co_prime) as [u v Eq];
  exists (a * v * n + b * u * m); split ; [ exists ((b-a)*u) | exists ((a-b)*v)]; nsatz.
Qed.