(*
7th TPP (2011) in AIST (Tsukuba) - TPPmark

Problem:

There are N children sitting in a circle, where each child has an even
number of candies. The following step is repeated indefinitely:

  every child passes half of their candies to the child on their left;
  any child who ends up with an odd number of candies is given another
  candy by the teacher.

Then, prove that eventually every child will hold the same number of
candies.
Proof outline:

Let m(i,k) be the number of candies held by the i'th
child (i in {1,...,N}) after k steps. At first, prove the following
lemmas:

 (1) max(k+1) <= max(k),
 (2) min(k) <= min(k+1),
 (3) if min(k) < m(i,k) then min(k) < m(i,k+1),
 (4) if m(i,k) < m(right(i),k) then m(i,k) < m(i,k+1),

where

    max(k) = max{m(i,k) | i in {1,...,N}},
    min(k) = min{m(i,k) | i in {1,...,N}},
  right(i) = (if (i < N) then (i+1) else 1).

Then, prove the following lemma:

 (5) if (min(k) < m(i,k)) for some i,
     then num(min(k),k+1) < num(min(k),k),

where

  num(m,k) is the number of children holding m candies after k steps.

Finally, it can be proven that all the children eventually hold the
same number of candies.
Reference:

Bohman, T., Pikhurko, O,, Frieze, A., Sleator, D.:
The Puzzle TOAD, Puzzle 6: Uniform Candy Distribution. 
Carnegie Mellon, School of Computer Science. Solution. Last access: 2011/10/13.
*)

Require Import Omega.

Section Candy_Distribution_Rule.

  (* We represent the number of candies using a natural number, but
     the actual number of candies is a double of the representing
     natural number (because the former is always even).  *)

  (* Ceiling of the average of the two given natural numbers.  *)
  Definition caverage (n m:nat) : nat := Div2.div2 (S (n + m)).

  Lemma caverage_comm : forall n m:nat, caverage n m = caverage m n.
  Proof.
  intros n m.
  unfold caverage.
  auto with arith.
  Qed.

  Lemma caverage_idempot : forall n:nat, caverage n n = n.
  Proof.
  intro n.
  unfold caverage.
  assert (n + n = 2 * n).
    omega.

    rewrite H.
    apply Div2.div2_double_plus_one.
  Qed.

  Lemma div2_mono : forall n m:nat, n <= m -> Div2.div2 n <= Div2.div2 m.
  Proof.
  intros n m Hle.
  elim Hle.
    trivial.

    intros m' Hle'.
    case (Even.even_or_odd m').
      intro Heven.
      rewrite (Div2.even_div2 _ Heven).
      trivial.

      intro Hodd.
      rewrite <- (Div2.odd_div2 _ Hodd).      
      auto.
  Qed.

  Lemma caverage_max : forall n m:nat, n <= m -> caverage n m <= m.
  Proof.
  intros n m Hle.
  elim Hle.
    rewrite caverage_idempot.
    trivial.

    intros m' Hle' Hcav.
    unfold caverage.
    rewrite <- plus_n_Sm.
    simpl.
    apply le_n_S.
    apply (le_trans (Div2.div2 (n + m')) (Div2.div2 (S (n + m')))).
      apply div2_mono.
      auto.

      assumption.
  Qed.

  Lemma caverage_min_strict : forall n m:nat, n < m -> n < caverage n m.
  Proof.
  intros n m Hlt.
  elim Hlt.
    unfold caverage.
    rewrite <- plus_n_Sm.
    simpl.
    apply le_n_S.
    assert (n + n = 2 * n).
      omega.

      rewrite H.
      rewrite Div2.div2_double.
      auto.

    intros m' H IH.
    apply (le_trans (S n) (caverage n m') (caverage n (S m'))).
      assumption.

      apply div2_mono.
      auto with arith.
  Qed.    

