(************************************************************************)
(*  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 Export Order.Quotients.
Require Import Coq.Program.Program.

Open Local Scope order_scope.

Class WellFounded `(StrictOrder A eqA ord) :=
  is_wellfounded : well_founded ord.

(** Not that we use the quotient order of [ord] here, implicitely. *)

Definition chain `{po : PartialOrder A eqA ord} (s : subset A) : Prop :=
  forall x y : object s, x <= y \/ x >= y.

(** Ascending chain condition on posets. *)

Class DescendingChainCondition `(po : PartialOrder A eqA ord) :=
  dcc : WellFounded (partial_order_restriction_strict po).

Class AscendingChainCondition `(po : PartialOrder A eqA ord) := 
  acc : DescendingChainCondition (partial_order_dual po).

(** Taken from "induction in Coq" by G. Huet. *)

Definition eternal {A} (R : relation A) := exists obj : A, forall x : A, exists y : A, R x y.

Definition classical_well_founded {A} (R : relation A) := ~ eternal R.

Class ClassicalWellFounded A (R : relation A) := 
  classical_wf : classical_well_founded R.

(** Classical chain conditions on posets. *)

(* Program Instance [ sa : Equivalence A eqA ] => setoid_flip : Equivalence A (flip eqA). *)

Class ClassicalAscendingChainCondition `(po : PartialOrder A eqA ord) :=
  classical_acc : ClassicalWellFounded A (partial_order_restriction ord).

Class ClassicalDescendingChainCondition `(po : PartialOrder A eqA ord) :=
  classical_dcc : ClassicalWellFounded A (flip (partial_order_restriction ord)).
    
(* Class [ po : PartialOrder A eqA ord ] => ClassicalAscendingChainCondition := *)
(*   classical_acc : classical_well_founded partial_order_restriction. *)

(** The constructive version entails the classical one. *)

Program Definition constructive_classical_chain_condition
  `{po : PartialOrder A, ! DescendingChainCondition po} : ClassicalDescendingChainCondition po.
  Proof.
    reduce_goal.
    destruct H as [obj H'].
    induction (dcc obj).
    destruct (H' x).
    apply H0 with x0 ; intros.
    apply H1.
  Qed.

Existing Instance constructive_classical_chain_condition.
    
(** The constructive descending chain condition can be restricted to a subset (not the classical one). *) 

Program Instance quotient_dcc `{dcc : DescendingChainCondition A eqA ord} (sub : subset A) : 
  DescendingChainCondition (quotient_partial_order sub).

  Next Obligation.
  Proof.
    destruct exist a Ha.
    induction (dcc0 a).
    apply Acc_intro.
    intros.
    destruct y as [y Hy].
    unfold partial_order_restriction, quotient_ord, le in H1.
    destruct H1 ; simpl in *.
    assert(partial_order_restriction ord y x).
    split ; auto. 
    apply H0.
    apply H3.
  Qed.

Require Import Coq.Logic.Classical.

(** Having the descending chain condition implies a minimal element in every subset. *)

(** This holds only for the classical definition of chain conditions, the rhs is not 
   strong enough for constructing the chain. *)

Lemma dsc_minimal_elements : forall `{po : PartialOrder A} (s : subset A), 
  ClassicalDescendingChainCondition (quotient_partial_order s) <-> 
  non_empty s -> exists x : object s, minimal_element x.
Proof.
  intros.
  split ; intros.

    do 2 red in H.
    unfold classical_well_founded, eternal in H.
    apply not_ex_all_not in H. 
    apply not_all_ex_not in H.
    destruct H as [x Hx].
    exists x.
    red ; intros.
    apply Hx. apply X.

    reduce_goal.
    destruct H0.
    specialize (H x).
    destruct H as [min Hmin].
    specialize (H0 min).
    apply Hmin. 
    destruct H0 as [ltmin Hltmin].
    exists ltmin. apply Hltmin.
Qed.

Lemma dsc_minimal_elements_set : forall `{po : PartialOrder A},
  ClassicalDescendingChainCondition po -> A -> exists x : A, forall y : A, ~ y </= x.
Proof.
  intros.
  destruct (dsc_minimal_elements (po:=po) full_subset).

  assert(ClassicalDescendingChainCondition (quotient_partial_order full_subset)).
  apply H1.
  intros.
  do 3 red in H.
  unfold eternal in H.
  apply not_ex_all_not in H ; auto.
  apply not_all_ex_not in H.
  destruct H. 
  exists (exist _ x I).
  reduce_goal. destruct H2 as [[min minI] Hmin].
  apply H. exists min ; apply Hmin.
  
  destruct (H0 H2 (exist _ X I)).
  destruct x.
  exists x.
  unfold minimal_element in H3.  
  intros.
  red ; intros.
  apply H3.
  exists (exist _ y I).
  apply H4.
Qed.

Lemma infinite_chains : forall `{po : PartialOrder A eqA ord},
  ~ (eternal (partial_order_restriction ord) \/ eternal (flip (partial_order_restriction ord))) <-> 
  ClassicalDescendingChainCondition po /\ ClassicalAscendingChainCondition po.
Proof.
  split ; intros.
  destruct (not_or_and _ _ H) ; clear H.
  split ; red ; red ; auto.

  destruct H.
  red ; intros.
  destruct H1 ; [ apply H0 | apply H ]; assumption.
Qed.