proposition: Theorem cf_eq_ac : forall t1 t2, well_formed t1 -> well_formed t2 -> canonical_form t1 = canonical_form t2 -> ac t1 t2.
proof: Proof. intro t1; pattern t1; apply term_rec2; clear t1; induction n as [ | n]. intros t1 St1; absurd (1 <= 0); auto with arith; apply Nat.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 _ (eq_refl _))); assert (Wa2 := Wl1 a2 (or_intror _ (or_introl _ (eq_refl _)))); assert (Wa3 := Wl2 a3 (or_introl _ (eq_refl _))); assert (Wa4 := Wl2 a4 (or_intror _ (or_introl _ (eq_refl _)))); simpl in St1; rewrite Nat.add_0_r in St1; simpl in St2; rewrite Nat.add_0_r in St2. assert (Sa1 : size a1 <= n). apply Nat.le_trans with (size a1 + size a2); auto with arith. assert (Sa2 : size a2 <= n). apply Nat.le_trans with (size a1 + size a2); auto with arith. assert (Sa3 : size a3 <= n). apply Nat.le_trans with (size a3 + size a4); auto with arith. assert (Sa4 : size a4 <= n). apply Nat.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); rewrite P1; intro; absurd (1 <= 0); auto with arith. generalize (size_size_aux3 Af Wa3); 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); rewrite P4; intro; absurd (1 <= 0); auto with arith. generalize (size_size_aux3 Af Wa2); 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 _ (eq_refl _))); assert (Wa2 := Wl1 a2 (or_intror _ (or_introl _ (eq_refl _)))); assert (Wa3 := Wl2 a3 (or_introl _ (eq_refl _))); assert (Wa4 := Wl2 a4 (or_intror _ (or_introl _ (eq_refl _)))); simpl in St1; rewrite Nat.add_0_r in St1; simpl in St2; rewrite Nat.add_0_r in St2. assert (Sa1 : size a1 <= n). apply Nat.le_trans with (size a1 + size a2); auto with arith. assert (Sa2 : size a2 <= n). apply Nat.le_trans with (size a1 + size a2); auto with arith. assert (Sa3 : size a3 <= n). apply Nat.le_trans with (size a3 + size a4); auto with arith. assert (Sa4 : size a4 <= n). apply Nat.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]; apply trans_clos_is_trans with (Term f (a3 :: a2 :: nil)). refine (context_in _ _ _ _ f nil (_ :: nil)). apply IHn; trivial. refine (context_in _ _ _ _ f (_ :: nil) nil). apply IHn; trivial. intros [C1 C2]; apply trans_clos_is_trans with (Term f (a2 :: a1 :: nil)). apply comm; left; trivial. apply trans_clos_is_trans with (Term f (a3 :: a1 :: nil)). refine (context_in _ _ _ _ f nil (_ :: nil)). apply IHn; trivial; apply sym_eq; trivial. refine (context_in _ _ _ _ f (_ :: nil) nil). 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; generalize (list_eq_bool_ok _ T.eq_bool_ok l1 l2); case (list_eq_bool T.eq_bool l1 l2); [intro l1_eq_l2 | intro 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 Nat.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 False_rect; apply H'; trivial. discriminate. discriminate. assert (H'' : ac t1 t2). apply IHn. apply Sl1; left; trivial. apply Wl1; left; trivial. apply Wl2; left; trivial. inversion H; trivial. intro H'; generalize (list_eq_bool_ok _ T.eq_bool_ok l1 l2); case (list_eq_bool T.eq_bool l1 l2); [intro l1_eq_l2 | intro l1_diff_l2]. subst l2; revert H''; clear; intro H; induction H as [t1 t2 H | t1 t2 t3 H1 H2]. do 2 left; assumption. right with (t2 :: l1); trivial. left; assumption. apply trans_clos_is_trans with (t2 :: l1). revert H''; clear; intro H; induction H as [t1 t2 H | t1 t2 t3 H1 H2]. do 2 left; assumption. right with (t2 :: l1); trivial. left; assumption. clear H''; assert (H'' : trans_clos (one_step_list (one_step (sym_refl ac_one_step_at_top))) l1 l2). apply IHl1; trivial. intros; apply Wl1; right; trivial. intros; apply Sl1; right; trivial. inversion H; trivial. intros; apply Wl2; right; trivial. revert H''; clear; intro H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. right with (t2 :: l2); trivial. right; assumption. Qed.
imports: Coq(Setoid Arith List Morphisms) CoLoR(closure more_list weaved_relation list_sort term_spec ac)