Require Import Relations. Require Import Rstar. Set Implicit Arguments. Section starclos. Variable A : Type. Variable R : A -> A -> Prop. Inductive starclos (R:A -> A -> Prop) (a:A) : A -> Prop := | starclos_0 : starclos R a a | starclos_n_1 : forall b c:A, starclos R a b -> R b c -> starclos R a c . Lemma r_starclos : forall a b:A, R a b -> starclos R a b. Proof. intros a b; constructor 2 with a; [ constructor | assumption ]. Qed. Lemma starclos_1_n : forall a b c:A, R a b -> starclos R b c -> starclos R a c. Proof. intros a b c H H0; elim H0. apply r_starclos; auto. intros; eapply starclos_n_1; eauto. Qed. Theorem R_Rstar : forall a b:A, R a b -> Rstar _ R a b. Proof. intros a b H; unfold Rstar. intros P H0 H1. apply H1 with b; auto. Qed. Lemma starclos_trans : forall a b c:A, starclos R a b -> starclos R b c -> starclos R a c. Proof. intros a b c H; elim H. trivial. intro H1. intros c0 H2 H3 ;intros; apply H3. eapply starclos_1_n; eauto. Qed. Theorem starclos_Rstar : forall a b:A, starclos R a b -> Rstar _ R a b. Proof. intros a b H; elim H. apply Rstar_reflexive. intros b0 H0 H1 Hrec H2; eapply Rstar_transitive. eexact Hrec. apply R_Rstar; trivial. Qed. Theorem Rstar_Rstarclos : forall a b:A, Rstar _ R a b -> starclos R a b. Proof. intros a b H; apply H. constructor. apply starclos_1_n; trivial. Qed. End starclos.