From Coq Require Import RelationPairs.
From Coq Require Import Setoid.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import BoolEq.
From Coq Require Import Morphisms.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.

Open Scope Z_scope.
Set Implicit Arguments.

Global Instance fold_right_compat {A: Type} (eqA: relation A)
       {B: Type} (eqB: relation B):
  Proper ((eqB ==> eqA ==> eqA) ==> eqA ==> eqlistA eqB ==> eqA)
         (fold_right (A := A) (B := B)).

Section Fold_Right_Compat.

  Context {A: Type} `{SA:Setoid A}.
  Context {B: Type} `{SB:Setoid B}.
  Context (f: A -> B -> B).
  Context (f_compat: Proper fequiv f).
  Context (commutative:
             forall x y acc, f x (f y acc) == f y (f x acc)).
  Context (idempotent:
             forall x acc, (f x (f x acc)) == (f x acc)).

  Lemma fold_right_before_after: forall x x0 l,
      (fold_right f (f x x0) l) == (f x (fold_right f x0 l)).

  Lemma fold_right_left: forall x l,
      (fold_right f x l) == (fold_left (fun b a => f a b) l x).

  Lemma fold_right_cons_app:
    forall x0 x l,
      fold_right f x0 (l ++ (x :: nil)) ==
      fold_right f x0 ((x :: nil) ++ l).

  Lemma fold_right_app_cons_app:
    forall x0 x a b,
      (fold_right f x0 (a ++ (x :: nil) ++ b)) ==
      (fold_right f x0 ((x :: nil) ++ a ++ b)).

  Lemma fold_right_app_app: forall x a b,
      equiv (fold_right f x (a ++ b)) (fold_right f x (b ++ a)).

  Context {A_dec: Decider (equiv (A:=A))}.

  Lemma InA_cases: forall (x:A) h t,
      InA equiv x (h :: t) ->
      {x == h /\ ~ (InA equiv x t)}
      + {x == h /\ InA equiv x t}
      + {~ (x == h) /\ InA equiv x t}.

  Lemma no_remove:
    forall x l,
      ~ InA (equiv (A:=A)) x l ->
      eqlistA equiv l (removeA (eqA:=equiv) A_dec x l).

  Lemma fold_right_remove:
    forall x acc l,
      InA equiv x l ->
      fold_right f acc l ==
      f x (fold_right f acc (removeA A_dec x l)).

  Instance fold_right_compat_equivlist:
    Proper (equiv (A:=B) ==>
                  equivlistA (equiv (A:=A)) ==> equiv (A:=B))
           (fold_right f).

  Lemma remove_duplicates:
    forall x l1 l2,
      InA equiv x l1 ->
      equivlistA equiv l1 l2 ->
      equivlistA equiv (x :: (removeA A_dec x l1)) l2.

End Fold_Right_Compat.

Section Fold_Right_min_compat.

  Global Instance fold_right_min_compat:
    Proper (equiv ==> equivlistA equiv ==> equiv)
           (fold_right Z.min).

End Fold_Right_min_compat.

Section Fold_Right_max_compat.

  Global Instance fold_right_max_compat:
    Proper (equiv ==> equivlistA equiv ==> equiv)
           (fold_right Z.max).

End Fold_Right_max_compat.

Section Fold_Right_f_dec.

  Context {A: Type} `{SA: Setoid A}
          {f: A -> A -> A} {f_compat: Proper fequiv f}
          (f_dec: forall x y:A, {(f x y) == x} + {(f x y) == y}).

  Lemma fold_right_f_dec:
    forall x l,
      {fold_right f x l == x} + {InA equiv (fold_right f x l) l}.

  Lemma fold_right_f_dec_restr:
    forall x l,
      (forall y, InA equiv y l -> equiv (f y x) y) ->
      {l = nil} + {InA equiv (fold_right f x l) l}.

End Fold_Right_f_dec.

Section Fold_Right_Zmin_dec.

  Lemma fold_right_Zmin_dec: forall x l,
    {fold_right Z.min x l == x} +
    {InA equiv (fold_right Z.min x l) l}.

  Lemma fold_right_Zmin_dec_restr: forall x l,
      (forall y, InA equiv y l -> Z.min y x == y) ->
      {l = nil} + {InA equiv (fold_right Z.min x l) l}.

End Fold_Right_Zmin_dec.

Section Fold_Right_Zmax_dec.

  Lemma fold_right_Zmax_dec: forall x l,
    {fold_right Z.max x l == x} +
    {InA equiv (fold_right Z.max x l) l}.

  Lemma fold_right_Zmax_dec_restr: forall x l,
      (forall y, InA equiv y l -> Z.max y x == y) ->
      {l = nil} + {InA equiv (fold_right Z.max x l) l}.

End Fold_Right_Zmax_dec.

Require Import RelationA.
Section Fold_Right_f_leA.

  Context
    {A: Type} `{SA: Setoid A}
    {f: A -> A -> A} {f_compat: Proper fequiv f}
    (leA: relation A)
    {leA_compat: Proper fequiv leA}
    {leA_refl: Reflexive leA}
    {leA_trans: Transitive leA}
    (f_leA_left: forall x y, leA (f x y) x)
    (f_leA_right: forall x y, leA (f x y) y)
  .

  Lemma fold_right_f_eqA_leA:
    forall x y l,
      equiv x y ->
      leA (fold_right f x l) y.

  Lemma fold_right_f_InA_leA:
    forall x y l,
      InA equiv y l ->
      leA (fold_right f x l) y.

