proposition: Lemma split_rel : forall dpR R (comp : term * term -> nat) (comp_approx : forall uv uv', are_connected dpR R uv uv' -> comp uv <= comp uv') (comp_def_on_dps : forall u v, comp (u,v) <> 0 <-> dpR v u) (split_graph : exists n0, forall u v, (dpR v u) <-> (exists i, i <= n0 /\ dpi comp i v u)), forall P, well_founded (rest P (rdp_step (axiom dpR) R)) <-> (forall n, well_founded (rest P (rdp_step (axiom (dpi comp n)) R))).
proof: Proof. intros dpR R comp comp_approx comp_def_on_dps split_graph P. split. intros W n; revert W; apply wf_incl; intros s t [K [As At]]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. split; [ | split; assumption]. constructor 1 with l2; trivial. rewrite <- H5; constructor. rewrite <- comp_def_on_dps. destruct n as [ | n]. destruct H3 as [ _ H3]; apply False_rect; apply H3; apply eq_refl. destruct H3 as [H3 _]; rewrite H3; discriminate. destruct split_graph as [n G]. revert comp comp_approx comp_def_on_dps G. induction n as [ | n]; intros comp comp_approx comp_def_on_dps G. intros _ t; apply Acc_intro. intros s [K [As At]]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. rewrite G in H3. destruct H3 as [ [ | i] [i_le_0 Hi]]. destruct Hi as [_ Hi]; apply False_rect; apply Hi; apply eq_refl. inversion i_le_0. intros W. destruct n as [ | n]. apply wf_incl with (rest P (rdp_step (axiom (dpi comp 1)) R)). intros s t [K [As At]]; split; [ | split; assumption]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. rewrite G in H3; destruct H3 as [[ | [ | i]] [i_le_1 [H3 i_diff_0]]]. apply False_rect; apply i_diff_0; apply eq_refl. constructor 1 with l2; trivial. rewrite <- H5; constructor. split; trivial. assert (H := le_S_n _ _ i_le_1); inversion H. apply (W 1). set (comp' := fun uv => match comp uv with 0 => 0 | S 0 => S 0 | S (S n) => S n end). apply (IHn comp'); clear IHn. intros uv uv' H; generalize (comp_approx _ _ H); unfold comp'. destruct (comp uv) as [ | [ | c]]; destruct (comp uv') as [ | [ | c']]; auto with arith. intros u v; rewrite <- (comp_def_on_dps u v). unfold comp'; destruct (comp (u,v)) as [ | [ | i]]; split; intro; (trivial || discriminate). intros u v; rewrite G; split. intros [[ | [ | i]] [i_le_n Hi]]. destruct Hi as [_ Hi]; apply False_rect; apply Hi; apply eq_refl. destruct Hi as [Hi _]; exists 1; split. apply le_n_S; apply Nat.le_0_l. split; [unfold comp'; rewrite Hi; apply eq_refl | discriminate]. exists (S i); split. apply le_S_n; assumption. split; [destruct Hi as [Hi _] | discriminate]. unfold comp'; rewrite Hi; apply eq_refl. intros [[ | i] [i_le_Sn Hi]]. destruct Hi as [_ Hi]; apply False_rect; apply Hi; apply eq_refl. destruct Hi as [Hi _]; exists (comp (u,v)); split. unfold comp' in Hi; destruct (comp (u,v)) as [ | [ | c]]; [ discriminate | apply le_n_S; apply Nat.le_0_l | injection Hi; intros; subst; apply le_n_S; assumption]. split; [apply eq_refl | unfold comp' in Hi; destruct (comp (u,v)); discriminate]. intros [ | [ | n0]]. apply wf_incl with (rest P (rdp_step (axiom (dpi comp 0)) R)). intros s t [K [As At]]; split; [ | split; assumption]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. destruct H3 as [_ i_diff_0]; apply False_rect; apply i_diff_0; apply eq_refl. apply W. apply wf_incl with (union _ (rest P (rdp_step (axiom (dpi comp 2)) R)) (rest P (rdp_step (axiom (dpi comp 1)) R))). intros s t [K [As At]]; inversion K as [f l1 l2 s' H1 H2]; subst; inversion H2 as [t1 t2 sigma H3 H4 H5]; subst; destruct H3 as [H3 _]; unfold comp' in H3. case_eq (comp (t2,t1)). intro c_eq_0; rewrite c_eq_0 in H3; discriminate. intros [ | [ | i]] c_eq_i; rewrite c_eq_i in H3. right; split; [ | split; assumption]. constructor 1 with l2; trivial. rewrite <- H5; constructor. split; [assumption | discriminate]. left; split; [ | split; assumption]. constructor 1 with l2; trivial. rewrite <- H5; constructor. split; [assumption | discriminate]. discriminate H3. clear comp'. intro a; rewrite <- (acc_union_alt _ (W 2)). intros t _; clear a. pattern t; apply (well_founded_ind (W 1)); clear t; intro t. set (R1 := rest P (rdp_step (axiom (dpi comp 1)) R)) in *. set (R2 := rest P (rdp_step (axiom (dpi comp 2)) R)) in *. intros IH1. rewrite accR2; apply Acc_intro; intros s H; rewrite <- accR2. inversion H as [a1 a3 a5 H13 H35]; clear H; subst s t. inversion H35 as [a3' a4 a5' H34 H45]; subst a3' a5'. inversion H34 as [a34 | a3' a4' K34]; clear H34. subst a3 a4. apply Acc_inv with a34; [ apply IH1 | ]; assumption. subst a3' a4'. assert (H : exists a, R2 a a4). rewrite trans_clos_trans_clos_alt in K34; inversion K34 as [a3' a4' H34 | a3' a a4' H3 H4]; clear K34; subst a3' a4'. exists a3; assumption. exists a; assumption. destruct H as [a H]; apply False_rect. destruct H45 as [H45 _]; destruct H as [H _]. inversion H45 as [f l5 l4 t4 H5 H4]; subst a4 a5; inversion H4 as [v4 u4 sigma4]; subst t4. inversion H as [g k4 l t K4 K]; subst a; inversion K as [v u sigma]; subst t. assert (C : are_connected dpR R (u,v) (u4,v4)). exists sigma4; exists sigma. split. rewrite <- comp_def_on_dps; destruct H0 as [e _]; rewrite e; discriminate. split. rewrite <- comp_def_on_dps; destruct H1 as [e _]; rewrite e; discriminate. rewrite H7; rewrite <- H3; split; trivial. generalize (comp_approx _ _ C). destruct H0 as [e _]; rewrite e. destruct H1 as [e' _]; rewrite e'. intro Abs; generalize (le_S_n _ _ Abs); clear Abs; intro Abs; inversion Abs. apply wf_incl with (rest P (rdp_step (axiom (dpi comp (S (S (S n0))))) R)). intros s t [K [As At]]; split; [ | split; assumption]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. constructor 1 with l2; trivial. rewrite <- H5; constructor. split; [ | discriminate]. destruct H3 as [H3 _]; unfold comp' in H3; destruct (comp (t2,t1)) as [ | [ | c]]. discriminate H3. discriminate H3. injection H3; intros; subst; apply eq_refl. apply W. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec)