proposition: Lemma unit_nf_is_sound : forall t, unit_th t (unit_nf t).
proof: Proof. unfold unit_th; intro t; pattern t; apply term_rec3; clear t. intros v; simpl; apply th_refl. intros f l IH; unfold th_eq; apply trans_clos_is_trans with (Term f (map unit_nf l)). destruct l as [ | a l]. apply th_refl. apply general_context. revert a IH; induction l as [ | b l]. intros a IH. assert (Ha := IH _ (or_introl _ (eq_refl _))). apply rwr_list_cons; assumption. intros a IH. assert (Ha := IH _ (or_introl _ (eq_refl _))). assert (Hl : rwr_list (one_step (sym_refl unit_one_step_at_top)) (b :: l) (map unit_nf (b :: l))). apply IHl. simpl; intros t [t_eq_b | t_in_l]; apply IH; right; [left | right]; assumption. simpl; apply rwr_list_split. apply IH; left; apply eq_refl. apply Hl. clear IH; destruct l as [ | t1 [ | t2 [ | t3 l ]]]; [apply th_refl | apply th_refl | idtac | apply th_refl]. simpl; case_eq (unit_theory f); [intros u UT | intros u UT | intros u UT | intro UT]. 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]. subst; apply R_in_rwr_R; rewrite t1_eq_u; left; apply left_unit; left; trivial. apply th_refl. 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]. subst; apply R_in_rwr_R; rewrite t2_eq_u; left; apply right_unit; left; trivial. apply th_refl. 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]. subst; apply R_in_rwr_R; rewrite t1_eq_u; left; apply left_unit; right; 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]. subst; apply R_in_rwr_R; rewrite t2_eq_u; left; apply right_unit; right; trivial. apply th_refl. apply th_refl. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)