change the implicit arguments of big cat nat

[KimayaBedarkar]

Motivation for this change

The current way arguments for the lemma big_cat_nat are declared makes it hard to use the lemma in developments. This MR changes the arguments that are considered implicit and explicit for the lemma.

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

~- [ ] added corresponding documentation in the headers~

• [x] tried to abide by the contribution guide
• [x] this PR contains an optimum number of meaningful commits

[proux01]

This is missing a changelog entry. If we want to do this (still a bit unclear to me, it's not consistent with common lemmas like leq_trans for instance) this will require a few overlays according to CI.

[CohenCyril]

This change is indeed not consistent with many lemmas. The hypotheses of the form _ <= _ can often be discharged with // instead, making it less essential direct access to these particular arguments. @KimayaBedarkar could you please show a few places where you find it "it hard to use"?

[proux01]

Ping @KimayaBedarkar , should we close this?

[KimayaBedarkar]

This change is indeed not consistent with many lemmas. The hypotheses of the form _ <= _ can often be discharged with // instead, making it less essential direct access to these particular arguments. @KimayaBedarkar could you please show a few places where you find it "it hard to use"?

Yeah sure. Maybe I am missing something here because this seems to be the generic style in mathcomp but my problem is as follows:

Lemma test (t_mid t1 t2 : nat) (f : nat -> nat) :
  (forall t, t1 <= t <= t_mid -> f t = 0) ->
  t1 <= t_mid < t2 ->
  \sum_(t1 <= t < t2) f t = \sum_(t_mid.+1 <= t < t2) f t.
Proof.
  move => ZERO RANGE.
  have INEQ : t_mid.+1 <= t2 by lia.
  rewrite (big_cat_nat _ _ _ _ INEQ) //=; last lia.
Abort.

I have now memorized that I have to put 4 underscores before my inequality. Then, a lot of times I do not have the exact inequality in my context but I have to use have and lia to get exactly what I want. What am I missing here?

What would be a better way to use big_cat_nat?

I also don't understand why the operator type is an explicit parameter.

[proux01]

We could do the following

From mathcomp Require Import all_ssreflect.

Lemma test t_mid t1 t2 f :
    (forall t, t1 <= t <= t_mid -> f t = 0) ->
    t1 <= t_mid < t2 ->
  \sum_(t1 <= t < t2) f t = \sum_(t_mid.+1 <= t < t2) f t.
Proof.
move=> f0 /andP[t1mid tmid2].
rewrite (big_cat_nat _ _ _ _ tmid2)/=; last exact: ltnW.
under eq_big_nat => i /andP[t1i /(eqbLR (ltnS _ _))/(conj t1i)/andP ?]
  do rewrite f0//.
by rewrite sum_nat_const_nat muln0 add0n.
Qed.

but I agree that if we consider big_cat_nat is to be used mostly with rewrite, then

Arguments big_cat_nat [R]%type_scope [idx op] [n m p]%nat_scope [P] [F]%function_scope _ _

would probably be more convenient than the current

Arguments big_cat_nat [R]%type_scope [idx] op [n m p]%nat_scope P F%function_scope _ _

(FWIW, the following variant of the lemma seems easier to prove

From mathcomp Require Import all_ssreflect.

Lemma test' t_mid t1 t2 f :
    (forall t, t1 <= t < t_mid -> f t = 0) ->
    t1 < t_mid <= t2 ->
  \sum_(t1 <= t < t2) f t = \sum_(t_mid <= t < t2) f t.
Proof.
move=> f0 /andP[t1mid tmid2].
rewrite (big_cat_nat _ _ _ (ltnW t1mid))//= (eq_big_nat _ _ f0).
by rewrite sum_nat_const_nat muln0 add0n.
Qed.

)

[KimayaBedarkar]

I am also a bit confused about why the operator type is an explicit parameter. Why is this needed to be explicit?

[proux01]

Sorry for the delay, I rebased and addressed the comments.

I am also a bit confused about why the operator type is an explicit parameter. Why is this needed to be explicit?

The automatic determination of implicit arguments is explained in details in Rocq's refman: https://rocq-prover.org/doc/V9.0.0/refman/language/extensions/implicit-arguments.html but basically, here R is made implicit because it appears in the type of idx which is itself implicit because it appears in the type of op and n, m and p are implicit because they appear in the inequalities n <= m and m <= p. But the mechanism doesn't see that the lemma is an equality whose left-hand-side contains op, P and F and doesn't make them implicit by default.

Anyway, if there is no disagreement and CI is happy, I'll merge this as it is, we've left this PR open for way too long.

[pi8027]

I have the impression that what this PR does is not very principled and I prefer to discuss it during the MathComp Sharing Day tomorrow.

[proux01]

I agree that there is (a lot of) room for improvement. But I also think this PR remains an improvement per se.

[proux01]

Thanks for the PR and sorry that it took us that long to merge it (quite ashamed of that)