## Stream: math-comp users

### Topic: Failure trying to use telescope_sumr

#### Julien Puydt (Sep 20 2022 at 22:24):

I wanted to prove a pretty simple statement. It turns out expressing the statement was ugly and proving it... well, I failed! Twice...

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.algebra_tactics Require Import ring.

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

Import GRing Num.Theory.

Section First.

Local Open Scope ring_scope.

Variable RR: realFieldType.

Lemma test_without_telescope n: \sum_(1 <= k < n.+1) 1/(k * (k+1))%:R = 1-1/n.+1%:R :> RR.
Proof.
elim: n => [|n Hn].
rewrite unlock //=.
by field.
rewrite big_nat_recr //= Hn.
field. (* there field does its job well! *)
Check natz. (* switch to integers *)
Fail rewrite natz. (* why does it fail? *)
(* this is too much! *)
apply/andP.
split.
apply lt0r_neq0.
by rewrite -natrD ltr0n.
apply lt0r_neq0.
Fail rewrite -natrD. (* doesn't work like the first... why!? Is what is printed lying? *)

Lemma test_with_telescope n: \sum_(1 <= k < n.+1) 1/(k * (k+1))%:R = 1-1/n.+1%:R :> RR.
Proof.
(* let's try to prepare the way *)
have simpl_elt_decomp k: 1/ (k * (k + 1))%:R = -1/(k+1)%:R - -1/k%:R.
Fail field. (* now field is failing me *)
rewrite div1r.
Check mulr1_eq. (* looks like it will help *)
Fail apply mulr1_eq. (* but no, and look at the error message! *)

(* here is how it should look afterward: *)
under eq_bigr => k do rewrite simple_elt_decomp k. (* use our preliminary work inside the sum *)
apply (@telescope_sumr RR 1 n.+1 (fun k => -1/k%:R)). (* now use telescoping *)
field. (* I doubt it will do the trick *)
Qed.

End First.


#### Paolo Giarrusso (Sep 21 2022 at 08:07):

Not an answer your question, but using apply on ssreflect/math-comp lemmas is unsupported. You want apply: or apply/.

#### Pierre Roux (Sep 21 2022 at 08:34):

I'm having a look but a first comment: don't import GRing, it's explicitly discouraged: https://github.com/math-comp/math-comp/blob/715c53507f9790e9aaff63f60df37539cd4dd86f/mathcomp/algebra/ssralg.v#L566-L567 (and could cause all kind of troubles)

#### Michael Soegtrop (Sep 21 2022 at 08:38):

@Pierre Roux : can you explain a bit the nature of the troubles one can expect from importing GRing? A bit of background information would help.

#### Kazuhiko Sakaguchi (Sep 21 2022 at 08:47):

The GRing module serves as a namespace that qualifies constant names like GRing.add. Importing GRing makes those names unqualified, which is problematic. The lemmas related to GRing are declared both in GRing and GRing.Theory and you may import (only) the latter to shorten the names of those lemmas.

#### Pierre Roux (Sep 21 2022 at 08:57):

And to answer the initial question, the following seems to work:

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.algebra_tactics Require Import ring.

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

Import GRing.Theory Num.Theory.

Section First.

Local Open Scope ring_scope.

Variable F : realFieldType.

(* Could you be more precise than "pretty bad" ? What is it precisely
that you don't like ? what would you expect ? *)
Lemma test_without_telescope n :
\sum_(1 <= k < n.+1) 1 / (k * k.+1)%:R = 1 - 1 / n.+1%:R :> F.
Proof.
elim: n => [|n IHn]; first by rewrite big_nil; field.
rewrite big_nat_recr //= IHn.
field.
(* produces:
(2 + n%:R != 0) && (1 + n%:R != 0)
which I would have hoped to be handled by lia *)
rewrite -[1 in X in _ && (X + _ != _)]/(1%:R) -!natrD.
by rewrite -[0]/(0%:R) !eqr_nat.
Qed.


#### Pierre Roux (Sep 21 2022 at 08:59):

Fail rewrite natz. (* why does it fail? *)


I encourage you to

Set Printing All.
Check natz


showing (as the name suggest) that the equality is on int (whereas you equality is on the realFiledType RR)

#### Pierre Roux (Sep 21 2022 at 09:05):

Lemma test_with_telescope n: \sum_(1 <= k < n.+1) 1/(k * (k+1))%:R = 1-1/n.+1%:R :> RR.
Proof.
have simpl_elt_decomp k: 1/ (k * (k + 1))%:R = -1/(k+1)%:R - -1/k%:R.
Fail field. (* now field is failing me *)


the error message of field is pretty explicit: Cannot find a declared fieldType, indeed if you look carefully, your goal looks like

 _t_ : unitRingType
k : nat
============================
1 / (k * (k + 1))%:R = -1 / (k + 1)%:R - -1 / k%:R


and the equality is on _t_ (c.f. Set Printing All to confirm) which is only a unitRingType, not a fieldType. To fix this you have to write

have simpl_elt_decomp k: 1/ (k * (k + 1))%:R = -1/(k+1)%:R - -1/k%:R :> RR.


to have an equality on your fieldType RR

#### Pierre Roux (Sep 21 2022 at 09:34):

Well, actually, this

  (2 + n%:R != 0) && (1 + n%:R != 0)
(* which I would have hoped to be handled by lia *)


should rather wait for lra since the equalities are on some arbitrary ring. But lra would fail to solve them by losing the non negativity information for n. @Kazuhiko Sakaguchi would you have any idea how this should be solved?

#### Kazuhiko Sakaguchi (Sep 21 2022 at 09:42):

It seems to me that the best solution is to have a tactic for quantifier-free linear mixed integer arithmetic (#10741), although it is over-engineering if you just want to propagate positivity conditions from nat to F.

#### Kazuhiko Sakaguchi (Sep 21 2022 at 09:46):

Then we also need another preprocessing tool that subsumes the functionalities of both zify and Algebra Tactics... I will think about it.

#### Julien Puydt (Sep 21 2022 at 18:28):

Thanks for the help ; I find the statement looks pretty bad because having to pepper an expression with %:R isn't natural at all (pun intended). The need for :> RR at the end can be understood, but those %:R shouldn't be there.

#### Julien Puydt (Sep 21 2022 at 18:30):

I had to change a little your rewritings adding () -- for example: rewrite -[1 in X in _ && (_ + X != _)]/(1%:R) ; I'm using Coq 8.16.0 and MC 1.15.0.

#### Julien Puydt (Sep 21 2022 at 18:31):

I had to change to: have simple_elt_decomp (k: nat): (1 <= k)%N -> 1/ (k * (k + 1))%:R = -1/(k+1)%:R - -1/k%:R :> RR. (statement was false as written)

#### Julien Puydt (Sep 21 2022 at 18:40):

Sigh, and I apparently don't know how to use under eq_bigr => k do ...

#### Julien Puydt (Sep 21 2022 at 20:41):

Ah, calling eq_big_nat looks better!

#### Julien Puydt (Sep 21 2022 at 20:59):

I have working proofs ; but I'm pretty annoyed by how difficult telescoping is to use:

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.algebra_tactics Require Import ring.

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

Import GRing.Theory Num.Theory.

Section First.

Local Open Scope ring_scope.

Variable RR: realFieldType.

Lemma test_without_telescope n: \sum_(1 <= k < n.+1) 1/(k * (k+1))%:R = 1-1/n.+1%:R :> RR.
Proof.
elim: n => [|n Hn].
rewrite unlock //=.
by field.
rewrite big_nat_recr //= Hn.
field. (* there field does its job well! *)
rewrite -[1 in X in _ && (X + _ != _)]/(1%:R) -!natrD.
by rewrite  -[0]/(0%:R) !eqr_nat.
Qed.

Lemma test_with_telescope n: \sum_(1 <= k < n.+1) 1/(k * (k+1))%:R = 1-1/n.+1%:R :> RR.
Proof.
(* let's try to prepare the way *)
pose f: nat -> RR := fun k => (-1 / k%:R).
have simple_elt_decomp (k: nat): (1 <= k)%N -> f(k.+1) - f(k) = 1/ (k * (k + 1))%:R :> RR.
move=> kneq0.
unfold f.
field.
rewrite -[1 in X in (_ + X != _) && _]/(1%:R) -!natrD.
rewrite -[0]/(0%:R) !eqr_nat.
apply/andP ; split.
by case k.
by apply: lt0n_neq0.

under eq_big_nat => k /andP [kneq0 klen] do rewrite -simple_elt_decomp //=.
rewrite telescope_sumr.
unfold f.
field.
rewrite -[1 in X in (X + _ != _)]/(1%:R) -natrD -[0]/(0%:R) !eqr_nat //=.
by case n.
Qed.

End First.


#### abab9579 (Sep 21 2022 at 23:59):

Just curious, where is telescope_sumr lemma located?

#### Julien Puydt (Sep 22 2022 at 05:32):

@abab9579 in mathcomp/algebra/ssralg.v

#### abab9579 (Sep 22 2022 at 14:21):

Oh, strange that it did not appear in index.

#### Pierre Roux (Sep 22 2022 at 14:48):

Note that your proof can be simpplified a bit:

Lemma test_with_telescope n :
\sum_(1 <= k < n.+1) 1 / (k * k.+1)%:R = 1 - 1 / n.+1%:R :> RR.
Proof.
have simple_elt_decomp k : (1 <= k)%N ->
1 / (k * k.+1)%:R = -1 / k.+1%:R - -1 / k%:R :> RR.
move=> kne0.
by field; rewrite -[1 in X in X + _]/(1%:R) -natrD !pnatr_eq0 !lt0n_neq0.
under eq_big_nat => k /andP[? _] do rewrite simple_elt_decomp //.
rewrite telescope_sumr//.
by field; rewrite -[1 in X in X + _]/(1%:R) -natrD pnatr_eq0.
Qed.


The painful -[1 in X in X + _]/(1%:R) should be replaced by nat1r in future versions (c.f. https://github.com/math-comp/math-comp/pull/914 )

#### Pierre Roux (Sep 22 2022 at 14:50):

Julien Puydt said:

Sigh, and I apparently don't know how to use under eq_bigr => k do ...

Sometimes I just do under eq_bigr => k. try my thing, then over. to test before compressing into a one liner with under eq_bigr => i _ do rewrite...

#### Pierre Roux (Sep 22 2022 at 14:56):

Julien Puydt said:

I have working proofs ; but I'm pretty annoyed by how difficult telescoping is to use:

I don't see how we could get rid of the have eq : ... under ... rewrite eq, how would you like it to be easier? (I do agree the postprocessing of field is painful but that's pretty unrelated to telescope_sumr)

#### Pierre Roux (Sep 22 2022 at 15:02):

Julien Puydt said:

Thanks for the help ; I find the statement looks pretty bad because having to pepper an expression with %:R isn't natural at all (pun intended). The need for :> RR at the end can be understood, but those %:R shouldn't be there.

Well, k is a nat and we want a value in RR so we have to perform the injection in one way or another. Ideally this %:R would be a coercion (hence wouldn't have to be typed and wouldn't be displayed by default) but that's not possible for technical reasons (coercions in Coq require a constant output type (whereas RR is a section variable)).

#### Julien Puydt (Sep 22 2022 at 21:39):

@Pierre Roux I don't know how to quote as good as you but I'll try to answer:

1. I discovered how to do several-lines under by looking at the doc - I didn't know how to do that before as I hadn't seen it used in the code I studied - thanks for the tip ;
2. What I would like is try to apply telescope_sumr to sigma_{1 <= k < n.+1}u_k by giving it explicitly f, and it would give me as first goal to prove that for all k with 1 <= k < n.+1, indeed u_k=f(k.+1)-f(k) -- and have simplified my previous goal to f(n.+1)-f(1).
3. I know that Coq cannot guess every type, but I find it often unnerving how much help it needs: :> RR at the end of line should be pretty explicit on what is meant. :rolling_eyes:

#### Paolo Giarrusso (Sep 23 2022 at 04:49):

One reason why Coq can't infer :> RR here is because you're doing forward reasoning: by definition, that's not limited to subterms of the goal, so if you must mention a subterm, you have to duplicate it by hand. have isn't limited to subterms of the goal while set, rewrite, replace look at rhe goal at all. If you start by under eq_big_nat => k. you can probably do more backwards reasoning instead.

#### Paolo Giarrusso (Sep 23 2022 at 04:53):

(but I generally dislike forward reasoning since I've run into much worse duplication)

#### Pierre Roux (Sep 23 2022 at 08:26):

Julien Puydt said:

Pierre Roux I don't know how to quote as good as you

Hamburger icon on top right corner of the message you want to cite, then Quote and reply or forward (>) (or keyboard shortcut >)

#### Pierre Roux (Sep 23 2022 at 08:28):

Julien Puydt said:

1. I discovered how to do several-lines under by looking at the doc - I didn't know how to do that before as I hadn't seen it used in the code I studied

Yes we often compact the final code into one liners so the multi line form often doesn't appear in final scripts.

#### Pierre Roux (Sep 23 2022 at 08:30):

Julien Puydt said:

1. What I would like is try to apply telescope_sumr to sigma_{1 <= k < n.+1}u_k by giving it explicitly f, and it would give me as first goal to prove that for all k with 1 <= k < n.+1, indeed u_k=f(k.+1)-f(k) -- and have simplified my previous goal to f(n.+1)-f(1).

You can maybe do a lemma like telescope_sumr_eq : (forall k, (1 <= k < n)%N -> u_k = f _k.+1 - f k) -> \sum_(1 <= k < n) u_k = f n - f 1. If you find it useful, please open a pull request to add it to ssralg.v

#### Pierre Roux (Sep 23 2022 at 08:34):

Julien Puydt said:

1. I know that Coq cannot guess every type, but I find it often unnerving how much help it needs: :> RR at the end of line should be pretty explicit on what is meant. :rolling_eyes:

If you use %:R a lot inside a single section, you can maybe try to make it a coercion inside that section. But making it a more generic coercion seems difficult in the current state of Coq and would probably require developments in Coq itself. That could be an interesting development, but maybe a non negligible amount of work. Or maybe the new reversible coercion mechanism could help here? Not clear to me.

#### Pierre Roux (Sep 23 2022 at 08:39):

@Paolo Giarrusso indeed forward reasoning often leads to more duplication. However, it is a common practice in mathematical proofs and making cuts also helps cutting longer proofs in smaller bits, making them easier to understand / more maintanable. So I would say that the amount of have to use in a proof is a matter of trade off between maintanability and duplication.

Last updated: Jul 25 2024 at 15:02 UTC