Library hydras.rpo.closure

Set Implicit Arguments.

From Coq Require Import Relations.

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.

Lemma acc_trans :
 ∀ (A : Set) (R : relation A) a, Acc R a → Acc (trans_clos R) a.

Lemma wf_trans :
  ∀ (A : Set) (R : relation A) , well_founded R →
                                      well_founded (trans_clos R).

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.