Library prosa.classic.util.minmax

Require Export prosa.util.minmax.
Require Import prosa.classic.util.tactics prosa.classic.util.notation prosa.classic.util.sorting prosa.classic.util.nat prosa.classic.util.list.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Section MinMaxSeq.

  Section ArgGeneric.

    Context {T1 T2: eqType}.

    Variable rel: T2 T2 bool.
    Variable F: T1 T2.

    Fixpoint seq_argmin (l: seq T1) :=
      if l is x :: l' then
        if seq_argmin l' is Some y then
          if rel (F x) (F y) then Some x else Some y
        else Some x
      else None.

    Fixpoint seq_argmax (l: seq T1) :=
      if l is x :: l' then
        if seq_argmax l' is Some y then
          if rel (F y) (F x) then Some x else Some y
        else Some x
      else None.

    Section Lemmas.

      Lemma seq_argmin_exists:
         l x,
          x \in l
          seq_argmin l != None.
      Proof.
        induction l; first by done.
        intros x; rewrite in_cons.
        move ⇒ /orP [/eqP EQ | IN] /=;
          first by subst; destruct (seq_argmin l); first by case: ifP.
        by destruct (seq_argmin l); first by case: ifP.
      Qed.

      Lemma seq_argmin_in_seq:
         l x,
          seq_argmin l = Some x
          x \in l.
      Proof.
        induction l; simpl; first by done.
        intros x ARG.
        destruct (seq_argmin l);
          last by case: ARGEQ; subst; rewrite in_cons eq_refl.
        destruct (rel (F a) (F s));
          first by case: ARGEQ; subst; rewrite in_cons eq_refl.
        case: ARGEQ; subst.
        by rewrite in_cons; apply/orP; right; apply IHl.
      Qed.

      Lemma seq_argmax_exists:
         l x,
          x \in l
          seq_argmax l != None.
      Proof.
        induction l; first by done.
        intros x; rewrite in_cons.
        move ⇒ /orP [/eqP EQ | IN] /=;
          first by subst; destruct (seq_argmax l); first by case: ifP.
        by destruct (seq_argmax l); first by case: ifP.
      Qed.

      Lemma seq_argmax_in_seq:
         l x,
          seq_argmax l = Some x
          x \in l.
      Proof.
        induction l; simpl; first by done.
        intros x ARG.
        destruct (seq_argmax l);
          last by case: ARGEQ; subst; rewrite in_cons eq_refl.
        destruct (rel (F s) (F a));
          first by case: ARGEQ; subst; rewrite in_cons eq_refl.
        case: ARGEQ; subst.
        by rewrite in_cons; apply/orP; right; apply IHl.
      Qed.

      Section TotalOrder.

        Hypothesis H_transitive: transitive rel.

        Variable l: seq T1.
        Hypothesis H_total_over_list:
           x y,
            x \in l
            y \in l
            rel (F x) (F y) || rel (F y) (F x).

        Lemma seq_argmin_computes_min:
           x y,
            seq_argmin l = Some x
            y \in l
            rel (F x) (F y).
        Proof.
          rename H_transitive into TRANS, H_total_over_list into TOT, l into l'.
          induction l'; first by done.
          intros x y EQmin IN; simpl in EQmin.
          rewrite in_cons in IN.
          move: IN ⇒ /orP [/eqP EQ | IN].
          {
            subst; destruct (seq_argmin l') eqn:ARG; last first.
            {
              case: EQminEQ; subst.
              by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb.
            }
            {
              destruct (rel (F a) (F s)) eqn:REL; case: EQminEQ; subst;
                first by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb.
              exploit (TOT a x).
              - by rewrite in_cons eq_refl.
              - by rewrite in_cons; apply/orP; right; apply seq_argmin_in_seq.
              - by rewrite REL /=.
            }
          }
          {
            destruct (seq_argmin l') eqn:ARG.
            {
              destruct (rel (F a) (F s)) eqn:REL; case: EQminEQ; subst; last first.
              {
                apply IHl'; [| by done | by done].
                by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right.
              }
              {
                apply TRANS with (y := F s); first by done.
                apply IHl'; [| by done | by done].
                by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right.
              }
            }
            {
              case: EQminEQ; subst.
              by apply seq_argmin_exists in IN; rewrite ARG in IN.
            }
          }
        Qed.

        Lemma seq_argmax_computes_max:
           x y,
            seq_argmax l = Some x
            y \in l
            rel (F y) (F x).
        Proof.
          rename H_transitive into TRANS, H_total_over_list into TOT, l into l'.
          induction l'; first by done.
          intros x y EQmin IN; simpl in EQmin.
          rewrite in_cons in IN.
          move: IN ⇒ /orP [/eqP EQ | IN].
          {
            subst; destruct (seq_argmax l') eqn:ARG; last first.
            {
              case: EQminEQ; subst.
              by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb.
            }
            {
              destruct (rel (F s) (F a)) eqn:REL; case: EQminEQ; subst;
                first by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb.
              exploit (TOT a x).
              - by rewrite in_cons eq_refl.
              - by rewrite in_cons; apply/orP; right; apply seq_argmax_in_seq.
              - by rewrite REL orbF.
            }
          }
          {
            destruct (seq_argmax l') eqn:ARG.
            {
              destruct (rel (F s) (F a)) eqn:REL; case: EQminEQ; subst; last first.
              {
                apply IHl'; [| by done | by done].
                by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right.
              }
              {
                apply TRANS with (y := F s); last by done.
                apply IHl'; [| by done | by done].
                by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right.
              }
            }
            {
              case: EQminEQ; subst.
              by apply seq_argmax_exists in IN; rewrite ARG in IN.
            }
          }
        Qed.

      End TotalOrder.

    End Lemmas.

  End ArgGeneric.

  Section MinGeneric.

    Context {T: eqType}.
    Variable rel: rel T.

    Definition seq_min := seq_argmin rel id.
    Definition seq_max := seq_argmax rel id.

    Section Lemmas.

      Lemma seq_min_exists:
         l x,
          x \in l
          seq_min l != None.
      Proof.
        by apply seq_argmin_exists.
      Qed.

      Lemma seq_min_in_seq:
         l x,
          seq_min l = Some x
          x \in l.
      Proof.
        by apply seq_argmin_in_seq.
      Qed.

      Lemma seq_max_exists:
         l x,
          x \in l
          seq_max l != None.
      Proof.
        by apply seq_argmax_exists.
      Qed.

      Lemma seq_max_in_seq:
         l x,
          seq_max l = Some x
          x \in l.
      Proof.
        by apply seq_argmax_in_seq.
      Qed.

      Section TotalOrder.

        Hypothesis H_transitive: transitive rel.

        Variable l: seq T.
        Hypothesis H_total_over_list:
           x y,
            x \in l
            y \in l
            rel x y || rel y x.

        Lemma seq_min_computes_min:
           x y,
            seq_min l = Some x
            y \in l
            rel x y.
        Proof.
          by apply seq_argmin_computes_min.
        Qed.

        Lemma seq_max_computes_max:
           x y,
            seq_max l = Some x
            y \in l
            rel y x.
        Proof.
          by apply seq_argmax_computes_max.
        Qed.

      End TotalOrder.

    End Lemmas.

  End MinGeneric.

  Section ArgNat.

    Context {T: eqType}.

    Variable F: T nat.

    Definition seq_argmin_nat := seq_argmin leq F.
    Definition seq_argmax_nat := seq_argmax leq F.

    Section Lemmas.

      Lemma seq_argmin_nat_exists:
         l x,
          x \in l
          seq_argmin_nat l != None.
      Proof.
        by apply seq_argmin_exists.
      Qed.

      Lemma seq_argmin_nat_in_seq:
         l x,
          seq_argmin_nat l = Some x
          x \in l.
      Proof.
        by apply seq_argmin_in_seq.
      Qed.

      Lemma seq_argmax_nat_exists:
         l x,
          x \in l
          seq_argmax_nat l != None.
      Proof.
        by apply seq_argmax_exists.
      Qed.

      Lemma seq_argmax_nat_in_seq:
         l x,
          seq_argmax_nat l = Some x
          x \in l.
      Proof.
        by apply seq_argmax_in_seq.
      Qed.

      Section TotalOrder.

        Lemma seq_argmin_nat_computes_min:
           l x y,
            seq_argmin_nat l = Some x
            y \in l
            F x F y.
        Proof.
          intros l x y SOME IN.
          try ( apply seq_argmin_computes_min with (l0 := l); try (by done) ) ||
          apply seq_argmin_computes_min with (l := l); try (by done).
          - by intros x1 x2 x3; apply leq_trans.
          - by intros x1 x2 IN1 IN2; apply leq_total.
        Qed.

        Lemma seq_argmax_nat_computes_max:
           l x y,
            seq_argmax_nat l = Some x
            y \in l
            F x F y.
        Proof.
          intros l x y SOME IN.
          try ( apply seq_argmax_computes_max with (l0 := l); try (by done) ) ||
          apply seq_argmax_computes_max with (l := l); try (by done).
          - by intros x1 x2 x3; apply leq_trans.
          - by intros x1 x2 IN1 IN2; apply leq_total.
        Qed.

      End TotalOrder.

    End Lemmas.

  End ArgNat.

  Section MinNat.

    Definition seq_min_nat := seq_argmin leq id.
    Definition seq_max_nat := seq_argmax leq id.

    Section Lemmas.

      Lemma seq_min_nat_exists:
         l x,
          x \in l
          seq_min_nat l != None.
      Proof.
        by apply seq_argmin_exists.
      Qed.

      Lemma seq_min_nat_in_seq:
         l x,
          seq_min_nat l = Some x
          x \in l.
      Proof.
        by apply seq_argmin_in_seq.
      Qed.

      Lemma seq_max_nat_exists:
         l x,
          x \in l
          seq_max_nat l != None.
      Proof.
        by apply seq_argmax_exists.
      Qed.

      Lemma seq_max_nat_in_seq:
         l x,
          seq_max_nat l = Some x
          x \in l.
      Proof.
        by apply seq_argmax_in_seq.
      Qed.

      Section TotalOrder.

        Lemma seq_min_nat_computes_min:
           l x y,
            seq_min_nat l = Some x
            y \in l
            x y.
        Proof.
          intros l x y SOME IN.
          try ( apply seq_min_computes_min with (l0 := l); try (by done) ) ||
          apply seq_min_computes_min with (l := l); try (by done).
          - by intros x1 x2 x3; apply leq_trans.
          - by intros x1 x2 IN1 IN2; apply leq_total.
        Qed.

        Lemma seq_max_nat_computes_max:
           l x y,
            seq_max_nat l = Some x
            y \in l
            x y.
        Proof.
          intros l x y SOME IN.
          try ( apply seq_max_computes_max with (l0 := l); try (by done) ) ||
          apply seq_max_computes_max with (l := l); try (by done).
          - by intros x1 x2 x3; apply leq_trans.
          - by intros x1 x2 IN1 IN2; apply leq_total.
        Qed.

      End TotalOrder.

    End Lemmas.

  End MinNat.

  Section NatRange.

    Definition values_between (a b: nat) :=
      filter (fun xx a) (map (@nat_of_ord _) (enum 'I_b)).

    Lemma mem_values_between a b:
       x, x \in values_between a b = (a x < b).
    Proof.
      intros x; rewrite mem_filter.
      apply/idP/idP.
      {
        move ⇒ /andP [GE IN].
        move: IN ⇒ /mapP [x' IN] EQ; subst.
        rewrite mem_enum in IN.
        by apply/andP; split.
      }
      {
        move ⇒ /andP [GE LT].
        rewrite GE andTb.
        apply/mapP; (Ordinal LT); last by done.
        by rewrite mem_enum.
      }
    Qed.

    Definition min_nat_cond P (a b: nat) :=
      seq_min_nat (filter P (values_between a b)).

    Definition max_nat_cond P (a b: nat) :=
      seq_max_nat (filter P (values_between a b)).

    Lemma min_nat_cond_exists:
       (P: nat bool) (a b: nat) x,
        a x < b
        P x
        min_nat_cond P a b != None.
    Proof.
      intros P a b x LE HOLDS.
      try ( apply seq_argmin_exists with (x0 := x) ) ||
      apply seq_argmin_exists with (x := x).
      by rewrite mem_filter mem_values_between HOLDS LE.
    Qed.

    Lemma min_nat_cond_in_seq:
       P a b x,
        min_nat_cond P a b = Some x
        a x < b P x.
    Proof.
      intros P a b x SOME.
      apply seq_min_nat_in_seq in SOME.
      rewrite mem_filter in SOME; move: SOME ⇒ /andP [Px LE].
      by split; first by rewrite mem_values_between in LE.
    Qed.

    Lemma min_nat_cond_computes_min:
       P a b x,
        min_nat_cond P a b = Some x
        ( y, a y < b P y x y).
    Proof.
      intros P a b x SOME y LE Py.
      apply seq_min_nat_computes_min with (y := y) in SOME; first by done.
      by rewrite mem_filter Py andTb mem_values_between.
    Qed.

    Lemma max_nat_cond_exists:
       (P: nat bool) (a b: nat) x,
        a x < b
        P x
        max_nat_cond P a b != None.
    Proof.
      intros P a b x LE HOLDS.
      try ( apply seq_argmax_exists with (x0 := x) ) ||
      apply seq_argmax_exists with (x := x).
      by rewrite mem_filter mem_values_between HOLDS LE.
    Qed.

    Lemma max_nat_cond_in_seq:
       P a b x,
        max_nat_cond P a b = Some x
        a x < b P x.
    Proof.
      intros P a b x SOME.
      apply seq_max_nat_in_seq in SOME.
      rewrite mem_filter in SOME; move: SOME ⇒ /andP [Px LE].
      by split; first by rewrite mem_values_between in LE.
    Qed.

    Lemma max_nat_cond_computes_max:
       P a b x,
        max_nat_cond P a b = Some x
        ( y, a y < b P y y x).
    Proof.
      intros P a b x SOME y LE Py.
      apply seq_max_nat_computes_max with (y := y) in SOME; first by done.
      by rewrite mem_filter Py andTb mem_values_between.
    Qed.

  End NatRange.

End MinMaxSeq.

Section Kmin.

    Context {T1 T2: eqType}.

    Variable rel: T2 T2 bool.
    Variable F: T1 T2.

    Fixpoint seq_argmin_k (l: seq T1) (k: nat) :=
      if k is S k' then
        if (seq_argmin rel F l) is Some min_x then
          let l_without_min := rem min_x l in
            min_x :: seq_argmin_k l_without_min k'
        else [::]
      else [::].

      Lemma seq_argmin_k_exists:
         k l x,
          k > 0
          x \in l
          seq_argmin_k l k != [::].
      Proof.
        induction k; first by done.
        movel x _ IN /=.
        destruct (seq_argmin rel F l) as [|] eqn:MIN; first by done.
        suff NOTNONE: seq_argmin rel F l != None by rewrite MIN in NOTNONE.
        try ( by apply seq_argmin_exists with (x0 := x) ) ||
        by apply seq_argmin_exists with (x := x).
      Qed.

End Kmin.