proposition: Theorem build_comp : forall (l1 l2 : list (btree A)) (t1 t2 : btree A), build l1 t1 -> build l2 t2 -> weight_tree_list f l1 = weight_tree_list f l2 -> same_sum_leaves f l1 l2 -> weight_tree f t1 = weight_tree f t2.
proof: Proof. intros l1 l2 t1 t2 H; generalize l2 t2; elim H; clear H l1 t1 l2 t2. intros t l2 t2 H H0 (l3, (l4, (H1, (H2, H3)))). generalize H0; inversion H; clear H0. simpl in |- *; repeat rewrite <- plus_n_O; auto. case H4. intros l5 (t3, (t4, (H8, (H9, H10)))). absurd (length l2 = length (t3 :: t4 :: l5)). rewrite Permutation_length with (1 := H2). rewrite <- map_length with (f := sum_leaves f) (l := l4). rewrite <- H3. rewrite map_length with (f := sum_leaves f). rewrite Permutation_length with (1 := Permutation_sym H1). simpl in |- *; red in |- *; intros; discriminate. apply Permutation_length with (1 := H9). intros t l1 l2 H H0 H1 l0 t2 H2 H3 H4. inversion H2. case H. intros l5 (t3, (t4, (H8, (H9, H10)))). case H4. intros l6 (l7, (H11, (H12, H13))). absurd (length l1 = length (t3 :: t4 :: l5)). rewrite Permutation_length with (1 := H11). rewrite <- map_length with (f := sum_leaves f) (l := l6). rewrite H13. rewrite map_length with (f := sum_leaves f). rewrite Permutation_length with (1 := Permutation_sym H12). rewrite <- H5; simpl in |- *; red in |- *; intros; discriminate. apply Permutation_length with (1 := H9). apply H1 with (1 := H6). case one_step_comp with (3 := H) (4 := H5); auto. case one_step_comp with (3 := H) (4 := H5); auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)