Require Import List Arith Lia Bool Permutation.

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

Set Implicit Arguments.

Section prime.

  Hint Resolve divides_mult divides_refl divides_0_inv : core.

  Infix "<d" := divides (at level 70, no associativity).

  Definition prime p := p 1 q, q <d p q = 1 q = p.

  Fact prime_2 : prime 2.
  Proof.
    split; try .
    apply divides_2_inv.
  Qed.


  Hint Resolve : core.

  Fact prime_algo p : prime p p = 2 3 p 2 <d p n, 3+2*n < p 3+2*n <d p.
  Proof.
    split.
    + intros ( & ).
      destruct (le_lt_dec 3 p) as [ H | H ].
      * right; split; auto; split.
        - intros ; apply in ; .
        - intros n Hn C; apply in C; .
      * left; destruct p as [ | [ | [ | p ] ] ]; try .
        destruct ( 2); try .
        exists 0; auto.
    + intros [ | ( & & ) ].
      * subst; auto.
      * split; try .
        intros q Hq.
        destruct (euclid_2 q) as (k & [ | ]).
        - destruct ; apply divides_trans with (2 := Hq).
          exists k; .
        - destruct k; try .
          destruct (le_lt_dec p (3+2*k)) as [ | ].
          ++ apply divides_le in Hq; .
          ++ destruct ( k); auto.
             eq goal Hq; f_equal; .
  Qed.


  Definition divides_bool n p :=
    match p mod n with
      | 0 true
      | _ false
    end.

  Fact modS_divide n p : p mod S n = 0 S n <d p.
  Proof.
    rewrite Nat.mod_divide; try discriminate; tauto.
  Qed.


  Fact divides_bool_spec n p : divides_bool (S n) p = true S n <d p.
  Proof.
    unfold divides_bool.
    generalize (modS_divide n p).
    case_eq (p mod S n); try tauto.
    intros k ; split; discriminate.
  Qed.


  Fact divides_bool_spec' n p : divides_bool (S n) p = false S n <d p.
  Proof.
    rewrite divides_bool_spec.
    destruct (divides_bool (S n) p); now split.
  Qed.


  Fixpoint prime_bool_rec n p : bool :=
    match n with
      | 0 true
      | 1 true
      | 2 true
      | S (S n') negb (divides_bool n p) && prime_bool_rec n' p
    end.

  Fact prime_bool_rec_spec n p : n p prime_bool_rec n p = true k, 3 n-2*k n-2*k <d p.
  Proof.
    induction on n as IHn with measure n; intros Hn.
    destruct n as [ | [ | [ | n' ] ] ].
    1-3: split; try (simpl; auto; fail); intros _ k H; .
    unfold prime_bool_rec; fold (prime_bool_rec (S n') p).
    revert Hn; set (m := S n'); intros Hn.
    rewrite andb_true_iff, negb_true_iff, divides_bool_spec', IHn; try .
    split.
    + intros ( & ) [ | q ] .
      * apply in ; auto.
      * apply ( q); try .
        eq goal ; f_equal; .
    + intros ; split.
      * apply ( 0); .
      * intros k ; apply ( (S k)); try .
        eq goal ; f_equal; .
  Qed.



  Definition prime_bool p :=
    Nat.eqb p 2 || Nat.leb 3 p && negb (divides_bool 2 p) && prime_bool_rec (p-2) p.

  Theorem prime_bool_spec p : prime_bool p = true prime p.
  Proof.
    unfold prime_bool.
    rewrite orb_true_iff, !andb_true_iff, negb_true_iff, divides_bool_spec'.
    rewrite Nat.eqb_eq, Nat.leb_le.
    split.
    + intros [ | (( & ) & ) ].
      * subst; auto.
      * split; try .
        destruct (euclid_2 p) as (p' & [ Hp | Hp ]).
        { destruct ; exists p'; . }
        destruct p' as [ | p' ]; try (exfalso; ).
        rewrite prime_bool_rec_spec in ; try .
        intros q Hq.
        destruct (euclid_2 q) as (k & [ | ]).
        - destruct ; apply divides_trans with (2 := Hq); exists k; .
        - destruct k as [ | k ]; try .
          destruct (le_lt_dec p q) as [ | ].
          ++ apply divides_le in Hq; .
          ++ assert (k < p') as by .
             destruct ( (p'-S k)); try .
             eq goal Hq; f_equal; .
    + intros ( & ).
      destruct (le_lt_dec 3 p) as [ | ].
      * right; lsplit 2; auto.
        - intros C; apply in C; .
        - apply prime_bool_rec_spec; try .
          intros q .
          apply in ; .
      * left; destruct p; try .
        destruct ( 2); try .
        exists 0; auto.
  Qed.


  Fact prime_ge_2 p : prime p 2 p.
  Proof.
    destruct p as [ | [ | p ] ]; try .
    + intros [ _ H ]; subst.
      destruct (H 2); auto; discriminate.
    + intros [ [] _ ]; auto.
  Qed.


  Fact prime_gcd p q : prime p is_gcd p q 1 p <d q.
  Proof.
    intros H.
    generalize (gcd p q) (gcd_spec p q); intros g Hg.
    destruct (proj2 H _ (proj1 Hg)); subst; auto.
    right; apply Hg.
  Qed.


  Fact prime_div_mult p x y : prime p p <d x*y p <d x p <d y.
  Proof.
    intros .
    destruct (prime_gcd x ); auto.
    right; revert H ; apply is_rel_prime_div.
  Qed.


  Definition prime_or_div p : 2 p { q | 2 q < p q <d p } + { prime p }.
  Proof.
    intros Hp.
    destruct bounded_search with (m := S p) (P := n 2 n < p n <d p)
      as [ (q & & ) | ].
    + intros n _.
      destruct (le_lt_dec p n).
      { right; intros; . }
      destruct (le_lt_dec 2 n).
      * destruct (divides_dec p n) as [ (?&?) | ].
        - left; subst; auto.
        - right; tauto.
      * right; .
    + left; exists q; split; try tauto; try .
    + right; split; auto.
      * .
      * intros q Hq.
        destruct q as [ | q]; auto.
        - apply divides_0_inv in Hq; auto.
        - assert ( 2 S q < p) as .
          { intros H; apply ( (S q)); auto.
            apply le_n_S, divides_le; auto; . }
          apply divides_le in Hq; .
  Qed.


  Theorem prime_factor n : 2 n { p | prime p p <d n }.
  Proof.
    induction on n as IHn with measure n; intro Hn.
    destruct (prime_or_div Hn) as [ (q & & ) | ].
    2: exists n; auto.
    destruct (IHn q) as (p & & ); try .
    exists p; split; auto.
    apply divides_trans with (1 := ); auto.
  Qed.


  Section prime_rect.

    Variables (P : Type)
              ( : P 0)
              ( : P 1)
              (HPp : p, prime p P p)
              (HPm : x y, P x P y P (x*y)).

    Theorem prime_rect n : P n.
    Proof.
      induction on n as IHn with measure n.
      destruct n as [ | [ | n ] ]; auto.
      destruct (@prime_factor (S (S n))) as (p & & ); try .
      apply divides_div in .
      rewrite .
      apply HPm.
      + apply IHn.
        rewrite at 2.
        rewrite Nat.mul_1_r at 1.
        apply prime_ge_2 in .
        apply mult_lt_compat_l; try .
      + apply HPp, .
    Qed.


  End prime_rect.

  Corollary no_common_prime_is_coprime x y : x 0 ( p, prime p p <d x p <d y False) is_gcd x y 1.
  Proof.
    intros Hx H; split; [ | split ].
    + apply divides_1.
    + apply divides_1.
    + intros k .
      destruct k as [ | [ | k ] ].
      * apply divides_0_inv in ; .
      * apply divides_1.
      * destruct prime_factor with (n := S (S k)) as (p & & ); try .
        exfalso; apply H with p; auto; apply divides_trans with (S (S k)); auto.
  Qed.


  Fact rel_prime_mult a b c : is_gcd a c 1 is_gcd b c 1 is_gcd (a*b) c 1.
  Proof.
    intros ; msplit 2; try apply divides_1.
    intros k .
    apply ; auto.
    apply is_rel_prime_div with (2 := ).
    apply is_gcd_sym in .
    revert ; apply divides_is_gcd; auto.
  Qed.


  Fact is_rel_prime_mult p q l : is_gcd p q 1 is_gcd p l 1 is_gcd p (q*l) 1.
  Proof.
    intros .
    destruct p as [ | p ].
    + generalize (is_gcd_fun (is_gcd_0l _)) (is_gcd_fun (is_gcd_0l _)).
      intros; subst; auto.
    + apply no_common_prime_is_coprime; try .
      do 2 (apply proj2 in ; apply proj2 in ).
      intros k Hk .
      apply prime_div_mult with (1 := Hk) in .
      destruct as [ | ];
      [ generalize ( _ )
      | generalize ( _ ) ];
        intro ; apply divides_1_inv in ; subst;
        destruct Hk; .
  Qed.


  Fact is_rel_prime_expo p q l : is_gcd p q 1 is_gcd p (mscal mult 1 l q) 1.
  Proof.
    intros H.
    induction l as [ | l IHl ].
    + rewrite mscal_0; apply is_gcd_1r.
    + rewrite mscal_S; apply is_rel_prime_mult; auto.
  Qed.



  Notation lprod := (fold_right mult 1).

  Fact lprod_ge_1 l : Forall prime l 1 lprod l.
  Proof.
    induction 1 as [ | x l H IH ]; simpl; auto.
    change 1 with (1*1) at 1; apply mult_le_compat; auto.
    apply prime_ge_2 in H; .
  Qed.


  Fact lprod_app l m : lprod (lm) = lprod l * lprod m.
  Proof. induction l; simpl; . Qed.

  Theorem prime_decomp n : n 0 { l | n = lprod l Forall prime l }.
  Proof.
    induction on n as IHn with measure n; intro Hn.
    destruct (eq_nat_dec n 1) as [ Hn' | Hn' ].
    + exists nil; simpl; auto.
    + destruct (@prime_factor n) as (p & & ); try .
      apply divides_div in ; revert .
      generalize (div n p); intros k Hk.
      assert (k 0) as Hk'.
      { intros ?; subst; destruct Hn; auto. }
      destruct (IHn k) as (l & & ); auto.
      - rewrite Hk.
        generalize (prime_ge_2 ).
        rewrite mult_comm.
        destruct p as [ | [ | p ] ]; simpl; intros; .
      - exists (p::l); split; auto.
        simpl; rewrite , mult_comm; auto.
  Qed.


  Hint Resolve lprod_ge_1 prime_ge_2 : core.

  Fact prime_in_decomp p l : prime p Forall prime l p <d lprod l In p l.
  Proof.
    intros .
    induction 1 as [ | x l Hl IHl ]; simpl; intros .
    + apply divides_1_inv in ; apply (proj1 ); auto.
    + destruct (prime_gcd x ) as [ | ].
      apply is_rel_prime_div with (1 := ) in ; auto.
      apply (proj2 Hl) in .
      destruct as [ | ]; auto.
      contradict ;apply .
  Qed.



  Theorem prime_decomp_uniq l m : Forall prime l Forall prime m lprod l = lprod m l p m.
  Proof.
    intros H; revert H m.
    induction 1 as [ | x l Hx Hl IHl ].
    + induction 1 as [ | y m Hy Hm IHm ]; simpl; auto.
      intros C; exfalso.
      assert (2*1 y*lprod m) as D.
      { apply mult_le_compat; auto. }
      simpl in D; .
    + simpl; intros m Hm .
      assert (In x m) as .
      { apply prime_in_decomp with (1 := Hx); auto.
        exists (lprod l); rewrite mult_comm; auto. }
      apply in_split in .
      destruct as ( & & ); subst.
      apply Permutation_cons_app, IHl.
      * rewrite Forall_app in Hm.
        destruct Hm as [ ? Hm ].
        inversion Hm.
        apply Forall_app; auto.
      * rewrite lprod_app.
        rewrite lprod_app in ; simpl in .
        rewrite mult_assoc, (mult_comm _ x), mult_assoc in .
        apply Nat.mul_cancel_l in ; auto.
        apply prime_ge_2 in Hx; .
  Qed.


End prime.

Section base_decomp.


  Fixpoint expand p l :=
    match l with
      | nil 0
      | x::l x+p*expand p l
    end.

  Notation power := (mscal mult 1).

  Fact expand_app p l m : expand p (lm) = expand p l + power (length l) p * expand p m.
  Proof.
    induction l as [ | x l IH ]; simpl; try .
    rewrite power_S, IH, Nat.mul_add_distr_l, mult_assoc; .
  Qed.


  Fact expand_0 p l : Forall (eq 0) l expand p l = 0.
  Proof.
    induction 1 as [ | x l ]; simpl; subst; auto.
    rewrite , mult_comm; auto.
  Qed.


  Section base_p.

    Variables (p : ) (Hp : 2 p).

    Let base_p_full n : { l | n = expand p l }.
    Proof.
      induction on n as IH with measure n.
      destruct (eq_nat_dec n 0) as [ Hn | Hn ].
      + exists nil; auto.
      + destruct (@euclid n p) as (m & r & & ); try .
        destruct (IH m) as (l & ).
        * destruct m; try .
          rewrite , mult_comm.
          apply lt_le_trans with (2*S m + r); try .
          apply plus_le_compat; auto.
          apply mult_le_compat; auto.
        * exists (r::l); simpl.
          rewrite mult_comm, plus_comm, , ; auto.
    Qed.


    Definition base_p n := proj1_sig (base_p_full n).
    Fact base_p_spec n : n = expand p (base_p n).
    Proof. apply (proj2_sig (base_p_full n)). Qed.

    Fact base_p_uniq l1 l2 : ( x y x < p y < p) expand p = expand p = .
    Proof.
      induction 1 as [ | ]; auto; simpl; intros .
      rewrite (plus_comm ), (plus_comm ), (mult_comm p), (mult_comm p) in .
      apply div_rem_uniq in ; try .
      destruct as [ ]; subst; f_equal; auto.
    Qed.


  End base_p.

End base_decomp.