Require Import RingLike.IterMax.

From Stdlib Require Import Utf8 Arith.
Import List.ListNotations.
Open Scope list.

Require Import Core Misc Utils.

Notation "'Max' ( i = b , e ) , g" :=
  (iter_seq b e (λ c i, rngl_max c (g)) 0%L)
  (at level 45, i at level 0, b at level 60, e at level 60).

Notation "'Max' ( i ∈ l ) , g" :=
  (iter_list l (λ c i, rngl_max c (g)) 0%L)
  (at level 45, i at level 0, l at level 60).

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.

Theorem fold_left_rngl_max_fun_from_0 :
  rngl_is_ordered T = true →
  ∀ A a l (f : A → _),
  (0 ≤ a)%L
  → (∀ b, b ∈ l → (0 ≤ f b)%L)
  → (List.fold_left (λ c i, rngl_max c (f i)) l a =
     rngl_max a (List.fold_left (λ c i, rngl_max c (f i)) l 0)%L).

Theorem rngl_max_iter_list_app :
  rngl_is_ordered T = true →
  ∀ A (la lb : list A) f,
  (∀ x, x ∈ lb → rngl_max 0 (f x) = f x)
  → Max (i ∈ la ++ lb), f i =
      rngl_max (Max (i ∈ la), f i) (Max (i ∈ lb), f i).

Theorem rngl_max_iter_list_cons :
  rngl_is_ordered T = true →
  ∀ A a (la : list A) f,
  (∀ x, x ∈ a :: la → rngl_max 0 (f x) = f x)
  → Max (i ∈ a :: la), f i = rngl_max (f a) (Max (i ∈ la), f i).

Theorem rngl_le_max_list_r :
  rngl_is_ordered T = true →
  ∀ A l (a : A) f,
  (∀ x, x ∈ l → rngl_max 0 (f x) = f x)%L
  → a ∈ l
  → (f a ≤ Max (i ∈ l), f i)%L.

Theorem rngl_le_max_seq_r :
  rngl_is_ordered T = true →
  ∀ b e a f,
  (∀ x, x ∈ List.seq b (S e - b) → rngl_max 0 (f x) = f x)%L
  → a ∈ List.seq b (S e - b)
  → (f a ≤ Max (i = b, e), f i)%L.

Theorem rngl_max_list_empty : ∀ A g (l : list A),
  l = [] → Max (i ∈ l), g i = 0%L.

Theorem rngl_iter_max_list_nonneg :
  rngl_is_ordered T = true →
  ∀ A l (f : A → _),
  (∀ a, a ∈ l → (0 ≤ f a))%L
  → (0 ≤ Max (i ∈ l), f i)%L.

Theorem rngl_iter_max_seq_nonneg :
  rngl_is_ordered T = true →
  ∀ b e f,
  (∀ i, b ≤ i ≤ e → (0 ≤ f i)%L)
  → (0 ≤ Max (i = b, e), f i)%L.

Theorem eq_rngl_max_list_0 :
  rngl_is_ordered T = true →
  ∀ l (f : nat → T),
  Max (i ∈ l), f i = 0%L
  → (∀ i, i ∈ l → (0 ≤ f i)%L)
  → ∀ i, i ∈ l
  → f i = 0%L.

Theorem eq_rngl_max_seq_0 :
  rngl_is_ordered T = true →
  ∀ b e (f : nat → T),
  Max (i = b, e), f i = 0%L
  → (∀ i, b ≤ i ≤ e → (0 ≤ f i)%L)
  → ∀ i, b ≤ i ≤ e
  → f i = 0%L.

End a.