(* From now on, we don't use the definition of caverage.  So, the
   argument below can also be applied to other implementations of
   `caverage', such as `max', as long as we have the following lemmas:

    Lemma caverage_comm : forall n m:nat, caverage n m = caverage m n.
    Lemma caverage_idempot : forall n:nat, caverage n n = n.
    Lemma caverage_max : forall n m:nat, n <= m -> caverage n m <= m.
    Lemma caverage_min_strict : forall n m:nat, n < m -> n < caverage n m.
 *)
  Opaque caverage.

  Lemma caverage_min : forall n m:nat, n <= m -> n <= caverage n m.
  Proof.
  intros n m Hle.
  assert (n = m \/ n < m).
    omega.

    elim H.
      intro Heq.
      rewrite Heq.
      rewrite caverage_idempot.
      trivial.

      intro Hlt.
      generalize (caverage_min_strict _ _ Hlt).
      auto with arith.
  Qed.

  Lemma caverage_ub : forall n m p:nat, n <= p -> m <= p -> caverage n m <= p.
  Proof.
  intros n m p Hn Hm.
  case (le_or_lt n m).
    intro H.
    apply (le_trans (caverage n m) m p).
      apply caverage_max.
      assumption.

      assumption.

    intro H.
    apply (le_trans (caverage n m) n p).
      rewrite caverage_comm.
      apply caverage_max.
      auto with arith.

      assumption.
  Qed.

  Lemma caverage_lb_strict : forall n m p:nat,
    p < n -> p <= m -> p < caverage n m.
  Proof.
  intros n m p Hn Hm.
  case (le_or_lt n m).
    intro Hle.
    apply (lt_le_trans p n (caverage n m)).
      assumption.

      apply caverage_min.
      assumption.

    intro Hlt.
    apply (le_lt_trans p m (caverage n m)).
      assumption.

      rewrite caverage_comm.
      apply caverage_min_strict.
      assumption.
  Qed.

  Lemma caverage_lb_eq : forall n m p:nat,
    p <= n -> p <= m -> caverage n m = p -> n = p /\ m = p.
  Proof.
  intros n m p Hpn Hpm Hpc.
  split.
    case (le_lt_or_eq _ _ Hpn).
      intro Hlt.
      assert (p < caverage n m).
        apply caverage_lb_strict; assumption.

        omega.

      auto.

    case (le_lt_or_eq _ _ Hpm).
      intro Hlt.
      assert (p < caverage n m).
        rewrite caverage_comm.
        apply caverage_lb_strict; assumption.

        omega.

      auto.
  Qed.      

End Candy_Distribution_Rule.

