(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** Prime numbers *)

Require Import List Arith Omega Permutation.

Require Import utils_tac utils_list utils_nat gcd sums.

Set Implicit Arguments.

Section prime.

  Hint Resolve divides_0 divides_mult divides_refl divides_0_inv.

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

  Definition prime p := p <> 1 /\ forall q, q <d p -> q = 1 \/ q = p.

  Fact prime_2 : prime 2.
  Proof. 
(* Goal: prime (S (S O)) *)
    split; try omega.
(* Goal: forall (q : nat) (_ : divides q (S (S O))), or (@eq nat q (S O)) (@eq nat q (S (S O))) *)
    apply divides_2_inv.
  Qed.

  Fact prime_ge_2 p : prime p -> 2 <= p.
  Proof.
(* Goal: forall _ : prime p, le (S (S O)) p *)
    destruct p as [ | [ | p ] ]; try omega.
    + intros [ _ H ]; subst.
(* Goal: le (S (S O)) O *)
      destruct (H 2); auto; discriminate.
    + intros [ [] _ ]; auto.
  Qed.

  Fact prime_gcd p q : prime p -> is_gcd p q 1 \/ p <d q.
  Proof.
(* Goal: forall _ : is_gcd p q (S O), is_gcd p (@mscal nat Init.Nat.mul (S O) l q) (S O) *)
    intros H.
(* Goal: or (is_gcd p q (S O)) (divides p q) *)
    generalize (gcd p q) (gcd_spec p q); intros g Hg.
(* Goal: or (is_gcd p q (S O)) (divides p q) *)
    destruct (proj2 H _ (proj1 Hg)); subst; auto.
(* Goal: or (is_gcd p q (S O)) (divides p q) *)
    right; apply Hg.
  Qed.

  Fact prime_div_mult p x y : prime p -> p <d x*y -> p <d x \/ p <d y. 
  Proof.
(* Goal: forall (_ : is_gcd p q (S O)) (_ : is_gcd p l (S O)), is_gcd p (Init.Nat.mul q l) (S O) *)
    intros H1 H2.
(* Goal: or (divides p x) (divides p y) *)
    destruct (prime_gcd x H1); auto.
(* Goal: or (divides p x) (divides p y) *)
    right; revert H H2; apply is_rel_prime_div.
  Qed.

  Definition prime_or_div p : 2 <= p -> { q | 2 <= q < p /\ q <d p } + { prime p }.
  Proof.
(* Goal: forall _ : le (S (S O)) p, sumor (@sig nat (fun q : nat => and (and (le (S (S O)) q) (lt q p)) (divides q p))) (prime p) *)
    intros Hp.
    destruct bounded_search with (m := S p) (P := fun n => 2 <= n < p /\ n <d p)
      as [ (q & H1 & H2) | H1 ].
    + intros n _.
(* Goal: sum (and (and (le (S (S O)) n) (lt n p)) (divides n p)) (forall _ : and (and (le (S (S O)) n) (lt n p)) (divides n p), False) *)
      destruct (le_lt_dec p n).
