proposition: Theorem CRT_informative n (m v : vec nat n) : (forall p, vec_pos m p <> 0) -> (forall p q, p <> q -> is_gcd (vec_pos m p) (vec_pos m q) 1) -> { w | forall p, rem w (vec_pos m p) = rem (vec_pos v p) (vec_pos m p) }.
proof: Proof. destruct n as [ | n ]; [ exists 0; intros p; invert pos p | ]. revert m v. induction n as [ | n IHn ]; intros m v H1 H2. + exists (vec_pos v pos0); intros p; invert pos p; auto. invert pos p. + revert H1 H2. vec split m with m1. vec split m with m2. vec split v with v1. vec split v with v2. intros H1 H2. generalize (H1 pos0) (H1 pos1) (H2 pos0 pos1); intros Hm1 Hm2 H12; simpl in Hm1, Hm2, H12. destruct (@CRT_bin_informative m1 m2 v1 v2) as (w0 & H3 & H4 & _); auto. { apply H12; discriminate. } destruct (IHn (m1*m2 ## m) (w0 ## v)) as (w & Hw). * intros p; invert pos p. - assert (0 < m1 * m2); try lia. - apply H1 with (p := pos_nxt (pos_nxt p)). * intros p q; invert pos p; invert pos q; intros H; try (destruct H; auto; fail). 2: apply is_gcd_sym. 1,2: apply rel_prime_mult; [ apply (H2 pos0 (pos_nxt (pos_nxt _))) | apply (H2 pos1 (pos_nxt (pos_nxt _))) ]; discriminate. apply (H2 (pos_nxt (pos_nxt _)) (pos_nxt (pos_nxt _))). contradict H; apply pos_nxt_inj in H; auto. * exists w. intros p; repeat invert pos p. - rewrite <- H3. generalize (Hw pos0); simpl. apply divides_rem_congr, divides_mult_r, divides_refl. - rewrite <- H4. generalize (Hw pos0); simpl. apply divides_rem_congr, divides_mult, divides_refl. - apply Hw with (p := pos_nxt _). Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd prime binomial) Undecidability.Shared.Libs.DLW.Vec(pos vec)