proposition: Lemma size_size : forall t, well_formed t -> size t = ac_size (canonical_form t).
proof: Proof. intros t; pattern t; apply term_rec3; clear t. intros v _; trivial. intros f l H Wt; destruct (well_formed_unfold Wt) as [Wl Ll]. assert (Hl : forall t, In t l -> size t = ac_size (canonical_form t)). intros; apply H; trivial; apply Wl; trivial. clear H Wt; assert (Hl' : list_size size l = list_size ac_size (map canonical_form l)). clear Ll; induction l as [ | t l]; trivial. simpl; rewrite (Hl t (or_introl _ (eq_refl _))); rewrite IHl; trivial. intros; apply Wl; right; trivial. intros; apply Hl; right; trivial. simpl; rewrite (list_size_fold size); rewrite (list_size_fold ac_size); destruct_arity f n Af. assert (Dummy : DOS.A = term). apply eq_refl. rewrite length_quicksort. assert (Dummy2 : forall l, @length DOS.A l = @length term l). intro k; apply eq_refl. rewrite Dummy2. replace (list_size ac_size (quicksort (flatten f (map canonical_form l)))) with (list_size ac_size (flatten f (map canonical_form l))). destruct l as [ | t1 [ | t2 [ | t3 l]]]; [absurd (0 = 2) | absurd (1 = 2) | idtac | absurd (S(S(S(length l))) = 2)]; auto with arith. simpl map; simpl list_size; rewrite Nat.add_0_r; rewrite (Hl t1 (or_introl _ (eq_refl _))); rewrite (Hl t2 (or_intror _ (or_introl _ (eq_refl _)))). assert (W1 : well_formed_cf (canonical_form t1)). apply well_formed_cf_is_well_formed_cf_conv; exists t1; split; trivial; apply Wl; left; trivial. assert (W2 : well_formed_cf (canonical_form t2)). apply well_formed_cf_is_well_formed_cf_conv; exists t2; split; trivial; apply Wl; right; left; trivial. destruct (canonical_form t1) as [v1 | f1 ll1]; destruct (canonical_form t2) as [v2 | f2 ll2]; trivial. simpl flatten; generalize (F.Symb.eq_bool_ok f f2); case (F.Symb.eq_bool f f2); [intros f_eq_f2; subst f2 | intros f_diff_f2]. simpl; rewrite <- app_nil_end; simpl; rewrite Af. rewrite (list_size_fold ac_size); rewrite Nat.sub_0_r. generalize (well_formed_cf_length Af W2). intro Lll2; destruct (length ll2) as [ | n2]. absurd (2 <= 0); auto with arith. simpl; rewrite Nat.sub_0_r; apply sym_eq; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. simpl; rewrite Nat.add_0_r; trivial. simpl flatten; generalize (F.Symb.eq_bool_ok f f1); case (F.Symb.eq_bool f f1); [intros f_eq_f1; subst f1 | intros f_diff_f1]. simpl; rewrite Af; rewrite (list_size_fold ac_size). generalize (well_formed_cf_length Af W1); intro Lll1; rewrite length_app; destruct (length ll1) as [ | n1]. absurd (2 <= 0); auto with arith. rewrite list_size_app; simpl; do 2 rewrite Nat.sub_0_r; rewrite (Nat.add_comm n1 1); simpl; rewrite Nat.add_assoc; trivial. trivial. replace (flatten f (Term f1 ll1 :: Term f2 ll2 :: nil)) with ((flatten f (Term f1 ll1 :: nil)) ++ (flatten f (Term f2 ll2 :: nil))). rewrite length_app. simpl; generalize (F.Symb.eq_bool_ok f f1); case (F.Symb.eq_bool f f1); [intros f_eq_f1; subst f1 | intros f_diff_f1]; (generalize (F.Symb.eq_bool_ok f f2); case (F.Symb.eq_bool f f2); [intros f_eq_f2; subst f2 | intros f_diff_f2]). do 2 rewrite <- app_nil_end; rewrite Af; do 2 rewrite (list_size_fold ac_size); rewrite list_size_app. unfold DOS.A in *; generalize (well_formed_cf_length Af W1); intro Lll1; destruct (length ll1) as [ | n1]. absurd (2 <= 0); auto with arith. unfold DOS.A in *; generalize (well_formed_cf_length Af W2); intro Lll2; destruct (length ll2) as [ | n2]. absurd (2 <= 0); auto with arith. simpl; do 3 rewrite Nat.sub_0_r; rewrite (Nat.add_comm n1 (S n2)); simpl; rewrite (Nat.add_comm n2 n1); do 2 rewrite <- Nat.add_assoc; apply (f_equal (fun n => S (n1 + n))); rewrite Nat.add_comm; rewrite <- Nat.add_assoc; apply (f_equal (fun n => n2 + n)); apply Nat.add_comm. rewrite Af; rewrite <- app_nil_end; rewrite list_size_app; simpl; do 2 rewrite (list_size_fold ac_size); simpl; rewrite Nat.add_0_r; rewrite (Nat.add_comm (length ll1) 1); simpl; rewrite Nat.sub_0_r; unfold DOS.A in *; generalize (well_formed_cf_length Af W1); intro Lll1; destruct (length ll1) as [ | n1]. absurd (2 <= 0); auto with arith. simpl; rewrite Nat.sub_0_r; rewrite <- Nat.add_assoc; trivial. rewrite Af; rewrite <- app_nil_end. do 2 rewrite (list_size_fold ac_size). unfold DOS.A in *; generalize (well_formed_cf_length Af W2); intro Lll2; destruct (length ll2) as [ | n2]. absurd (2 <= 0); auto with arith. simpl minus; rewrite Nat.sub_0_r; simpl plus; do 3 rewrite Nat.add_assoc; apply (f_equal (fun n => S (n + list_size ac_size ll2))). rewrite Nat.add_comm; rewrite Nat.add_assoc; rewrite (list_size_fold ac_size); trivial. simpl; rewrite Nat.add_0_r; trivial. rewrite <- flatten_app; simpl app; trivial. apply permut_size with (@eq term). intros; subst; trivial. apply quick_permut. rewrite Hl'; simpl; apply (f_equal S). apply permut_size with (@eq term). intros; subst; trivial. apply quick_permut. rewrite Hl'; simpl; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)