Stream: Coq users

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

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:

• unfold Rdiv.
  Search (?x * ?y <= ?z * ?y).
  apply Rmult_le_compat_r.
  apply Rlt_le.
  Search (0 < / ?x).
  apply invR_gt0.
  lra.
  rewrite <- sqrt_Rsqr_abs.
  apply sqrt_le_1_alt.
  unfold "^2". simpl. unfold "o".
  unfold "`E".
  unfold ambient_dist.
  rewrite big_distrr.

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.

Cyril Cohen (Apr 15 2021 at 19:12):

@Reynald Affeldt ?

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.)

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: Sep 23 2023 at 08:01 UTC