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.