(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Order Theory

   Well-founded relations and chains.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Require Import Coq.Program.Program.
Require Export Order.Chains.

Open Local Scope order_scope.

Class Supremum `(po : PartialOrder A) (top : A) := 
  supremum : forall x, x <= top.

Class Infimum `(po : PartialOrder A) (bot : A) := 
  infimum :> Supremum (partial_order_dual po) bot.

Class Bounded `(po : PartialOrder A) :=
  { bottom : A ; top : A ;
    is_bottom : Infimum po bottom ;
    is_top : Supremum po top }.

Lemma top_le_eq : forall `{Bounded A} (x : A), top <= x -> top === x.
Proof.
  intros.
  apply (antisymmetry H0).
  apply is_top.
Qed.

Lemma le_bottom_eq : forall `{Bounded A} (x : A), x <= bottom -> x === bottom.
Proof.
  intros.
  apply (antisymmetry H0).
  apply is_bottom.
Qed.

Lemma unique_supremum : forall `{po : PartialOrder A, stop : ! Supremum po top₁, stop' : ! Supremum po top₂},
  top₁ === top₂.
Proof.
  intros. pose (supremum (top:=top₁) top₂) ; pose (supremum (top:=top₂) top₁). 
  apply (antisymmetry l0 l). 
Qed.

Lemma unique_infimum : forall `{po : PartialOrder A, ! Infimum po x, ! Infimum po y},
  x === y.
Proof. intros. apply (unique_supremum (po:=partial_order_dual po) (stop:=Infimum0) (stop':=Infimum1)) ; auto. Qed.

(** decreasing, down-set, ideal *)

Class DownwardClosed `(po : PartialOrder A) (B : subset A) :=
  downward_closed : forall (x : object B) (y : A), y <= `x -> y ∈ B.

(** increasing, upset, filter *)

Class UpwardClosed `(po : PartialOrder A) (B : subset A) :=
  upward_closed : forall (x : object B) (y : A), `x <= y -> y ∈ B.

Bind Scope type_scope with subset.

Definition downset `{po : PartialOrder A} (s : subset A) : subset A := 
  (fun y : A => exists x : object s, y <= `x)%type.

Definition upset `{po : PartialOrder A} (s : subset A) := 
  (fun y : A => exists x : object s, y >= `x)%type.

Section Downsets.
  Context `{po : PartialOrder A}.

  Inductive downsets : subset A -> Prop :=
  | downset_intro : forall s : subset A, downsets (downset s).

  Definition downsets_preorder : PreOrder (quotient_ord downsets) :=
    quotient_preorder downsets.

  Existing Instance downsets_preorder.

  Definition downsets_partial_order : PartialOrder (quotient_eq downsets) (quotient_ord downsets) :=
    quotient_partial_order downsets.

  Existing Instance downsets_partial_order.

End Downsets.

Definition upper_bound `{po : PartialOrder A eqA} (sub : subset A) (sup : A) := 
  forall y : object sub, `y <= sup.

Definition lower_bound `{po : PartialOrder A eqA} :=
  upper_bound (po:=partial_order_dual po).

Definition least_upper_bound `{po : PartialOrder A eqA} (sub : subset A) (sup : A) := 
  forall b, upper_bound sub b <-> sup <= b.

Lemma least_upper_bound_upper `{po : PartialOrder A} (sub : subset A) (sup : A) :
  least_upper_bound sub sup -> upper_bound sub sup.
Proof. intros. red in H. apply <- (H sup). order. Qed.

Lemma least_upper_bound_least `{po : PartialOrder A} (sub : subset A) (sup : A) :
  least_upper_bound sub sup -> forall up, upper_bound sub up -> sup <= up.
Proof. intros. red in H. apply -> (H up). apply H0. Qed.

Definition greatest_lower_bound `{po : PartialOrder A} := 
  least_upper_bound (po:=partial_order_dual po).

Definition unique `{Equivalence A} (P : A -> Prop) (x:A) :=
  P x /\ forall x', P x' -> x === x'.

Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
  (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
Notation "'exists' ! x : A , P" :=
  (ex (unique (fun x:A => P)))
  (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.

(* Lemma least_upper_bound_unique `{po : PartialOrder A} (sub : subset A) :  *)
(*   exists ! x, least_upper_bound sub x. *)


Definition fn_upper_bound {A}`{PartialOrder B eqB} (sub : subset A) (f : A -> B) :=
  least_upper_bound (fun y => forall x : object sub, y === f (`x)).

Require Import Ensembles.

Definition binary_lub `{po : PartialOrder A eqA} x y := 
  least_upper_bound (Couple _ x y).

Section Bounds.
  Context `{po : PartialOrder A eqA ord}.

  Lemma empty_upper_bound_infimum :
    (exists x : A, least_upper_bound empty_subset x) <-> exists x : A, Infimum po x.
  Proof.
    split ; unfold Infimum, Supremum, least_upper_bound, upper_bound ; intros H ; destruct H.
    exists x. intro x0.
    apply -> (H x0).
    intros.
    destruct y.
    inversion e.

    exists x.
    intros.
    split ; intros.
    apply H.
    inversion y. inversion H1.
  Qed.

  (** Interestingly, this proof requires reflexivity and transitivity at the end. *)

  Lemma full_upper_bound_supremum :
    (exists x : A, least_upper_bound full_subset x) <-> exists x : A, Supremum po x.
  Proof.
    intros.
    split ; unfold Infimum, Supremum, least_upper_bound, upper_bound ; intros H. 

    destruct H.
    exists x.
    intros.
    destruct (H x).
    apply (H1 (reflexivity x) (exist _ x0 I)). 
    
    destruct H.
    exists x.
    intros.
    split ; intros.
    apply (H0 (exist _ x I)).
    destruct y.
    pose (H x0) ; simpl. transitivity x ; auto.
  Qed.

End Bounds.

(** Dual theorems. *)

Lemma full_lower_bound_supremum `{po : PartialOrder A eqA ord} :
  (exists x, greatest_lower_bound empty_subset x) <-> exists x, Supremum po x.
Proof. intros. 
  apply empty_upper_bound_infimum. 
Qed.

Lemma full_lower_bound_infimum `{po : PartialOrder A eqA ord} :
  (exists x, greatest_lower_bound full_subset x) <-> exists x, Infimum po x.
Proof.
  intros.
  apply full_upper_bound_supremum.
Qed.

Lemma least_upper_bound_inclusion `{po : PartialOrder A} :
  forall F G, subset_inclusion F G -> 
    forall x y, least_upper_bound F x ->
      least_upper_bound G y -> x <= y.
Proof.
  unfold least_upper_bound, upper_bound.
  unfold flip, le in *.
  intros.
  apply -> H0.
  intros [y0 Hy0]. simpl.
  destruct (H1 y).
  exact (H3 (reflexivity y) (exist _ y0 (H _ Hy0))).
Qed.

Lemma greatest_lower_bound_inclusion `{po : PartialOrder A} :
  forall F G, subset_inclusion F G -> 
    forall x y, greatest_lower_bound F x ->
      greatest_lower_bound G y -> x >= y.
Proof.
  intros.
  eapply (least_upper_bound_inclusion (po:=partial_order_dual po)) ; eauto.
Qed.