Ssreflect の練習． http://www.tcp-ip.or.jp/~n01/math/binomial.pdf を参考に補題作ってごりごりやってみた．大変だった... でも楽しい!

binomial_prime_exp.v

Require Import 
        Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun
        Ssreflect.ssrnat Ssreflect.prime Ssreflect.seq
        Ssreflect.div Ssreflect.binomial Ssreflect.bigop.

Lemma coprime_plus a b:
  coprime a (b+a) -> coprime b (b+a).
Proof.
  by rewrite /coprime gcdnDl gcdnDr gcdnC.
Qed.  

Lemma coprime_minus_coprime a b:
  a < b -> coprime a b -> coprime (b - a) b.
Proof.
  by move => Hlt; rewrite -{1 3}(subnK (ltnW Hlt)); apply coprime_plus.
Qed.

Lemma exp_plus p n m a b:
  a*p^(m+n) - b*p^n = p^n*(a*p^m - b).
Proof.
  by rewrite expnD mulnA mulnC (mulnC b _) mulnBr.
Qed.
  
Lemma exp_sub p n m a b:
  n < m -> a*p^m - b*p^n = p^n*(a*p^(m-n) - b).
Proof.
  by move => Hltnm; rewrite -{1}(subnK (ltnW Hltnm)); apply exp_plus.
Qed.

Lemma coprime_logn p m:
  coprime p m -> logn p m = 0.
Proof.
  by move => Hcoprime; rewrite -(mul1n m) mulnC (logn_Gauss _ Hcoprime) logn1.
Qed.

Lemma logn_prime_exp p n i:
  prime p -> 0 < i < p^n -> logn p (p^n-i) = logn p i.
Proof.
  move => Hprime Hltlt; destruct (andP Hltlt) as [Hlt0i Hltipn].
  move: (pfactor_coprime Hprime Hlt0i) Hltipn => [m [ Hcoprime Heq ]].
  rewrite {1 2}Heq -{2}(mul1n (p^n)).

  move: (Hlt0i) => Hlt ; rewrite Heq muln_gt0 in Hlt.
  destruct (andP Hlt) as [Hlt0m Hlt0ppi]; clear Hlt.
  move => Hlt.
  move: (leq_pmull (p^logn p i) Hlt0m) => Hle.
  move: (leq_ltn_trans Hle Hlt) => Hltp.
  rewrite (ltn_exp2l _ _  (prime_gt1 Hprime)) in Hltp.
  rewrite (exp_sub _ _ _ _ _ Hltp) (lognM _ Hlt0ppi).
  - rewrite (pfactorK _ Hprime) mul1n.
    rewrite (coprime_logn p (p^(n-logn p i) - m)); auto.
    rewrite -subn_gt0 in Hltp.
    rewrite -(coprime_pexpl _ _ Hltp) coprime_sym; apply coprime_minus_coprime. 
    + rewrite subn_gt0 in Hltp.
      by rewrite -(ltn_pmul2r (pfactor_gt0 p i)) -expnD (subnK (ltnW Hltp)).
    + by apply coprime_expr; rewrite coprime_sym.
  - by rewrite mul1n subn_gt0 -(ltn_pmul2r (pfactor_gt0 p i))
               -expnD (subnK (ltnW Hltp)).
Qed.

Lemma ffact_prod m n:
  m ^_ n = \prod_(0 <= i < n) (m - i).
Proof.
  elim: n => [ | n IHn ].
  - by rewrite ffactn0 /index_iota big_nil.
  - by rewrite -{2}addn1 ffactnSr IHn /index_iota
               subn0 subn0 iota_add big_cat /= add0n big_seq1. 
Qed.

Lemma logn_prod_lt0 m n F:
  (forall i, m <= i < m + n -> 0 < F i) ->
  0 < \prod_(m <= i < m + n) (F i).
