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.
(* that looks pretty bad already *)
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? *)
Admitted.
(* same bad-looking statement *)
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.
```

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

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)

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

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.

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.
(* that looks pretty bad already *)
(* 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.
```

To answer that one:

```
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`

)

To answer that one

```
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

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?

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`

.

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

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.

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.

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)

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

Ah, calling `eq_big_nat`

looks better!

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.
(* that looks pretty bad already *)
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.
(* same bad-looking statement *)
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.
```

Just curious, where is `telescope_sumr`

lemma located?

@abab9579 in `mathcomp/algebra/ssralg.v`

Oh, strange that it did not appear in index.

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 )

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

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)

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

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

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

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.

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

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 `>`

)

Julien Puydt said:

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

Julien Puydt said:

- 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

Julien Puydt said:

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

@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