proposition: Lemma well_formed_cf_is_well_formed_cf : forall cf, well_formed_cf cf -> exists t, well_formed t /\ cf = canonical_form t.
proof: Proof. intros cf Wcf; generalize (well_formed_cf_unfold _ Wcf); pattern cf; apply term_rec3; clear cf Wcf. intros v _; exists (Var v); unfold well_formed; simpl; split; trivial. intros f l Hrec [Wl Ll]; assert (Wl' : forall u, In u l -> exists s, well_formed s /\ u = canonical_form s). intros u In_u; apply Hrec; trivial; apply well_formed_cf_unfold; apply Wl; trivial. destruct_arity f n Af. revert Ll; intros [Ll [Sl Al]]; induction l as [ | t1 l]. absurd (0 >= 2); trivial; unfold ge; auto with arith. destruct l as [ | t2 l]. absurd (1 >= 2); trivial; unfold ge; auto with arith. elim (Wl' t1). intros u1 [Wu1 Hu1] . elim (Wl' t2). intros u2 [Wu2 Hu2] . assert (At1 : match t1 with Var _ => True | Term g _ => f <> g end). apply Al; left; trivial. assert (At2 : match t2 with Var _ => True | Term g _ => f <> g end). apply Al; right; left; trivial. destruct l as [ | t3 l]. exists (Term f (u2 :: u1 :: nil)); split. apply well_formed_fold; rewrite Af; split; trivial. intros u In_u; elim In_u; clear In_u; intro In_u; try subst u; trivial; elim In_u; clear In_u; intro In_u; try subst u; trivial; contradiction. simpl; rewrite Af; rewrite <- Hu1; rewrite <- Hu2. destruct t1 as [v1 | g1 ll1]; destruct t2 as [v2 | g2 ll2]. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Var v2 :: nil) (Var v1 :: nil)). generalize (F.Symb.eq_bool_ok f g2); case (F.Symb.eq_bool f g2); [intro f_eq_g2 | intro f_diff_g2]. absurd (f=g2); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Term g2 ll2 :: nil) (Var v1 :: nil)). generalize (F.Symb.eq_bool_ok f g1); case (F.Symb.eq_bool f g1); [intro f_eq_g1 | intro f_diff_g1]. absurd (f=g1); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Var v2 :: nil) (Term g1 ll1 :: nil)). generalize (F.Symb.eq_bool_ok f g2); case (F.Symb.eq_bool f g2); [intro f_eq_g2 | intro f_diff_g2]. absurd (f=g2); trivial. generalize (F.Symb.eq_bool_ok f g1); case (F.Symb.eq_bool f g1); [intro f_eq_g1 | intro f_diff_g1]. absurd (f=g1); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Term g2 ll2 :: nil) (Term g1 ll1 :: nil)). elim IHl. intros s2 [Ws2 Hs2]; exists (Term f (s2 :: u1 :: nil)); split. apply well_formed_fold; rewrite Af; split; trivial. intros u In_u; elim In_u; clear In_u; intro In_u; try subst u; trivial; elim In_u; clear In_u; intro In_u; try subst u; trivial; contradiction. simpl; rewrite Af; rewrite <- Hu1; rewrite <- Hs2. 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]. destruct t1 as [v1 | g1 ll1]. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply permut_sym; rewrite <- permut_cons_inside. rewrite <- app_nil_end; apply permut_refl. reflexivity. generalize (F.Symb.eq_bool_ok f g1); case (F.Symb.eq_bool f g1); [intro f_eq_g1 | intro f_diff_g1]. absurd (f=g1); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply permut_sym; rewrite <- permut_cons_inside. rewrite <- app_nil_end; apply permut_refl. reflexivity. intros; apply Hrec; trivial; right; trivial. intros; apply Wl; right; trivial. intros; apply Wl'; right; trivial. simpl; auto with arith. apply sorted_tl_sorted with t1; trivial. intros; apply Al; right; trivial. right; left; trivial. left; trivial. generalize Ll; clear Ll; intros [Ll Sl]; destruct l as [ | t1 l]. absurd (0 = 2); auto with arith. destruct l as [ | t2 l]. absurd (1 = 2); auto with arith. destruct l as [ | t3 l]. elim (Wl' t1). intros u1 [Wu1 Hu1] . elim (Wl' t2). intros u2 [Wu2 Hu2] . exists (Term f (u1 :: u2 :: nil)); split. apply well_formed_fold; rewrite Af; split; trivial. intros u In_u; elim In_u; clear In_u; intro In_u; try subst u; trivial; elim In_u; clear In_u; intro In_u; try subst u; trivial; contradiction. simpl; rewrite Af; subst; apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial; [ apply quick_sorted | apply quick_permut ]. right; left; trivial. left; trivial. absurd (S(S(S(length l))) = 2); auto. assert (H : exists l', (forall s, In s l' -> well_formed s) /\ map canonical_form l' = l). generalize l Wl'; clear l Hrec Wl Wl' Ll; induction l as [ | t l]. intros _; exists (nil (A := term)); split; trivial; contradiction. intros Wl; elim IHl. intros l' [Wl' Hl']; elim (Wl t). intros t' [Wt' Ht']; exists (t' :: l'); split; trivial. intros s [ s_eq_t' | In_s]; try subst s; trivial; apply Wl'; trivial. simpl; subst; trivial. left; trivial. intros; apply Wl; right; trivial. elim H; clear H; intros l' [Wl'' Hl']; exists (Term f l'); split. apply well_formed_fold; rewrite Af; subst; rewrite length_map; split; trivial. simpl; rewrite Af; subst; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)