Require Import FunctionalExtensionality Nat Arith Lia.

Require Import List.
Import ListNotations.

From Typonomikon Require Export BC2g.

Class CoTransitive {A : Type} (R : rel A) : Prop :=
  cotransitive : forall {x z : A}, R x z -> forall y : A, R x y \/ R y z.

#[export]
Instance CoTransitive_Empty :
  forall R : rel Empty_set, CoTransitive R.

#[export]
Instance CoTransitive_RTrue :
  forall A : Type, CoTransitive (@RTrue A A).

#[export]
Instance CoTransitive_RFalse :
  forall A : Type, CoTransitive (@RFalse A A).

Lemma CoTransitive_eq_unit :
  CoTransitive (@eq unit).

Lemma not_CoTransitive_eq_two_elems :
  forall {A : Type} {x y : A},
    x <> y -> ~ CoTransitive (@eq A).

#[export]
Instance CoTransitive_Rinv :
  forall (A : Type) (R : rel A),
    CoTransitive R -> CoTransitive (Rinv R).

Lemma not_CoTransitive_Rcomp :
  exists (A : Type) (R S : rel A),
    CoTransitive R /\ CoTransitive S /\ ~ CoTransitive (Rcomp R S).

Lemma not_CoTransitive_Rnot :
  exists (A : Type) (R : rel A),
    CoTransitive R /\ ~ CoTransitive (Rnot R).

#[export]
Instance CoTransitive_Ror :
  forall (A : Type) (R S : rel A),
    CoTransitive R -> CoTransitive S -> CoTransitive (Ror R S).

Lemma not_CoTransitive_Rand :
  exists (A : Type) (R S : rel A),
    CoTransitive R /\ CoTransitive S /\ ~ CoTransitive (Rand R S).

Class Apartness {A : Type} (R : rel A) : Prop :=
{
  Apartness_Antireflexive :> Antireflexive R;
  Apartness_Symmetric :> Symmetric R;
  Apartness_Cotransitive :> CoTransitive R;
}.

#[export]
Instance Apartness_Empty :
  forall R : rel Empty_set, Apartness R.

Lemma not_Apartness_RTrue :
  forall {A : Type}, A -> ~ Apartness (@RTrue A A).

#[export]
Instance Apartness_RFalse :
  forall {A : Type}, Apartness (@RFalse A A).

Lemma not_Apartness_eq :
  forall {A : Type}, A -> ~ Apartness (@eq A).

From Typonomikon Require Import BC4a.

Lemma Apartness_neq :
  forall {A : Type}, Apartness (Rnot (@eq A)).

Lemma Apartnes_neq :
  (forall {A : Type}, Apartness (Rnot (@eq A))) ->
    (forall {A : Type} (x y : A), x <> y \/ ~ x <> y).

#[export]
Instance Apartness_Rinv :
  forall (A : Type) (R : rel A),
    Apartness R -> Apartness (Rinv R).

Lemma not_Apartness_Rcomp :
  exists (A : Type) (R S : rel A),
    Apartness R /\ Apartness S /\ ~ Apartness (Rcomp R S).

Lemma not_Apartness_Rnot :
  exists (A : Type) (R : rel A),
    Apartness R /\ ~ Apartness (Rnot R).

#[export]
Instance Apartness_Ror :
  forall (A : Type) (R S : rel A),
    Apartness R -> Apartness S -> Apartness (Ror R S).

Lemma not_Rand_Apartness :
  exists (A : Type) (R S : rel A),
    Apartness R /\ Apartness S /\ ~ Apartness (Rand R S).

Class Trichotomous {A : Type} (R : rel A) : Prop :=
{
  trichotomous : forall x y : A, R x y \/ x = y \/ R y x
}.

#[export]
Instance Trichotomous_Total :
  forall (A : Type) (R : rel A),
    Total R -> Trichotomous R.

#[export]
Instance Trichotomous_Empty :
  forall R : rel Empty_set, Trichotomous R.

