Require Import Arith Lia.

From Typonomikon Require Import BC4e.

Class WeaklyExtensional {A : Type} (R : rel A) : Prop :=
{
  weakly_extensional : forall x y : A, (forall t : A, R t x <-> R t y) -> x = y;
}.

Lemma WeaklyExtensional_lt :
  WeaklyExtensional lt.

Lemma WeaklyExtensional_le :
  WeaklyExtensional le.

Lemma WeaklyExtensional_gt :
  WeaklyExtensional gt.

Lemma WeaklyExtensional_ge :
  WeaklyExtensional ge.

Lemma not_WeaklyExtensional_RTrue :
  exists A : Type,
    ~ WeaklyExtensional (@RTrue A A).

Lemma not_WeaklyExtensional_RFalse :
  exists A : Type,
    ~ WeaklyExtensional (@RFalse A A).

Lemma WeaklyExtensional_Rid :
  forall A : Type,
    WeaklyExtensional (@eq A).

Lemma not_WeaklyExtensional_Rinv :
  exists (A : Type) (R : rel A),
    WeaklyExtensional R /\ ~ WeaklyExtensional (Rinv R).

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

Lemma not_WeaklyExtensional_Rnot :
  exists (A : Type) (R : rel A),
    WeaklyExtensional R /\ ~ WeaklyExtensional (Rnot R).

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

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

Class WellFounded {A : Type} (R : rel A) : Prop :=
  well_founded : forall x : A, Acc R x.

CoInductive Inaccessible {A : Type} (R : rel A) (x : A) : Prop :=
{
  inaccessible : exists y : A, R y x /\ Inaccessible R y
}.

Class IllFounded {A : Type} (R : rel A) : Prop :=
  ill_founded : exists x : A, Inaccessible R x.

Lemma not_IllFounded_WellFounded :
  forall {A : Type} (R : rel A),
    WellFounded R -> IllFounded R -> False.

#[export]
Instance WellFounded_Empty :
  forall R : rel Empty_set, WellFounded R.

Lemma not_IllFounded_Empty :
  forall R : rel Empty_set, ~ IllFounded R.

Lemma IllFounded_RTrue_inhabited :
  forall A : Type, A -> IllFounded (@RTrue A A).

Lemma not_WellFounded_RTrue_inhabited :
  forall A : Type, A -> ~ WellFounded (@RTrue A A).

#[export]
Instance WellFounded_RFalse :
  forall A : Type, WellFounded (@RFalse A A).

Lemma not_IllFounded_RFalse :
  forall A : Type, ~ IllFounded (@RFalse A A).

#[export]
Instance IllFounded_eq :
  forall A : Type, A -> IllFounded (@eq A).

Lemma not_WellFounded_eq :
  forall A : Type, A -> ~ WellFounded (@eq A).

#[export]
Instance WellFounded_lt :
  WellFounded lt.

#[export]
Instance IllFounded_le :
  IllFounded le.

#[export]
Instance IllFounded_ge :
  IllFounded ge.

#[export]
Instance IllFounded_gt :
  IllFounded gt.

Lemma not_WellFounded_Rinv :
  exists (A : Type) (R : rel A),
    WellFounded R /\ ~ WellFounded (Rinv R).

Lemma not_IllFounded_Rinv :
  exists (A : Type) (R : rel A),
    IllFounded R /\ ~ IllFounded (Rinv R).

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

Lemma not_WellFounded_Rcomp :
  exists (A : Type) (R S : rel A),
    WellFounded R /\ WellFounded S /\ IllFounded (Rcomp R S).

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

Lemma not_WellFounded_Rnot :
  exists (A : Type) (R : rel A),
    WellFounded R /\ ~ WellFounded (Rnot R).

Lemma not_IllFounded_Rnot :
  exists (A : Type) (R : rel A),
    IllFounded R /\ ~ IllFounded (Rnot R).

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

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

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

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

#[export] Instance Antireflexive_WellFounded
  {A : Type} {R : rel A} (WF : WellFounded R) : Antireflexive R.

Class WellOrder {A : Type} (R : rel A) : Prop :=
{
  WellOrder_Transitive :> Transitive R;
  WellOrder_WellFounded :> WellFounded R;
  WellOrder_WeaklyExtensional :> WeaklyExtensional R;
}.

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

Lemma WellOrder_not_Total :
  forall {A : Type} (R : rel A) (x : A),
    WellOrder R -> ~ Total R.