# Library Cantor.prelude.closure

Set Implicit Arguments.

Require Import Relations.
Require Import List.

Inductive trans_clos (A : Set) (R : relation A) : relation A:=
| t_step : x y, R x y trans_clos R x y
| t_trans : x y z, R x y trans_clos R y z trans_clos R x z.

Lemma trans_clos_is_trans :
(A :Set) (R : relation A) a b c,
trans_clos R a b trans_clos R b c trans_clos R a c.
Proof.
intros A R a b c Hab; generalize c; clear c; induction Hab as [a b Hab | a b c Hab Hbc].
intros c Hbc; apply t_trans with b; trivial.
intros d Hcd; apply t_trans with b; trivial.
apply IHHbc; trivial.
Qed.

Lemma acc_trans :
(A : Set) (R : relation A) a, Acc R a Acc (trans_clos R) a.
Proof.
intros A R a Acc_R_a.
induction Acc_R_a as [a Acc_R_a IH].
apply Acc_intro.
intros b b_Rp_a; induction b_Rp_a.
apply IH; trivial.
apply Acc_inv with y.
apply IHb_Rp_a; trivial.
apply t_step; trivial.
Qed.

Lemma wf_trans :
(A : Set) (R : relation A) , well_founded R well_founded (trans_clos R).
Proof.
unfold well_founded; intros A R WR.
intro; apply acc_trans; apply WR; trivial.
Qed.

Lemma inv_trans :
(A : Set) (R : relation A) (P : A Prop),
( a b, P a R a b P b)
a b, P a trans_clos R a b P b.
Proof.
intros A R P Inv a b Pa a_Rp_b; induction a_Rp_b.
apply Inv with x; trivial.
apply IHa_Rp_b; apply Inv with x; trivial.
Qed.