前順序

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 is_preorder (A : Type) (R : bin_rel A) : Prop := make_is_preorder
  { refl : forall x : A, R x x;
    trans : forall x y z : A, R x y -> R y z -> R x z }.

Arguments is_preorder A%_type_scope R
Arguments make_is_preorder [A]%_type_scope R (refl trans)%_function_scope
Arguments refl [A]%_type_scope [R] i {x}
Arguments trans [A]%_type_scope [R] i {x y z} _ _

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).
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
is_preorder {x : A | P x} (restriction_to_subset P)
  Proof.
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
is_preorder {x : A | P x} (restriction_to_subset P)
    constructor.
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
forall x : {x : A | P x}, restriction_to_subset P x x
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
forall (x : {x : A | P x}) (y z : {x : A | P x}),
restriction_to_subset P x y ->
restriction_to_subset P y z -> restriction_to_subset P x z
    -
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
forall x : {x : A | P x}, restriction_to_subset P x x
      intros.
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
x: {x : A | P x}
restriction_to_subset P x x
      unfold restriction_to_subset.
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
x: {x : A | P x}
R (proj1_sig x) (proj1_sig x)
      apply H.
    -
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
forall (x : {x : A | P x}) (y z : {x : A | P x}),
restriction_to_subset P x y ->
restriction_to_subset P y z -> restriction_to_subset P x z
      intros.
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
x, y, z: {x : A | P x}
H0: restriction_to_subset P x y
H1: restriction_to_subset P y z
restriction_to_subset P x z
      unfold restriction_to_subset in *.
A: Type
R: bin_rel A
H: is_preorder A R
P: A -> Prop
x, y, z: {x : A | P x}
H0: R (proj1_sig x) (proj1_sig y)
H1: R (proj1_sig y) (proj1_sig z)
R (proj1_sig x) (proj1_sig z)
      apply (H.(trans) H0 H1).
  Qed.
End Preorder.