#[export]
Instance Trichotomous_RTrue :
  forall A : Type, Trichotomous (@RTrue A A).

#[export]
Instance Trichotomous_RFalse_subsingleton :
  forall A : Type, (forall x y : A, x = y) -> Trichotomous (@RFalse A A).

Lemma not_Trichotomous_RFalse_two_elems :
  forall {A : Type} {x y : A},
    x <> y -> ~ Trichotomous (@RFalse A A).

#[export]
Instance Trichotomous_eq_subsingleton :
  forall A : Type, (forall x y : A, x = y) -> Trichotomous (@eq A).

Lemma not_Trichotomous_eq :
  exists A : Type, ~ Trichotomous (@eq A).

#[export]
Instance Trichotomous_Rinv :
  forall (A : Type) (R : rel A),
    Trichotomous R -> Trichotomous (Rinv R).

Lemma not_Trichotomous_Rcomp :
  exists (A : Type) (R S : rel A),
    Trichotomous R /\ Trichotomous S /\ ~ Trichotomous (Rcomp R S).

Lemma not_Trichotomous_Rnot :
  exists (A : Type) (R : rel A),
    Trichotomous R /\ ~ Trichotomous (Rnot R).

#[export]
Instance Trichotomous_Ror :
  forall (A : Type) (R S : rel A),
    Trichotomous R -> Trichotomous S -> Trichotomous (Ror R S).

Lemma not_Trichotomous_Rand :
  exists (A : Type) (R S : rel A),
    Trichotomous R /\ Trichotomous S /\ ~ Trichotomous (Rand R S).

Class Connected {A : Type} (R : rel A) : Prop :=
{
  connected : forall x y : A, ~ R x y /\ ~ R y x -> x = y;
}.

#[export]
Instance Connected_Total :
  forall (A : Type) (R : rel A),
    Total R -> Connected R.

#[export]
Instance Connected_Empty :
  forall R : rel Empty_set, Connected R.

#[export]
Instance Connected_unit :
  forall R : rel unit, Connected R.

#[export]
Instance Connected_RTrue :
  forall A : Type,
    Connected (@RTrue A A).

Lemma not_Connected_RFalse_two_elems :
  forall {A : Type} {x y : A},
    x <> y -> ~ Connected (@RFalse A A).

#[export]
Instance Connected_Rinv :
  forall (A : Type) (R : rel A),
    Connected R -> Connected (Rinv R).

Lemma not_Connected_Rcomp :
  exists (A : Type) (R S : rel A),
    Connected R /\ Connected S /\ ~ Connected (Rcomp R S).

Lemma not_Connected_Rnot :
  exists (A : Type) (R : rel A),
    Connected R /\ ~ Connected (Rnot R).

#[export]
Instance Connected_Ror :
  forall (A : Type) (R S : rel A),
    Connected R -> Connected S ->
      Connected (Ror R S).

Lemma not_Connected_Rand :
  exists (A : Type) (R S : rel A),
    Connected R
      /\
    Connected S
      /\
    ~ Connected (Rand R S).

Class WeaklyTotal {A : Type} (R : rel A) : Prop :=
{
  weakly_total : forall x y : A, ~ R x y -> R y x
}.

#[export]
Instance WeaklyTotal_RTrue :
  forall A : Type,
    WeaklyTotal (@RTrue A A).

Lemma WeaklyTotal_Empty :
  forall R : rel Empty_set, WeaklyTotal R.

Lemma not_WeaklyTotal_RFalse_inhabited :
  forall A : Type,
    A -> ~ WeaklyTotal (@RFalse A A).

Lemma WeaklyTotal_eq_Empty :
  WeaklyTotal (@eq Empty_set).

Lemma WeaklyTotal_eq_unit :
  WeaklyTotal (@eq unit).

Lemma not_WeaklyTotal_eq_two_elems :
  forall {A : Type} {x y : A},
    x <> y -> ~ WeaklyTotal (@eq A).

