proposition: Lemma ac_one_step_at_top_cf_eq : forall t1 t2, ac_one_step_at_top t1 t2 -> canonical_form t1 = canonical_form t2.
proof: Proof. assert (P12 : forall t1 t2, permut (t1 :: t2 :: nil) (t2 :: t1 :: nil)). intros t1 t2; replace (t1 :: t2 :: nil) with ((t1 :: nil) ++ (t2 :: nil)); trivial; replace (t2 :: t1 :: nil) with ((t2 :: nil) ++ (t1 :: nil)); trivial; apply list_permut_app_app. assert (Ccase : forall f, arity f = C \/ arity f = AC -> forall t1 t2, canonical_form (Term f (t1 :: t2 :: nil)) = canonical_form (Term f (t2 :: t1 :: nil))). intros f [Af | Af] t1 t2; simpl; rewrite Af; apply (f_equal (fun l => Term f l)); apply sort_is_unique; try apply quick_sorted; do 2 (apply quick_permut_bis; apply permut_sym). apply P12. destruct (canonical_form t1) as [v1 | f1 ll1]; destruct (canonical_form t2) as [v2 | f2 ll2]. apply P12. case (F.Symb.eq_bool f f2); [ rewrite <- permut_cons_inside; auto | apply P12 ]. reflexivity. case (F.Symb.eq_bool f f1); [ apply permut_sym; rewrite <- permut_cons_inside; auto | apply P12 ]. reflexivity. case (F.Symb.eq_bool f f1); case (F.Symb.eq_bool f f2). do 2 rewrite <- app_nil_end; apply list_permut_app_app. apply permut_sym; rewrite <- permut_cons_inside; auto. reflexivity. rewrite <- permut_cons_inside; auto. reflexivity. apply P12. assert (ACcase : forall f, arity f = AC -> forall t1 t2 t3, canonical_form (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil)) = canonical_form (Term f (t1 :: Term f (t2 :: t3 :: nil) :: nil))). intros f Af t1 t2 t3; simpl; rewrite Af; 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]. apply (f_equal (fun l => Term f l)); apply sort_is_unique. apply quick_sorted. apply quick_sorted. do 2 (apply quick_permut_bis; apply permut_sym). generalize (canonical_form t1) (canonical_form t2) (canonical_form t3); clear t1 t2 t3; intros t1 t2 t3; rewrite <- app_nil_end. transitivity ((flatten f (t1 :: t2 :: nil)) ++ (flatten f (t3 :: nil))). rewrite <- permut_app2. apply permut_sym; apply quick_permut. transitivity ((flatten f (t1 :: nil)) ++ (flatten f (t2 :: t3 :: nil))). do 2 rewrite <- flatten_app; simpl app; apply permut_refl. destruct t1 as [v1 | g1 ll1]. simpl; rewrite <- permut_cons. apply quick_permut. reflexivity. simpl; case (F.Symb.eq_bool f g1). rewrite <- app_nil_end; rewrite <- permut_app1; apply quick_permut. simpl; rewrite <- permut_cons. apply quick_permut. reflexivity. intros t1 t2 H; destruct H; auto; apply sym_eq; auto. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)