End Fold_Right_f_leA.

Section Fold_Right_Zmin_leA.

  Lemma fold_right_Zmin_eqA_leA:
    forall x y l,
      x == y ->
      Z.le (fold_right Z.min x l) y.

  Lemma fold_right_Zmin_InA_leA:
    forall x y l,
      InA equiv y l ->
      Z.le (fold_right Z.min x l) y.

  Lemma fold_right_Zmin_InA:
    forall x l,
      let y := fold_right Z.min x l in
      y == x \/ InA equiv y l.

End Fold_Right_Zmin_leA.

Section Fold_Right_Zmax_leA.

  Lemma Zge_wd: Proper (eq ==> eq ==> iff) Z.ge.

  Lemma Zge_refl: Reflexive Z.ge.

  Lemma Zge_trans: Transitive Z.ge.

  Lemma Zge_max_l: forall n m: Z, Z.max n m >= n.

  Lemma Zge_max_r: forall n m: Z, Z.max n m >= m.

  Lemma fold_right_Zmax_eqA_leA:
    forall x y l,
      equiv x y ->
      Z.ge (fold_right Z.max x l) y.

  Lemma fold_right_Zmax_InA_leA:
    forall x y l,
      InA equiv y l ->
      Z.ge (fold_right Z.max x l) y.

  Lemma fold_right_Zmax_InA: forall x l,
      let y := fold_right Z.max x l in
      equiv y x \/ InA equiv y l.

End Fold_Right_Zmax_leA.

Section Fold_Right_Min.

  Context {A: Type} `{SA:Setoid A}
          {A_dec: Decider (equiv (A:=A))}.

  Variable (lt: relation A)
           (lt_dec: forall a b, { lt a b } + { ~ lt a b })
           (lt_compat: Proper fequiv lt)
           (lt_trans: forall x y z, lt x y -> lt y z -> lt x z)
           (lt_strict: forall x y, lt x y -> ~x == y)
           (lt_total: forall x y, x == y \/ lt x y \/ lt y x)
  .

  Notation le x y := (x == y \/ lt x y).

  Lemma le_refl: forall x, le x x.

  Lemma le_trans: forall x y z, le x y -> le y z -> le x z.

  Lemma le_antisym: forall x y, le x y -> le y x -> x == y.

  Lemma not_lt_le: forall x y, ~lt x y -> le y x.

  Lemma not_le_lt: forall x y, ~le x y -> lt y x.

  Definition min a b := (if lt_dec a b then a else b).

  Lemma min_compat: Proper fequiv min.

  Lemma min_id: forall a, a == (min a a).

  Lemma lt_nonsym: forall x y, lt x y -> lt y x -> False.

  Lemma min_commut: forall a b, (min a b) == (min b a).

  Lemma min_assoc: forall a b c,
      (min a (min b c)) == (min (min a b) c).

  Lemma min_commut': forall a b c,
      (min a (min b c)) == (min b (min a c)).

  Lemma min_id': forall a b, (min a (min a b)) == (min a b).

  Lemma fold_right_min_InA:
    forall a b l, a == (fold_right min b l) ->
                  InA equiv a (b :: l).

  Lemma fold_right_min_after_before:
    forall a b l,
      (fold_right min a (b :: l)) == (fold_right min b (a :: l)).

  Lemma fr_min_le: forall a l, le (fold_right min a l) a.

  Lemma fr_min_tool:
    forall a l, (fold_right min a (a :: l)) ==
                (fold_right min a l).

  Lemma fr_min_tool':
    forall a b l,
      InA equiv a (b::l) -> (fold_right min a (b :: l)) ==
                            (fold_right min b l).

  Lemma removeA_insert:
    forall a b l,
      ~ a == b ->
      equivlistA equiv (b::(removeA A_dec a l))
                 (removeA A_dec a (b::l)).

  Lemma fold_right_min_cons:
    forall a b la lb,
      equivlistA equiv (a :: la) (b :: lb) ->
      (fold_right min a la) == (fold_right min b lb).

End Fold_Right_Min.

Close Scope Z_scope.
Unset Implicit Arguments.