#[export]
Instance WeaklyTotal_Rinv :
  forall (A : Type) (R : rel A),
    WeaklyTotal R -> WeaklyTotal (Rinv R).

#[export]
Instance WeaklyTotal_Rcomp :
  forall (A : Type) (R S : rel A),
    WeaklyTotal R -> WeaklyTotal S -> WeaklyTotal (Rcomp R S).

Lemma not_WeaklyTotal_Rnot :
  exists (A : Type) (R : rel A),
    WeaklyTotal R /\ ~ WeaklyTotal (Rnot R).

#[export]
Instance WeaklyTotal_Ror :
  forall (A : Type) (R S : rel A),
    WeaklyTotal R -> WeaklyTotal S -> WeaklyTotal (Ror R S).

Lemma not_WeaklyTotal_Rand :
  exists (A : Type) (R S : rel A),
    WeaklyTotal R /\ WeaklyTotal S /\ ~ WeaklyTotal (Rand R S).

Lemma not_Antireflexive_WeaklyTotal_inhabited :
  forall (A : Type) (R : rel A) (x : A),
    WeaklyTotal R -> ~ Antireflexive R.

Class WeaklyTrichotomous {A : Type} (R : rel A) : Prop :=
{
  weakly_trichotomous : forall x y : A, x <> y -> R x y \/ R y x
}.

#[export]
Instance WeaklyTrichotomous_Total :
  forall (A : Type) (R : rel A),
    Total R -> WeaklyTrichotomous R.

#[export]
Instance WeaklyTrichotomous_Empty :
  forall R : rel Empty_set, WeaklyTrichotomous R.

#[export]
Instance WeaklyTrichotomous_unit :
  forall R : rel unit, WeaklyTrichotomous R.

#[export]
Instance WeaklyTrichotomous_RTrue :
  forall A : Type,
    WeaklyTrichotomous (@RTrue A A).

Lemma not_WeaklyTrichotomous_RFalse_two_elems :
  forall {A : Type} {x y : A},
    x <> y -> ~ WeaklyTrichotomous (@RFalse A A).

#[export]
Instance WeaklyTrichotomous_Rinv :
  forall (A : Type) (R : rel A),
    WeaklyTrichotomous R -> WeaklyTrichotomous (Rinv R).

Lemma not_WeaklyTrichotomous_Rcomp :
  exists (A : Type) (R S : rel A),
    WeaklyTrichotomous R /\ WeaklyTrichotomous S /\ ~ WeaklyTrichotomous (Rcomp R S).

Lemma not_WeaklyTrichotomous_Rnot :
  exists (A : Type) (R : rel A),
    WeaklyTrichotomous R /\ ~ WeaklyTrichotomous (Rnot R).

#[export]
Instance WeaklyTrichotomous_Ror :
  forall (A : Type) (R S : rel A),
    WeaklyTrichotomous R -> WeaklyTrichotomous S -> WeaklyTrichotomous (Ror R S).

Lemma not_WeaklyTrichotomous_Rand :
  exists (A : Type) (R S : rel A),
    WeaklyTrichotomous R /\ WeaklyTrichotomous S /\ ~ WeaklyTrichotomous (Rand R S).

Class StrictPreorder {A : Type} (R : rel A) : Prop :=
{
  StrictPreorder_Antireflexive :> Antireflexive R;
  StrictPreorder_CoTransitive :> CoTransitive R;
}.

Class StrictPartialOrder {A : Type} (R : rel A) : Prop :=
{
  StrictPartialOrder_Preorder :> StrictPreorder R;
  StrictPartialOrder_Antisymmetric :> Antisymmetric R;
}.

Class StrictTotalOrder {A : Type} (R : rel A) : Prop :=
{
  StrictTotalOrder_PartialOrder :> StrictPartialOrder R;
  StrictTotalOrder_Connected : Connected R;
}.

Class Quasiorder {A : Type} (R : rel A) : Prop :=
{
  Quasiorder_Antireflexive :> Antireflexive R;
  Quasiorder_Transitive :> Transitive R;
}.