Require Import List Arith Lia Permutation Extraction.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac utils_list utils_nat
                 gcd prime binomial.

From Undecidability.Shared.Libs.DLW.Vec
  Require Import pos vec.

Set Implicit Arguments.

Section Informative_Chinese_Remainder_theorems.

  Hint Resolve divides_refl divides_mult divides_mult_r : core.

  Section Binary.

    Variable (u v a b : nat) (Hu : u <> 0) (Hv : v <> 0) (Huv : is_gcd u v 1).

    Theorem CRT_bin_informative : { w | rem w u = rem a u /\ rem w v = rem b v /\ 2 < w }.
    Proof.
      destruct bezout_rel_prime with (1 := Huv) as (x & y & H1).
      assert (rem (x*u) v = rem 1 v) as H2.
      { rewrite rem_plus_div with (a := 1) (b := u*v); auto.
        rewrite <- H1; apply rem_plus_div; auto. }
      assert (rem (y*v) u = rem 1 u) as H3.
      { rewrite rem_plus_div with (a := 1) (b := u*v); auto.
        rewrite <- H1, plus_comm.
        apply rem_plus_div; auto. }
      exists (3*(u*v)+a*(y*v)+b*(x*u)); msplit 2.
      + rewrite <- rem_plus_rem, (mult_assoc b).
        rewrite rem_scal with (k := b*x), rem_diag; auto.
        rewrite Nat.mul_0_r, rem_of_0, Nat.add_0_r.
        rewrite <- rem_plus_rem, rem_scal, H3, <- rem_scal, Nat.mul_1_r.
        rewrite rem_plus_rem, plus_comm.
        symmetry; apply rem_plus_div; auto.
      + rewrite <- plus_assoc, (plus_comm (a*_)), plus_assoc.
        rewrite <- rem_plus_rem, (mult_assoc a).
        rewrite rem_scal with (k := a*y), rem_diag; auto.
        rewrite Nat.mul_0_r, rem_of_0, Nat.add_0_r.
        rewrite <- rem_plus_rem, rem_scal, H2, <- rem_scal, Nat.mul_1_r.
        rewrite rem_plus_rem, plus_comm.
        symmetry; apply rem_plus_div; auto.
      + apply lt_le_trans with (3*1); try lia.
    Qed.

  End Binary.

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

End Informative_Chinese_Remainder_theorems.

Theorem CRT u v a b : u <> 0 -> v <> 0 -> is_gcd u v 1 -> exists w, rem w u = rem a u /\ rem w v = rem b v /\ 2 < w.
Proof.
  intros Hu Hv H.
  destruct (@CRT_bin_informative u v a b) as (w & ?); auto.
  exists w; auto.
Qed.

Section sequence_of_coprimes.

  Let seq_of_coprimes_lt n i j : i < j <= n -> is_gcd (1+i*fact n) (1+j*fact n) 1.
  Proof.
    intros (H1 & H2).
    apply no_common_prime_is_coprime; try discriminate.
    intros p Hp H3 H4.
    assert (divides p ((j-i)*fact n)) as H5.
    { replace ((j-i)*fact n) with (1+j*fact n - (1+i*fact n)).
      + apply divides_minus; auto.
      + rewrite Nat.mul_sub_distr_r; lia. }
    assert (~ divides p (fact n)) as H6.
    { intros H6.
      rewrite plus_comm in H3.
      apply divides_plus_inv in H3.
      + apply divides_1_inv, Hp in H3; trivial.
      + apply divides_mult; trivial. }
    apply prime_div_mult with (1 := Hp) in H5.
    destruct H5 as [ H5 | H5 ]; try tauto.
    apply H6, divides_fact.
    assert (p <> 0) as H7.
    { apply prime_ge_2 in Hp; lia. }
    destruct Hp.
    split; try lia.
    apply divides_le in H5; lia.
  Qed.

  Theorem seq_of_coprimes n i j :
          i <= n
       -> j <= n
       -> i <> j
       -> is_gcd (1+i*fact n) (1+j*fact n) 1.
  Proof.
    intros H1 H2 H3.
    destruct (lt_eq_lt_dec i j) as [ [] | ]; try tauto;
      [ | apply is_gcd_sym ]; apply seq_of_coprimes_lt; lia.
  Qed.

End sequence_of_coprimes.

Section Godel_beta.


  Definition godel_beta a b n := rem a (S ((S n)*b)).

  Theorem godel_beta_inv n (v : vec nat n) :
     { a : nat & { b | forall p, godel_beta a b (pos2nat p) = vec_pos v p } }.
  Proof.
    set (j := S (lmax (n :: vec_list v))).
    assert (n < j) as Hm1.
    { apply le_n_S, lmax_prop; left; auto. }
    assert (forall p, vec_pos v p < j) as Hm2.
    { intros p; apply le_n_S, lmax_prop.
      right; apply vec_list_In. }
    revert Hm1 Hm2; generalize j; clear j.
    intros j Hj1 Hj2.
    set (m := vec_set_pos (fun p : pos n => 1+(S (pos2nat p)*fact j))).
    destruct (CRT_informative m v) as (w & Hw).
    + intros p; unfold m; rewrite vec_pos_set; discriminate.
    + intros p q H; unfold m; repeat rewrite vec_pos_set.
      apply seq_of_coprimes.
      * generalize (pos2nat_prop p); lia.
      * generalize (pos2nat_prop q); lia.
      * contradict H; inversion H.
        apply pos2nat_inj; auto.
    + exists w, (fact j).
      intros p; unfold godel_beta.
      generalize (Hw p); unfold m; repeat rewrite vec_pos_set.
      intros E; unfold plus in E; rewrite E.
      apply rem_idem.
      apply lt_le_trans with (1 := Hj2 _).
      apply le_trans with (S (1*j)); try lia.
      apply le_n_S, mult_le_compat; try lia.
      apply divides_le.
      * generalize (fact_gt_0 j); lia.
      * apply divides_n_fact_n; lia.
  Qed.

  Corollary godel_beta_fun_inv n f : { a : _ & { b | forall p, p < n -> f p = godel_beta a b p } }.
  Proof.
    destruct godel_beta_inv with (v := vec_set_pos (fun p : pos n => f (pos2nat p)))
       as (a & b & H).
    exists a, b; intros p Hp.
    specialize (H (nat2pos Hp)).
    rewrite vec_pos_set, pos2nat_nat2pos in H.
    auto.
  Qed.

  Theorem godel_beta_fun_inv_triples n f :
     { a : _ & { b | forall p, p < n -> f p = (godel_beta a b ( 3*p),
                                               godel_beta a b (1+3*p),
                                               godel_beta a b (2+3*p)) } }.
  Proof.
    assert (H3 : 3 <> 0) by lia.
    set (g n := match rem n 3, f (div n 3) with
      | 0, (x,_,_) => x
      | 1, (_,y,_) => y
      | _, (_,_,z) => z
    end).
    destruct (godel_beta_fun_inv (3*n) g) as (a & b & Hab).
    exists a, b; intros p Hp.
    rewrite mult_comm.
    do 2 rewrite (plus_comm _ (p*_)).
    replace (p*3) with (p*3+0) at 1 by lia.
    rewrite <- (Hab (p*3+0)), <- (Hab (p*3+1)), <- (Hab (p*3+2)); try lia.
    unfold g.
    do 3 rewrite (rem_erase p 3 _ eq_refl).
    repeat (rewrite rem_idem; try lia).
    repeat (rewrite (@div_prop (p*3+_) 3 _ _ eq_refl); try lia).
    destruct (f p) as ((?,?),?); auto.
  Qed.

End Godel_beta.