Library discprob.basic.seq_ext

From discprob.basic Require Import base nify.
From mathcomp Require Import ssreflect seq ssrbool eqtype.
Import Omega.

Lemma undup_map {A B: eqType} (l: seq A) (f: A → B):
  undup [seq f x | x <- l] = undup [seq f x | x <- undup l].

Lemma nth_legacy {A: Type} (d: A) l x:
  nth d l x = List.nth x l d.

Lemma nth_error_nth1 {A: Type} (d: A) l x:
  x < length l →
  List.nth_error l x = Some (nth d l x).

Lemma nth_error_nth2 {A: Type} (d: A) l x v:
  List.nth_error l x = Some v →
  nth d l x = v.

Lemma size_legacy {A: Type} (l: list A):
  size l = length l.

Lemma map_legacy {A B: Type} (f: A → B) l:
  map f l = List.map f l.

Lemma mem_seq_legacy {A: eqType} (x: A) (l: seq A):
  x \in l ↔ In x l.

Require Import Reals Psatz.

Local Open Scope R.
From discprob.basic Require Import base nify order.
From Coquelicot Require Import Rcomplements Rbar Series Lim_seq Hierarchy Markov.
Import List.

Lemma fold_left_Rmin_init l x:
  fold_left Rmin l x ≤ x.

Lemma fold_left_Rmin_mono_init l x x':
  x ≤ x' →
  fold_left Rmin l x ≤ fold_left Rmin l x'.

Lemma fold_left_Rmin_cons a l x:
  fold_left Rmin (a :: l) x ≤ fold_left Rmin l x.

Lemma fold_left_ext {A B} (f f': A → B → A) l l' x x':
  (∀ a b, f a b = f' a b) → l = l' → x = x' → fold_left f l x = fold_left f' l' x'.

Lemma fold_left_Rmin_glb l r x:
  (∀ r', In r' l → r ≤ r') → r ≤ x → r ≤ fold_left Rmin l x.

Lemma fold_left_Rmin_lb l x:
  (∀ r', In r' l → fold_left Rmin l x ≤ r').

Lemma fold_left_Rmin_witness1 l x:
  (∃ r, In r l ∧ r = fold_left Rmin l x) ∨ ((∀ r, In r l → x < r) ∧ fold_left Rmin l x = x).

Lemma fold_left_Rmax_init l x:
  x ≤ fold_left Rmax l x.

Lemma fold_left_Rmax_ub l x:
  (∀ r', In r' l → r' ≤ fold_left Rmax l x).

Lemma fold_left_Rmax_mono_init l x x':
  x ≤ x' →
  fold_left Rmax l x ≤ fold_left Rmax l x'.

Lemma fold_left_Rmax_cons a l x:
   fold_left Rmax l x ≤ fold_left Rmax (a :: l) x.

Lemma fold_left_Rmax_lub l r x:
  (∀ r', In r' l → r' ≤ r) → x ≤ r → fold_left Rmax l x ≤ r.

Lemma fold_left_Rmax_witness1 l x:
  (∃ r, In r l ∧ r = fold_left Rmax l x) ∨ ((∀ r, In r l → r < x) ∧ fold_left Rmax l x = x).

Lemma fold_left_Rmax_Rmin_map {A} (l: list A) (x: R) f:
   fold_left Rmax (map f l) x = - fold_left Rmin (map (λ x, - f x) l) (- x).

Lemma allpairs_comp {A A' B B'} (f1: A → A') (f2: B → B') l1 l2:
  [seq (f1 x1, f2 x2) | x1 <- l1, x2 <- l2] =
  [seq (x1, x2) | x1 <- [seq f1 i | i <- l1], x2 <- [seq f2 i | i <- l2]].

Lemma foldl_Rmin l:
  ∀ x, foldl Rmin x l ≤ x.

Lemma NoDup_uniq {T: eqType} (l: list T) : NoDup l ↔ uniq l.

Lemma NoDup_map {T1 T2: Type} (f: T1 → T2) (l: list T1) :
  (∀ x y, f x = f y → x = y) →
  NoDup l → NoDup (map f l).

Lemma NoDup_map_inv {T1 T2: Type} (f: T1 → T2) (l: list T1) :
  NoDup (map f l) → NoDup l.

Local Open Scope Z.
Lemma fold_left_Zmax_init l x:
  x ≤ fold_left Z.max l x.

Lemma fold_left_Zmax_ub l x:
  (∀ r', In r' l → r' ≤ fold_left Z.max l x).

Lemma fold_left_Zmax_mono_init l x x':
  x ≤ x' →
  fold_left Z.max l x ≤ fold_left Z.max l x'.

Lemma fold_left_Zmax_cons a l x:
   fold_left Z.max l x ≤ fold_left Z.max (a :: l) x.

Lemma fold_left_Zle_max_lub l r x:
  (∀ r', In r' l → r' ≤ r) → x ≤ r → fold_left Z.max l x ≤ r.

Lemma fold_left_Zmax_witness1 l x:
  (∃ r, In r l ∧ r = fold_left Z.max l x) ∨ ((∀ r, In r l → r < x) ∧ fold_left Z.max l x = x).

Local Open Scope positive.
Lemma fold_left_Pmax_init l x:
  x ≤ fold_left Pos.max l x.

Lemma fold_left_Pmax_ub l x:
  (∀ r', In r' l → r' ≤ fold_left Pos.max l x).

Lemma fold_left_Pmax_mono_init l x x':
  x ≤ x' →
  fold_left Pos.max l x ≤ fold_left Pos.max l x'.

Lemma fold_left_Pmax_cons a l x:
   fold_left Pos.max l x ≤ fold_left Pos.max (a :: l) x.

Lemma fold_left_Ple_max_lub l r x:
  (∀ r', In r' l → r' ≤ r) → x ≤ r → fold_left Pos.max l x ≤ r.

Lemma fold_left_Pmax_witness1 l x:
  (∃ r, In r l ∧ r = fold_left Pos.max l x) ∨ ((∀ r, In r l → r < x) ∧ fold_left Pos.max l x = x).

Lemma NoDup_inj_in_map {T1 T2: Type} (f: T1 → T2) (l: list T1) :
  (∀ x y, In x l → In y l → f x = f y → x = y) →
  NoDup l → NoDup (map f l).