Library Padec.Tools.Min_list

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.

From Padec Require Import SetoidUtil.
From Padec Require FoldRight.
From Padec Require Import Graph_Diameter.


Open Scope nat_scope.
Set Implicit Arguments.

Section Min_list.

  Definition Min_list x l := fold_right min x l.

  Notation minFR := (FoldRight.min lt lt_dec).
  Lemma min_FR_Natmin: fequiv minFR Init.Nat.min.
  Notation Min_listFR := (fun x l => fold_right minFR x l).

  Lemma Min_listFR_compat:
    Proper (eq ==> (equivlistA eq) ==> eq) Min_listFR.
  Lemma fold_right_change_function:
    forall A (SA: Setoid A),
    forall (f g: A -> A -> A) x l,
      pequiv f g ->
      fold_right f x l == fold_right g x l.
  Lemma fold_right_change_min:
    forall x l, fold_right minFR x l = fold_right min x l.

  Lemma Min_list_equiv:
    
    forall a b,
      a = b ->
      forall l1 l2, equivlistA eq l1 l2 ->
                    Min_listFR a l1 = Min_list b l2.

  Lemma Min_list_compat:
    Proper (eq ==> (equivlistA eq) ==> eq) Min_list.

  Lemma Min_list_compat': Proper pequiv Min_list.

  Lemma Min_min_list1:
    forall x l, Some (Min_list x l) = min_list (x::l).
    Lemma Min_min_list2: forall a l,
      exists m, min_list (a::l) = Some m /\
                  Min_list a l = m.
    Lemma Min_min_list3: forall a l,
        InA equiv a l ->
        exists m, min_list l = Some m /\
                    Min_list a l = m.
    Lemma Min_list_in:
      forall x l, InA equiv (Min_list x l) (x::l).

    Lemma Min_list_le:
      forall y x l, InA equiv y (x::l) -> Min_list x l <= y.

    Lemma Min_list_spec:
      forall m x l,
        InA equiv m (x::l) /\ (forall y, InA equiv y (x::l) -> m <= y)
        <-> m = Min_list x l.

    Lemma Min_list_incl:
      forall x l y ll,
        (inclA eq) (x::l) (y::ll) -> Min_list y ll <= Min_list x l.

    Lemma Min_list_mono:
      forall (A: Type) {SA: Setoid A} (f g: A -> nat) a l,
        (forall x, InA equiv x (a :: l) -> f x <= g x) ->
        Min_list (f a) (map f l) <= Min_list (g a) (map g l).

    Lemma Min_list_lep:
      forall (A: Type) {SA: Setoid A} a l b ll,
        (forall x, InA equiv x (b::ll) -> exists y, InA equiv y (a::l) /\ y <= x) ->
        Min_list a l <= Min_list b ll.

    Lemma Min_list_eq:
      forall (A: Type) {SA: Setoid A} a l b ll,
        (forall x, InA equiv x (b::ll) -> exists y, InA equiv y (a::l) /\ y <= x) ->
        (forall x, InA equiv x (a::l) -> exists y, InA equiv y (b::ll) /\ y <= x) ->
        Min_list a l = Min_list b ll.

    Lemma map_inclA:
      forall (A: Type) {SA: Setoid A}
             (B: Type) {SB: Setoid B}
             (f: A -> B) (pf: Proper pequiv f)
             a b,
        inclA equiv a b -> inclA equiv (map f a) (map f b).

    Lemma fold_right_compose:
      forall (A: Type)
             (f: A -> A -> A) (g: A -> A)
             a l
             (H: forall x y, f (g x) (g y) = g (f x y)),
        fold_right f (g a) (map g l) =
          g (fold_right f a l).

    Lemma min_max_list:
      forall (A: Type) (SA: Setoid A) a l
             (f: A -> nat) (g: A -> nat)
             (pf: Proper pequiv f) (pg: Proper pequiv g)
             (H: forall x, InA equiv x (a :: l) -> f x <= g x),
        Min_list (f a) (map f l) <= fold_right max (g a) (map g l).

    Lemma max_list_mono:
      forall (A: Type) {SA: Setoid A} (f g: A -> nat)
             (a: A) (l: list A),
        (forall x: A, InA equiv x (a :: l) -> f x <= g x) ->
        fold_right max (f a) (map f l) <= fold_right max (g a) (map g l).

    Lemma min_list_compat_equivlist:
      Proper (equivlistA equiv ==> equiv) min_list.
    Lemma Min_list_const:
      forall a b l1 l2,
        (equivlistA equiv) (a :: l1) (b :: l2) ->
        Min_list a l1 = Min_list b l2.

End Min_list.

Unset Implicit Arguments.
Close Scope nat_scope.