Require Import FunctionalExtensionality Nat Arith Lia.

Require Import List.
Import ListNotations.

From Typonomikon Require Export BC2h.

Class PER {A : Type} (R : rel A) : Prop :=
{
  PER_Symmetric :> Symmetric R;
  PER_Transitive :> Transitive R;
}.

#[export]
Instance PER_Empty :
  forall R : rel Empty_set, PER R.

#[export]
Instance PER_RTrue :
  forall A : Type, PER (@RTrue A A).

#[export]
Instance PER_RFalse :
  forall A : Type, PER (@RFalse A A).

#[export]
Instance PER_eq :
  forall A : Type, PER (@eq A).

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

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

Lemma not_PER_Rnot :
  exists (A : Type) (R : rel A),
    PER R /\ ~ PER (Rnot R).

Lemma not_PER_Ror :
  exists (A : Type) (R S : rel A),
    PER R /\ PER S /\ ~ PER (Ror R S).

#[export]
Instance PER_Rand :
  forall (A : Type) (R S : rel A),
    PER R -> PER S -> PER (Rand R S).

Class Tolerance {A : Type} (R : rel A) : Prop :=
{
  Tolerance_Reflexive :> Reflexive R;
  Tolerance_Symmetric :> Symmetric R;
}.

#[export]
Instance Tolerance_Empty :
  forall R : rel Empty_set, Tolerance R.

#[export]
Instance Tolerance_RTrue :
  forall A : Type, Tolerance (@RTrue A A).

Lemma not_Tolerance_RFalse_inhabited :
  forall A : Type, A -> ~ Tolerance (@RFalse A A).

#[export]
Instance Tolerance_eq :
  forall A : Type, Tolerance (@eq A).

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

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

Lemma not_Tolerance_Rnot :
  exists (A : Type) (R : rel A),
    Tolerance R /\ ~ Tolerance (Rnot R).

#[export]
Instance Tolerance_Ror :
  forall {A : Type} (R S : rel A),
    Tolerance R -> Tolerance S -> Tolerance (Ror R S).

#[export]
Instance Tolerance_Rand :
  forall (A : Type) (R S : rel A),
    Tolerance R -> Tolerance S -> Tolerance (Rand R S).

Class CoReflexive {A : Type} (R : rel A) : Prop :=
{
  coreflexive : forall x y : A, R x y -> x = y;
}.

#[export]
Instance CoReflexive_Empty :
  forall R : rel Empty_set, CoReflexive R.

#[export]
Instance CoReflexive_RFalse :
  forall A : Type, CoReflexive (@RFalse A A).

#[export]
Instance CoReflexive_eq :
  forall A : Type, CoReflexive (@eq A).

Lemma CoReflexive_subrelation_eq :
  forall {A : Type} {R : rel A},
    CoReflexive R -> subrelation R (@eq A).

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

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

Lemma not_CoReflexive_Rnot :
  exists (A : Type) (R : rel A),
    CoReflexive R /\ ~ CoReflexive (Rnot R).

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

#[export]
Instance CoReflexive_Rand_l :
  forall (A : Type) (R S : rel A),
    CoReflexive R -> CoReflexive (Rand R S).

#[export]
Instance CoReflexive_Rand_r :
  forall (A : Type) (R S : rel A),
    CoReflexive S -> CoReflexive (Rand R S).

Class LeftQuasiReflexive {A : Type} (R : rel A) : Prop :=
  left_quasireflexive : forall x y : A, R x y -> R x x.

#[export]
Instance LeftQuasiReflexive_Empty :
  forall R : rel Empty_set, LeftQuasiReflexive R.

#[export]
Instance LeftQuasiReflexive_eq {A : Type} : LeftQuasiReflexive (@eq A).

#[export]
Instance LeftQuasiReflexive_RFalse :
  forall A : Type, LeftQuasiReflexive (@RFalse A A).

#[export]
Instance LeftQuasiReflexive_RTrue :
  forall A : Type, LeftQuasiReflexive (@RTrue A A).

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

Lemma not_LeftQuasiReflexive_Rinv :
  exists (A : Type) (R : rel A),
    LeftQuasiReflexive R /\ ~ LeftQuasiReflexive (Rinv R).

