Library hydras.Schutte.GRelations

From Coq Require Import Ensembles Classical Lia Arith.
From hydras Require Import PartialFun.

Section General_Relations.

  Section Definitions.
    Variables A B : Type.

    Variable DA : Ensemble A.

    Variable DB : Ensemble B.

    Definition GRelation := A → B → Prop.

    Variable R : GRelation.

    Inductive rel_injection : Prop :=
     rel_inj_i : rel_domain DA R →
          rel_codomain DA DB R →
          rel_inj DA R →
          rel_injection.

    Inductive rel_surjection : Prop :=
     rel_surj_i : rel_codomain DA DB R →
          rel_functional DA R →
          rel_onto DA DB R →
          rel_surjection.
  End Definitions.

 Arguments rel_injection [A B].
 Arguments rel_surjection [A B].

  Variables A B : Type.
  Variable DA : Ensemble A.
  Variable DB : Ensemble B.

  Section injection2surjection.
    Variable R : GRelation A B.
    Hypothesis R_inj : rel_injection DA DB R.

    Lemma R_inv_surj : rel_surjection DB DA (rel_inv DA DB R).

  End injection2surjection.

  Section surjection2injection.
    Variable R : GRelation A B.
    Hypothesis R_surj : rel_surjection DA DB R.

    Definition R_inv := rel_inv DA DB R.

    Lemma R_inv_inj : rel_injection DB DA (rel_inv DA DB R).
  End surjection2injection.

  Section elagage.
    Section to_nat_elagage.
      Variable R : GRelation A nat.

      Definition R_nat_elaguee (x : A) (n : nat) : Prop :=
        R x n ∧ (∀ p, R x p → n ≤ p).

      Lemma R_nat_elaguee_fun :
        rel_functional DA R_nat_elaguee.

      Lemma R_nat_elaguee_domain :
        ∀ y n, R y n → ∃ p, R_nat_elaguee y p.

    End to_nat_elagage.
  End elagage.

End General_Relations.

Arguments rel_injection {A B}.
Arguments rel_surjection {A B}.