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:
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 ;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).:> 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: Oct 13 2024 at 01:02 UTC