Library Exercise_3_4_2_7


Require Import Setoid Utf8.
Require Import Common Orders.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 3.4.2.7

Section Exercise_3_4_2_7.

Problem

Suppose that S' := (S, ≤) is an preorder. If S' is a partial order, is S'op also a partial order? If S' is a linear order, is S'op a linear order?

  Variable S : Type.
  Variable le : Relation_Definitions.relation S.
  Local Infix "≤" := le.

  Instance PreOrder_op_is_PreOrder `(H : PreOrder S le)
  : PreOrder (opposite_relation le).
  Proof.
    firstorder.
  Qed.

  Instance PartialOrder_op_is_PartialOrder
           `(H : PreOrder S le)
           `(PartialOrder S eq le)
  : PartialOrder eq (opposite_relation le).
  Proof.
    firstorder.
  Qed.

  Instance LinearOrder_op_is_LinearOrder `(H : LinearOrder S le)
  : LinearOrder (opposite_relation le).
  Proof.
    firstorder.
  Qed.
End Exercise_3_4_2_7.