Library Exercise_3_4_1_7


Require Import Setoid Utf8.
Require Import ProofIrrelevance.
Require Import ZArith Omega.
Require Import Common Orders.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 3.4.1.7

Section Exercise_3_4_1_7.

Problem

Let S = {1, 2, 3, 4}. Find a preorder R S × S such that the set R is as small as possible. Is it a partial order? Is it a linear order?
Find a preorder R' S × S such that the set R' is as large as possible. Is it a partial order? Is it a linear order?

  Let S := { n | 1 n 4 }.

  Let R : relation S := fun n mproj1_sig n = proj1_sig m.
  Let R' : relation S := fun n mTrue.

  Local Ltac t :=
    unfold R, R';
    repeat match goal with
             | _split
             | _progress (compute in *; subst)
             | _progress trivial
             | _progress intuition
             | _intro
             | [ H : sig _ |- _ ] ⇒ destruct H
             | _apply proof_irrelevance
             | _omega
             | _apply f_equal
           end.

  Instance Exercise_3_4_1_7_R_preorder : PreOrder R.
  Proof.
    t.
  Qed.

  Example Exercise_3_4_1_7_R'_preorder : PreOrder R'.
  Proof.
    t.
  Qed.

  Example Exercise_3_4_1_7_R_partial_order : PartialOrder _ R.
  Proof.
    t.
  Qed.

  Example Exercise_3_4_1_7_R_not_comparable : ¬(Comparable R).
  Proof.
    intro H.
    assert (S1 : 1 1 4) by omega.
    assert (S2 : 1 2 4) by omega.
    specialize (H (exist _ 1 S1) (exist _ 2 S2)).
    t.
  Qed.

  Example Exercise_3_4_1_7_R'_not_antisymmetric : ¬(Antisymmetric _ _ R').
  Proof.
    intro H.
    assert (S1 : 1 1 4) by omega.
    assert (S2 : 1 2 4) by omega.
    specialize (H (exist _ 1 S1) (exist _ 2 S2) I I).
    inversion H.
  Qed.
End Exercise_3_4_1_7.