proposition: Lemma well_formed_cf_is_well_formed_cf_conv : forall cf, (exists t, well_formed t /\ cf = canonical_form t) -> well_formed_cf cf.
proof: Proof. intros cf [t [Wt Ct]]; subst; generalize Wt; clear Wt. pattern t; apply term_rec2; clear t; induction n as [ | n ]; intros t St Wt. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t); trivial; apply size_ge_one. apply well_formed_cf_fold; destruct t as [ v | f l ]; simpl; trivial. generalize (well_formed_unfold Wt); intros [Wl L]. assert (Wl' : forall t, In t (map canonical_form l) -> well_formed_cf t). clear Wt L; rewrite size_unfold in St; induction l as [ | t1 l ]. contradiction. intros t In_t; elim In_t; clear In_t; intro In_t; subst. apply IHn; [ apply Nat.le_trans with (list_size size (t1 :: l)); simpl; auto with arith | apply Wl; left; trivial ]. apply IHl; trivial; [ apply Nat.le_trans with (1 + list_size size (t1 :: l)); simpl; auto with arith | intros; apply Wl; right; trivial]. destruct_arity f a Af. split; [idtac | split; [idtac | split]]. intros u In_u; rewrite <- in_quick_in in In_u. generalize (map canonical_form l) Wl' In_u; clear l St Wt Wl L Wl' In_u; intro l; induction l as [ | t l ]; intros Wl In_u. contradiction. assert (H:=flatten_app f (t :: nil) l); simpl app in H; rewrite H in In_u; clear H; elim (in_app_or _ _ _ In_u); clear In_u; intro In_u. assert (Wt : well_formed_cf t). apply Wl; left; trivial. destruct t as [v | g h]. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. revert In_u; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g In_u | intros f_diff_g In_u]. rewrite <- app_nil_end in In_u; apply (well_formed_cf_subterms Wt); trivial. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. apply IHl; trivial; intros; apply Wl; right; trivial. rewrite length_quicksort; rewrite <- L; unfold ge; apply length_flatten; trivial. apply quick_sorted. intros u In_u; rewrite <- in_quick_in in In_u. generalize (map canonical_form l) In_u Wl'; clear l St Wt Wl L Wl' In_u; intro l; pattern l; apply (list_rec3 size); clear l; induction n0 as [ | m]; destruct l as [ | t l ]. contradiction. intro H; absurd (1 <= 0); auto with arith; apply Nat.le_trans with (list_size size (t :: l)); trivial; apply Nat.le_trans with (size t); simpl; auto with arith; apply size_ge_one. contradiction. assert (H:=flatten_app f (t :: nil) l); simpl app in H; rewrite H; clear H. intros Sl In_u Wl; elim (in_app_or _ _ _ In_u); clear In_u; intro In_u. assert (Wt : well_formed_cf t). apply Wl; left; trivial. destruct t as [ v | g ll ]. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. revert In_u; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g In_u | intros f_diff_g In_u]. subst g; rewrite <- app_nil_end in In_u; apply well_formed_cf_alien with ll; trivial. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. apply (IHm l); trivial. apply le_S_n; apply Nat.le_trans with (1 + list_size size l); auto with arith; apply Nat.le_trans with (size t + list_size size l); trivial; apply Nat.add_le_mono_r; apply size_ge_one. intros; apply Wl; right; trivial. split; [idtac | split]. intros u In_u; rewrite <- in_quick_in in In_u. apply Wl'; trivial. rewrite length_quicksort; rewrite length_map; trivial. apply quick_sorted. split; trivial; rewrite length_map; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)