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

(** * Booleans.

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


Definition pointwise_product_dep {A B} (R₁ : relation A)
  (R₂ : forall x y : A, B x -> B y -> Prop) : relation (sigT B) :=
  fun p q =>
    let (x₁, y₁) := p in
    let (x₂, y₂) := q in
      R₁ x₁ x₂ /\ R₂ x₁ x₂ y₁ y₂.

(** A [DepPreOrder] is both Reflexive and Transitive. *)

Definition dep_relation {A} (B : A -> Type) : Type := forall x y : A, B x -> B y -> Prop.

Class DepReflexive A (B : A -> Type) (R : dep_relation B) :=
  reflexivity : forall (a : A) (x : B a), R a a x x.

Class DepIrreflexive A (B : A -> Type) (R : dep_relation B) :=
  irreflexivity : forall x (y : B x), R x x y y -> False.

Class DepSymmetric A (B : A -> Type) (R : dep_relation B) :=
  symmetry : forall a b (x : B a) (y : B b), R a b x y -> R b a y x.

Class Asymmetric A (B : A -> Type) (R : dep_relation B) :=
  asymmetry : forall a b (x : B a) (y : B b), R a b x y -> R b a y x -> False.

Class DepTransitive A (B : A -> Type) (R : dep_relation B) :=
  transitivity : forall a b c (x : B a) (y : B b) (z : B c), R a b x y -> R b c y z -> R a c x z.

Class DepPreOrder A (B : A -> Type) (R : dep_relation B) :=
  preorder_refl :> DepReflexive A B R ;
  preorder_trans :> DepTransitive A B R.

Class DepEquivalence A (B : A -> Type) (R : dep_relation B) :=
  equiv_refl :> DepReflexive A B R ;
  equiv_sym :> DepSymmetric A B R ;
  equiv_trans :> DepTransitive A B R.

Class [ DepEquivalence A B eqB ] => DepAntisymmetric (R : dep_relation B) := 
  antisymmetry_dep : forall a b (x : B a) (y : B b), R a b x y -> R b a y x -> eqB a b x y.


Notation " R [ x y ] ===> R' " := (@respectful_hetero _ _ _ _ (R%signature) (fun x y => R'%signature))
  (x ident, y ident, right associativity, at level 0) : signature_scope.

Notation " R ===> R' " := (@respectful_hetero _ _ _ _ (R%signature) (fun _ _ => R'%signature))
  (right associativity, at level 0) : signature_scope.

Class [ eqa : Equivalence A eqA, equ : DepEquivalence A B eqB, DepPreOrder A B R ] => DepPartialOrder :=
  partial_order_morphism :> 
  Morphism ( eqA [ x y ] ===> eqA [ x' y' ] ===> (eqB x y) ===> (eqB x' y') ===> iff) R ;
  partial_order_antisym :> DepAntisymmetric equ R.

Definition lexicographic_product_dep {A B} (R₁ : relation A) [ po : PartialOrder A eqA R₁ ]
  (R₂ : forall x y : A, B x -> B y -> Prop) 
  [ pb : DepPreOrder A B R₂ ] : relation (sigT B) :=
  fun p q =>
    let (x₁, y₁) := p in
    let (x₂, y₂) := q in
      x₁ <= x₂ \/ (x₁ === x₂ /\ R₂ x₁ x₂ y₁ y₂).

Program Instance [ pa : PreOrder A R₁, pb : DepPreOrder A B R₂ ] =>
  pointwise_preorder : PreOrder (sigT B) (pointwise_product_dep R₁ R₂).

  Solve Obligations using red ; intros; destruct_conjs; firstorder.
  
  Next Obligation.
  Proof.
    intros. red ; intros. simpl in *. destruct_conjs. split. transitivity y ; auto. 
    clapply transitivity.
  Qed.

Program Instance [ pa : Equivalence A R₁, pb : DepEquivalence A B R₂ ] =>
  pointwise_equivalence : Equivalence (sigT B) (pointwise_product_dep R₁ R₂).

  Next Obligation.
  Proof. red ; intros; destruct_conjs; firstorder. Qed.

  Next Obligation.
  Proof. red ; intros; destruct_conjs; firstorder. Qed.

  Next Obligation.
  Proof. red ; intros; destruct_conjs. simpl in *. 
    intuition order. transitivity y ; order. clapply transitivity.
  Qed.

Instance [ pa : PartialOrder A eqA R₁, pb : DepPartialOrder A eqA B eqB R₂ ] =>
  pointwise_partial_order : ! PartialOrder (sigT B) (pointwise_product_dep eqA eqB) (pointwise_product_dep R₁ R₂).

  Proof.
    red ; intros. simpl_relation. 
    simpl. unfold relation_conjunction. simpl.

    pose (partial_order_morphism x y). simpl in r.
    unfold respectful_hetero in r.

    firstorder.
    apply <- H1. clapply reflexivity.  clapply reflexivity. apply H0.
    reflexivity.
    
    apply -> H1. clapply reflexivity.  clapply reflexivity. 
    order. order.

    apply antisymmetry_dep ; auto.
  Qed.

Program Instance [ pa : PartialOrder A eqA R₁, pb : DepPreOrder A B R₂ ] =>
  lexicographic_dep_preorder : PreOrder (sigT B) (lexicographic_product_dep R₁ R₂).

  Solve Obligations using red ; intros; destruct_conjs; firstorder.
  
  Next Obligation.
  Proof.
    intros. red ; intros. simpl in *. destruct_conjs. left ; reflexivity. 
  Qed.

  Next Obligation.
  Proof.
    intros. red ; intros. simpl in *. destruct H. 

    left. destruct H0 as [H0 | [H0 H1]]. order. rewrite <- H0. assumption.
    destruct_conjs. setoid_rewrite H at 1 2. intuition. right ; intuition.
    clapply transitivity.
  Qed.
Print DepPartialOrder.

Print DepPartialOrder.

Instance [ pa : PartialOrder A eqA R₁, pb : DepPreOrder A B R₂, ! DepPartialOrder equ pb ] =>
  lexicographic_dep_partial_order : 
  ! PartialOrder (sigT B) (pointwise_product_dep eqA eqB) (lexicographic_product_dep R₁ R₂).

  Proof.
    red ; intros. simpl_relation. 
    simpl. unfold relation_conjunction. simpl.

    split ; intros.
    destruct_conjs. setoid_rewrite H at 1 4. split ; left ; reflexivity.

    destruct_conjs.

    intuition. order. apply antisymmetry_dep.
    clapply antisymmetry_dep. 


    apply <- H1. clapply reflexivity.  clapply reflexivity. apply H0.
    reflexivity.
    
    apply -> H1. clapply reflexivity.  clapply reflexivity. 
    order. order.

    apply antisymmetry_dep ; auto.
  Qed.