CODEWITHSUNDEEP
coqcoq-tacticssreflect
VHarisop
VHarisop

Reputation: 2826

Coq - Proving strict inequality involving bigops in Ssreflect

I am trying to prove the following using the Mathematical Components library:

Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R):
  (forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) ->
  \sum_(i < q) F i < \sum_(i < q) G i.

Initially, I was trying to find some Lemma equivalent to bigsum_aux in the documentation of ssralg or bigop, but I couldn't find any; so this is what I have been able to do so far:

Proof.
 move => [Hall Hex]. rewrite ltr_neqAle ler_sum; last first.
 - move => ? _. exact: Hall.
 - rewrite andbT. (* A: What now? *)

Any help or pointers towards relevant lemmas would be welcome.

Upvotes: 1

Views: 93

Answers (1)

ejgallego
ejgallego

Reputation: 6852

You want to split the sum in the "bad" (<) part, then the rest is trivial:

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Import Num.Theory.

Lemma bigsum_aux (R : numDomainType) q (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R)
      (hle : forall i0, F i0 <= G i0) z (hlt : F z < G z) :
  \sum_(i < q) F i < \sum_(i < q) G i.
Proof.
by rewrite [\sum__ F _](bigD1 z) ?[\sum__ G _](bigD1 z) ?ltr_le_add ?ler_sum.
Qed.

Upvotes: 2

Related Questions