proposition: Lemma eval_merge_bin : forall (h k: mset T), eval (sum i (merge_msets compare h k)) == @Bin.value _ _ (e_bin i) (eval (sum i h)) (eval (sum i k)).
proof: Proof. induction h as [[a n]|[a n] h IHh]; intro k. - simpl; induction k as [[b m]|[b m] k IHk]; simpl. * destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. apply copy_plus; auto. * destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. rewrite copy_plus,law_assoc; auto. rewrite IHk; clear IHk. rewrite 2 law_assoc. apply proper; [apply law_comm|reflexivity]. - induction k as [[b m]|[b m] k IHk]; simpl; simpl in IHh. * destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus, Pplus_comm; auto. rewrite <- law_assoc, IHh. reflexivity. rewrite law_comm. reflexivity. * simpl in IHk. destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. rewrite IHh; clear IHh. rewrite 2 law_assoc. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus, Pplus_comm; auto. rewrite IHh; clear IHh. simpl. rewrite law_assoc. reflexivity. rewrite 2 (law_comm (copy m (eval b))). rewrite law_assoc. apply proper; [ | reflexivity]. rewrite <- IHk. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)