proposition: Lemma rwr_list_expand_strong : forall A R (l l' : list A), trans_clos (one_step_list R) l' l <-> exists t, exists t', exists l1, exists l2, exists l2', l = l1 ++ t :: l2 /\ l' = l1 ++ t' :: l2' /\ trans_clos R t' t /\ refl_trans_clos (one_step_list R) l2' l2.
proof: Proof. intros A R l l'; split; intro H. induction H as [l l' H | l l' l'' H H']. destruct (one_step_in_list H) as [t [t' [l1 [l2 [H1 [H2 H3]]]]]]. exists t; exists t'; exists l1; exists l2; exists l2; split; [assumption | split; [assumption | split]]. left; assumption. left. destruct (one_step_in_list H) as [t [t' [l1 [l2 [H1 [H2 H3]]]]]]. destruct IHH' as [u [u' [k1 [k2 [k2' [K1 [K2 [K3 K4]]]]]]]]. rewrite K2 in H2. destruct (in_in_split_set _ _ _ _ _ _ H2) as [[[k [J1 J2]] | [k [J1 J2]]] | [k [J1 J2]]]; subst. exists t; exists t'; exists l1; exists (k ++ u :: k2); exists (k ++ u' :: k2'); split; [idtac | split; [idtac | split]]. rewrite <- ass_app; apply eq_refl. apply eq_refl. left; assumption. apply rwr_list_chop with (l1 ++ t :: nil) (l1 ++ t :: nil); trivial. do 2 rewrite <- ass_app in H'; simpl in H; do 2 rewrite <- ass_app; simpl; trivial. exists u; exists u'; exists k1; exists k2; exists (k ++ t' :: l2); split; [idtac | split; [idtac | split]]. apply eq_refl. rewrite <- ass_app; apply eq_refl. assumption. apply refl_trans_clos_is_trans with (k ++ t :: l2); trivial. right; left. revert H1; clear; intro H1; induction k as [ | a k]. left; assumption. right; assumption. exists u; exists t'; exists l1; exists k2; exists l2; split; [idtac | split; [idtac | split]]. apply eq_refl. apply eq_refl. apply trans_clos_is_trans with t; trivial. left; assumption. assumption. destruct H as [t [t' [l1 [l2 [l2' [H1 [H2 [H3 H4]]]]]]]]. assert (H5 : trans_clos (one_step_list R) (l1 ++ t' :: l2) (l1 ++ t :: l2)). clear H4; subst; induction H3 as [t1 t2 H | t1 t2 t3 H1 H2]. left; induction l1 as [ | a l1]; [left | right]; assumption. apply trans_clos_is_trans with (l1 ++ t2 :: l2); trivial. revert H1; clear; left; induction l1 as [ | a l1]; [left | right]; assumption. inversion H4 as [k2 | k3 k2 H]; clear H4; subst. assumption. apply trans_clos_is_trans with (l1 ++ t' :: l2); trivial. revert H. replace (l1 ++ t' :: l2) with ((l1 ++ t' :: nil) ++ l2). replace (l1 ++ t' :: l2') with ((l1 ++ t' :: nil) ++ l2'). generalize (l1 ++ t' :: nil); clear. intros l; revert l2 l2'; induction l as [ | a l]; intros l2 l2' H; trivial. generalize (IHl _ _ H); simpl; generalize (l ++ l2') (l ++ l2); clear. intros l1 l2 H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. apply trans_clos_is_trans with (a :: l2); trivial. left; right; assumption. rewrite <- ass_app; simpl; apply eq_refl. rewrite <- ass_app; simpl; apply eq_refl. Qed.
imports: Coq(Setoid Relations List Wellfounded)