(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
      { right; intros; omega. }
(* Goal: sum (and (and (le (S (S O)) n) (lt n p)) (divides n p)) (forall _ : and (and (le (S (S O)) n) (lt n p)) (divides n p), False) *)
      destruct (le_lt_dec 2 n).
      * destruct (divides_dec p n) as [ (?&?) | ].
        - left; subst; auto.
        - right; tauto.
      * right; omega.
    + left; exists q; split; try tauto; try omega.
    + right; split; auto.
      * omega.
      * intros q Hq.
(* Goal: or (@eq nat q (S O)) (@eq nat q p) *)
        destruct q as [ | q]; auto.
        - apply divides_0_inv in Hq; auto.
        - assert (~ 2 <= S q < p) as H2.
(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
          { intros H; apply (H1 (S q)); auto.
            apply le_n_S, divides_le; auto; omega. }
(* Goal: not (@eq nat p (S O)) *)
          apply divides_le in Hq; omega.
  Qed.

(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
  Theorem prime_factor n : 2 <= n -> { p | prime p /\ p <d n }.
  Proof.
(* Goal: forall _ : not (@eq nat n O), @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
    induction on n as IHn with measure n; intro Hn.
    destruct (prime_or_div Hn) as [ (q & H1 & H2) | H1 ].
    2: exists n; auto.
(* Goal: not (@eq nat p (S O)) *)
    destruct (IHn q) as (p & H3 & H4); try omega.
    exists p; split; auto.
    apply divides_trans with (1 := H4); auto.
  Qed.

  Section prime_rect.

    Variables (P : nat -> Type)
              (HP0 : P 0)
              (HP1 : P 1)
              (HPp : forall p, prime p -> P p)
              (HPm : forall x y, P x -> P y -> P (x*y)).

    Theorem prime_rect n : P n.
    Proof.
(* Goal: P n *)
      induction on n as IHn with measure n.
(* Goal: P n *)
      destruct n as [ | [ | n ] ]; auto.
(* Goal: not (@eq nat p (S O)) *)
      destruct (@prime_factor (S (S n))) as (p & H1 & H2); try omega.
(* Goal: P (S (S n)) *)
      apply divides_div in H2.
(* Goal: P (S (S n)) *)
      rewrite H2.
(* Goal: P (Init.Nat.mul (div (S (S n)) p) p) *)
      apply HPm.
      + apply IHn.
(* Goal: lt (div (S (S n)) p) (S (S n)) *)
        rewrite H2 at 2.
        rewrite <- Nat.mul_1_r at 1.
(* Goal: lt (Nat.mul (div (S (S n)) p) (S O)) (Init.Nat.mul (div (S (S n)) p) p) *)
        apply prime_ge_2 in H1.
(* Goal: not (@eq nat p (S O)) *)
        apply mult_lt_compat_l; try omega.
(* Goal: not (@eq nat p (S O)) *)
        revert H2; destruct (div (S (S n)) p); intros; omega.
      + apply HPp, H1.
    Qed.

  End prime_rect.

  Corollary no_common_prime_is_coprime x y : x <> 0 -> (forall p, prime p -> p <d x -> p <d y -> False) -> is_gcd x y 1.
  Proof.
(* Goal: forall (_ : not (@eq nat x O)) (_ : forall (p : nat) (_ : prime p) (_ : divides p x) (_ : divides p y), False), is_gcd x y (S O) *)
    intros Hx H; split; [ | split ].
    + apply divides_1.
    + apply divides_1.
    + intros k H1 H2.
(* Goal: divides k (S O) *)
      destruct k as [ | [ | k ] ].
      * apply divides_0_inv in H1; omega.
      * apply divides_1.
      * destruct prime_factor with (n := S (S k)) as (p & P1 & P2); try omega.
(* Goal: divides (S (S k)) (S O) *)
        exfalso; apply H with p; auto; apply divides_trans with (S (S k)); 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.
(* Goal: forall (_ : is_gcd p q (S O)) (_ : is_gcd p l (S O)), is_gcd p (Init.Nat.mul q l) (S O) *)
    intros H1 H2.
(* Goal: is_gcd p (Init.Nat.mul q l) (S O) *)
    destruct p as [ | p ].
    + generalize (is_gcd_fun H1 (is_gcd_0l _)) (is_gcd_fun H2 (is_gcd_0l _)).
(* Goal: forall (_ : @eq nat (S O) q) (_ : @eq nat (S O) l), is_gcd O (Init.Nat.mul q l) (S O) *)
      intros; subst; auto.
    + apply no_common_prime_is_coprime; try omega.
(* Goal: forall (p0 : nat) (_ : prime p0) (_ : divides p0 (S p)) (_ : divides p0 (Init.Nat.mul q l)), False *)
      do 2 (apply proj2 in H1; apply proj2 in H2).
(* Goal: forall (p0 : nat) (_ : prime p0) (_ : divides p0 (S p)) (_ : divides p0 (Init.Nat.mul q l)), False *)
      intros k Hk H3 H4.
(* Goal: False *)
      apply prime_div_mult with (1 := Hk) in H4.
      destruct H4 as [ H4 | H4 ]; 
      [ generalize (H1 _ H3 H4) 
      | generalize (H2 _ H3 H4) ];
        intro H5; apply divides_1_inv in H5; subst; 
(* Goal: not (@eq nat p (S O)) *)
        destruct Hk; omega.
  Qed.

  Fact is_rel_prime_expo p q l : is_gcd p q 1 -> is_gcd p (mscal mult 1 l q) 1.
  Proof.
(* Goal: forall _ : is_gcd p q (S O), is_gcd p (@mscal nat Init.Nat.mul (S O) l q) (S O) *)
    intros H.
(* Goal: is_gcd p (@mscal nat Init.Nat.mul (S O) l q) (S O) *)
    induction l as [ | l IHl ].
    + rewrite mscal_0; apply is_gcd_1r.
    + rewrite mscal_S; apply is_rel_prime_mult; auto.
  Qed.

  (* Every positive number is the product of a list of primes *)

  Notation lprod := (fold_right mult 1).

  Fact lprod_ge_1 l : Forall prime l -> 1 <= lprod l.
  Proof.
(* Goal: forall _ : @Forall nat prime l, le (S O) (@fold_right nat nat Init.Nat.mul (S O) l) *)
    induction 1 as [ | x l H IH ]; simpl; auto.
    change 1 with (1*1) at 1; apply mult_le_compat; auto.
(* Goal: not (@eq nat p (S O)) *)
    apply prime_ge_2 in H; omega.
  Qed.

  Fact lprod_app l m : lprod (l++m) = lprod l * lprod m.
  Proof.
(* Goal: not (@eq nat p (S O)) *)
    induction l; simpl; try omega.
(* Goal: @eq nat (Init.Nat.mul a (@fold_right nat nat Init.Nat.mul (S O) (@app nat l m))) (Init.Nat.mul (Init.Nat.mul a (@fold_right nat nat Init.Nat.mul (S O) l)) (@fold_right nat nat Init.Nat.mul (S O) m)) *)
    rewrite IHl, mult_assoc; auto.
  Qed.

(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
  Theorem prime_decomp n : n <> 0 -> { l | n = lprod l /\ Forall prime l }.
  Proof.
(* Goal: forall _ : not (@eq nat n O), @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
    induction on n as IHn with measure n; intro Hn.
(* Goal: @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
    destruct (eq_nat_dec n 1) as [ Hn' | Hn' ].
    + exists nil; simpl; auto.
    + destruct (@prime_factor n) as (p & H1 & H2); try omega.
(* Goal: @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
      apply divides_div in H2; revert H2.
(* Goal: forall _ : @eq nat n (Init.Nat.mul (div n p) p), @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
      generalize (div n p); intros k Hk.
(* Goal: @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
      assert (k <> 0) as Hk'.
(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
      { intros ?; subst; destruct Hn; auto. }
(* Goal: @sig (list nat) (fun l : list nat => and (@eq nat n (@fold_right nat nat Init.Nat.mul (S O) l)) (@Forall nat prime l)) *)
      destruct (IHn k) as (l & H2 & H3); auto.
      - rewrite Hk.
(* Goal: lt k (Init.Nat.mul k p) *)
        generalize (prime_ge_2 H1).
(* Goal: forall _ : le (S (S O)) p, lt k (Init.Nat.mul k p) *)
        rewrite mult_comm.
(* Goal: not (@eq nat p (S O)) *)
        destruct p as [ | [ | p ] ]; simpl; intros; try omega.
        generalize (p*k); intros; omega.
      - exists (p::l); split; auto.
        simpl; rewrite <- H2, mult_comm; auto.
  Qed.

  Hint Resolve lprod_ge_1 prime_ge_2.

  Fact prime_in_decomp p l : prime p -> Forall prime l -> p <d lprod l -> In p l.
  Proof.
(* Goal: forall (_ : prime p) (_ : @Forall nat prime l) (_ : divides p (@fold_right nat nat Init.Nat.mul (S O) l)), @In nat p l *)
    intros H1.
(* Goal: forall (_ : @Forall nat prime l) (_ : divides p (@fold_right nat nat Init.Nat.mul (S O) l)), @In nat p l *)
    induction 1 as [ | x l Hl IHl ]; simpl; intros H2.
    + apply divides_1_inv in H2; apply (proj1 H1); auto.
    + destruct (prime_gcd x H1) as [ H3 | H3 ].
(* Goal: or (@eq nat x p) (@In nat p l) *)
(* Goal: or (@eq nat x p) (@In nat p l) *)
      apply is_rel_prime_div with (1 := H3) in H2; auto.
(* Goal: or (@eq nat x p) (@In nat p l) *)
      apply (proj2 Hl) in H3.
(* Goal: or (@eq nat x p) (@In nat p l) *)
      destruct H3 as [ H3 | H3 ]; auto.
(* Goal: or (@eq nat x p) (@In nat p l) *)
      contradict H3;apply H1.
  Qed.

  (* Prime decomposition is unique up-to permutation *) 

  Theorem prime_decomp_uniq l m : Forall prime l -> Forall prime m -> lprod l = lprod m -> l ~p m.
  Proof.
(* Goal: forall (_ : @Forall nat prime l) (_ : @Forall nat prime m) (_ : @eq nat (@fold_right nat nat Init.Nat.mul (S O) l) (@fold_right nat nat Init.Nat.mul (S O) m)), @Permutation nat l m *)
    intros H; revert H m.
(* Goal: forall (_ : @Forall nat prime l) (m : list nat) (_ : @Forall nat prime m) (_ : @eq nat (@fold_right nat nat Init.Nat.mul (S O) l) (@fold_right nat nat Init.Nat.mul (S O) m)), @Permutation nat l m *)
    induction 1 as [ | x l Hx Hl IHl ].
    + induction 1 as [ | y m Hy Hm IHm ]; simpl; auto.
(* Goal: forall _ : @eq nat (S O) (Init.Nat.mul y (@fold_right nat nat Init.Nat.mul (S O) m)), @Permutation nat (@nil nat) (@cons nat y m) *)
      intros C; exfalso.
      assert (2*1 <= y*lprod m) as D.
(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
      { apply mult_le_compat; auto. }
(* Goal: not (@eq nat p (S O)) *)
      simpl in D; omega.
    + simpl; intros m Hm H1.
(* Goal: @Permutation nat (@cons nat x l) m *)
      assert (In x m) as H2.
(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
      { apply prime_in_decomp with (1 := Hx); auto.
        exists (lprod l); rewrite mult_comm; auto. }
(* Goal: @Permutation nat (@cons nat x l) m *)
      apply in_split in H2.
(* Goal: @Permutation nat (@cons nat x l) m *)
      destruct H2 as (m1 & m2 & H2); subst.
(* Goal: @Permutation nat (@cons nat x l) (@app nat m1 (@cons nat x m2)) *)
      apply Permutation_cons_app, IHl.
      * rewrite Forall_app in Hm.
(* Goal: @Forall nat prime (@app nat m1 m2) *)
        destruct Hm as [ ? Hm ].
(* Goal: @Forall nat prime (@app nat m1 m2) *)
        inversion Hm.
(* Goal: @Forall nat prime (@app nat m1 m2) *)
        apply Forall_app; auto.
      * rewrite lprod_app.
(* Goal: @eq nat (@fold_right nat nat Init.Nat.mul (S O) l) (Init.Nat.mul (@fold_right nat nat Init.Nat.mul (S O) m1) (@fold_right nat nat Init.Nat.mul (S O) m2)) *)
        rewrite lprod_app in H1; simpl in H1.
        rewrite mult_assoc, (mult_comm _ x), <- mult_assoc in H1.
(* Goal: @eq nat (@fold_right nat nat Init.Nat.mul (S O) l) (Init.Nat.mul (@fold_right nat nat Init.Nat.mul (S O) m1) (@fold_right nat nat Init.Nat.mul (S O) m2)) *)
        apply Nat.mul_cancel_l in H1; auto.
(* Goal: not (@eq nat p (S O)) *)
        apply prime_ge_2 in Hx; omega.
  Qed.

End prime.

Section base_decomp.

  (* [m0;m1;...;mk] -> m0 + p*(m1+....) *)

  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 (l++m) = expand p l + power (length l) p * expand p m.
  Proof.
(* Goal: not (@eq nat p (S O)) *)
    induction l as [ | x l IH ]; simpl; try omega.
(* Goal: not (@eq nat p (S O)) *)
    rewrite power_S, IH, Nat.mul_add_distr_l, mult_assoc; omega.
  Qed.

  Fact expand_0 p l : Forall (eq 0) l -> expand p l = 0.
  Proof.
(* Goal: forall _ : @Forall nat (@eq nat O) l, @eq nat (expand p l) O *)
    induction 1 as [ | x l H1 H2 IH2 ]; simpl; subst; auto.
(* Goal: @eq nat (Init.Nat.add O (Init.Nat.mul p (expand p l))) O *)
    rewrite IH2, mult_comm; auto.
  Qed.

  Section base_p.

    Variables (p : nat) (Hp : 2 <= p).

(* Goal: @In nat x m *)
(* Goal: @Permutation nat (@cons nat x l) m *)
    Let base_p_full n : { l | n = expand p l }.
    Proof.
(* Goal: @sig (list nat) (fun l : list nat => @eq nat n (expand p l)) *)
      induction on n as IH with measure n.
(* Goal: @sig (list nat) (fun l : list nat => @eq nat n (expand p l)) *)
      destruct (eq_nat_dec n 0) as [ Hn | Hn ].
      + exists nil; auto.
      + destruct (@euclid n p) as (m & r & H1 & H2); try omega.
(* Goal: @sig (list nat) (fun l : list nat => @eq nat n (expand p l)) *)
        destruct (IH m) as (l & H3).
        * destruct m; try omega.
(* Goal: lt (S m) n *)
          rewrite H1, mult_comm.
          apply lt_le_trans with (2*S m + r); try omega.
(* Goal: le (Init.Nat.add (Init.Nat.mul (S (S O)) (S m)) r) (Init.Nat.add (Nat.mul p (S m)) r) *)
          apply plus_le_compat; auto.
(* Goal: le (Init.Nat.mul (S (S O)) (S m)) (Nat.mul p (S m)) *)
          apply mult_le_compat; auto.
        * exists (r::l); simpl.
          rewrite mult_comm, plus_comm, <- H3, H1; 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 : Forall2 (fun x y => x < p /\ y < p) l1 l2 -> expand p l1 = expand p l2 -> l1 = l2.
    Proof.
(* Goal: forall (_ : @Forall2 nat nat (fun x y : nat => and (lt x p) (lt y p)) l1 l2) (_ : @eq nat (expand p l1) (expand p l2)), @eq (list nat) l1 l2 *)
      induction 1 as [ | x1 x2 l1 l2 H1 H2 IH2 ]; auto; simpl; intros H3.
(* Goal: @eq (list nat) (@cons nat x1 l1) (@cons nat x2 l2) *)
      rewrite (plus_comm x1), (plus_comm x2), (mult_comm p), (mult_comm p) in H3.
(* Goal: not (@eq nat p (S O)) *)
      apply div_rem_uniq in H3; try omega.
(* Goal: @eq (list nat) (@cons nat x1 l1) (@cons nat x2 l2) *)
      destruct H3 as [ H3 ]; subst; f_equal; auto.
    Qed.

  End base_p.

End base_decomp.
