TPPmark7

gistfile1.txt

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

Section Sec.
  Parameter n : nat.
  Parameter m : nat -> nat -> nat.
  Parameter mmax : nat -> nat.
  Parameter mmin : nat -> nat.
  Parameter right : nat -> nat.

  Parameter npos : n > 0.
  Parameter meven0 : forall i, 0 < i <= n -> odd (m i 0) = false.
  Parameter mmax_leq : forall k i, 0 < i <= n -> m i k <= mmax k.
  Parameter mmin_leq : forall k i, 0 < i <= n -> mmin k <= m i k.
  Parameter mmax_ex : forall k, exists i, 0 < i <= n /\ mmax k = m i k.
  Parameter mmin_ex : forall k, exists i, 0 < i <= n /\ mmin k = m i k.

  Parameter right_S : forall i, 0 < i < n -> right i = i.+1.
  Parameter right_1 : forall i, n <= i -> right i = 1.

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

  Lemma right_in : forall i, 0 < i <= n -> 0 < right i <= n.
  Proof.
    move=> i; case/andP => Hlt0 Hlen.
    case: (ltnP i n) => H2.
      by rewrite right_S; apply/andP.
    by rewrite right_1 //= npos.
  Qed.

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

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

  Lemma max_le : forall k, mmax k.+1 <= mmax k.
  Proof.
    move=> k.
    case: (mmax_ex k.+1) => [i [Hin ->]].
    rewrite turn_spec.
    have :=  right_in i Hin.
    move: (right i) => j Hjn.
    set ci := m i k; set cj := m j 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 => Heq; rewrite Heq in Ho.
      case: (mmax_ex k) => [im [Himin Heq']].
      by rewrite Heq' meven in Ho.
    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 min_le : forall k, mmin k <= mmin k.+1.
  Proof.
    move=> k.
    case: (mmin_ex k.+1) => [i [Hin ->]].
    rewrite turn_spec.
    have := right_in i Hin.
    move: (right i) => j Hjn.
    set ci := m i k; set cj := m j 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_lt : forall k i, 0 < i <= n ->
    mmin k < m i k -> mmin k < m i k.+1.
  Proof.
    move=> k i Hin Hlt.
    rewrite turn_spec.
    have := right_in i Hin.
    move: (right i) => j Hjn.
    set ci := m i k in Hlt *; set cj := m j k.
    apply (@leq_trans (ci./2 + cj./2)); last first.
      by apply leq_addr.
    have Hdbl : mmin k = (mmin k)./2.*2.
      rewrite -{1}(odd_double_half (mmin k)).
      case: (mmin_ex k) => [im [Him ->]].
      by rewrite meven.
    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.
    
  Lemma m_lt : forall k i, 0 < i <= n ->
    m i k < m (right i) k -> m i k < m i k.+1.
  Proof.
    move=> k i Hin Hlt.
    rewrite turn_spec.
    have := right_in i Hin.
    move: (right i) Hlt => j Hlt Hjn.
    set ci := m i k in Hlt *; set cj := m j 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.
    apply leq_add; first by rewrite leqnn.
    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 => Heq.
    have : odd ci.+1.
      by rewrite /= meven.
    by rewrite Heq meven.
  Qed.

  Fixpoint num_aux (n x k : nat) : nat :=
    match n with
      | 0 => 0
      | S n' => (x == m n k) + num_aux n' x k
    end.

  Definition num x k := num_aux n x k.

  Lemma num_leq : forall (i x k : nat),
    i <= n ->
    (forall i, 0 < i <= n -> (x == m i k.+1) <= (x == m i k)) ->
    num_aux i x k.+1 <= num_aux i x k.
  Proof.
    move=> i x k Hin H.
    elim: i Hin => //= i IH Hin.
    apply leq_add; last by apply IH; apply ltnW.
    apply H.
    by rewrite ltn0Sn.
  Qed.

  Lemma num_lt : forall (x k j : nat),
    (forall i, 0 < i <= n -> (x == m i k.+1) <= (x == m i k)) ->
    0 < j <= n -> x == m j k -> x != m j k.+1 ->
    num x k.+1 < num x k.
  Proof.
    rewrite /num => x k j Hall.
    move=> Hjn Hj1 Hj2.
    have: n <= n by done.
    elim: {1 2 4 5}(n) Hjn => //=.
      by case/andP; rewrite ltnNge=> Hn H; case/negP: Hn.
    move=> i IH Hjn Hin.
    case: (i.+1 =P j) => [->|Hne].
      rewrite Hj1 (negbTE Hj2) /= add0n addSn ltnS add0n.
      by apply num_leq => //; apply ltnW.
    rewrite -addnS.
    apply leq_add.
      by apply Hall; rewrite ltn0Sn.
    apply IH; last by apply ltnW.
    case/andP: Hjn => H1 H2.
    apply/andP; split=> //.
    case: (ltngtP j i.+1); first by rewrite ltnS.
      by rewrite ltnNge H2.
    by move=> H; rewrite H in Hne.
  Qed.

  Fixpoint find_aux n k : option nat :=
    match n with
      | 0 => None
      | S n' =>
        if (mmin k == m n k) && (mmin k != m (right n) k) then
          Some n
        else
          find_aux n' k
    end.

  Lemma find_aux_Some :
    forall k i, find_aux n k = Some i ->
      (0 < i <= n) && (mmin k == m i k) && (mmin k != m (right i) k).
  Proof.
    move=> k i Heq.
    elim: (n) Heq => //= n' IH.
    case E: (_ && _).
      case=> <-.
      case/andP: E => H1 H2.
      by repeat (apply/andP; split => //).
    move/IH.
    case/andP; case/andP; case/andP => -> H -> -> /=.
    rewrite !andbT.
    by apply (@leq_trans n').
  Qed.

  Lemma find_aux_None :
    forall k i,
      find_aux n k == None -> 0 < i <= n -> mmin k == m i k.
  Proof.
    move=> k i Hnone Hin.
    have Hall: forall j, 0 < j <= n ->
      ~~((mmin k == m j k) && (mmin k != m (right j) k)).
      elim: (n) Hnone.
        by move=> _ j; rewrite ltnNge andNb.
      move=> n IH /= Hnone j Hjn.
      case: (j =P n.+1) => [->|Hne].
        by case: (_ && _) Hnone.
      apply IH.
        by case: (_ && _) Hnone.
      case/andP: Hjn => H1 H2.
      apply/andP; split=> //.
      case: (ltngtP j n.+1); first by rewrite ltnS.
        by rewrite ltnNge H2.
      by move=> H; rewrite H in Hne.
    have Hall': forall j, 0 < j <= n ->
      mmin k = m j k -> mmin k = m (right j) k.
      move=> j; move/Hall => H H1.
      rewrite -H1 eqxx /= negbK in H.
      by apply/eqP.      
    move=> {Hall Hnone}.

    have Hx : forall j n',
      mmin k = m j k ->
      0 < j <= n' -> n' <= n ->
      mmin k = m n' k.
      move=> j; elim.
        by rewrite ltnNge andNb.
      move=> n' IH.
      case (j =P n'.+1) => [-> //|Hne].
      move=> Heq Hjn Hn.
      have Hjn' : j <= n'.
        case: (ltngtP j n'.+1); first by rewrite ltnS.
          by rewrite ltnNge; case/andP: Hjn => _ ->.
        tauto.
      have -> : n'.+1 = right n'.
        rewrite right_S //.
        case/andP: Hjn => H1 H2.
        apply/andP; split=> //.
        by apply (@leq_trans j).
      apply Hall'.
        apply/andP; split; last by apply ltnW.
        apply (@leq_trans j) => //.
        by case/andP: Hjn.
      apply IH => //; last by apply ltnW.
      apply/andP; split=> //.
      by case/andP: Hjn.

    have Hn : mmin k = m n k.
      case: (mmin_ex k) => [j [Hjn Heq]].
      by apply (Hx j) => //.

    have H1 : mmin k = m 1 k.
      have -> : 1 = right n by rewrite right_1.
      apply Hall' => //.
      by apply/andP; split=> //; apply npos.

    apply/eqP.
    by apply (Hx 1) => //=; case/andP: Hin.
  Qed.
      
  Lemma num_min_lt : forall k i, 0 < i <= n ->
    mmin k < m i k ->
    num (mmin k) k.+1 < num (mmin k) k.
  Proof.
    move=> k i Hin H.
    have [j Hj] : exists j, 0 < j <= n /\ mmin k == m j k /\ mmin k != m (right j) k.
      case: (find_aux n k) (find_aux_Some k) (find_aux_None k).
        move=> j Hs _.
        exists j.
        by case/andP: (Hs j (erefl _)); case/andP => -> -> ->.
      move=> _ Hn.
      move/eqP: (Hn i (erefl _) Hin) => Heq.
      by rewrite Heq ltnn in H.
    move=> {i Hin H}.
    case: Hj => [Hj1 [Hj2 Hj3]].
    apply num_lt with j => //.
      move=> i Hin.
      case E1: (_ == _); case E2: (_ == _) => //.
      have H: mmin k < m i k.
        rewrite ltn_neqAle E2 /=.
        by apply mmin_leq.
      move/min_lt: Hin.
      move/(_ _ H).
      by rewrite ltn_neqAle E1.
    have H: m j k < m (right j) k.
      move/eqP: Hj2 => <-.
      rewrite ltn_neqAle Hj3 /=.
      apply mmin_leq.
      by apply right_in.
    move/m_lt: Hj1.
    move/(_ _ H).
    move/eqP: Hj2 => ->.
    rewrite ltn_neqAle.
    by case/andP.
  Qed.

  Lemma num_le_n : forall x k, num x k <= n.
  Proof.
    rewrite /num => x k.
    elim: (n) => //= n' H.
    rewrite -{2}add1n.
    by apply leq_add; first by apply leq_b1.
  Qed.

  Lemma ex : exists k, mmin k = mmax k.
  Proof.
    have Hinc: forall k, mmin k < mmax k -> mmin k < mmin (k + n.+1).
      have Hn: forall k r j, 0 < j <= n -> mmin k < m j k ->
        mmin k < mmin (k + r) \/
          mmin (k + r) < m j (k + r) /\ mmin k = mmin (k + r) /\ num (mmin (k + r)) (k + r) + r <= n.
        move=> k r j Hjn H.
        elim r.
          by right; rewrite !addn0 num_le_n.
        move=> i [Hlt|[Hlt [Heq Hle]]].
          left; apply: leq_trans; first by apply Hlt.
          by rewrite addnS min_le.
        rewrite ltn_neqAle.
        case: (_ =P _) => [<-|_].
          right; split.
            by rewrite Heq addnS min_lt.
          split => //.
          apply: leq_trans; last by apply Hle.
          rewrite !addnS Heq ltn_add2r.
          by apply (num_min_lt _ j).
        left.
        by rewrite andTb Heq addnS min_le.
      move=> k Hk.
      case: (mmax_ex k) => [j [Hjn Hj]].
      rewrite Hj in Hk.
      case: (Hn k n.+1 j) => //.
      case=> [_ [_]].
      by rewrite addnS addnC ltn_add_sub subnn.
    exists ((mmax 0).+1 * n.+1).
    have H: forall r,
      mmin (r * n.+1) == mmax (r * n.+1) \/ mmin 0 + r <= mmin (r * n.+1).
      elim.
        by rewrite mul0n addn0; right.
      have Hcmp: forall k i, mmin k <= mmin (k + i) /\ mmax (k + i) <= mmax k.
        move=> k; elim.
          by rewrite addn0.
        move=> i [H1 H2]; split.
          apply: leq_trans; first by apply H1.
          by rewrite addnS min_le.
        apply: leq_trans; last by apply H2.
        by rewrite addnS max_le.
      move=> r [Heq|Hle].
        left.
        rewrite mulSnr.
        case: (Hcmp (r * n.+1) n.+1) => H1 H2.
        rewrite eqn_leq; apply/andP; split.
          by apply min_leq_max.
        rewrite (eqP Heq) in H1.
        by eapply leq_trans; eauto.
      case: (_ =P _) => [Heq|Hne].
        by left.
      right.
      apply (@leq_trans (mmin (r * n.+1)).+1).
        by rewrite addnS ltnS.
      rewrite mulSnr in Hne *.
      apply Hinc.
      rewrite ltn_neqAle; apply/andP; split; last first.
        by apply min_leq_max.
      apply/eqP => Heq; apply/Hne.
      case: (Hcmp (r * n.+1) n.+1) => H1 H2.
      apply/eqP; rewrite eqn_leq; apply/andP;split.
        by apply min_leq_max.
      rewrite Heq in H1.
      by eapply leq_trans; eauto.
    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.
      elim: (_ * _) => // i IH.
      by apply: leq_trans; first by apply max_le.
    by rewrite addnS addnC ltn_add_sub subnn ltn0.
  Qed.
End Sec.