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.