Chapter 1, section 1.6 : given \sum_ doesn't work

[SnarkBoojum]

Reading chapter 1 section 1.6 of the mathcomp book, there is a definition of \sum_, but trying to experiment with it gets ugly:

• I tried to first Compute \sum(0 <= i < 5) (i*i). before entering this definition (I saw \sum existed already), and it didn't give me a straight answer (I would say something makes it lazily evaluated ; it's my second reading so I think there was something about big operators later on -- a new reader will probably be more annoyed) ;
• I then proceeded to enter the definition of \sum_ in the text : refusal because it already exists (d'oh!), then after renaming refusal because it lacks a level : "(at level 0)" makes it pass ;
• I was still unable to make it compute a simple sum, because of a syntax error : '<=' expected after [constr:operconstr level 200] (in [constr:operconstr]) - and there I didn't find how to get away with it.

[SnarkBoojum]

Here is a minimal example to reproduce ; I'm using mathcomp 1.12.0 et coq 8.12.0 (Debian box) :

 From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section chapitre_1.
  Compute \sum_(0 <= i < 5) (i*i). (* le \sum_ de mathcomp n'est pas simplifié! *)

  Notation "\chap1_sum_ ( m <= i < n ) F" :=
    (foldr (fun i a => F + a) 0 (iota m (n-m)))
    (at level 0). (* j'ai dû rajouter ça sinon ça coince! *)
  (* Compute \chap1_sum_ (0 <= i < 5) (i*i). le \sum_ du texte ne marche pas! *)

  Compute (foldr (fun i a => i*i+a) 0 (iota 0 5)).
End chapitre_1.

[gares]

All the snippets are now online with a context which makes them work, here the one about ch1: https://math-comp.github.io/mcb/snippets/ch1.html

[SnarkBoojum]

Nice, but I'm trying to read the text with coqide on my second screen, and that isn't working : what's wrong in my context that makes things fail?

[ybertot]

The initial intent was that code snippets from chapter 1 have to be all be executed in the order they appear in the chapter for the experiment to work to the end of the chapter.

If you do follow this discipline, the objects that you are referring to later are the ones that you defined yourself, not the ones that are pre-existing (in fact the pre-existing ones are still around, they can only be accessed using a longer name). The ones that are you are defining can compute, but the pre-existing ones often have extra features attached to them, like the feature of having their execution blocked. At the moment of writing an introductory chapter, it is very difficult to explain this without getting beginners drown in details.

So, if you want to play the code in your own instance of coqide, the right way to do it is to look at the page that was given above: https://math-comp.github.io/mcb/snippets/ch1.html and to copy-paste all the code from the beginning of the file to the definition you are interested in in your coqide buffer. You can then experiment with the defined functions and they will behave in a manner that is consistent with the explanations of that chapter.

At the moment of writing an introductory chapter, it is very difficult to explain this without getting beginners drown in details. The fact that you did not follow the process we intended is a sign that our explanations are not clear enough. Thanks for the feedback.

[SnarkBoojum]

Now I find this very confusing : I tried to match my minimal problem sample to the official snippet code: it seems the renaming of \sum_ to \chap1sum explains both the need to add level 0 and the syntax error at compute-time ; so in a sense the "\sum" is triggering magic. I'm pretty sure I had an error about redefining \sum_ yesterday, which is the reason why I renamed it in the first place and not this morning.

I remember from my first read a few months ago that there's something about big ops later on in the book ; perhaps it's too early to mention them at that point?

[ybertot]

yes, there is some untold truth here, which I had forgotten to explain (untold knowledge is often called magic).

The notation system is pretty much imperative: once a notation is defined, it is placed in a "syntax level" and so are its arguments. So, what you do in your script, is to say that you are going to reuse the notation "\sum_ ..." that is already declared in all_ssreflect (more precisely in bigop, which is loaded by allsreflect), but attach it to a function of your choice. So you can already type "\sum ..." and by default it maps to the math-comp bigop function. Once you add the notation declaration as in the snippet code, you attach it to the foldr construction. Is this clearer?

And yes, I would be wary of mentioning the bigop constructions at this point, but maybe a short sentence like "we are now going to use a notation that is defined precisely in bigop and attach it to our function."

It may be that the whole bad experience that you had will be avoided if we explain clearly that the snippets have to be followed precisely, without explaining why they have to. This way, in case of failure, you do not try to find a turnaround like the one you had with \chap1sum.

[ybertot]

Just for your information, this is how the specific sum notation that is used in chapter 1 is declared, in file bigop.v

Reserved Notation "\sum_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \sum_ ( m  <=  i  <  n ) '/  '  F ']'").