proposition: Lemma split_cf : forall f, arity f = AC -> forall t u1 u2, well_formed t -> permut (flatten f (canonical_form t :: nil)) (u1 ++ u2) -> u1 = nil \/ u2 = nil \/ (exists t1, exists t2, well_formed t1 /\ well_formed t2 /\ ac t (Term f (t1 :: t2 :: nil)) /\ permut (flatten f (canonical_form t1 :: nil)) u1 /\ permut (flatten f (canonical_form t2 :: nil)) u2).
proof: Proof. intros f Af t; pattern t; apply term_rec3; clear t. intros v l1 l2 _ P; simpl in P; destruct l1 as [ | t1 l1]; [left; trivial | idtac]; destruct l2 as [ | t2 l2]; [right; left; trivial | idtac]; generalize (list_permut.permut_length P); rewrite length_app; simpl; rewrite Nat.add_comm; intro; discriminate. intros g l IHl l1 l2 Wt; simpl. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; subst g | intro f_diff_g]; intro P'. subst; rewrite Af in P'; rewrite <- app_nil_end in P'. assert (P : permut (flatten f (map canonical_form l)) (l1 ++ l2)). rewrite <- P'; apply quick_permut. clear P'; elim (well_formed_unfold Wt); rewrite Af; intros Wl Ll; destruct l as [ | t1 l]; [absurd (0=2); auto with arith | idtac]; destruct l as [ | t2 l]; [absurd (1=2); auto with arith | idtac]; destruct l as [ | t3 l]; [idtac | absurd (S(S(S(length l)))=2); auto with arith]; replace (map canonical_form (t1 :: t2 :: nil)) with ((canonical_form t1 :: nil) ++ canonical_form t2 :: nil) in P; trivial; rewrite flatten_app in P; assert (Wt1 := Wl t1 (or_introl _ (eq_refl t1))); assert (Wt2 := Wl t2 (or_intror _ (or_introl _ (eq_refl t2)))); elim (ac_syntactic _ _ _ _ P); intros k1 [k2 [k3 [k4 [P2 [P1 [P3 P4]]]]]]. generalize (IHl t1 (or_introl _ (eq_refl _)) k3 k4 Wt1 P1); intros [Hk3 | [Hk4 | [t11 [t12 [Wt11 [Wt12 [H1 [Q11 Q12]]]]]]]]; generalize (IHl t2 (or_intror _ (or_introl _ (eq_refl _))) k1 k2 Wt2 P2); intros [Hk1 | [Hk2 | [t21 [t22 [Wt21 [Wt22 [H2 [Q21 Q22]]]]]]]]. subst; right; left; apply list_permut.permut_nil with term (@eq term); trivial. subst; right; right; exists t1; exists t2; intuition. unfold ac; apply th_refl. rewrite P1; apply permut_sym; trivial. rewrite P3; trivial. subst; right; right; exists (Term f (t1 :: t22 :: nil)); exists t21; intuition. apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t1 | [u_eq_t2 | In_u_nil]]; subst; trivial; contradiction. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t21 :: t22 :: nil) :: nil))). refine (context_in _ t2 (Term f (t21 :: t22 :: nil)) _ f (t1 :: nil) nil); trivial. apply trans_clos_is_trans with (Term f (t1 :: Term f (t22 :: t21 :: nil) :: nil)). refine (context_in _ (Term f (t21 :: t22 :: nil)) (Term f (t22 :: t21 :: nil)) _ f (t1 :: nil) nil). apply comm; right; assumption. apply r_assoc; trivial. rewrite P4; rewrite <- P1; rewrite <- Q22; rewrite <- flatten_app; transitivity (flatten f ((canonical_form t1 :: nil) ++ canonical_form t22 :: nil)). simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. apply list_permut_flatten; apply list_permut_app_app. rewrite P3; rewrite <- app_nil_end; trivial. right; right; exists t2; exists t1; subst; intuition. apply comm; right; trivial. rewrite P4; rewrite P2; rewrite <- app_nil_end; apply permut_refl. rewrite P1; rewrite P3; rewrite <- app_nil_end; apply permut_refl. subst; left; apply list_permut.permut_nil with term (@eq term); trivial. subst; right; right; exists t22; exists (Term f (t1 :: t21 :: nil)); intuition. apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t1 | [u_eq_t21 | In_u_nil]]; subst; trivial; contradiction. unfold ac, th_eq; apply trans_clos_is_trans with (Term f (t1 :: (Term f (t21 :: t22 :: nil) :: nil))). refine (context_in _ t2 (Term f (t21 :: t22 :: nil)) _ f (t1 :: nil) nil); trivial. apply trans_clos_is_trans with (Term f (Term f (t1 :: t21 :: nil) :: t22 :: nil)). apply r_assoc; trivial. apply comm; right; trivial. rewrite P4; rewrite <- Q22; rewrite <- app_nil_end; auto. transitivity (flatten f ((canonical_form t1 :: nil) ++ canonical_form t21 :: nil)). simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. rewrite P3; rewrite <- app_nil_end in P1; rewrite <- P1; rewrite <- Q21; rewrite flatten_app; apply list_permut_app_app. subst; right; right; exists (Term f (t12 :: t2 :: nil)); exists t11; intuition. apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t12 | [u_eq_t2 | In_u_nil]]; subst; trivial; contradiction. unfold ac, th_eq; apply trans_clos_is_trans with (Term f (Term f (t11 :: t12 :: nil) :: t2 :: nil)). refine (context_in _ t1 (Term f (t11 :: t12 :: nil)) _ f nil (t2 :: nil)); trivial. apply trans_clos_is_trans with (Term f (t11 :: (Term f (t12 :: t2 :: nil)) :: nil)). apply l_assoc; trivial. apply comm; right; trivial. rewrite P4; rewrite <- P2; rewrite <- Q12; transitivity (flatten f ((canonical_form t12 :: nil) ++ canonical_form t2 :: nil)). simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. rewrite flatten_app; apply list_permut_app_app. rewrite P3; trivial. subst; right; right; exists t12; exists (Term f (t11 :: t2 :: nil)); intuition. apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t11 | [u_eq_t2 | In_u_nil]]; subst; trivial; contradiction. unfold ac, th_eq; apply trans_clos_is_trans with (Term f (Term f (t11 :: t12 :: nil) :: t2 :: nil)). refine (context_in _ t1 (Term f (t11 :: t12 :: nil)) _ f nil (t2 :: nil)); trivial. apply trans_clos_is_trans with (Term f (Term f (t12 :: t11 :: nil) :: t2 :: nil)). refine (context_in _ (Term f (t11 :: t12 :: nil)) (Term f (t12 :: t11 :: nil)) _ f nil (t2 :: nil)); trivial. apply comm; right; trivial. apply l_assoc; trivial. rewrite P4; auto. rewrite P3; rewrite <- app_nil_end in P2; rewrite <- P2; rewrite <- Q11; transitivity (flatten f ((canonical_form t11 :: nil) ++ canonical_form t2 :: nil)). simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. rewrite flatten_app; apply list_permut_app_app. right; right; exists (Term f (t12 :: t22 :: nil)); exists (Term f (t11 :: t21 :: nil)); intuition. apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t12 | [u_eq_t22 | In_u_nil]]; subst; trivial; contradiction. apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t11 | [u_eq_t21 | In_u_nil]]; subst; trivial; contradiction. apply trans_clos_is_trans with (Term f (Term f (t11 :: t12 :: nil) :: t2 :: nil)). refine (context_in _ _ _ _ f nil (t2 :: nil)); trivial. apply trans_clos_is_trans with (Term f (Term f (t11 :: t12 :: nil) :: (Term f (t21 :: t22 :: nil)) :: nil)). refine (context_in _ _ _ _ f (_ :: nil) nil); trivial. apply trans_clos_is_trans with (Term f (t11 :: (Term f (t12 :: (Term f (t21 :: t22 :: nil)) :: nil)) :: nil)). apply l_assoc; trivial. apply trans_clos_is_trans with (Term f (t11 :: (Term f (Term f (t12 :: t21 :: nil) :: t22 :: nil)) :: nil)). refine (context_in _ _ _ _ f (t11 :: nil) nil). apply r_assoc; trivial. apply trans_clos_is_trans with (Term f (t11 :: (Term f (Term f (t21 :: t12 :: nil) :: t22 :: nil)) :: nil)). refine (context_in _ _ _ _ f (t11 :: nil) nil). refine (context_in _ _ _ _ f nil (t22 :: nil)). apply comm; right; trivial. apply trans_clos_is_trans with (Term f (t11 :: (Term f (t21 :: (Term f (t12 :: t22 :: nil)) :: nil)) :: nil)). refine (context_in _ _ _ _ f (t11 :: nil) nil). apply l_assoc; trivial. apply trans_clos_is_trans with (Term f (Term f (t11:: t21 :: nil) :: Term f (t12 :: t22 :: nil) :: nil)). apply r_assoc; trivial. apply comm; right; trivial. rewrite P4; rewrite <- Q12; rewrite <- Q22. transitivity (flatten f (canonical_form t12 :: nil) ++ flatten f (canonical_form t22 :: nil)). rewrite <- flatten_app; simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. apply list_permut_app_app. rewrite P3; rewrite <- Q11; rewrite <- Q21. transitivity (flatten f (canonical_form t11 :: nil) ++ flatten f (canonical_form t21 :: nil)). rewrite <- flatten_app; simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. apply list_permut_app_app. assert ( Ll := list_permut.permut_length P'); clear P'; destruct l1 as [ | t1 l1]; [left; trivial | idtac]; destruct l2 as [ | t2 l2]; [right; left; trivial | idtac]; rewrite length_app in Ll; simpl in Ll; rewrite Nat.add_comm in Ll; simpl in Ll; discriminate. Qed.
imports: Coq(Setoid Arith List Morphisms) CoLoR(closure more_list weaved_relation list_sort term_spec ac)