比较总和ssreflect

Question

我的目标是说，如果我们有

sum(a) = sum(b)

然后

a = b.

如果目标看起来像这样，那么做这件事的合适策略是什么：

\big[Radd_comoid/0]_(i <- fin_img (A:=U) (B:=R_eqType) X)
   Radd_comoid
     (Pr P F * (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: F) / Pr P F))
     (Pr P (~: F) *
      (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: ~: F) / Pr P (~: F))) =
\sum_(u in U) X u * `p_ X u

已编辑。上下文包含：

X: {RV (P) -> (R)}
F: {set U}
H: 0 < Pr P F
H0: Pr P F < 1

rewrite /=.之后的目标如下所示：

\big[Rplus/0]_(i <- fin_img (A:=U) (B:=R_eqType) X)
   (Pr P F * (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: F) / Pr P F) +
    Pr P (~: F) *
    (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: ~: F) / Pr P (~: F))) =
\sum_(u in U) X u * `p_ X u

Answer 1

如果这是真的，您可能需要使用右侧的sum_parti_finType，并尝试使用eq_bigr识别求和的一般项。左手边的通用术语可以在+的两侧使用mulrC mulfVK (或类似这样的东西)来简化。然后识别具有不相交并集的概率的概率和。不管怎么说，这不仅仅是“一种策略”...