TPPmark7 その2

gistfile1.txt

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
Require Import finfun path fingraph bigop.

Section Sec.
  Parameter ch : finType.
  Parameter m : ch -> nat -> nat.
  Parameter right : ch -> ch.

  Parameter chpos : #|ch| > 0.
  Parameter meven0 : forall c, odd (m c 0) = false.
  Parameter right_connect : forall cl cr, fconnect right cl cr.

  Parameter turn_spec :
    forall k cl,
      let my := m cl k in
      let ri := m (right cl) k in
      let nx := my./2 + ri./2 in
        m cl k.+1 = nx + odd nx.

  Definition mmax k := \max_c m c k.
  Definition mmin k := mmax k - \max_c (mmax k - m c k).

  Definition mk k := m^~ k.
  Lemma mkE : forall k c, m c k = mk k c.
  Proof. by done. Qed.

  Lemma mmax_leq : forall c k, m c k <= mmax k .
  Proof. by move=> c k; rewrite mkE leq_bigmax. Qed.

  Lemma mmax_ex : forall k, exists c, mmax k = m c k.
  Proof.
    move=> k.
    case: (eq_bigmax (mk k) chpos) => c H.
    by exists c.
  Qed.

  Lemma mmin_leq : forall c k, mmin k <= m c k.
  Proof.
    move=> c k; rewrite /mmin leq_sub_add.
    apply (@leq_trans (mmax k - m c k + m c k)).
      by rewrite subnK // mmax_leq.
    by rewrite leq_add2r (leq_bigmax (F := fun c => mmax k - m c k)).
  Qed.

  Lemma mmin_ex : forall k, exists c, mmin k = m c k.
  Proof.
    move=> k; rewrite /mmin.
    case: (eq_bigmax (fun c => mmax k - m c k) chpos) => c H.
    by exists c; rewrite H subKn // mmax_leq.
  Qed.

  Lemma meven : forall c k, odd (m c k) = false.
  Proof.
    move=> c; elim; first exact: meven0.
    move=> k IH.
    by rewrite turn_spec odd_add oddb addbb.
  Qed.

  Lemma min_leq_max : forall k, mmin k <= mmax k.
  Proof.
    by move=> k; case: (mmax_ex k) => i ->; apply mmin_leq.
  Qed.

  Lemma mmax_even : forall k, odd (mmax k) = false.
  Proof.
    by move=> k; case: (mmax_ex k) => i ->; apply meven.
  Qed.

  Lemma min_even : forall k, odd (mmin k) = false.
  Proof.
    by move=> k; case: (mmin_ex k) => i ->; apply meven.
  Qed.

  (* (1) *)
  Lemma max_le : forall k, mmax k.+1 <= mmax k.
  Proof.
    move=> k; case: (mmax_ex k.+1) => c ->.
    rewrite turn_spec.
    set ci := m c k; set cj := m (right c) k.
    suff: ci./2 + cj./2 <= mmax k.
      case Ho: (odd _) => H; last by rewrite addn0.
      rewrite addn1 ltn_neqAle.
      apply/andP; split=> //.
      apply/eqP; move/(congr1 odd).
      by rewrite Ho mmax_even.
    apply (@leq_trans (ci + cj)./2).
      by rewrite half_add leq_addl.
    rewrite -(doubleK (mmax k)) -addnn.
    by apply half_leq; apply leq_add; apply mmax_leq.
  Qed.

  Lemma max_le' : forall k k', k <= k' -> mmax k' <= mmax k.
  Proof.
    move=> k k'; move/subnKC => <-.
    elim: (k' - k).
      by rewrite addn0.
    move=> n H.
    rewrite addnS.
    apply: leq_trans; last by apply H.
    by apply max_le.
  Qed.

  (* (2) *)
  Lemma min_le : forall k, mmin k <= mmin k.+1.
  Proof.
    move=> k; case: (mmin_ex k.+1) => c ->.
    rewrite turn_spec.
    set ci := m c k; set cj := m (right c) k.
    apply (@leq_trans (ci./2 + cj./2)); last first.
      by apply leq_addr.
    apply (@leq_trans (ci + cj)./2); last first.
      by rewrite half_add meven.
    rewrite -(doubleK (mmin k)) -addnn.
    by apply half_leq; apply leq_add; apply mmin_leq.
  Qed.

  Lemma min_le' : forall k k', k <= k' -> mmin k <= mmin k'.
    move=> k k'; move/subnKC => <-.
    elim: (k' - k).
      by rewrite addn0.
    move=> n H.
    rewrite addnS.
    apply: leq_trans; first by apply H.
    by apply min_le.
  Qed.

  (* (3) *)
  Lemma min_lt : forall c k, mmin k < m c k -> mmin k < m c k.+1.
  Proof.
    move=> c k Hlt.
    rewrite turn_spec.
    set ci := m c k in Hlt *; set cj := m (right c) k.
    apply (@leq_trans (ci./2 + cj./2)); last first.
      by apply leq_addr.
    have Hdbl : mmin k = (mmin k)./2.*2.
      by rewrite -{1}(odd_double_half (mmin k)) min_even.
    rewrite Hdbl -addnn -addSn.
    apply leq_add; last by apply half_leq; apply mmin_leq.
    rewrite ltn_neqAle; apply/andP.
    split; last by apply half_leq; apply mmin_leq.
    apply/eqP => Heq.
    rewrite Heq in Hdbl.
    have Hdbl' : ci = (ci./2).*2.
      by rewrite -{1}(odd_double_half ci) meven.
    by rewrite Hdbl -Hdbl' ltnn in Hlt.
  Qed.
    
  (* (4) *)
  Lemma m_lt : forall c k, m c k < m (right c) k -> m c k < m c k.+1.
  Proof.
    move=> c k Hlt.
    rewrite turn_spec.
    set ci := m c k in Hlt *; set cj := m (right c) k in Hlt *.
    apply (@leq_trans (ci./2 + cj./2)); last first.
      by apply leq_addr.
    have Hdbl : ci = ci./2.*2.
      by rewrite -{1}(odd_double_half ci) meven.
    rewrite {1}Hdbl -addnn -addnS.
    rewrite leq_add2l.
    have -> : ci./2.+1 = (ci + 2)./2.
      by rewrite half_add andbF add0n addn1.
    apply half_leq.
    suff: ci.+1 < cj.
      by rewrite -addn1 -addn1 -addnA.
    rewrite ltn_neqAle; apply/andP; split => //.
    apply/eqP; move/(congr1 odd).
    by rewrite /= !meven.
  Qed.

  Definition num x k := #|[pred c | x == m c k]|.
      
  (* (5) *)
  Lemma num_min_lt : forall c k,
    mmin k < m c k ->
    num (mmin k) k.+1 < num (mmin k) k.
  Proof.
    move=> c k Hlt.
    apply: proper_card.
    rewrite properE; apply/andP; split.
      apply/subsetP => c'.
      rewrite !inE.
      case E1: (_ == _); case E2: (_ == _) => //.
      have: mmin k < m c' k.
        by rewrite ltn_neqAle E2 /= mmin_leq.
      by move/min_lt; rewrite ltn_neqAle E1.
    apply/subsetP => H.
    have Hall: forall c, mmin k == m c k -> mmin k == m (right c) k.
      move=> c' He.
      rewrite eqn_leq; apply/andP; split.
        apply mmin_leq.
      rewrite (eqP He) leqNgt.
      apply/negP; move/m_lt; rewrite -(eqP He).
      move/H: He; rewrite inE /=; move/eqP => <-.
      by rewrite ltnn.
    have Hc: fclosed right [pred c | mmin k == m c k].
      apply intro_closed.
        by move=> *; rewrite !right_connect.
      move=> c' cr; move/eqP => <- /=.
      by apply Hall.
    case: (mmin_ex k) => c' Heq.
    move/(closed_connect Hc): (right_connect c c') => /=.
    by rewrite -Heq eqxx; move/eqP => Heq'; rewrite Heq' ltnn in Hlt.
  Qed.

  Theorem ex : exists k, forall c c', m c k = m c' k.
  Proof.
    suff: exists k, mmin k = mmax k.
      case=> k H; exists k.
      have Hc: forall c, mmin k = m c k.
        by move=> c; apply/eqP; rewrite eqn_leq mmin_leq H mmax_leq.
      by move=> c c'; rewrite -!Hc.
    exists ((mmax 0).+1 * #|ch|.+1).

    have Hinc: forall k, mmin k < mmax k -> mmin k < mmin (k + #|ch|.+1).
      move=> k.
      have Hn: forall r c, mmin k < m c k ->
        mmin k == mmin (k + r) ->
          mmin (k + r) < m c (k + r) /\ num (mmin (k + r)) (k + r) + r <= #|ch|.
        move=> r c H.
        elim: r.
          by rewrite !addn0 => _; split => //; apply: max_card.
        move=> c' IH Heq.
        have Heq': mmin k == mmin (k + c').
          rewrite eqn_leq {2}(eqP Heq) addnS min_le.
          by rewrite min_le' // leq_addr.
        case/IH: (Heq') => Hlt Hle.
        rewrite -(eqP Heq) (eqP Heq').
        split.
          by rewrite addnS min_lt.
        rewrite -addSnnS.
        apply: leq_trans; last by apply Hle.
        by rewrite leq_add2r addnS (num_min_lt c).
      case: (mmax_ex k) => c -> H.
      rewrite ltn_neqAle min_le' ?leq_addr // andbT.
      apply/eqP; move/eqP => Heq.
      move/Hn: H; case/(_ _ Heq) => _.
      by rewrite addnS addnC ltn_add_sub subnn.

    have H: forall r,
      mmin (r * #|ch|.+1) == mmax (r * #|ch|.+1) \/ mmin 0 + r <= mmin (r * #|ch|.+1).
      elim.
        by rewrite mul0n addn0; right.
      move=> r [Heq|Hle].
        left.
        rewrite mulSnr.
        rewrite eqn_leq min_leq_max andTb.
        apply (@leq_trans (mmin (r * #|ch|.+1))).
          by rewrite (eqP Heq) max_le' ?leq_addr.
        by rewrite min_le' ?leq_addr.
      case: (_ =P _) => [Heq|Hne]; first by left.
      right.
      apply (@leq_trans (mmin (r * #|ch|.+1)).+1).
        by rewrite addnS ltnS.
      rewrite mulSnr in Hne *.
      apply Hinc.
      rewrite ltn_neqAle min_leq_max andbT.
      apply/eqP => Heq; apply/Hne.
      apply/eqP; rewrite eqn_leq min_leq_max andTb.
      apply (@leq_trans (mmin (r * #|ch|.+1))).
        by rewrite Heq max_le' ?leq_addr.
      by rewrite min_le' ?leq_addr.

    case: (H (mmax 0).+1).
      by apply/eqP.
    move=> Hle; exfalso.
    have: mmin 0 + (mmax 0).+1 <= mmax 0.
      apply: leq_trans; first by apply Hle.
      apply: leq_trans; first by apply min_leq_max.
      by rewrite max_le' ?leq_addr.
    by rewrite addnS addnC ltn_add_sub subnn ltn0.
  Qed.
End Sec.