Library ac_matching.cf_eq_ac

``` Add LoadPath "basis". Add LoadPath "list_extensions". Add LoadPath "term_algebra". Add LoadPath "term_orderings". Require Import Arith. Require Import List. Require Import closure. Require Import more_list. Require Import list_sort. Require Import term. Require Import ac. Set Implicit Arguments. Module Type S. Declare Module Import Ac : ac.S. Import Ac.EqTh.T. Axiom cf_eq_ac :   forall t1 t2, well_formed t1 -> well_formed t2 ->   canonical_form t1 = canonical_form t2 -> ac t1 t2. End S. Module Make (Ac1 : ac.S) <: S with Module Ac := Ac1. Module Import Ac := Ac1. Import EqTh. Import Sort. Import LPermut. Import T. Import F. Import X. 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. 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 plus_comm; intro; discriminate. intros g l IHl l1 l2 Wt P'; simpl in P'; destruct (eq_symbol_dec f g) as [f_eq_s | f_diff_g]. subst; rewrite Af in P'; rewrite <- app_nil_end in P'. assert (P : permut (flatten g (map canonical_form l)) (l1 ++ l2)). setoid_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 _ (refl_equal t1))); assert (Wt2 := Wl t2 (or_intror _ (or_introl _ (refl_equal t2)))); elim (ac_syntactic _ _ _ _ P); intros k1 [k2 [k3 [k4 [P2 [P1 [P3 P4]]]]]]. generalize (IHl t1 (or_introl _ (refl_equal _)) k3 k4 Wt1 P1); intros [Hk3 | [Hk4 | [t11 [t12 [Wt11 [Wt12 [H1 [Q11 Q12]]]]]]]]; generalize (IHl t2 (or_intror _ (or_introl _ (refl_equal _))) 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. setoid_rewrite P1; apply permut_sym; trivial. setoid_rewrite P3; trivial. subst; right; right; exists (Term g (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. unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term g (t1 :: (Term g (t21 :: t22 :: nil) :: nil))). apply general_context; simpl; right; left; split; trivial. left; split; simpl; trivial. apply trans_clos_is_trans with (Term g (t1 :: Term g (t22 :: t21 :: nil) :: nil)). apply general_context; simpl; right; left; trivial. split; simpl; trivial; left; split; trivial. apply comm; right; trivial. apply r_assoc; trivial. setoid_rewrite P4; setoid_rewrite <- P1; setoid_rewrite <- Q22; rewrite <- flatten_app; transitivity (flatten g ((canonical_form t1 :: nil) ++ canonical_form t22 :: nil)). simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g]; [idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. apply list_permut_flatten; apply list_permut_app_app. setoid_rewrite P3; rewrite <- app_nil_end; trivial. right; right; exists t2; exists t1; subst; intuition. apply comm; right; trivial. setoid_rewrite P4; setoid_rewrite P2; rewrite <- app_nil_end; apply permut_refl. setoid_rewrite P1; setoid_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 g (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, rwr; apply trans_clos_is_trans with (Term g (t1 :: (Term g (t21 :: t22 :: nil) :: nil))). apply general_context; simpl; right; left; split; trivial. left; split; simpl; trivial. apply trans_clos_is_trans with (Term g (Term g (t1 :: t21 :: nil) :: t22 :: nil)). apply r_assoc; trivial. apply comm; right; trivial. setoid_rewrite P4; setoid_rewrite <- Q22; rewrite <- app_nil_end; auto. transitivity (flatten g ((canonical_form t1 :: nil) ++ canonical_form t21 :: nil)). simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g]; [idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. setoid_rewrite P3; rewrite <- app_nil_end in P1; setoid_rewrite <- P1; setoid_rewrite <- Q21; rewrite flatten_app; apply list_permut_app_app. subst; right; right; exists (Term g (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, rwr; apply trans_clos_is_trans with (Term g (Term g (t11 :: t12 :: nil) :: t2 :: nil)). apply general_context; simpl; left; split; trivial. apply trans_clos_is_trans with (Term g (t11 :: (Term g (t12 :: t2 :: nil)) :: nil)). apply l_assoc; trivial. apply comm; right; trivial. setoid_rewrite P4; setoid_rewrite <- P2; setoid_rewrite <- Q12; transitivity (flatten g ((canonical_form t12 :: nil) ++ canonical_form t2 :: nil)). simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g]; [idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. rewrite flatten_app; apply list_permut_app_app. setoid_rewrite P3; trivial. subst; right; right; exists t12; exists (Term g (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, rwr; apply trans_clos_is_trans with (Term g (Term g (t11 :: t12 :: nil) :: t2 :: nil)). apply general_context; simpl; left; split; trivial. apply trans_clos_is_trans with (Term g (Term g (t12 :: t11 :: nil) :: t2 :: nil)). apply general_context; simpl; left; split; trivial; apply comm; right; trivial. apply l_assoc; trivial. setoid_rewrite P4; auto. setoid_rewrite P3; rewrite <- app_nil_end in P2; setoid_rewrite <- P2; setoid_rewrite <- Q11; transitivity (flatten g ((canonical_form t11 :: nil) ++ canonical_form t2 :: nil)). simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g]; [idtac | absurd (g=g); trivial]; 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 g (t12 :: t22 :: nil)); exists (Term g (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. unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term g (Term g (t11 :: t12 :: nil) :: (Term g (t21 :: t22 :: nil)) :: nil)). apply general_context; simpl; right; right; split; trivial. left; split; trivial. apply trans_clos_is_trans with (Term g (t11 :: (Term g (t12 :: (Term g (t21 :: t22 :: nil)) :: nil)) :: nil)). apply l_assoc; trivial. apply trans_clos_is_trans with (Term g (t11 :: (Term g (Term g (t12 :: t21 :: nil) :: t22 :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial. apply r_assoc; trivial. apply trans_clos_is_trans with (Term g (t11 :: (Term g (Term g (t21 :: t12 :: nil) :: t22 :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial. apply general_context; simpl; left; split; trivial. apply comm; trivial; right; trivial. apply trans_clos_is_trans with (Term g (t11 :: (Term g (t21 :: (Term g (t12 :: t22 :: nil)) :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial. apply l_assoc; trivial. apply trans_clos_is_trans with (Term g (Term g (t11:: t21 :: nil) :: Term g (t12 :: t22 :: nil) :: nil)). apply r_assoc; trivial. apply comm; right; trivial. setoid_rewrite P4; setoid_rewrite <- Q12; setoid_rewrite <- Q22. transitivity (flatten g (canonical_form t12 :: nil) ++ flatten g (canonical_form t22 :: nil)). rewrite <- flatten_app; simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g]; [idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end; apply quick_permut_bis; apply permut_refl. apply list_permut_app_app. setoid_rewrite P3; setoid_rewrite <- Q11; setoid_rewrite <- Q21. transitivity (flatten g (canonical_form t11 :: nil) ++ flatten g (canonical_form t21 :: nil)). rewrite <- flatten_app; simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g]; [idtac | absurd (g=g); trivial]; 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 plus_comm in Ll; simpl in Ll; discriminate. Qed. Lemma syntactic_dec :   forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->                    well_formed t2 ->                    canonical_form t1 = canonical_form t2 -> ac t1 t2) ->   forall f, arity f = AC -> forall a1 a2 a3 a4,   size a1 <= n -> well_formed a1 ->   size a2 <= n -> well_formed a2 ->   well_formed a3 -> well_formed a4 ->   forall k1 k4,   permut (flatten f (canonical_form a1 :: nil)) k1 ->   permut (flatten f (canonical_form a2 :: nil)) k4 ->   permut (flatten f (canonical_form a3 :: nil)) k1->   permut (flatten f (canonical_form a4 :: nil)) k4 ->   ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil)). Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Wa3 Wa4 k1 k4 P1 P2 P3 P4; unfold ac, th_eq; apply general_context; simpl. right; right; split. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P1; setoid_rewrite P3; auto. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P2; setoid_rewrite P4; auto. Qed. Lemma commutativity :  forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->                    well_formed t2 ->                    canonical_form t1 = canonical_form t2 -> ac t1 t2) ->  forall f, arity f = AC -> forall a1 a2 a3 a4,   size a1 <= n -> well_formed a1 ->   size a2 <= n -> well_formed a2 ->   well_formed a3 -> well_formed a4 ->   forall k2 k3,   permut (flatten f (canonical_form a1 :: nil)) k2 ->   permut (flatten f (canonical_form a2 :: nil)) k3 ->   permut (flatten f (canonical_form a3 :: nil)) k3 ->   permut (flatten f (canonical_form a4 :: nil)) k2 ->  ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil)). Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Wa3 Wa4 k2 k3 P1 P2 P3 P4; unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f (a2 :: a1 :: nil)). apply comm; right; trivial. apply general_context; simpl; right; right; split. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P2; setoid_rewrite P3; auto. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P1; setoid_rewrite P4; auto. Qed. Lemma associativity :  forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->                    well_formed t2 ->                    canonical_form t1 = canonical_form t2 -> ac t1 t2) ->  forall f, arity f = AC -> forall a1 a2 a3 a4,   size a1 <= n -> well_formed a1 ->   size a2 <= n -> well_formed a2 ->   size a3 <= n -> well_formed a3 ->   size a4 <= n -> well_formed a4 ->   forall k1 k2 k4, k1 = nil \/ k2 = nil \/ k4 = nil \/   (permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) ->    permut (flatten f (canonical_form a2 :: nil)) k4 ->    permut (flatten f (canonical_form a3 :: nil)) k1 ->    permut (flatten f (canonical_form a4 :: nil)) (k2 ++ k4) ->  ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))). Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k1 k2 k4. destruct k1 as [ | h1 k1]; [left; trivial | right]; destruct k2 as [ | h2 k2]; [left; trivial | right]; destruct k4 as [ | h4 k4]; [left; trivial | right]; intros P1 P2 P3 P4; generalize (split_cf Af _ _ _ Wa1 P1); intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]]; generalize (split_cf Af _ _ _ Wa4 P4); intros [Hk2' | [Hk4 | [t2' [t4 [Wt2' [Wt4 [H2 [Q2' Q4]]]]]]]]; subst; try discriminate. unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: t4 :: nil)). apply general_context; simpl; right; right; split; trivial. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P2; setoid_rewrite Q4; auto. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t2 :: t4 :: nil)) :: nil)). apply l_assoc; trivial. assert (Wt24 : well_formed (Term f (t2 :: t4 :: nil))). apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t2 | [u_eq_t4 | In_u_nil]]; subst; trivial; contradiction. apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split. apply IH; trivial; apply flatten_cf_cf with f; trivial. setoid_rewrite P3; setoid_rewrite Q1; auto. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial. setoid_rewrite P4; setoid_rewrite <- Q2; setoid_rewrite <- Q4. rewrite <- flatten_app; simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial]; apply quick_permut. Qed. Lemma swap_left :  forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->                    well_formed t2 ->                    canonical_form t1 = canonical_form t2 -> ac t1 t2) ->  forall f, arity f = AC -> forall a1 a2 a3 a4,   size a1 <= n -> well_formed a1 ->   size a2 <= n -> well_formed a2 ->   size a3 <= n -> well_formed a3 ->   size a4 <= n -> well_formed a4 ->   forall k2 k3 k4, k2 = nil \/ k3 = nil \/ k4 = nil \/   (permut (flatten f (canonical_form a1 :: nil)) k2 ->   permut (flatten f (canonical_form a2 :: nil)) (k3 ++ k4) ->   permut (flatten f (canonical_form a3 :: nil)) k3 ->   permut (flatten f (canonical_form a4 :: nil)) (k2 ++ k4) ->   ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))). Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k2 k3 k4. destruct k2 as [ | h2 k2]; [left; trivial | right]; destruct k3 as [ | h3 k3]; [left; trivial | right]; destruct k4 as [ | h4 k4]; [left; trivial | right]; intros P1 P2 P3 P4; generalize (split_cf Af _ _ _ Wa2 P2); intros [Hk1 | [Hk2 | [t3 [t4 [Wt3 [Wt4 [H2 [Q3 Q4]]]]]]]]; generalize (split_cf Af _ _ _ Wa4 P4); intros [Hk2' | [Hk4 | [t2' [t4' [Wt2' [Wt4' [H4 [Q2' Q4']]]]]]]]; subst; try discriminate. unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f (t2' :: (Term f (t3 :: t4 :: nil)) :: nil)). apply general_context; simpl; right; right; split. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P1; setoid_rewrite Q2'; auto. left; split; trivial. apply trans_clos_is_trans with (Term f ((Term f (t2' :: t3 :: nil)) :: t4 :: nil)). apply r_assoc; trivial. apply trans_clos_is_trans with (Term f ((Term f (t3 :: t2' :: nil)) :: t4 :: nil)). apply general_context; simpl; left; split; trivial. apply comm; trivial; right; trivial. apply trans_clos_is_trans with (Term f (t3 :: (Term f (t2' :: t4 :: nil)) :: nil)). apply l_assoc; trivial. assert (Wt24 : well_formed (Term f (t2' :: t4 :: nil))). apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t2' | [u_eq_t4 | In_u_nil]]; subst; trivial; contradiction. apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split. apply IH; trivial; apply flatten_cf_cf with f; trivial. setoid_rewrite P3; setoid_rewrite Q3; auto. left; split; trivial; apply IH; trivial; apply flatten_cf_cf with f; trivial. setoid_rewrite P4; setoid_rewrite <- Q2'; setoid_rewrite <- Q4; rewrite <- flatten_app; simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial]; apply quick_permut. Qed. Lemma swap_right :  forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->                    well_formed t2 ->                    canonical_form t1 = canonical_form t2 -> ac t1 t2) ->  forall f, arity f = AC -> forall a1 a2 a3 a4,   size a1 <= n -> well_formed a1 ->   size a2 <= n -> well_formed a2 ->   size a3 <= n -> well_formed a3 ->   size a4 <= n -> well_formed a4 ->   forall k1 k2 k3, k1 = nil \/ k2 = nil \/ k3 = nil \/   (permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) ->   permut (flatten f (canonical_form a2 :: nil)) k3 ->   permut (flatten f (canonical_form a3 :: nil)) (k1 ++ k3) ->   permut (flatten f (canonical_form a4 :: nil)) k2 ->   ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))). Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k1 k2 k3. destruct k1 as [ | h1 k1]; [left; trivial | right]; destruct k2 as [ | h2 k2]; [left; trivial | right]; destruct k3 as [ | h3 k3]; [left; trivial | right]; intros P1 P2 P3 P4; generalize (split_cf Af _ _ _ Wa1 P1); intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]]; generalize (split_cf Af _ _ _ Wa3 P3); intros [Hk1' | [Hk3 | [t1' [t3 [Wt1' [Wt3 [H3 [Q1' Q3]]]]]]]]; subst; try discriminate. unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: t3 :: nil)). apply general_context; simpl; right; right; split; trivial. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P2; setoid_rewrite Q3; auto. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil)). apply l_assoc; trivial. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t3 :: t2 :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial; apply comm; right; trivial. apply trans_clos_is_trans with (Term f ((Term f (t1 :: t3 :: nil)) :: t2 :: nil)). apply r_assoc; trivial. assert (Wt13 : well_formed (Term f (t1 :: t3 :: nil))). apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t1 | [u_eq_t3 | In_u_nil]]; subst; trivial; contradiction. apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split. apply IH; trivial; apply flatten_cf_cf with f; trivial. setoid_rewrite P3; setoid_rewrite <- Q1; setoid_rewrite <- Q3. rewrite <- flatten_app; simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial]; apply quick_permut. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial. setoid_rewrite P4; setoid_rewrite Q2; auto. Qed. Lemma middle_commutativity :  forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->                    well_formed t2 ->                    canonical_form t1 = canonical_form t2 -> ac t1 t2) ->  forall f, arity f = AC -> forall a1 a2 a3 a4,   size a1 <= n -> well_formed a1 ->   size a2 <= n -> well_formed a2 ->   size a3 <= n -> well_formed a3 ->   size a4 <= n -> well_formed a4 ->   forall k1 k2 k3 k4, k1 = nil \/ k2 = nil \/ k3 = nil \/ k4 = nil \/   (permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) ->    permut (flatten f (canonical_form a2 :: nil)) (k3 ++ k4) ->    permut (flatten f (canonical_form a3 :: nil)) (k1 ++ k3) ->    permut (flatten f (canonical_form a4 :: nil)) (k2 ++ k4) ->    ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))). Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k1 k2 k3 k4. destruct k1 as [ | h1 k1]; [left; trivial | right]; destruct k2 as [ | h2 k2]; [left; trivial | right]; destruct k3 as [ | h3 k3]; [left; trivial | right]; destruct k4 as [ | h4 k4]; [left; trivial | right]; intros P1 P2 P3 P4; generalize (split_cf Af _ _ _ Wa1 P1); intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]]; generalize (split_cf Af _ _ _ Wa2 P2); intros [Hk3 | [Hk4 | [t3 [t4 [Wt3 [Wt4 [H2 [Q3 Q4]]]]]]]]; generalize (split_cf Af _ _ _ Wa3 P3); intros [Hk1' | [Hk3' | [t1' [t3' [Wt1' [Wt3' [H3 [Q1' Q3']]]]]]]]; generalize (split_cf Af _ _ _ Wa4 P4); intros [Hk2' | [Hk4' | [t2' [t4' [Wt2' [Wt4' [H4 [Q2' Q4']]]]]]]]; subst; try discriminate. unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: (Term f (t3 :: t4 :: nil)) :: nil)). apply general_context; simpl; right; right; split; trivial. left; split; trivial. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t2 :: (Term f (t3 :: t4 :: nil)) :: nil)) :: nil)). apply l_assoc; trivial. apply trans_clos_is_trans with (Term f (t1 :: (Term f ((Term f (t2 :: t3 :: nil)) :: t4 :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial. apply r_assoc; trivial. apply trans_clos_is_trans with (Term f (t1 :: (Term f ((Term f (t3 :: t2 :: nil)) :: t4 :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial. apply general_context; simpl; left; split; trivial. apply comm; right; trivial. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t3 :: (Term f (t2 :: t4 :: nil)) :: nil)) :: nil)). apply general_context; simpl; right; left; split; trivial. left; split; trivial. apply l_assoc; trivial. apply trans_clos_is_trans with (Term f ((Term f (t1 :: t3 :: nil)) :: (Term f (t2 :: t4 :: nil)) :: nil)). apply r_assoc; trivial. apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split. assert (Wt13 : well_formed (Term f (t1 :: t3 :: nil))). apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t1 | [u_eq_t3 | In_u_nil]]; subst; trivial; contradiction. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P3; setoid_rewrite <- Q1; setoid_rewrite <- Q3. rewrite <- flatten_app; simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial]; apply quick_permut. assert (Wt24 : well_formed (Term f (t2 :: t4 :: nil))). apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t2 | [u_eq_t4 | In_u_nil]]; subst; trivial; contradiction. left; split; trivial. apply IH; trivial; apply flatten_cf_cf with f; trivial; setoid_rewrite P4; setoid_rewrite <- Q2; setoid_rewrite <- Q4. rewrite <- flatten_app; simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial]; apply quick_permut. Qed. Add Morphism (length (A:=term))         with signature permut ==> (@eq nat)         as length_morph. Proof. apply list_permut.permut_length. Qed. Theorem cf_eq_ac :   forall t1 t2, well_formed t1 -> well_formed t2 ->   canonical_form t1 = canonical_form t2 -> ac t1 t2. Proof. intro t1; pattern t1; apply term_rec2; clear t1; induction n as [ | n]. intros t1 St1; absurd (1 <= 0); auto with arith; apply le_trans with (size t1); trivial; apply size_ge_one. intros [v1 | f1 l1] St1 [v2 | f l2] Wt1 Wt2 H; [simpl in H; rewrite H; unfold ac; apply th_refl | discriminate | discriminate | idtac]. assert (St2 : size (Term f l2) <= S n). rewrite size_size; trivial; rewrite <- H; rewrite <- size_size; trivial. simpl in H; injection H; clear H; intros H f1_eq_f; subst f1; destruct_arity f m Af. generalize (well_formed_unfold _ Wt1); rewrite Af; intros [Wl1 Ll1]; generalize (well_formed_unfold _ Wt2); rewrite Af; intros [Wl2 Ll2]; destruct l1 as [ | a1 l1]; [absurd (0=2); auto with arith | idtac]; destruct l1 as [ | a2 l1]; [absurd (1=2); auto with arith | idtac]; destruct l1 as [ | a3 l1]; [clear Ll1 | absurd (S(S(S(length l1)))=2); auto with arith]; destruct l2 as [ | a3 l2]; [absurd (0=2); auto with arith | idtac]; destruct l2 as [ | a4 l2]; [absurd (1=2); auto with arith | idtac]; destruct l2 as [ | a5 l2]; [clear Ll2 | absurd (S(S(S(length l2)))=2); auto with arith]; assert (Wa1 := Wl1 a1 (or_introl _ (refl_equal _))); assert (Wa2 := Wl1 a2 (or_intror _ (or_introl _ (refl_equal _)))); assert (Wa3 := Wl2 a3 (or_introl _ (refl_equal _))); assert (Wa4 := Wl2 a4 (or_intror _ (or_introl _ (refl_equal _)))); simpl in St1; rewrite plus_0_r in St1; simpl in St2; rewrite plus_0_r in St2. assert (Sa1 : size a1 <= n). apply le_trans with (size a1 + size a2); auto with arith. assert (Sa2 : size a2 <= n). apply le_trans with (size a1 + size a2); auto with arith. assert (Sa3 : size a3 <= n). apply le_trans with (size a3 + size a4); auto with arith. assert (Sa4 : size a4 <= n). apply le_trans with (size a3 + size a4); auto with arith. elim (ac_syntactic (flatten f (canonical_form a1 :: nil)) (flatten f (canonical_form a2 :: nil)) (flatten f (canonical_form a3 :: nil)) (flatten f (canonical_form a4 :: nil))). intros k1 [k2 [k3 [k4 [P1 [P2 [P3 P4]]]]]]. destruct k1 as [ | h1 k1]; destruct k4 as [ | h4 k4]. apply commutativity with n k2 k3; trivial; [rewrite <- app_nil_end in P2 | rewrite <- app_nil_end in P4]; trivial. generalize (swap_left IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k2 k3 (h4 :: k4)); intros [Hk2 | [Hk3 | [Hk4 | H']]]; subst. generalize (size_size_aux3 _ Af Wa1); setoid_rewrite P1; intro; absurd (1 <= 0); auto with arith. generalize (size_size_aux3 _ Af Wa3); setoid_rewrite P3; intro; absurd (1 <= 0); auto with arith. discriminate. apply H'; trivial. generalize (swap_right IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 (h1 :: k1) k2 k3); intros [Hk1 | [Hk2 | [Hk3 | H']]]; subst. discriminate. generalize (size_size_aux3 _ Af Wa4); setoid_rewrite P4; intro; absurd (1 <= 0); auto with arith. generalize (size_size_aux3 _ Af Wa2); setoid_rewrite P2; intro; absurd (1 <= 0); auto with arith. rewrite <- app_nil_end in P2; rewrite <- app_nil_end in P4; apply H'; trivial. destruct k2 as [ | h2 k2]; destruct k3 as [ | h3 k3]. apply (syntactic_dec IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Wa3 Wa4 P1 P2 P3 P4). generalize (associativity IHn Af _ _ _ _ Sa3 Wa3 Sa4 Wa4 Sa1 Wa1 Sa2 Wa2 (h1::k1) (h3 :: k3) (h4::k4)); intros [Hk1 | [Hk3 | [Hk4 | H']]]; subst. discriminate. discriminate. discriminate. rewrite <- app_nil_end in P1; unfold ac; apply th_sym; apply H'; trivial. generalize (associativity IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 (h1::k1) (h2 :: k2) (h4::k4)). intros [Hk1 | [Hk2 | [Hk4 | H']]]; subst. discriminate. discriminate. discriminate. rewrite <- app_nil_end in P3; unfold ac; apply H'; trivial. generalize (middle_commutativity IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 (h1 :: k1) (h2 :: k2) (h3 :: k3) (h4 :: k4)); intros [Hk1 | [Hk2 | [Hk3 | [Hk4 | H']]]]. discriminate. discriminate. discriminate. discriminate. apply H'; trivial. simpl map in H; refine (permut_trans (list_permut_app_app _ _) _); refine (permut_trans _ (list_permut_app_app _ _)); do 2 rewrite <- flatten_app; refine (permut_trans (quick_permut _) _). simpl app; rewrite H; apply quick_permut_bis; apply permut_refl. generalize (well_formed_unfold _ Wt1); rewrite Af; intros [Wl1 Ll1]; generalize (well_formed_unfold _ Wt2); rewrite Af; intros [Wl2 Ll2]; destruct l1 as [ | a1 l1]; [absurd (0=2); auto with arith | idtac]; destruct l1 as [ | a2 l1]; [absurd (1=2); auto with arith | idtac]; destruct l1 as [ | a3 l1]; [clear Ll1 | absurd (S(S(S(length l1)))=2); auto with arith]; destruct l2 as [ | a3 l2]; [absurd (0=2); auto with arith | idtac]; destruct l2 as [ | a4 l2]; [absurd (1=2); auto with arith | idtac]; destruct l2 as [ | a5 l2]; [clear Ll2 | absurd (S(S(S(length l2)))=2); auto with arith]; assert (Wa1 := Wl1 a1 (or_introl _ (refl_equal _))); assert (Wa2 := Wl1 a2 (or_intror _ (or_introl _ (refl_equal _)))); assert (Wa3 := Wl2 a3 (or_introl _ (refl_equal _))); assert (Wa4 := Wl2 a4 (or_intror _ (or_introl _ (refl_equal _)))); simpl in St1; rewrite plus_0_r in St1; simpl in St2; rewrite plus_0_r in St2. assert (Sa1 : size a1 <= n). apply le_trans with (size a1 + size a2); auto with arith. assert (Sa2 : size a2 <= n). apply le_trans with (size a1 + size a2); auto with arith. assert (Sa3 : size a3 <= n). apply le_trans with (size a3 + size a4); auto with arith. assert (Sa4 : size a4 <= n). apply le_trans with (size a3 + size a4); auto with arith. elim (@list_permut.permut_length_2 _ term (@eq term) (canonical_form a1) (canonical_form a2) (canonical_form a3) (canonical_form a4)). intros [D1 D2]; unfold ac, th_eq; apply general_context; simpl. right; right; split. apply IHn; trivial. left; split; trivial; apply IHn; trivial. intros [C1 C2]; unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f (a2 :: a1 :: nil)). apply comm; left; trivial. apply general_context; simpl; right; right; split. apply IHn; trivial; apply sym_eq; trivial. left; split; trivial; apply IHn; trivial. apply permut_trans with (quicksort (map canonical_form (a1 :: a2 :: nil))); [ apply quick_permut | rewrite H; apply quick_permut_bis; auto ]. unfold ac, th_eq; destruct (list_eq_dec eq_term_dec l1 l2) as [l1_eq_l2 | l1_diff_l2]. subst; apply th_refl. apply general_context; generalize (well_formed_unfold _ Wt1); intros [Wl1 _]; generalize (well_formed_unfold _ Wt2); intros [Wl2 _]. assert (Sl1 : forall t1, In t1 l1 -> size t1 <= n). intros t1 In_t1; apply le_S_n; apply lt_le_trans with (size (Term f l1)); trivial; apply size_direct_subterm; trivial. generalize l2 H Wl2 l1_diff_l2; clear St1 Wt1 l2 Wt2 St2 H Wl2 l1_diff_l2; induction l1 as [ | t1 l1]; intros l2 H Wl2; destruct l2 as [ | t2 l2]; simpl; trivial. intro H'; apply H'; trivial. discriminate. discriminate. intro H'; destruct (list_eq_dec eq_term_dec l1 l2) as [l1_eq_l2 | l1_diff_l2']. left; split; trivial; apply IHn. apply Sl1; left; trivial. apply Wl1; left; trivial. apply Wl2; left; trivial. inversion H; trivial. right; right; split. apply IHn.  apply Sl1; left; trivial. apply Wl1; left; trivial. apply Wl2; left; trivial. inversion H; trivial. apply IHl1; trivial. intros; apply Wl1; right; trivial. intros; apply Sl1; right; trivial. inversion H; trivial. intros; apply Wl2; right; trivial. Qed. End Make. ```