(* From now on, we only need the following 2 lemmas for caverage:

    Lemma caverage_ub : forall n m p:nat,
      n <= p -> m <= p -> caverage n m <= p.
    Lemma caverage_lb_eq : forall n m p:nat,
      p <= n -> p <= m -> caverage n m = p -> n = p /\ m = p.

   They would be equivalent with the following 3 lemmas if we use
   min/max instead of lower/upper bounds:

    forall n m:nat, caverage n m <= max n m.
    forall n m:nat, min n m <= caverage n m.
    forall n m:nat, caverage n m = min n m -> n = m.

   The lemma below is also used, but is derivable from caverage_lb_eq.

    Lemma caverage_lb : forall n m p:nat,
      p <= n -> p <= m -> p <= caverage n m.

   The lemmas below are also used, but only within unused lemmas, so
   we don't need them:

    Lemma caverage_idempot : forall n:nat, caverage n n = n.
    Lemma caverage_min_strict : forall n m:nat, n < m -> n < caverage n m.
    Lemma caverage_lb_strict : forall n m p:nat,
      p < n -> p <= m -> p < caverage n m.

   Actually, these 3 lemmas can be derived from the first 2 lemmas at
   the beginning of this comment.

   Note that we no longer require caverage_comm to hold,

    Lemma caverage_comm : forall n m:nat, caverage n m = caverage m n.

   and this means the argument below can also be applied to yet
   another kind of implementations of `caverage' such as the ceiling
   of a weighted mean (not necessarily linear).
 *)

Section Uniform_Candy_Distribution.

  Set Implicit Arguments.
  
  (* From Coq'Art Sect. 6.2.5.4, p.160.  *)
  Ltac caseEq f := generalize (refl_equal f); pattern f at -1; case f.

  (* Parameterized candy distribution rule *)
  Variable rho : nat->nat->nat.
  Hypothesis rho_ub : forall n m p:nat,
    n <= p -> m <= p -> rho n m <= p.
  Hypothesis rho_lb_eq : forall n m p:nat,
    p <= n -> p <= m -> rho n m = p -> n = p /\ m = p.

  Lemma rho_lb : forall n m p:nat, p <= n -> p <= m -> p <= rho n m.
  Proof.
  intros n m p Hpn Hpm.
  destruct (le_or_lt p (rho n m)).
    assumption.

    assert (n = rho n m /\ m = rho n m).
      apply rho_lb_eq.
        omega.

        omega.

        trivial.

      omega.
  Qed.

  (* Used only in an unused lemma *)
  Lemma rho_idempot : forall n:nat, rho n n = n.
  Proof.
  intro n.
  apply le_antisym.
    apply rho_ub; auto.

    apply rho_lb; auto.
  Qed.

  (* Used only in an unused lemma *)
  Lemma rho_min_strict : forall n m:nat, n < m -> n < rho n m.
  Proof.
  intros n m Hlt.
  assert (n <= rho n m).
    apply rho_lb; auto with arith.

    destruct (le_lt_or_eq _ _ H).
      assumption.

      assert (n = n /\ m = n).
        apply rho_lb_eq; auto with arith.

        omega.
  Qed.

  (* Used only in an unused lemma *)
  Lemma rho_lb_strict : forall n m p:nat, p < n -> p <= m -> p < rho n m.
  Proof.
  intros n m p Hn Hm.
  assert (p <= rho n m).
    apply rho_lb; auto with arith.

    destruct (le_lt_or_eq _ _ H).
      assumption.

      assert (n = p /\ m = p).
        apply rho_lb_eq; auto with arith.

        omega.
  Qed.

  Definition periodic (A:Set) (p:nat) (f:nat->A) : Prop :=
    forall x:nat, f (x + p) = f x.

  Definition shift (A:Set) (f:nat->A) (x:nat) : A := f (S x).

  Lemma shift_periodic : forall (A:Set) (p:nat) (f:nat->A),
    periodic p f -> periodic p (shift f).
  Proof.
  intros A p f H x.
  unfold shift.
  assert (S (x + p) = (S x) + p).
    omega.

    rewrite H0.
    apply H.
  Qed.

  Definition map2 (A B C:Set) (op:A->B->C) (f:nat->A) (g:nat->B) (x:nat) :=
    op (f x) (g x).

  Lemma map2_periodic :
    forall (A B C:Set) (op:A->B->C) (f:nat->A) (g:nat->B) (p:nat),
      periodic p f -> periodic p g -> periodic p (map2 op f g).
  Proof.
  intros A B C op f g p Hf Hg x.
  unfold map2.
  rewrite Hf, Hg.
  trivial.
  Qed.

  Definition next (f:nat->nat) : nat->nat := map2 rho f (shift f).

  Lemma next_periodic : forall (p:nat) (f:nat->nat),
    periodic p f -> periodic p (next f).
  Proof.
  intros p f H.
  apply map2_periodic.
    assumption.

    apply shift_periodic.
    assumption.
  Qed.

  (* ub m f ... m is an upper bound of {f x | x in nat}.  *)
  Definition ub (m:nat) (f:nat->nat) : Prop := forall x:nat, f x <= m.

  (* lb m f ... m is a lower bound of {f x | x in nat}.  *)
  Definition lb (m:nat) (f:nat->nat) : Prop := forall x:nat, m <= f x.

  Lemma lb_ub_le : forall (l u:nat) (f:nat->nat), lb l f -> ub u f -> l <= u.
  Proof.
  intros l u f Hlb Hub.
  apply (le_trans l (f 0) u); auto.
  Qed.

  Lemma lb_ub_eq : forall (m: nat) (f : nat -> nat),
    lb m f -> ub m f -> forall x:nat, f x = m.
  Proof.
  intros m f Hlb Hub x.
  generalize (Hlb x).
  generalize (Hub x).
  auto with arith.
  Qed.

  Lemma ub_shift : forall (m:nat) (f:nat->nat), ub m f -> ub m (shift f).
  Proof.
  intros m f H x.
  apply H.
  Qed.

  Lemma lb_shift : forall (m:nat) (f:nat->nat), lb m f -> lb m (shift f).
  Proof.
  intros m f H x.
  apply H.
  Qed.

  (* Lemma (1) *)
  Lemma ub_next : forall (m:nat) (f:nat->nat), ub m f -> ub m (next f).
  Proof.
  intros m f H x.
  apply rho_ub.
    apply H.

    apply (ub_shift H).
  Qed.

  (* Lemma (2) *)
  Lemma lb_next : forall (m:nat) (f:nat->nat), lb m f -> lb m (next f).
  Proof.
  intros m f H x.
  apply rho_lb.
    apply H.

    apply (lb_shift H).
  Qed.

  (* Lemma (3), but unused *)
  Lemma lb_next1 : forall (m:nat) (f:nat->nat),
    lb m f -> forall x:nat, f x <> m -> m < (next f) x.
  Proof.
  intros m f Hlb x Hfx.
  assert (m < f x).
    generalize (Hlb x).
    omega.

    apply rho_lb_strict.
      assumption.

      apply lb_shift.
      assumption.
  Qed.

  (* Lemma (4), but unused *)
  Lemma increase_spacial_temporal : forall (f:nat->nat) (x:nat),
    f x < f (S x) -> f x < next f x.
  Proof.
  intros f x H.
  apply rho_min_strict.
  assumption.
  Qed.

  (* Rather than Lemma (3) and (4) above, we extensively use the
     following lemma.  *)
  Lemma lb_eq_next : forall (m:nat) (f:nat->nat), lb m f ->
    forall x:nat, next f x = m -> f x = m /\ f (S x) = m.
  Proof.
  intros m f Hlb x.
  unfold next, map2, shift.
  apply rho_lb_eq; apply Hlb.
  Qed.

  (* Used only in an unused lemma *)
  Lemma next_eq : forall (f:nat->nat) (x:nat), f x = f (S x) -> next f x = f x.
  Proof.
  intros f x H.
  unfold next, map2, shift.
  rewrite <- H.
  apply rho_idempot.
  Qed.

  (* occ_count m f p = #{x | x < p /\ f x = m } *)
  Fixpoint occ_count (m:nat) (f:nat->nat) (p:nat) : nat :=
    match p with
      O => O
      | S q =>
        if eq_nat_dec (f q) m then S (occ_count m f q) else occ_count m f q
    end.

  Lemma occ_count_le : forall (m:nat) (f:nat->nat) (p:nat),
    occ_count m f p <= p.
  Proof.
  induction p; simpl.
    trivial.

    case (eq_nat_dec (f p) m).
      auto with arith.

      auto with arith.
  Qed.

  (* right to left (<-) unused *)
  Lemma occ_count_zero : forall (m:nat) (f:nat->nat) (p:nat),
    occ_count m f p = 0 <-> forall x:nat, x < p -> f x <> m.
  Proof.
  induction p; simpl.
    split.
      intros H x.
      omega.

      trivial.

    split.
      case (eq_nat_dec (f p) m).
        discriminate.

        intros Hfp Hcnt x Hlt.
        apply le_S_n in Hlt.
        case (le_lt_or_eq _ _ Hlt).
          apply IHp.
          assumption.

          intro Hx.
          rewrite Hx.
          assumption.

      intro H.
      case (eq_nat_dec (f p) m).
        intro Hfp.
        elim (H p).
          auto.

          assumption.

        intro Hfp.
        apply IHp.
        intros x Hlt.
        apply H.
        auto.
  Qed.

  Lemma occ_count_all : forall (m:nat) (f:nat->nat) (p:nat),
    occ_count m f p = p <-> forall x:nat, x < p -> f x = m.
  Proof.
  induction p; simpl.
    split.
      intros H x.
      omega.

      trivial.

    split.
      case (eq_nat_dec (f p) m).
        intros Heq H x Hlt.
        apply le_S_n in Hlt.
        case (le_lt_or_eq _ _ Hlt).
          apply IHp.
            injection H.
            trivial.

          intro Hx.
          rewrite Hx.
          assumption.

        intros Hfp Hcnt.
        absurd (occ_count m f p <= p).
          rewrite Hcnt.
          auto with arith.

          apply occ_count_le.

      intro H.
      case (eq_nat_dec (f p) m).
        intro Hfp.
        apply eq_S.
        apply IHp.
        intros x Hlt.
        apply H.
        auto.

        intros Hfp.
        elim Hfp.
        apply H.
        auto.
  Qed.

  (* unused *)
  Lemma occ_count_some : forall (m:nat) (f:nat->nat) (p:nat),
    occ_count m f p <> 0 <-> exists x:nat, x < p /\ f x = m.
  Proof.
  induction p; simpl.
    split.
      intro H.
      contradiction H.
      trivial.

      intros [x [H1 H2]].
      inversion H1.

    split.
      case (eq_nat_dec (f p) m).
        intros Hfp Hcnt.
        exists p.
        auto.

        intros Hfp Hcnt.
        destruct IHp as [IHp1 IHp2].
        elim (IHp1 Hcnt).
        intros x [H2 H3].
        exists x.
        auto.

      intro H.
      case (eq_nat_dec (f p) m).
        auto.

        intro Hfp.
        apply IHp.
        elim H.
        intros x [H1 H2].
        exists x.
        split.
          apply le_S_n in H1.
          elim (le_lt_or_eq _ _ H1).
            trivial.

            intro Heq.
            elim Hfp.
            rewrite <- Heq.
            assumption.

          assumption.          
  Qed.

  Lemma lb_occ_count_le : forall (m:nat) (f:nat->nat), lb m f ->
    forall p:nat, occ_count m (next f) p <= occ_count m f p.
  Proof.
  induction p; simpl.
    trivial.
   
    case (eq_nat_dec (f p) m);
      case (eq_nat_dec (next f p) m).
        auto with arith.

        auto.

        intros Hnfp Hfp.
        elim Hfp.

        apply lb_eq_next; assumption.

        auto.
  Qed.

  (* unused *)
  Lemma lb_occ_count_zero : forall (m:nat) (f:nat->nat), lb m f ->
    forall p:nat, occ_count m f p = 0 -> occ_count m (next f) p = 0.
  Proof.
    intros m f H p.
    generalize (lb_occ_count_le H p).
    omega.
  Qed.

  (* unused *)
  Lemma occ_count_all_next : forall (m:nat) (f:nat->nat) (p:nat),
    occ_count m f p = p -> f p = m -> occ_count m (next f) p = p.
  Proof.
    induction p; simpl.
      trivial.

      case (eq_nat_dec (f p) m).
        intros Hfp Hcnt HfSp.
        case (eq_nat_dec (next f p) m).
          intro Hnfp.
          apply eq_S.
          apply IHp.
            injection Hcnt.
            trivial.

            assumption.

          intro Hnfp.
          elim Hnfp.
          rewrite <- Hfp.
          apply next_eq.
          rewrite Hfp, HfSp.
          trivial.

        intros Hfp Hcnt.
        absurd (occ_count m f p <= p).
          rewrite Hcnt.
          auto with arith.

          apply occ_count_le.
  Qed.

  Lemma lb_occ_count_eq : forall (m:nat) (f:nat->nat), lb m f ->
    forall p:nat, (f p = m -> f 0 = m) -> occ_count m f p <> 0 ->
      occ_count m (next f) p = occ_count m f p ->
      occ_count m f p = p /\ f p = m.
  Proof.
  induction p; simpl.
    tauto.

    case (eq_nat_dec (f p) m); case (eq_nat_dec (next f p) m).
      intros Hnfp Hfp Hf0 Hcnt0 Hcntp.
      clear Hcnt0.
      caseEq p.
        split.
        trivial.

        apply lb_eq_next.
          assumption.

          rewrite <- H0.
          assumption.

        intros n Hpn.
        rewrite <- Hpn.
        assert (f 0 = m).
          apply Hf0.
          apply lb_eq_next; assumption.

          split.
            apply eq_S.
            apply IHp.
              trivial.

              intro Hcnt0.
              destruct (occ_count_zero m f p) as [H1 H2].
              generalize H0.
              apply H1.
                assumption.

                rewrite Hpn.
                auto with arith.

            inversion Hcntp.
            trivial.

          apply lb_eq_next; assumption.

      intros Hnfp Hfp Hfp0 Hcnt0 Hcntp.
      generalize (lb_occ_count_le H p).
      rewrite Hcntp.
      omega.

      intros Hnfp Hfp.
      elim Hfp.
      apply lb_eq_next; assumption.

      intros Hnfp Hfp Hfp0 Hcnt0 Hcntp.
      elim Hfp.
      apply IHp.
        intro Hfp'.
        contradiction.

        assumption.

        assumption.
  Qed.

  (* Lemma (5) *)
  Lemma lb_occ_count_lt : forall (m:nat) (f:nat->nat), lb m f ->
    forall p:nat, (f p = m -> f 0 = m) -> occ_count m f p <> 0 ->
      ~(occ_count m f p = p /\ f p = m) ->
      occ_count m (next f) p < occ_count m f p.
  Proof.
  intros m f H p Hfp0 Hcnt0 Hcntp.
  assert (occ_count m (next f) p <= occ_count m f p).
    apply lb_occ_count_le; assumption.

    destruct (le_lt_or_eq _ _ H0).
      assumption.

      elim Hcntp.
      apply lb_occ_count_eq; assumption.
  Qed.

  Require Import Relations.
  Require Import Wellfounded.

  Definition f_lt (m p:nat) (f1 f2:nat->nat) : Prop :=
    (occ_count m f2 p <> 0 /\ (occ_count m f2 p <> p \/ f2 p <> m))
      /\ occ_count m f1 p < occ_count m f2 p.

  Lemma f_lt_wf : forall m p:nat, well_founded (f_lt m p).
  Proof.
  intros m p.
  assert (inclusion _ (f_lt m p)
    (fun f1 f2:nat->nat => occ_count m f1 p < occ_count m f2 p)).
    unfold f_lt, inclusion.
    tauto.

    apply (wf_incl _ _ _ H).
    apply wf_inverse_image.
    exact lt_wf.
  Qed.

  Lemma lb_occ_count_converge : forall (p:nat) (m:nat) (f:nat->nat),
    periodic p f -> lb m f ->
    exists n:nat, let fn := iter_nat n _ next f in
      occ_count m fn p = 0 \/ occ_count m fn p = p.
  Proof.
    intros p m f Hper Hlb.
    induction f using (well_founded_ind (f_lt_wf m p)).
    case (eq_nat_dec (occ_count m x p) 0).
      intro H1.
      exists 0; simpl.
      auto.

      case (eq_nat_dec (occ_count m x p) p).
        intros H1 H2.
        exists 0; simpl.
        auto.

        intros H1 H2.
        assert (f_lt m p (next x) x /\ periodic p (next x) /\ lb m (next x)).
          split.
            unfold f_lt.
            split.
              auto.
            
              apply lb_occ_count_lt; try assumption.
                assert (x (0 + p) = x 0).
                  apply Hper.

                  rewrite <- H0.
                  auto.

                intros [H3 H4].
                contradiction.

            split.
              apply next_periodic.
              assumption.

              apply lb_next.
              assumption.

          destruct H0 as [H00 [H01 H02]].
          destruct (H (next x) H00 H01 H02) as [n H0].
          exists (n + 1).
          rewrite iter_nat_plus.
          apply H0.
  Qed.

  Lemma periodic_mod : forall (p:nat) (f:nat->nat), 
    periodic p f -> forall q r:nat, f (q * p + r) = f r.
  Proof.
  induction q;simpl.
    trivial.

    intro r.
    assert (p + q * p + r = (q * p + r) + p).
      omega.

      rewrite <- (IHq r).
      rewrite H0.
      apply H.
  Qed.

  Require Import Euclid.

  Lemma periodic_ub : forall (p:nat) (m:nat) (f:nat->nat), p > 0 ->
    periodic p f -> (forall x:nat, x < p -> f x <= m) -> ub m f.
  Proof.
  intros p m f Hp Hper H x.
  destruct (modulo _ Hp x) as [r [q [Heq Hgt]]].
  assert (f x = f r).
    rewrite Heq.
    apply periodic_mod.
    assumption.
 
    rewrite H0.
    apply H.
    auto.
  Qed.

  Lemma periodic_lb : forall (p:nat) (m:nat) (f:nat->nat), p > 0 ->
    periodic p f -> (forall x:nat, x < p -> m <= f x) -> lb m f.
  Proof.
  intros p m f Hp Hper H x.
  destruct (modulo _ Hp x) as [r [q [Heq Hgt]]].
  assert (f x = f r).
    rewrite Heq.
    apply periodic_mod.
    assumption.
 
    rewrite H0.
    apply H.
    auto.
  Qed.

  Lemma lb_0 : forall f:nat->nat, lb 0 f.
  Proof.
  intros f x.
  auto with arith.
  Qed.

  Lemma periodic_lb_refine : forall (p:nat) (m:nat) (f:nat->nat), p > 0 ->
    periodic p f -> lb m f -> occ_count m f p = 0 -> lb (S m) f.
  Proof.
  intros p m f Hp Hper Hlb Hcnt0.
  apply (periodic_lb Hp Hper).
  intros x Hlt.
  case (le_lt_or_eq _ _ (Hlb x)).
    auto.

    intro Hm.
    destruct (occ_count_zero m f p) as [H1 H2].
    generalize (H1 Hcnt0 _ Hlt).
    rewrite Hm.
    tauto.
  Qed.

  Lemma iter_next_periodic : forall (p:nat) (f:nat->nat), periodic p f ->
    forall n:nat, periodic p (iter_nat n _ next f).
  Proof.
  induction n; simpl.
    assumption.

    apply next_periodic.
    assumption.
  Qed.

  Lemma lb_iter_next : forall (m:nat) (f:nat->nat),
    lb m f -> forall n:nat, lb m (iter_nat n _ next f).
  Proof.
  induction n; simpl.
    assumption.

    apply lb_next.
    assumption.
  Qed.

  Lemma ub_iter_next : forall (m:nat) (f:nat->nat),
    ub m f -> forall n:nat, ub m (iter_nat n _ next f).
  Proof.
  induction n; simpl.
    assumption.

    apply ub_next.
    assumption.
  Qed.

  Lemma lb_ub_occ_count_converge : forall p:nat, p > 0 -> 
    forall (d l:nat) (f:nat->nat), periodic p f -> lb l f -> ub (d + l) f ->
      exists n:nat, exists m:nat, occ_count m (iter_nat n _ next f) p = p.
  Proof.
  intros p Hp.
  induction d; simpl.
    intros l f Hper Hlb Hub.
    exists 0.
    exists l.
    apply occ_count_all.
    intros x Hlt.
    apply lb_ub_eq; assumption.

    intros l f Hper Hlb Hub.
    destruct (lb_occ_count_converge Hper Hlb) as [n [H1 | H2]].
      assert (exists n0 : nat, exists m : nat,
        occ_count m (iter_nat n0 _ next (iter_nat n _ next f)) p = p).
        assert (periodic p (iter_nat n (nat -> nat) next f)).
          apply iter_next_periodic.
          assumption.

          apply (IHd (S l)).
            assumption.

            apply (periodic_lb_refine Hp).
            assumption.

            apply lb_iter_next.
            assumption.

            assumption.

            apply ub_iter_next.
            rewrite <- plus_n_Sm.
            assumption.

        destruct H as [n0 [m0 H]].
        exists (n0 + n).
        exists m0.
        rewrite iter_nat_plus.
        assumption.
    
      exists n.
      exists l.
      assumption.
  Qed.

  Fixpoint bounded_max p (f:nat->nat) : nat :=
    match p with
      O => O
      | S q => MinMax.max (f q) (bounded_max q f)
    end.

  Lemma periodic_bounded_max_ub : forall (f:nat->nat) (p:nat), p > 0 ->
    periodic p f -> ub (bounded_max p f) f.
  Proof.
  intros f p Hp Hper.
  apply (periodic_ub Hp Hper).
  clear Hper.
  intros x Hlt.
  induction Hlt; simpl.
    auto with arith.

    apply (le_trans (f x) (bounded_max m f)
      (MinMax.max (f m) (bounded_max m f))).
      apply IHHlt.
      omega.

      auto with arith.
  Qed.

  Theorem uniform_candy_distribution : forall (p:nat) (f:nat->nat),
    p > 0 -> periodic p f ->
    exists n:nat, exists m:nat,
      forall x:nat, x < p -> (iter_nat n _ next f) x = m.
  Proof.
  intros p f Hp Hper.
  assert (exists n:nat, exists m:nat, occ_count m (iter_nat n _ next f) p = p).
    apply lb_ub_occ_count_converge with (d := (bounded_max p f)) (l := 0).
      assumption.

      assumption.

      apply lb_0.

      rewrite plus_0_r.
      apply (periodic_bounded_max_ub Hp Hper).

    destruct H as [n [m H0]].
    exists n.
    exists m.
    apply occ_count_all.
    assumption.
  Qed.

End Uniform_Candy_Distribution.

(* Main Theorem *)
Theorem uniform_candy_distribution_for_caverage: forall (p:nat) (f:nat->nat),
  p > 0 -> periodic p f ->
  exists n:nat, exists m:nat,
    forall x:nat, x < p -> iter_nat n _ (next caverage) f x = m.
Proof uniform_candy_distribution _ caverage_ub caverage_lb_eq.

(* Bonus *)
Theorem uniform_candy_distribution_for_max: forall (p:nat) (f:nat->nat),
  p > 0 -> periodic p f ->
  exists n:nat, exists m:nat,
    forall x:nat, x < p -> iter_nat n _ (next MinMax.max) f x = m.
Proof.
apply uniform_candy_distribution.
  apply Max.max_lub.

  intros n m p Hn Hm Hmax.
  split.
    apply le_antisym.
      rewrite <- Hmax.
      apply Max.le_max_l.

      assumption.

    apply le_antisym.
      rewrite <- Hmax.
      apply Max.le_max_r.

      assumption.
Qed.