Library Exercise_3_4_1_8


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.8

Section Exercise_3_4_1_8.

Problem

List all the preorder relations possible on the set {1, 2}.
For any n , how many linear orders exist on the set {1, 2, 3, ..., n}. Does your formula work when n = 0?

  Let finite_set n := { m | 1 m n }.
  Let finite_set_relation n : Relation_Definitions.relation Relation_Definitions.relation (finite_set n)
    := fun r ⇒ (fun x yr (proj1_sig x) (proj1_sig y)).

  Local Ltac t :=
    unfold finite_set, finite_set_relation;
    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.

  Example Exercise_3_4_1_8_R1 : Relation_Definitions.relation (finite_set 2) :=
    finite_set_relation (@eq ).
  Example Exercise_3_4_1_8_R2 : Relation_Definitions.relation (finite_set 2) :=
    finite_set_relation (fun x yx y).
  Example Exercise_3_4_1_8_R3 : Relation_Definitions.relation (finite_set 2) :=
    finite_set_relation (fun x yy x).
  Example Exercise_3_4_1_8_R4 : Relation_Definitions.relation (finite_set 2) :=
    fun _ _True.

  Example Exercise_3_4_1_8_R1_preorder : PreOrder Exercise_3_4_1_8_R1.
  Proof. t. Qed.
  Example Exercise_3_4_1_8_R2_preorder : PreOrder Exercise_3_4_1_8_R2.
  Proof. t. Qed.
  Example Exercise_3_4_1_8_R3_preorder : PreOrder Exercise_3_4_1_8_R3.
  Proof. t. Qed.
  Example Exercise_3_4_1_8_R4_preorder : PreOrder Exercise_3_4_1_8_R4.
  Proof. t. Qed.
End Exercise_3_4_1_8.