Proof.
  elim: n F => [ | n IHn ] => F HF.
  - by rewrite addn0 /index_iota subnn big_nil.
  - rewrite /index_iota (addnC m _) -(addnBA _ (leqnn m)) subnn addn0 -(addn1 n)
            iota_add big_cat /= muln_gt0.
    apply /andP; split.
    + rewrite -(addn0 n) -{3}(subnn m) (addnBA _ (leqnn m))
              -(addnC m _) -/index_iota.
      apply IHn.
      by move => i Hlelt; apply HF; apply /andP; destruct (andP Hlelt);
         split; [ | rewrite addnS]; auto.
    + by rewrite big_seq1; apply HF; apply /andP;
         split; [ apply leq_addr |  rewrite addnS ]; auto.
Qed.

Lemma logn_prod_sum_logn p m n F:
  (forall i, m <= i < m + n -> 0 < F i) ->
  logn p (\prod_(m <= i < m + n) (F i)) = \sum_(m <= i < m + n) (logn p (F i)).
Proof.
  move => HF.
  elim: n HF => [ | n IHn ] HF.
  - by rewrite addn0 /index_iota subnn /= big_nil big_nil logn1.
  - rewrite addnS (big_cat_nat _ _ (n:=m+n) _ (leq_addr n m) (leqnSn _)) /=
          {2 3}/index_iota -(addn1 (m+n)) (addnC (m+n) 1)
          -(addnBA _ (leq_addr n m)) {5}(addnC m n) -(addnBA _ (leqnn m))
            subnn addn0 (addnC 1 n) iota_add
          -(addnBA _ (leqnn _)) (subnn (m+n)) addn0 /=
          big_seq1 big_cat /= big_seq1 lognM. 
    + rewrite IHn.
      * by rewrite /index_iota {1}(addnC m n) -(addnBA _ (leqnn m)) subnn addn0.
      * move => i Hlelt.
        apply HF; apply /andP; destruct (andP Hlelt); split; auto.
        by rewrite addnS; auto.
    + apply logn_prod_lt0.
      move => i Hlelt; destruct (andP Hlelt).
      by apply HF; apply /andP; split; [ | rewrite addnS]; auto.
    + by apply HF; apply /andP; split; [ apply leq_addr | rewrite addnS ]; auto.
Qed.

Lemma logn_prod_sum_logn_0 p n F:
  (forall i, i < n -> 0 < F i) ->
  logn p (\prod_(0 <= i < n) (F i)) = \sum_(0 <= i < n) (logn p (F i)).
Proof.
  move => HF.
  rewrite -(add0n n); apply logn_prod_sum_logn.
  move => i Hlelt.
  apply HF.
  destruct (andP Hlelt); auto.
Qed.

