Library probsa.util.min

Require Export Reals.
From mathcomp Require Export ssreflect ssrnat ssrbool seq.

Definition min_option (xs : seq nat) : option nat :=
  match xs with
  | [::] ⇒ None
  | h::tl ⇒ Some (foldl minn h tl)
  end.

Definition min_default (d : nat) (xs : seq nat) : nat := foldl minn d xs.
Definition min1 (xs : seq R) : R := foldl Rmin 1%R xs.

Lemma min1_cons :
  ∀ xs x0,
    min1 (x0 :: xs) = Rmin x0 (min1 xs).
Proof.
  have L: ∀ s x xs, foldl Rmin s (x::xs) = Rmin x (foldl Rmin s xs).
  { clear; intros.
    generalize dependent s; generalize dependent x.
    induction xs.
    { by intros; rewrite Rmin_comm. }
    { intros; simpl in *;
      by rewrite Rmin_comm IHxs [Rmin s a]Rmin_comm IHxs Rmin_assoc [Rmin s x]Rmin_comm. }
  }
  by intros; rewrite /min1 L.
Qed.

Lemma Rle_min_compat :
  ∀ (x y z w : R),
    (x ≤ z)%R →
    (y ≤ w)%R →
    (Rmin x y ≤ Rmin z w)%R.
Proof.
  intros; rewrite /Rmin.
  destruct Rle_dec as [LE1|LE1]; destruct Rle_dec as [LE2|LE2] ⇒ //.
  { by eapply Rle_trans; [apply LE1 | done]. }
  { apply Rnot_le_gt, Rgt_lt, Rlt_le in LE1.
    by eapply Rle_trans; [apply LE1 | by done]. }
Qed.