(************************************************************************)
(*  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

   Quotient orders.

   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.Order.

Definition subset A := A -> Prop.

(* Open Scope subset_scope. *)

Notation object := sig (only parsing).
Notation non_empty := sig (only parsing).

(** Extensional equality of subsets. *)

Definition subset_equality {A} : relation (subset A) :=
  fun s s' => forall x, s x <-> s' x.

Program Instance subset_equivalence : @Equivalence (subset A) subset_equality.

  Next Obligation.
  Proof.
    unfold subset_equality in *.
    rewrite H. reflexivity.
  Qed.

  Next Obligation.
  Proof.
    unfold subset_equality in *.
    rewrite H. rewrite H0. reflexivity.
  Qed.

Definition subset_inclusion {A} : relation (subset A) :=
  fun s s' => forall x, s x -> s' x.

Program Instance inclusion_preorder : 
  ! PreOrder (subset A) subset_inclusion.

Program Instance inclusion_partial_order : 
  ! PartialOrder (subset A) subset_equality subset_inclusion.

  Solve Obligations using firstorder order.
    
(* Bind Scope type_scope with relation. *)

Definition quotient_eq `{sa : Equivalence A eqA} (s : subset A) : relation (sig s) := 
  fun x y : sig s => `x === `y.

Program Instance quotient_setoid `{equ : Equivalence A eqA} (s : subset A)
  : @Equivalence (sig s) (quotient_eq s).

  Solve Obligations using unfold quotient_eq ; simpl_relation ; firstorder order.
  
  Next Obligation.
  Proof.
    unfold quotient_eq in * ; simpl_relation. 
    transitivity y; auto.
  Qed.


Definition quotient_ord `{p : PreOrder A ord} (s : subset A) : relation (sig s) := 
  fun x y : sig s => ord (`x) (`y).

Instance preorder_rewrite `(PreOrder A R) : RewriteRelation R.

(** Naming bug if sub -> s *)
Program Instance quotient_preorder `{pre : PreOrder A ord} (sub : subset A)
  : ! PreOrder (sig sub) (quotient_ord sub).

  Next Obligation.
  Proof.
    unfold quotient_ord. reflexivity. 
  Qed.

  Next Obligation.
  Proof.
    unfold quotient_ord in *. simpl in *.
    rewrite <- H0. assumption.
  Qed.

Program Instance quotient_partial_order `{po : PartialOrder A eqA ord} (sub : subset A)
  : PartialOrder (quotient_eq sub) (quotient_ord sub).

  Next Obligation.
  Proof.
    unfold quotient_ord, quotient_eq in *. simpl. split ; intros.
    reduce. rewrite H. split ; order.
    repeat red in H. order_antisymmetry ord; firstorder.
  Qed.

(*   Next Obligation. *)
(*   Proof. *)
(*     unfold quotient_ord, quotient_eq in *. *)
(*     rewrite H ; rewrite H0. reflexivity. *)
(*   Qed. *)

(*   Next Obligation. *)
(*   Proof. *)
(*     unfold quotient_ord in * ; red ; simpl proj1_sig in *.  *)
(*     order_antisymmetry ord ; auto. *)
(*   Qed. *)

(** Talking about quotients. *)

Program Definition maximal_element `{po : PartialOrder A eqA ord} {s : subset A} (m : object s) :=
  ~ exists x : object s, partial_order_restriction ord m x.

Definition maximal_elements `{po : PartialOrder A} (s : subset A) := 
  { m : object s | maximal_element m }.

Program Definition minimal_element `{po : PartialOrder A eqA ord}
  {s : subset A} (m : object s) :=
 ~ exists x : sig s, partial_order_restriction ord x m.

Definition minimal_elements `{po : PartialOrder A} (s : subset A) := 
  { m : object s | minimal_element m }.

(* Open Local Scope subset_scope. *)

Definition empty_subset {A} : subset A := fun _ : A => False.
Definition full_subset {A} : subset A := fun _ : A => True.

Definition in_subset {A} (s : subset A) x := s x.

Notation " x ∈ s " := (in_subset s x) (at level 20).