coq - Ssreflect 概率（事件和非事件）总和为 1

Question

我是一名初学者，希望您能帮助我将事件 F 的概率和事件非 F 的概率相加为一。有没有快速前进的方法？

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

===

X i * P i * ((if i \in F then R1 else R0) + (if i \in ~: F then R1 else R0)) =
X i * P i

Answer 1

在我看来，您需要重写以inE使其i \in ~: F成为i \notin F，然后进行案例分析（case: (i \in F)），然后rewrite (addr0, add0r) mulr1可能就足够了。