Stream: Coq users

Topic: Real numbers sum <= sum Unable to unify error


view this post on Zulip ieja (Apr 09 2021 at 07:21):

Hi all,

I am a beginner and have a question related to solving the goal when comparing sums of reals. We are using infotheo and inside a proof need this assertion.

assert (
let x := mknonnegreal (E ((X -cst E X) ^2 * Ind (A:=U) F: {RV P -> R}) * E (Ind (A:=U) F:{RV P -> R})) H2 in
| E ((X -cst E X) `* Ind (A:=U) F: {RV P -> R})| / Pr P F <=
sqrt (x) / Pr P F).

During the proof:

We hit a goal with a comparison of 2 sums:
delta: R
X: {RV (P) -> (R)}
F: {set U}
H: 0 < delta
H0: delta <= Pr P F
H1: |E_[X | F] - E X| = |E ((X -cst E X) * Ind (A:=U) F : {RV (P) -> (R)})| / Pr P F
H2: 0 <=
E (((X -cst E X) ^2) * Ind (A:=U) F : {RV (P) -> (R)}) * E (Ind (A:=U) F : {RV (P) -> (R)})
===
(1/2)
(\sum_(u in U) (X -cst \sum_(u0 in U) X u0 * P u0) u * Ind (A:=U) F u * P u)² <= \big[Radd_add_law/0]_(i in U) Rmul_mul_law (\sum_(u in U) (X -cst \sum_(u0 in U) X u0 * P u0) u * ((X `-cst \sum_(u0 in U) X u0 * P u0) u * 1) *
Ind (A:=U) F u * P u) (Ind (A:=U) F i * P i)

The idea was to use Lemma leq_sum from bigop.v, modified to fit Real numbers.

Lemma leq_sumR I r (P : pred I) (E1 E2 : I -> R) :
(forall i, P i -> E1 i <= E2 i) ->
\sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i.
Proof. move=> leE12. elim/big_ind2: _ => // m1 m2 n1 n2. lra. Qed.

But it ends with an 'Unable to unify' error.
Any tips on how to proceed would be very valuable.

view this post on Zulip Cyril Cohen (Apr 15 2021 at 19:12):

@Reynald Affeldt ?

view this post on Zulip Reynald Affeldt (Apr 16 2021 at 01:51):

Hi @Ieva Daukantas . Would you have a self-contained proof script that I can copy-paste for inspection? (I am wondering whether `* is a notation of your own.)

view this post on Zulip ieja (Apr 19 2021 at 08:31):

Hi, thank you for the help. It was solved by rewriting previous asserts as there were mistakes.


Last updated: Jan 29 2023 at 06:02 UTC