(*|
前順序
======
|*)

Require Import relation.

Set Implicit Arguments.

Record is_preorder
  (A : Type)
  (R : bin_rel A)
  : Prop :=
  make_is_preorder {
    refl {x} : R x x;

    trans {x y z} :
      R x y ->
      R y z ->
      R x z;
  }.

Arguments is_preorder : clear implicits.
Print is_preorder.

Record preorder (A : Type) : Type :=
  make_preorder {
    R             :> bin_rel A;
    R_is_preorder :> is_preorder A R;
  }.

Record preordered_type : Type :=
  make_preordered_type {
    A             :> Type;
    preorder_on_A :  preorder A;
  }.

Section Preorder.
  Context {A : Type}.
  Context {R : bin_rel A}.
  Context {H : is_preorder A R}.

  Definition restriction_to_subset
    (P : A -> Prop)
    : bin_rel { a : A | P a } :=
    fun x y => R (proj1_sig x) (proj1_sig y).

  Lemma restriction_is_preorder
    (P : A -> Prop)
    : is_preorder (sig P) (restriction_to_subset P).
  Proof.
    constructor.
    -
      intros.
      unfold restriction_to_subset.
      apply H.
    -
      intros.
      unfold restriction_to_subset in *.
      apply (H.(trans) H0 H1).
  Qed.
End Preorder.