Lemma binomial_dvdn n m:
  m`! %| n ^_ m.
Proof.  
  by rewrite -bin_ffact; apply dvdn_mull, dvdnn.
Qed. 

Lemma logn_binomial p m k:
  0 < k <= p^m -> prime p -> logn p ('C(p^m,k)) = m - logn p k.
Proof.
  move => Hltle0kpm Hprime.
  destruct (andP Hltle0kpm) as [Hlt0k Hlekpm].
  rewrite bin_ffactd (logn_div _ (binomial_dvdn _ _)).
  rewrite ffact_prod logn_prod_sum_logn_0.
  - rewrite fact_prod logn_prod_sum_logn.
    + rewrite 
        (big_ltn Hlt0k) subn0 (addnC 1 k) (pfactorK _ Hprime)
        (@big_cat_nat _ _ _ k 1 (k+1) _ _ Hlt0k (leq_addr 1 k)) /=
        {3}/index_iota (addnC k 1) -(addnBA _ (leqnn k)) subnn addn0 /=
        big_seq1.
      rewrite
        (@eq_big_nat _ _ _ 1 k (fun i => logn p (p^m - i)) (fun i => logn p i)).
      * by rewrite (addnC m _) subnDl.
      * move => i Hltlt; destruct (andP Hltlt) as [Hlt0i Hltik].
        apply logn_prime_exp; auto.
        apply /andP; split; auto.
        by apply leq_trans with k; auto.
    + by move => i Hltlt; destruct (andP Hltlt); auto.
  - by move => i Hlt; rewrite subn_gt0; apply leq_trans with k; auto.
Qed.

Lemma factor_lt p i:
  prime p -> logn p i.+1 <= i.
Proof.
  move => Hprime.
  move: (pfactor_coprime Hprime (ltn0Sn i)) => [m [Hcoprime Heq]].
  remember (logn p i.+1) as k.
  rewrite -(leq_add2r 1) (addn1 i) Heq.
  cut (0 < m).
  move => Hlt.
  clear Heqk Heq i.
  induction k as [ | k IHk ].
  by rewrite add0n expn0 muln1.
  rewrite expnS mulnCA.
  apply leq_trans with (p*(k+1)).
  apply leq_trans with (2*(k+1)).
  rewrite -addn1 -addnA mulnDr muln1 mul2n -addnn -addnA leq_add2l; simpl; auto.
  rewrite addnn -mul2n muln1 addn2 -addn1 -(addn1(k.+1)) leq_add2r; apply ltn0Sn.
  by rewrite leq_pmul2r; [ apply prime_gt1 | rewrite addn1; apply ltn0Sn ].
  by rewrite leq_pmul2l; [ | apply prime_gt0 ].
  by rewrite -(ltn_pmul2r (pfactor_gt0 p (i.+1))) -Heqk -Heq mul0n; apply ltn0Sn.
Qed.

Lemma exp_plus_lt p n i:
  1 < p -> i < p ^ (n + i).
Proof.
  move => Hlt1p.
  induction i as [ | i IHi ].
  rewrite addn0 expn_gt0.
  by apply /orP; left; apply ltnW in Hlt1p.
  rewrite addnS expnS -addn1.
  rewrite -addn1 in IHi.
  apply leq_trans with (p*(i+1)).
  rewrite addn1.
  apply leq_ltn_trans with (1*(i.+1)).
  rewrite -addn1.
  rewrite -{1}(mul1n (i+1)).
  by apply leq_pmul2r; rewrite addn1; apply ltn0Sn.
  by rewrite -(addn1 i) ltn_pmul2r ; [ auto | rewrite addn1; apply ltn0Sn ].
  by rewrite leq_pmul2l; auto. 
Qed.

Goal (forall p i n, 2 < p -> prime p -> p ^ n %| 'C(p ^ (n + i), i.+1)).
Proof.
  move => p i n Hlt2p Hprime.
  rewrite pfactor_dvdn; auto.
  rewrite logn_binomial; auto.
  rewrite -addnBA.
  rewrite -{1}(addn0 n) leq_add2l.
  by rewrite -(subnn (logn p i.+1)); apply leq_sub2r; apply factor_lt.
  by apply factor_lt.
  apply /andP; split; auto.
  by apply exp_plus_lt; apply ltnW in Hlt2p.
  rewrite bin_gt0.
  by apply exp_plus_lt; apply ltnW in Hlt2p.
Qed.

(* 2 < p はなくてもよい *)
Goal (forall p i n, prime p -> p ^ n %| 'C(p ^ (n + i), i.+1)).
Proof.
  move => p i n Hprime.
  rewrite pfactor_dvdn; auto.
  rewrite logn_binomial; auto.
  rewrite -addnBA.
  rewrite -{1}(addn0 n) leq_add2l.
  by rewrite -(subnn (logn p i.+1)); apply leq_sub2r; apply factor_lt.
  by apply factor_lt.
  apply /andP; split; auto.
  by apply exp_plus_lt; apply prime_gt1.
  rewrite bin_gt0.
  by apply exp_plus_lt; apply prime_gt1.
Qed.