#[export]
Instance LeftQuasiReflexive_Rand :
  forall (A : Type) (R S : rel A),
    LeftQuasiReflexive R -> LeftQuasiReflexive S -> LeftQuasiReflexive (Rand R S).

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

Class RightQuasiReflexive {A : Type} (R : rel A) : Prop :=
  right_quasireflexive : forall x y : A, R x y -> R y y.

Lemma RightQuasiReflexive_spec :
  forall {A : Type} (R : rel A),
    RightQuasiReflexive R <-> LeftQuasiReflexive (Rinv R).

Class QuasiReflexive {A : Type} (R : rel A) : Prop :=
{
  QR_LeftQuasiReflexive :> LeftQuasiReflexive R;
  QR_RightQuasiReflexive :> RightQuasiReflexive R;
}.

#[export]
Instance LeftQuasiReflexive_Rinv :
  forall {A : Type} (R : rel A),
    RightQuasiReflexive R -> LeftQuasiReflexive (Rinv R).

#[export]
Instance QuasiReflexive_Empty :
  forall R : rel Empty_set, QuasiReflexive R.

#[export]
Instance QuasiReflexive_eq {A : Type} : QuasiReflexive (@eq A).

#[export]
Instance QuasiReflexive_RFalse :
  forall A : Type, QuasiReflexive (@RFalse A A).

#[export]
Instance QuasiReflexive_RTrue :
  forall A : Type, QuasiReflexive (@RTrue A A).

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

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

#[export]
Instance QuasiReflexive_Rand :
  forall (A : Type) (R S : rel A),
    QuasiReflexive R -> QuasiReflexive S -> QuasiReflexive (Rand R S).

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

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

#[export]
Instance Antitransitive_Empty :
  forall R : rel Empty_set, Antitransitive R.

Lemma not_Antitransitive_RTrue_inhabited :
  forall A : Type, A -> ~ Antitransitive (@RTrue A A).

#[export]
Instance Antitransitive_RFalse :
  forall A : Type, Antitransitive (@RFalse A A).

Lemma not_Antitransitive_eq_inhabited :
  forall A : Type, A -> ~ Antitransitive (@eq A).

#[export]
Instance Antitransitive_successor :
  Antitransitive (fun x y => y = S x).

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

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

Lemma not_Antitransitive_Rnot :
  exists (A : Type) (R : rel A),
    Antitransitive R /\ ~ Antitransitive (Rnot R).

Lemma not_Antitransitive_Ror :
  exists (A : Type) (R S : rel A),
    Antitransitive R /\ Antitransitive S /\ ~ Antitransitive (Ror R S).

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

Definition SymmetricPart {A : Type} (R : rel A) : rel A :=
  fun x y : A => R x y /\ R y x.

Definition AsymmetricPart {A : Type} (R : rel A) : rel A :=
  fun x y : A => R x y /\ ~ R y x.

Class Quasitransitive {A : Type} (R : rel A) : Prop :=
  quasitransitive :> Transitive (AsymmetricPart R).

#[export]
Instance Symmetric_SymmetricPart :
  forall {A : Type} (R : rel A),
    Symmetric (SymmetricPart R).

#[export]
Instance Quasitransitive_Symmetric :
  forall {A : Type} (R : rel A),
    Symmetric R -> Quasitransitive R.

#[export]
Instance Quasitransitive_Transitive :
  forall {A : Type} (R : rel A),
    Transitive R -> Quasitransitive R.

Lemma Quasitransitive_char :
  forall {A : Type} (R : rel A),
    Quasitransitive R <-> (R <--> Ror (SymmetricPart R) (AsymmetricPart R)).

#[export]
Instance Quasitransitive_Empty :
  forall R : rel Empty_set, Quasitransitive R.

#[export]
Instance Quasitransitive_RTrue :
  forall A : Type, Quasitransitive (@RTrue A A).

#[export]
Instance Quasitransitive_RFalse :
  forall A : Type, Quasitransitive (@RFalse A A).

Lemma Quasitransitive_eq :
  forall A : Type, Quasitransitive (@eq A).

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

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

