proposition: Theorem build_correct : forall (l : list (btree A)) (t : btree A), l <> [] -> build l t -> cover_min _ f l t.
proof: Proof. intros l; elim l using list_length_ind. intros l0 H t H0 H1. case (cover_min_ex _ f) with (1 := H0); auto. intros t1 (Ht1, Ht2). case cover_ordered_cover with (1 := Ht1); auto. intros l1 (Hl1, Hm1). case (ordered_cover_height_pred A 0) with (1 := Hm1). intros ln0 Ht3. case exist_first_max with ln0. apply height_pred_not_nil1 with (1 := Ht3); auto. intros a (ln1, (ln2, (HH1, (HH2, HH3)))). cut (length ln0 = length l1); [ intros IL | apply height_pred_length with (1 := Ht3) ]. rewrite HH1 in Ht3; rewrite HH1 in IL; clear HH1 ln0. case height_pred_disj_larger with (1 := Ht3); auto. intros (ln3, HH4); rewrite HH4 in HH3; rewrite HH4 in IL; rewrite HH4 in Ht3; clear HH4 ln2; auto. case same_length_ex with (1 := IL); auto. intros l2 (l3, (t4, (HM1, (HM2, HM3)))). generalize HM2 HM3; case l3; try (simpl in |- *; intros; discriminate); clear HM2 HM3 l3. intros t5 l3 HM2 HM3; rewrite HM3 in Ht3; rewrite HM3 in IL; rewrite HM3 in Hm1; rewrite HM3 in Hl1; clear HM3 l1. cut (exists b1, (exists c1, (exists l4, Permutation (l2 ++ t4 :: t5 :: l3) (b1 :: c1 :: l4) /\ ordered (sum_order f) (b1 :: c1 :: l4)))). intros (b1, (c1, (l4, (HC1, HC2)))). case prod2list_reorder2 with (l1 := ln1) (l2 := ln3) (5 := HC1) (6 := HC2) (a := a); auto with datatypes. intros b H2; apply Nat.lt_le_incl; auto with arith. intros l5 (l6, (HB1, (HB2, (HB3, HB4)))). case height_pred_subst_pred with (1 := Ht3) (l2 := l5 ++ b1 :: c1 :: l6); auto. rewrite <- IL; repeat rewrite app_length; simpl in |- *; auto. intros t6 (HD1, HD2). case (buildf (l5 ++ node b1 c1 :: l6)); auto. case l5; simpl in |- *; intros; discriminate. intros t7 HD3. case H with (3 := HD3); auto with arith. rewrite Permutation_length with (1 := Hl1). rewrite Permutation_length with (1 := HC1). rewrite Permutation_length with (1 := HB3). repeat rewrite app_length; simpl in |- *; auto with arith. case l5; simpl in |- *; intros; discriminate. intros HD4 HD5. split; auto. apply build_cover with (1 := H1). intros t0 H2; apply Nat.le_trans with (weight_tree f t1); auto. rewrite (build_same_weight_tree l0 t t7); auto. apply Nat.le_trans with (weight_tree f t6). apply HD5; auto. apply ordered_cover_cover. apply (height_pred_ordered_cover A 0 (ln1 ++ pred a :: ln3)); auto. apply height_pred_shrink with (b := a); auto. replace (weight_tree f t1) with (0 * sum_leaves f t1 + weight_tree f t1); [ idtac | simpl in |- *; auto ]. rewrite height_pred_weight with (1 := Ht3). replace (weight_tree f t6) with (0 * sum_leaves f t6 + weight_tree f t6); [ idtac | simpl in |- *; auto ]. rewrite height_pred_weight with (1 := HD1); auto. apply build_step with (2 := HD3); auto. exists l4; exists b1; exists c1; repeat (split; auto). apply Permutation_trans with (1 := Hl1). apply Permutation_sym; apply Permutation_trans with (1 := HB3). apply Permutation_sym; apply Permutation_trans with (1 := HC1); auto. apply Permutation_trans with ((node b1 c1 :: l6) ++ l5); auto. simpl in |- *; apply perm_skip. apply Permutation_cons_inv with c1. apply Permutation_cons_inv with b1. apply Permutation_sym; apply Permutation_trans with (1 := HB3). apply (Permutation_app_swap l5 (b1 :: c1 :: l6)). generalize (isort_permutation _ (le_sum f) (l2 ++ t4 :: t5 :: l3)); generalize (isort_ordered _ (sum_order f) (le_sum f) (le_sum_correct1 _ f) (le_sum_correct2 _ f) (l2 ++ t4 :: t5 :: l3)). case (isort (le_sum f) (l2 ++ t4 :: t5 :: l3)); auto. intros H2 H3. absurd (l2 ++ t4 :: t5 :: l3 = []); auto. case l2; simpl in |- *; intros; discriminate. apply Permutation_sym in H3. apply Permutation_nil with (1 := H3). intros b l4; case l4. intros H2 H3; absurd (l2 ++ t4 :: t5 :: l3 = b :: []). case l2; simpl in |- *; try (intros; discriminate). intros b0 l5; case l5; try (intros; discriminate). apply Permutation_length_1_inv with (1 := Permutation_sym H3). intros b0 l5 H2 H3; exists b; exists b0; exists l5; auto. intros ((H2, (H3, H4)), H5); split. apply build_cover with (1 := H1). intros t2 H6; rewrite <- cover_one_inv with (t1 := t1) (t2 := t2). rewrite <- cover_one_inv with (t1 := t1) (t2 := t); auto. rewrite <- H5; apply cover_permutation with (2 := Hl1); auto. apply build_cover with (1 := H1). rewrite <- H5; apply cover_permutation with (2 := Hl1); auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)