proposition: Lemma gen_monotone_afs : forall (R : relation M.term), transitive _ R -> Trel_monotone R -> Trel_monotone (fun x y => R (afs x) (afs y)).
proof: Proof. intros R HtransR HmonoR f l1 l2 H. unfold afs. simpl; destruct (afs_symb f) as [g ns]. assert (Hl : one_step_list R (map afs l1) (map afs l2)); [ induction H; [ left | right ]; assumption |]; unfold afs in Hl; set (ll1 := map (afs_term afs_symb) l1) in *; clearbody ll1; set (ll2 := map (afs_term afs_symb) l2) in *; clearbody ll2; clear l1 l2 H; revert ll1 ll2 Hl; intros l1 l2 H. cut (trans_clos (one_step_list R) (afs_filt l1 (afs_rest ns ns (length l1))) (afs_filt l2 (afs_rest ns ns (length l2)))); [ intros Htc; induction Htc; [| apply HtransR with (M.Term g y); [| assumption ]]; apply HmonoR; assumption | clear f g ]. generalize (rest_safe ns (length l1)); intros Hin. assert (Hl : length l1 = length l2); [ apply one_step_list_length_eq in H; assumption |]; rewrite <- Hl; set (l := afs_rest ns ns (length l1)) in *; clearbody l; clear ns Hl. apply one_step_in_list in H; destruct H as [s [t [lh [lt [Rts [Hs Ht]]]]]]; subst. rewrite (inter_diss s l lh lt s); rewrite (inter_diss s l lh lt t); set (f:= afs_filt (lh ++ s :: lt)); clearbody f. cut (exists m1, exists m2, exists mm, m1 :: m2 :: mm = dissect (length lh) l); [| apply dissect_in; apply Hin; rewrite app_length; simpl; pattern (length lh) at 1; rewrite <- Nat.add_0_r; apply Nat.add_lt_mono_l; apply Nat.lt_0_succ ]. set (ll := dissect (length lh) l); clearbody ll; induction ll; intros [m1 [m2 [mm Hm]]]; rewrite <- Hm; [ discriminate Hm | destruct ll; [ discriminate Hm |]]; rewrite rwr_list_expand_strong; exists s; exists t; exists (f m1); exists (intersperse s (map f (m2::mm))); exists (intersperse t (map f (m2::mm))); split; [ reflexivity |]; split; [ reflexivity |]; split; [ left; assumption |]; destruct mm; [ left | right ]; injection Hm; intros; subst; apply IHll; exists l0; exists l1; exists mm; reflexivity. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)