#[export]
Instance Quasitransitive_Rnot :
  forall {A : Type} (R : rel A),
    Quasitransitive R -> Quasitransitive (Rnot R).

#[export]
Instance Quasitransitive_Rnot_conv :
  forall {A : Type} (R : rel A),
    Quasitransitive (Rnot R) -> Quasitransitive R.

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

#[export]
Instance Quasitransitive_Rand :
  forall {A : Type} (R S : rel A),
    Quasitransitive R -> Quasitransitive S -> Quasitransitive (Rand R S).

Class Circular {A : Type} (R : rel A) : Prop :=
{
  circular : forall x y z : A, R x y -> R y z -> R z x;
}.

#[export]
Instance Circular_Empty :
  forall R : rel Empty_set, Circular R.

#[export]
Instance Circular_RTrue :
  forall A : Type, Circular (@RTrue A A).

#[export]
Instance Circular_RFalse :
  forall A : Type, Circular (@RFalse A A).

#[export]
Instance Circular_eq {A : Type} : Circular (@eq A).

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

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

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

Lemma Circular_Ror :
  exists (A : Type) (R S : rel A),
    Circular R /\ Circular S /\ ~ Circular (Ror R S).

#[export]
Instance Circular_Rand :
  forall (A : Type) (R S : rel A),
    Circular R -> Circular S -> Circular (Rand R S).

Class RightEuclidean {A : Type} (R : rel A) : Prop :=
  right_euclidean : forall x y z : A, R x y -> R x z -> R y z.

#[export]
Instance RightEuclidean_Empty :
  forall R : rel Empty_set, RightEuclidean R.

#[export]
Instance RightEuclidean_eq {A : Type} : RightEuclidean (@eq A).

#[export]
Instance RightEuclidean_RFalse :
  forall A : Type, RightEuclidean (@RFalse A A).

#[export]
Instance RightEuclidean_RTrue :
  forall A : Type, RightEuclidean (@RTrue A A).

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

Lemma not_RightEuclidean_Rinv :
  exists (A : Type) (R : rel A),
    RightEuclidean R /\ ~ RightEuclidean (Rinv R).

#[export]
Instance RightEuclidean_Rand :
  forall (A : Type) (R S : rel A),
    RightEuclidean R -> RightEuclidean S -> RightEuclidean (Rand R S).

Lemma not_RightEuclidean_Ror :
  exists (A : Type) (R S : rel A),
    RightEuclidean R /\ RightEuclidean S /\ ~ RightEuclidean (Ror R S).

Class LeftEuclidean {A : Type} (R : rel A) : Prop :=
  left_euclidean : forall x y z : A, R y x -> R z x -> R y z.

Lemma RightEuclidean_Rinv :
  forall {A : Type} (R : rel A),
    RightEuclidean (Rinv R) <-> LeftEuclidean R.

Class Euclidean {A : Type} (R : rel A) : Prop :=
{
  Euclidean_RightEuclidean :> RightEuclidean R;
  Euclidean_LeftEuclidean :> LeftEuclidean R;
}.

#[export]
Instance Euclidean_Empty :
  forall R : rel Empty_set, Euclidean R.

#[export]
Instance Euclidean_eq {A : Type} : Euclidean (@eq A).

#[export]
Instance Euclidean_RFalse :
  forall A : Type, Euclidean (@RFalse A A).

#[export]
Instance Euclidean_RTrue :
  forall A : Type, Euclidean (@RTrue A A).

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

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

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

#[export]
Instance Euclidean_Rand :
  forall (A : Type) (R S : rel A),
    Euclidean R -> Euclidean S -> Euclidean (Rand R S).

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

Lemma not_Euclidean_Ror :
  exists (A : Type) (R S : rel A),
    Euclidean R /\ Euclidean S /\ ~ Euclidean (Ror R S).

#[export]
Instance Transitive_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> Transitive R.

#[export]
Instance Symmetric_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> Symmetric R.

#[export]
Instance LeftEuclidean_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> LeftEuclidean R.

#[export]
Instance RightEuclidean_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> RightEuclidean R.

#[export]
Instance Quasitransitive_LeftEuclidean :
  forall {A : Type} (R : rel A),
    LeftEuclidean R -> Quasitransitive R.

#[export]
Instance Quasitransitive_RightEuclidean :
  forall {A : Type} (R : rel A),
    RightEuclidean R -> Quasitransitive R.

#[export]
Instance LeftQuasiReflexive_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> LeftQuasiReflexive R.

#[export]
Instance RightQuasiReflexive_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> RightQuasiReflexive R.

#[export]
Instance QuasiReflexive_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> QuasiReflexive R.

#[export]
Instance LeftQuasiReflexive_Reflexive :
  forall {A : Type} (R : rel A),
    Reflexive R -> LeftQuasiReflexive R.

#[export]
Instance Dense_LeftQuasiReflexive :
  forall {A : Type} (R : rel A),
    LeftQuasiReflexive R -> Dense R.

#[export]
Instance Dense_RightQuasiReflexive :
  forall {A : Type} (R : rel A),
    RightQuasiReflexive R -> Dense R.

#[export]
Instance RightQuasiReflexive_Reflexive :
  forall {A : Type} (R : rel A),
    Reflexive R -> RightQuasiReflexive R.

#[export]
Instance QuasiReflexive_Reflexive :
  forall {A : Type} (R : rel A),
    Reflexive R -> QuasiReflexive R.

#[export]
Instance WeaklyAntisymmetric_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> WeaklyAntisymmetric R.

#[export]
Instance WeaklyAntisymmetric_Antisymmetric :
  forall {A : Type} (R : rel A),
    Antisymmetric R -> WeaklyAntisymmetric R.

#[export]
Instance Antireflexive_Antisymmetric :
  forall {A : Type} (R : rel A),
    Antisymmetric R -> Antireflexive R.

#[export]
Instance Antireflexive_Antitransitive :
  forall {A : Type} (R : rel A),
    Antitransitive R -> Antireflexive R.

#[export]
Instance Antisymmetric_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> Antisymmetric R.

#[export]
Instance CoReflexive_Symmetric_WeaklyAntisymmetric :
  forall {A : Type} (R : rel A),
    Symmetric R -> WeaklyAntisymmetric R -> CoReflexive R.

Lemma CoReflexive_spec :
  forall {A : Type} (R : rel A),
    CoReflexive R <-> Symmetric R /\ WeaklyAntisymmetric R.

Lemma eq_greatest_Symmetric_WeaklyAntisymmetric :
  forall {A : Type} (R : rel A),
    Symmetric R -> Antisymmetric R -> R --> eq.

Lemma Reflexive_Symmetric_WeaklyAntisymmetric_spec :
  forall {A : Type} (R : rel A),
    Reflexive R -> Symmetric R -> Antisymmetric R -> R <--> eq.

Lemma Symmetric_Total_spec :
  forall {A : Type} (R : rel A),
    Symmetric R -> Total R -> R <--> RTrue.

Lemma LeftEuclidean_spec :
  forall {A : Type} (R : rel A),
    LeftEuclidean R <-> forall x y z : A, R x y -> R x z -> R z y.

#[export]
Instance Equivalence_Reflexive_Circular :
  forall {A : Type} (R : rel A),
    Reflexive R -> Circular R -> Equivalence R.

#[export]
Instance CoReflexive_LeftUnique :
  forall {A : Type} (R : rel A),
    LeftUnique R -> CoReflexive (Rcomp R (Rinv R)).

#[export]
Instance LeftUnique_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> LeftUnique R.

#[export]
Instance RightUnique_CoReflexive :
  forall {A : Type} (R : rel A),
    CoReflexive R -> RightUnique R.

Inductive LeftQuasiReflexiveClosure {A : Type} (R : rel A) : rel A :=
| LQRC_step :
    forall x y : A, R x y -> LeftQuasiReflexiveClosure R x y
| LQRC_clos :
    forall x y : A, R x y -> LeftQuasiReflexiveClosure R x x.

#[export]
Instance LeftQuasiReflexive_LeftQuasiReflexiveClosure
  {A : Type} (R : rel A) : LeftQuasiReflexive (LeftQuasiReflexiveClosure R).