proposition: Lemma acu_is_ac_on_unit_nf : forall t1 t2, ac (unit_nf t1) (unit_nf t2) <-> acu t1 t2.
proof: Proof. unfold ac, acu, th_eq; intros t1 t2; split; intro H. apply trans_clos_is_trans with (unit_nf t1). apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 H; intros t1 t2 [H | [H | H]]. left; right; trivial. right; left; right; trivial. right; right; trivial. apply unit_nf_is_sound. apply trans_clos_is_trans with (unit_nf t2). apply rwr_incl with (sym_refl ac_one_step_at_top). clear t1 t2 H; intros t1 t2 [H | [H | H]]. left; left; trivial. right; left; left; trivial. right; right; trivial. trivial. apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 H; intros t1 t2 [H | [H | H]]. left; right; trivial. right; left; right; trivial. right; right; trivial. apply th_sym; apply unit_nf_is_sound. assert (No_need_of_inst : forall t1 t2, axiom (sym_refl (union _ ac_one_step_at_top unit_one_step_at_top)) t1 t2 -> sym_refl (union _ ac_one_step_at_top unit_one_step_at_top) t1 t2). clear t1 t2 H; intros t1 t2 H; inversion_clear H as [u1 u2 sigma H']. destruct H' as [[H | H] | [[H | H] | H]]. inversion_clear H. simpl; left; left; apply a_axiom; trivial. simpl; left; left; apply c_axiom; trivial. inversion_clear H. simpl; left; right; apply left_unit; trivial. simpl; left; right; apply right_unit; trivial. inversion_clear H. simpl; right; left; left; apply a_axiom; trivial. simpl; right; left; left; apply c_axiom; trivial. inversion_clear H. simpl; right; left; right; apply left_unit; trivial. simpl; right; left; right; apply right_unit; trivial. subst; right; right; trivial. assert (H1 : forall f u1 u2 u3, arity f = AC -> th_eq ac_one_step_at_top (unit_nf (Term f (Term f (u1 :: u2 :: nil) :: u3 :: nil))) (unit_nf (Term f (u1 :: Term f (u2 :: u3 :: nil) :: nil)))). intros f u1 u2 u3 Ar; simpl. assert (UT : forall g, g = f -> unit_theory g = unit_theory f). intros; subst; trivial. generalize (unit_for_AC _ Ar); destruct (unit_theory f) as [ u | u | u | ]; try contradiction; intros _; generalize (UT f (eq_refl _)); clear UT; intro UT. generalize (T.eq_bool_ok (unit_nf u1) (Term u nil)); case (T.eq_bool (unit_nf u1) (Term u nil)); [intro u1_eq_u | intro u1_diff_u]. apply th_refl. generalize (T.eq_bool_ok (unit_nf u2) (Term u nil)); case (T.eq_bool (unit_nf u2) (Term u nil)); [intro u2_eq_u | intro u2_diff_u]. generalize (T.eq_bool_ok (unit_nf u1) (Term u nil)); case (T.eq_bool (unit_nf u1) (Term u nil)); [intro u1_eq_u | intros _]. absurd (unit_nf u1 = Term u nil); trivial. generalize (T.eq_bool_ok (unit_nf u3) (Term u nil)); case (T.eq_bool (unit_nf u3) (Term u nil)); [intro u3_eq_u | intro u3_diff_u]. apply th_refl. apply th_refl. generalize (T.eq_bool_ok (Term f (unit_nf u1 :: unit_nf u2 :: nil)) (Term u nil)); case (T.eq_bool (Term f (unit_nf u1 :: unit_nf u2 :: nil)) (Term u nil)); [ intro H' | intros _]. discriminate. generalize (T.eq_bool_ok (unit_nf u3) (Term u nil)); case (T.eq_bool (unit_nf u3) (Term u nil)); [intro u3_eq_u | intro u3_diff_u]. generalize (T.eq_bool_ok (unit_nf u2) (Term u nil)); case (T.eq_bool (unit_nf u2) (Term u nil)); [intro u2_eq_u | intros _]. absurd (unit_nf u2 = Term u nil); trivial. apply th_refl. generalize (T.eq_bool_ok (Term f (unit_nf u1 :: unit_nf u2 :: nil)) (Term u nil)); case (T.eq_bool (Term f (unit_nf u1 :: unit_nf u2 :: nil)) (Term u nil)); [intro H' | intros _]. discriminate. generalize (T.eq_bool_ok (Term f (unit_nf u2 :: unit_nf u3 :: nil)) (Term u nil)); case (T.eq_bool (Term f (unit_nf u2 :: unit_nf u3 :: nil)) (Term u nil)); [intro H' | intros _]. discriminate. apply l_assoc; trivial. apply l_assoc; trivial. assert (H2 : forall f u1 u2, arity f = C \/ arity f = AC -> th_eq ac_one_step_at_top (unit_nf (Term f (u1 :: u2 :: nil))) (unit_nf (Term f (u2 :: u1 :: nil)))). intros f u1 u2 Ar; simpl; assert (UT : forall g, g = f -> unit_theory g = unit_theory f). intros; subst; trivial. generalize (unit_for_C _ Ar); destruct (unit_theory f) as [ u | u | u | ]; try contradiction; intros _; generalize (UT f (eq_refl _)); clear UT; intro UT. generalize (T.eq_bool_ok (unit_nf u1) (Term u nil)); case (T.eq_bool (unit_nf u1) (Term u nil)); [intro u1_eq_u | intro u1_diff_u]. generalize (T.eq_bool_ok (unit_nf u2) (Term u nil)); case (T.eq_bool (unit_nf u2) (Term u nil)); [intro u2_eq_u | intro u2_diff_u]. rewrite u1_eq_u; rewrite u2_eq_u; apply th_refl. apply th_refl. generalize (T.eq_bool_ok (unit_nf u2) (Term u nil)); case (T.eq_bool (unit_nf u2) (Term u nil)); [intro u2_eq_u | intro u2_diff_u]. apply th_refl. apply comm; trivial. apply comm; trivial. refine (rwr_inv _ (sym_refl (union _ ac_one_step_at_top unit_one_step_at_top)) (rwr (sym_refl ac_one_step_at_top)) unit_nf _ _ _ _ _); trivial. apply trans_clos_is_trans. clear t1 t2 H; intro t1; pattern t1; apply term_rec2; clear t1; induction n. intros t1 S_t1; absurd (1 <= 0); [auto with arith | apply Nat.le_trans with (size t1)]; [apply size_ge_one | trivial]. intros t1 S_t1 t2 H; inversion H as [H3 H4 H' | f l1 l2 H']; clear H. subst; induction H' as [t1 t2 sigma H']. destruct H' as [[H | H] | [[H | H] | H]]. inversion_clear H as [ f u1 u2 u3 Af | f u1 u2 Af]. unfold th_eq in *; simpl apply_subst; apply H1; trivial. unfold th_eq in *; simpl apply_subst; apply H2; trivial. generalize (unit_th_is_unit_nf_eq (apply_subst sigma t1) (apply_subst sigma t2)); intros [H' _]; unfold unit_th in *. rewrite H'; [ apply th_refl | left; apply at_top; apply instance; left; trivial ]. inversion_clear H as [ f u1 u2 u3 Af | f u1 u2 Af]. apply th_sym; unfold th_eq in *; simpl apply_subst; apply H1; trivial. apply th_sym; unfold th_eq in *; simpl apply_subst; apply H2; trivial. apply th_sym; generalize (unit_th_is_unit_nf_eq (apply_subst sigma t2) (apply_subst sigma t1)); intros [H' _]; unfold unit_th in *. rewrite H'; [ apply th_refl | left; apply at_top; apply instance; left; trivial ]. subst; apply th_refl. subst; assert (S_l1 : forall t, In t l1 -> size t <= n). intros t In_t; apply Nat.lt_succ_r; apply Nat.lt_le_trans with (size (Term f l1)); [apply size_direct_subterm | idtac]; trivial. assert (H : rwr_list (one_step (sym_refl ac_one_step_at_top)) (map unit_nf l1) (map unit_nf l2)). clear S_t1; generalize l2 H'; clear l2 H'; induction l1 as [ | t1 l1]; intros l2 H; inversion_clear H as [ t1' t2 l1' H' | t1' l1' l2' H']. apply rwr_list_cons; apply IHn; trivial. apply S_l1; left; apply eq_refl. simpl; apply rwr_list_tail; apply IHl1; trivial. intros; apply S_l1; right; trivial. clear S_t1; assert (UT : forall g, g = f -> unit_theory g = unit_theory f). intros; subst; trivial. generalize (rwr_list_length_eq H); do 2 rewrite length_map. destruct l1 as [ | s1 [ | t1 [ | u1 l1]]]; destruct l2 as [ | s2 [ | t2 [ | u2 l2]]]; simpl; intro L; try discriminate; clear L. apply th_refl. simpl; inversion H' as [H3 H4 H5 H'' | H3 H4 H5 H'']; subst. apply general_context; trivial. inversion H''. simpl; inversion H' as [H3 H4 H5 H'' | H3 H4 H5 H'']; subst. assert (s1_acu_s2 := IHn s1 (S_l1 _ (or_introl _ (eq_refl _))) s2 H''). destruct (unit_theory f) as [ u | u | u | ]; generalize (UT f (eq_refl _)); clear UT; intro UT; simpl. generalize (T.eq_bool_ok (unit_nf s1) (Term u nil)); case (T.eq_bool (unit_nf s1) (Term u nil)); [intro s1_eq_u | intro s1_diff_u]. generalize (T.eq_bool_ok (unit_nf s2) (Term u nil)); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. apply th_refl. rewrite s1_eq_u in s1_acu_s2; rewrite (ac_const u _ s1_acu_s2) in s2_diff_u; absurd (Term u nil = Term u nil); trivial. generalize (T.eq_bool_ok (unit_nf s2) (Term u nil)); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. rewrite s2_eq_u in s1_acu_s2; rewrite (ac_const u _ (th_sym _ _ _ s1_acu_s2)) in s1_diff_u; absurd (Term u nil = Term u nil); trivial. apply general_context; simpl; intuition. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. apply IHn; trivial; apply S_l1; left; trivial. apply general_context; simpl; intuition. generalize (T.eq_bool_ok (unit_nf s1) (Term u nil)); case (T.eq_bool (unit_nf s1) (Term u nil)); [intro s1_eq_u | intro s1_diff_u]. generalize (T.eq_bool_ok (unit_nf s2) (Term u nil)); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. apply th_refl. rewrite s1_eq_u in s1_acu_s2; rewrite (ac_const u _ s1_acu_s2) in s2_diff_u; absurd (Term u nil = Term u nil); trivial. generalize (T.eq_bool_ok (unit_nf s2) (Term u nil)); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. rewrite s2_eq_u in s1_acu_s2; rewrite (ac_const u _ (th_sym _ _ _ s1_acu_s2)) in s1_diff_u; absurd (Term u nil = Term u nil); trivial. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. trivial. apply general_context; simpl; intuition. apply general_context; simpl; intuition. inversion H'' as [H3 H4 H5 H''' | H3 H4 H5 H''']; subst. assert (t1_acu_t2 := IHn t1 (S_l1 _ (or_intror _ (or_introl _ (eq_refl _)))) t2 H'''). destruct (unit_theory f) as [ u | u | u | ]; generalize (UT f (eq_refl _)); clear UT; intro UT; simpl. generalize (T.eq_bool_ok ); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. trivial. apply general_context; simpl; intuition. generalize (T.eq_bool_ok (unit_nf t1) (Term u nil)); case (T.eq_bool (unit_nf t1) (Term u nil)); [intro t1_eq_u | intro t1_diff_u]. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. apply th_refl. rewrite t1_eq_u in t1_acu_t2; rewrite (ac_const u _ t1_acu_t2) in t2_diff_u; absurd (Term u nil = Term u nil); trivial. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. rewrite t2_eq_u in t1_acu_t2; rewrite (ac_const u _ (th_sym _ _ _ t1_acu_t2)) in t1_diff_u; absurd (Term u nil = Term u nil); trivial. apply general_context; simpl; intuition. generalize (T.eq_bool_ok (unit_nf s2) (Term u nil)); case (T.eq_bool (unit_nf s2) (Term u nil)); [intro s2_eq_u | intro s2_diff_u]. trivial. generalize (T.eq_bool_ok (unit_nf t1) (Term u nil)); case (T.eq_bool (unit_nf t1) (Term u nil)); [intro t1_eq_u | intro t1_diff_u]. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil));[intro t2_eq_u | intro t2_diff_u]. apply th_refl. rewrite t1_eq_u in t1_acu_t2; rewrite (ac_const u _ t1_acu_t2) in t2_diff_u; absurd (Term u nil = Term u nil); trivial. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. rewrite t2_eq_u in t1_acu_t2; rewrite (ac_const u _ (th_sym _ _ _ t1_acu_t2)) in t1_diff_u; absurd (Term u nil = Term u nil); trivial. apply general_context; simpl; intuition. apply general_context; simpl; intuition. inversion H'''. apply general_context; simpl; intuition. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)