1
$\begingroup$

I'm trying to prove the following lemma :

Definition SequenceSum {K : fieldType} (s : nat -> K) (n : nat) := \sum_(0 <= i < n.+1) s i.

Lemma one_minus_q_product_development {K : fieldType} (q : K) (n : nat) : (1-q) * SequenceSum (fun (i:nat) => q^+i) n = 1 - q^+(n+1).

I have currently done this :

Proof.
  rewrite /SequenceSum mulrBl.
  rewrite {1}big_nat_recl//.
  rewrite sum_distrr.
  rewrite big_nat_recr//.

So the current goal is :

  K : fieldType
  q : K
  n : nat
  ============================
  1 * (q ^+ 0 + \sum_(0 <= i < n) q ^+ i.+1) - GRing.add_monoid K (\big[GRing.add_monoid K/0]_(0 <= i < n) (q * q ^+ i)) (q * q ^+ n) = 1 - q ^+ (n + 1)

I'm seeking to use the exprS : forall (R : ringType) (x : R) (n : nat), x ^+ n.+1 = x * x ^+ n in order to turn the q * q +^ i into q ^+ i.+1, but upon using rewrite -exprS, it only rewrites the q * q ^+ n (note that it is outside of any \sum) into q ^+ n.+1.

rewrite -2!exprS yields the following error :

Error: At iteration 2: The RHS of exprS
    (_ * _ ^+ _)
does not match any subterm of the goal

Despite q * q +^ i being in the goal.

Any ideas on how to use this lemma in order to rewrite a term inside a \sum ?

$\endgroup$

1 Answer 1

0
$\begingroup$

In this file you'll see examples of using under eq_bigr ... do ... which is how you do such inside rewrites.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.