(************************************************************************)
(*  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 with Classes.
   
   Complete Partial Orders and Lattices.
   
   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Set Implicit Arguments.
Unset Strict Implicit.

Require Export Order.Lattice.
Require Export Order.Chains.

Open Local Scope order_scope.

Require Import Streams.

Definition chain [ po : PartialOrder A eqA ord ] : Type :=
  { f : nat -> A | forall n, f n <= f (S n) }.   (*forall x y : object s, x <= y \/ x >= y.*)

Definition directed_subset [ po : PartialOrder A eqA ord ] : subset A -> Prop :=
  fun s => forall x y : object s, exists z : object s, x <= z /\ y <= z.

Class [ po : PartialOrder A eqA ord ] => DCPO :=
  directed_supremum : forall x : subset A, directed_subset x -> 
    exists y, least_upper_bound x y.

Class [ DCPO A (po:=po) ] => DPCPO :=
  bottom : A ; bottom_inf : Infimum po bottom.

Program Definition chain_subset [ po : PartialOrder A eqA ord ] (c : chain) : subset A :=
  fun x => exists n, x = c n.

Require Import Order.Relations.
Require Import Coq.Lists.List.
Require Import Coq.Program.Program.
Require Import Ensembles.

Open Scope predicate_scope.

Class [ po : PartialOrder A eqA ord ] => CPO :=
  chain_lub : forall c : chain, exists y : A, least_upper_bound (chain_subset c) y ;
  bot : A ; bot_inf : Infimum po bot.

(* Instance [ Equivalence A eqA ] => pointed_dcpo : ! CPO (option A) pointed_eq pointed_le. *)
(* Proof. *)
(*   intros. unfold least_upper_bound, upper_bound. red in c. destruct c ; simpl. *)
(*   unfold chain_subset. simpl. *)
(*   exists None. destruct b. split ; intros; firstorder. *)
(*   destruct y.simpl. *)
  
(*   reduce. destruct x ; destruct y; firstorder. *)
(*   repeat red in H. destruct x ; destruct y; intuition. *)
(* Qed. *)