Library denumerable.GRelations
Require Import Ensembles.
Require Import PartialFun.
Section General_Relations.
Section Definitions.
Variables A B : Type.
domain
Variable DA : Ensemble A.
codomain
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.
Implicit Arguments rel_injection [A B].
Implicit 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).
Proof.
split.
intros b a _ a_R_inv_b.
repeat red in a_R_inv_b.
destruct a_R_inv_b as (a_In_DA, _, _).
assumption.
intros b a a' _ b_Rf_a b_Rf_a'.
destruct R_inj as (_, _, R_injec).
destruct b_Rf_a as (a_In_DA, (_, a_R_b));
destruct b_Rf_a' as (a'_In_DA, (_, a'_R_b));
apply R_injec with b; assumption.
intros a a_In_DB.
destruct R_inj as (R_domain, R_codomain, _).
elim (R_domain a a_In_DB).
intros x a_R_x.
exists x.
split.
apply R_codomain with a; assumption.
repeat split; [idtac | apply R_codomain with a | idtac]; assumption.
Qed.
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).
Proof.
split.
intros b b_In_DB.
destruct R_surj as (R_codomain, _, R_surjec).
elim (R_surjec b b_In_DB).
intros x (x_In_DA, x_R_b).
exists x.
repeat split; [idtac | apply R_codomain with x | idtac]; assumption.
intros b a b_in_DB b_R_inv_a.
destruct b_R_inv_a as (a_In_DA, _).
assumption.
intros b b' a b_in_DB b'_in_DB b_Ri_a b'_Ri_a.
destruct R_surj as (_, R_fun, _).
red in R_fun.
apply R_fun with a.
destruct b_Ri_a as (a_In_DA); assumption.
destruct b_Ri_a as (_, (_, a_R_b)); assumption.
destruct b'_Ri_a as (_, (_, a_R_b')); assumption.
Qed.
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 /\ (forall p, R x p -> n <= p).
Require Import Le.
Lemma R_nat_elaguee_fun :
rel_functional DA R_nat_elaguee.
Proof.
intros a b b' aInDA a_Re_b a_Re_b'.
destruct a_Re_b; destruct a_Re_b'.
apply le_antisym.
apply (H0 b'); assumption.
apply (H2 b); assumption.
Qed.
Require Import Classical.
Require Import Omega.
Lemma R_nat_elaguee_domain :
forall y n, R y n -> exists p, R_nat_elaguee y p.
Proof.
assert (forall (n : nat) (y : A), (exists q:nat, q <= n /\ R y q) ->
exists p : nat, R_nat_elaguee y p).
induction n.
intros y (q,(H1,H2)).
exists 0.
split; auto with arith.
inversion H1.
subst q; auto.
intros y (q,(H1,H2)).
case (classic (exists r, r <= n /\ R y r)).
intro H';case (IHn y H').
intros;exists x;auto.
exists q.
split.
auto.
intros.
case (le_lt_dec q p).
auto.
intro.
case H.
exists p.
split;auto with arith.
omega.
intros.
eapply H with n.
exists n;auto with arith.
Qed.
End to_nat_elagage.
End elagage.
End General_Relations.