Set Firstorder Depth 5.

Require Export RSetoid.

Set Implicit Arguments.

Record is_PartialOrder
 (car : Type)
 (eq : car → car → Prop)
 (le : car → car → Prop)
 (monotone : (car → car) → Prop)
 (antitone : (car → car) → Prop) : Prop :=
{ po_equiv_le_def : ∀ x y, eq x y ↔ (le x y ∧ le y x)
; po_le_refl : ∀ x, le x x
; po_le_trans : ∀ x y z, le x y → le y z → le x z
; po_monotone_def : ∀ f, monotone f ↔ (∀ x y, le x y → le (f x) (f y))
; po_antitone_def : ∀ f, antitone f ↔ (∀ x y, le x y → le (f y) (f x))
}.

Record PartialOrder : Type :=
{ po_car :> RSetoid
; le : po_car → po_car → Prop
; monotone : (po_car → po_car) → Prop
; antitone : (po_car → po_car) → Prop
; po_proof : is_PartialOrder (@st_eq po_car) le monotone antitone
}.

Notation "x == y" := (st_eq x y) (at level 70, no associativity) : po_scope.
Notation "x <= y" := (le _ x y) : po_scope.

Open Local Scope po_scope.

Lemma po_st : ∀ X eq le mnt ant, @is_PartialOrder X eq le mnt ant → Setoid_Theory X eq.
Proof with trivial.
 intros X eq le0 mnt ant H.
 split.
   firstorder.
  intros x y E. apply (po_equiv_le_def H), and_comm, (po_equiv_le_def H)...
 intros x y z.
 repeat rewrite ->(po_equiv_le_def H).
 firstorder.
Qed.

Section PartialOrder.

Variable X : PartialOrder.

Definition makePartialOrder car eq le monotone antitone p1 p2 p3 p4 p5 :=
let p := (@Build_is_PartialOrder car eq le monotone antitone p1 p2 p3 p4 p5) in
 @Build_PartialOrder (Build_RSetoid (po_st p)) le monotone antitone p.

Lemma equiv_le_def : ∀ x y:X, x == y ↔ (x ≤ y ∧ y ≤ x).
Proof (po_equiv_le_def (po_proof X)).

Lemma le_refl : ∀ x:X, x ≤ x.
Proof (po_le_refl (po_proof X)).

Lemma le_trans : ∀ x y z : X, x ≤ y → y ≤ z → x ≤ z.
Proof (po_le_trans (po_proof X)).

Lemma monotone_def : ∀ f, monotone X f ↔ (∀ x y, x ≤ y → (f x) ≤ (f y)).
Proof (po_monotone_def (po_proof X)).

Lemma antitone_def : ∀ f, antitone X f ↔ (∀ x y, x ≤ y → (f y) ≤ (f x)).
Proof (po_antitone_def (po_proof X)).

Lemma le_equiv_refl : ∀ x y:X, x == y → x ≤ y.
Proof.
 firstorder using equiv_le_def.
Qed.

Lemma le_antisym : ∀ x y:X, x ≤ y → y ≤ x → x == y.
Proof.
 firstorder using equiv_le_def.
Qed.

Definition Dual : PartialOrder.
Proof.
 eapply makePartialOrder with (eq := @st_eq X) (le:= (fun x y ⇒ le X y x)) (monotone := @monotone X)
   (antitone := @antitone X).
     firstorder using equiv_le_def.
    firstorder using le_refl.
   firstorder using le_trans.
  firstorder using monotone_def.  firstorder using antitone_def.
Defined.

End PartialOrder.

Module Default.

Section MonotoneAntitone.

Variable A : Type.
Variable le : A → A → Prop.

Definition monotone (f: A → A) := ∀ x y, le x y → le (f x) (f y).

Lemma monotone_def : ∀ f, monotone f ↔ (∀ x y, le x y → le (f x) (f y)).
Proof.
 firstorder.
Qed.

Definition antitone (f: A → A) := ∀ x y, le x y → le (f y) (f x).

Lemma antitone_def : ∀ f, antitone f ↔ (∀ x y, le x y → le (f y) (f x)).
Proof.
 firstorder.
Qed.

End MonotoneAntitone.

End Default.