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

(** * Cartesian product constructions: lexicographic and pointwise products.

   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.

Open Local Scope order_scope.

Definition pointwise_product {A B} (R₁ : relation A) (R₂ : relation B)  : relation (A * B) :=
  fun p q =>
    let (x₁, y₁) := p in
    let (x₂, y₂) := q in
      R₁ x₁ x₂ /\ R₂ y₁ y₂.

Require Import Classical.

Lemma complement_pointiwise_product_inv {A B} (R₁ : relation A) (R₂ : relation B) :
  forall x₁ x₂ y₁ y₂, complement (pointwise_product R₁ R₂) (x₁, y₁) (x₂, y₂) -> 
    complement R₁ x₁ x₂ \/ (R₁ x₁ x₂ /\ ~ R₂ y₁ y₂).
Proof.
  simpl. intros ; auto. red in H. simpl in H. unfold complement. 
  destruct (classic (R₁ x₁ x₂)). right. split ; auto.
  left ; apply H0.
Qed.

Program Instance pointwise_preorder `(pa : PreOrder A R₁, pb : PreOrder B R₂)
  : PreOrder (pointwise_product R₁ R₂).

  Solve Obligations using red ; intros; destruct_conjs; firstorder.

Program Instance pointwise_equivalence `(pa : Equivalence A R₁, pb : Equivalence B R₂) 
  : Equivalence (pointwise_product R₁ R₂).

  Solve Obligations using red ; intros; destruct_conjs; firstorder.

Instance pointwise_partial_order `(pa : PartialOrder A eqA R₁, pb : PartialOrder B eqB R₂)
  : PartialOrder (pointwise_product eqA eqB) (pointwise_product R₁ R₂).

  Proof.
    red ; intros. simpl_relation. firstorder.
  Qed.

Definition lexicographic_product {A} (R₁ : relation A) `{pa : PartialOrder A eqA R₁}
  {B} (R₂ : relation B) : relation (A * B) :=
  fun p q : A * B =>
    let (x₁, y₁) := p in
    let (x₂, y₂) := q in
      x₁ < x₂ \/ (x₁ === x₂ /\ R₂ y₁ y₂).

Program Instance lexicographic_preorder `(pa : PartialOrder A eqA R₁, pb : PreOrder B R₂)
  : PreOrder (lexicographic_product R₁ R₂).

  Next Obligation.
  Proof. 
    simpl. right. intuition order.
  Qed.

  Next Obligation.
  Proof.
    simpl in *.
    destruct H.
      left.
      destruct H0.
      rewrite H ; auto.
      destruct_conjs.
      rewrite <- H0. assumption.

      destruct_conjs.
      rewrite H.
      intuition.
      right ; split ; [ assumption | transitivity b0 ; auto ].
  Qed.

Instance lexicographic_partial_order `(pa : PartialOrder A eqA R₁, pb : PartialOrder B eqB R₂)
  : PartialOrder (pointwise_product eqA eqB) (lexicographic_product R₁ R₂).

  Proof.
    red ; intros. simpl_relation. split ; red ; intros ; orderify; simpl in *.
    destruct_conjs. split ; right ; intuition order. rewrite H0 ; reflexivity.
    symmetry ; auto. rewrite H0 ; reflexivity.

    repeat red in H ; simpl in *.
    destruct_conjs.
    destruct H ; destruct_conjs.

      destruct H0 as [H0 | [H0 H1]].
      order.
      rewrite H0 in H. elim (irreflexivity H).

      destruct H0 as [H0 | [Heq HR]].
      rewrite H in H0. elim (irreflexivity H0).
      rewrite (antisymmetry H1 HR). now rewrite Heq.
  Qed.

(** These two orders are well-founded. *)
  
Instance lexicographic_dcc `{pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB}
  `{acca : ! DescendingChainCondition pa, accb : ! DescendingChainCondition pb}
  : DescendingChainCondition (lexicographic_partial_order pa pb).
Proof.
  reduce_goal.
  destruct a.
  revert b.
  induction (acca a) as [a _ IHAcc].
  intro b.
  generalize dependent a.
  induction (accb b) as [b _ IHAcc']. intros.
  constructor. intros. 
  repeat red in H. destruct_conjs. 
  repeat red in H. destruct_conjs. orderify.
  unfold equiv in H0.
  destruct (complement_pointiwise_product_inv _ _ _ _ _ _ H0).

    apply IHAcc.
    firstorder order.

    destruct_conjs ; destruct H.
    rewrite H1 in H. order.

    destruct_conjs.
    apply IHAcc'. split ; auto.
    
    intros.
    apply IHAcc. rewrite <- H1. assumption.
Qed.

(** Well-foundedness. *)

Instance well_founded_subrelation_morphism : Proper (subrelation --> impl) (@well_founded A).
Proof.
  reduce. induction (H0 a) as [a _ IH].
  constructor. intros.
  apply IH. apply H. apply H1.
Qed.

Lemma subrelation_wf `(sa : StrictOrder A eqA (equ:=equ) ordA, sb : ! StrictOrder (equ:=equ) ordB,
  subrelation _ ordB ordA, acca : ! WellFounded sa) :
  WellFounded sb.
Proof.
  intros. unfold WellFounded in *.
  rewrite H. assumption.
Qed.

Lemma subrelation_dsc `(pa : PartialOrder A eqA (equ:=equ) ordA, pb : PartialOrder A eqA (equ:=equ) ordB,
  subrelation _ ordB ordA, acca : ! DescendingChainCondition pa) :
  DescendingChainCondition pb.
Proof. unfold DescendingChainCondition in *. 
  intros. eapply subrelation_wf; firstorder. 
Qed.
  
Lemma lexicographic_pointwise `{pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB} :
  subrelation (pointwise_product ordA ordB) (lexicographic_product ordA ordB).
Proof.
  reduce_goal. destruct x ; destruct x0. simpl in *.
  destruct_conjs. destruct (classic (a === a0)). 
  right ; auto.
  left ; firstorder order.
Qed.

Instance dcc_pointwise `(pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB,
  acca : ! DescendingChainCondition pa, accb : ! DescendingChainCondition pb)
: DescendingChainCondition (pointwise_partial_order pa pb).
Proof.
  intros. apply (subrelation_dsc (lexicographic_partial_order pa pb)).
  apply lexicographic_pointwise. 
  apply lexicographic_dcc.
Qed.