# Library basis.closure

``` Set Implicit Arguments. Require Import Relations. Require Import List. Inductive trans_clos (A : Set) (R : relation A) : relation A:=   | t_step : forall x y, R x y -> trans_clos R x y   | t_trans : forall x y z, R x y -> trans_clos R y z -> trans_clos R x z. Inductive refl_trans_clos (A : Set) (R : relation A) : relation A:=   | r_trans : forall x, refl_trans_clos R x x   | t_clos : forall x y, trans_clos R x y -> refl_trans_clos R x y. Lemma trans_clos_is_trans :   forall (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 trans_clos_is_clos :   forall (A :Set) (R : relation A) a b, trans_clos (trans_clos R) a b -> trans_clos R a b. Proof. intros A R a b Hab; induction Hab as [a b Hab | a b c Hab Hbc]; trivial. apply trans_clos_is_trans with b; trivial. Qed. Lemma acc_trans :  forall (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 :   forall (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 :   forall (A : Set) (R : relation A) (P : A -> Prop),   (forall a b, P a -> R a b -> P b) ->   forall 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. Lemma trans_inversion :   forall (A : Set) (R : relation A) a b, trans_clos R a b ->   (R a b \/ (exists c, trans_clos R a c /\ R c b)). Proof. intros A R a b H; induction H as [ a b H | a b c H H' [IH | IH]]. left; trivial. right; exists b; split; trivial; apply t_step; trivial. destruct IH as [d [H'' H''']]; right; exists d; split; trivial. apply trans_clos_is_trans with b; trivial; apply t_step; trivial. Qed. Lemma incl_trans :   forall (A : Set) (R1 R2 : relation A), inclusion _ R1 R2 -> inclusion _ (trans_clos R1) (trans_clos R2). Proof. intros A R1 R2 R1_in_R2 a b H; induction H as [a' b' H | a' b' c' H1 H2]. apply t_step; apply R1_in_R2; trivial. apply t_trans with b'; trivial. apply R1_in_R2; trivial. Qed. Lemma incl_trans2 :   forall (A B : Set) (f : A -> B) (R1 : relation A) (R2 : relation B),   (forall a1 a2, R1 a1 a2 -> R2 (f a1) (f a2)) ->         forall a1 a2, trans_clos R1 a1 a2 -> trans_clos R2 (f a1) (f a2). Proof. intros A B f R1 R2 R1_in_R2 a b H; induction H as [a' b' H | a' b' c' H1 H2]. apply t_step; apply R1_in_R2; trivial. apply t_trans with (f b'); trivial. apply R1_in_R2; trivial. Qed. Inductive product_o (A B : Set) (R1 : relation A) (R2 : relation B) : relation (A*B)%type :=         | CaseA : forall a a' b, R1 a a' -> product_o R1 R2 (a,b) (a',b)         | CaseB : forall a b b', R2 b b' -> product_o R1 R2 (a,b) (a,b'). Lemma acc_and :    forall (A B : Set) (R1 : relation A) (R2 : relation B),    forall a b, Acc R1 a -> Acc R2 b -> Acc (product_o R1 R2) (a,b). Proof. intros A B R1 R2 a b Acc_a; generalize b; clear b; induction Acc_a as [a Acc_a IHa]. intros b Acc_b; generalize a Acc_a IHa; clear a Acc_a IHa; induction Acc_b as [b Acc_b IHb]; intros a Acc_a IHa; apply Acc_intro; intros [a' b'] H; inversion H; clear H; subst. apply IHa; trivial. apply Acc_intro; trivial. apply IHb; trivial. Qed. Definition nf (A : Set) (R : relation A) t := forall s, R s t -> False. Lemma acc_nf : forall (A : Set) (R : relation A) FB, (forall t s, In s (FB t) <-> R s t) ->                           forall t, Acc R t -> { s : A | nf R s /\ (s = t \/ trans_clos R s t)}. Proof. intros A R FB red_dec t Acc_t; induction Acc_t as [t Acc_t IH]. case_eq (FB t). intro H; exists t; split. intros s H'; rewrite <- red_dec in H'; rewrite H in H'; trivial. left; trivial. intros a l H; destruct (IH a) as [a' [nf_a' H']]. rewrite <- red_dec; rewrite H; left; trivial. exists a'; split; trivial. destruct H' as [a'_eq_a | H']. subst; right; apply t_step; rewrite <- red_dec; rewrite H; left; trivial. right; apply trans_clos_is_trans with a; trivial. apply t_step; rewrite <- red_dec; rewrite H; left; trivial. Qed. Lemma dec_nf : forall (A : Set) (R : relation A) FB, (forall t s, In s (FB t) <-> R s t) ->                           forall t, {nf R t}+{~nf R t}. Proof. intros A R FB red_dec t. case_eq (FB t). intro H; left; unfold nf; intros s H'; rewrite <- red_dec in H'; rewrite H in H'; contradiction. intros a l H. right; intro H'; apply H' with a. rewrite <- red_dec; rewrite H; left; trivial. Defined. Lemma cycle_not_acc : forall (A : Set) (R : relation A) (a : A), R a a -> ~Acc R a. Proof. intros A R a H Acc_a; generalize H; clear H; induction Acc_a as [a Acc_a IH]. intro H; apply (IH a); trivial. Qed. ```