Q: working example with simplified version, but not the complete one

[SnarkBoojum]

In the "Iterators and mathematical notations" section, a trivial \sum_ notation is introduced and gives working examples.

If I try the same examples with the \sum_ in mathcomp using the bigop machinery, the computations don't get simplified ; more specifically Compute \sum_ (1 <= i < 5) i. gives: = \big[(fix Ffix (x0 x1 : nat) {struct x0} : nat := match x0 with | 0 => x1 | x2.+1 => (Ffix x2 x1).+1 end)/0]_(x <- [:: 1; 2; 3; 4]) x : nat instead of the expected 10 : nat.

Why?

[gares]

these notations are locked in real mathcomp. you can use unlock to have them compute. finally their actual implementation is a bit more complex to address notational issues.

[SnarkBoojum]

How am I supposed to unlock? I found the documentation for the unlock tactic, but that's used in a proof, not in a computation...

[gares]

Oh yes, unlock can only be used in proofs. I don't know exactly your use case, but Compute is also a tactic (actually called vm_compute). You can put the \sum in a lemma statement if you want to have it compute.

The reason why things are locked is indeed that there is a trade off. Most of the times the iterated op is not fully explicit, and computation steps are better controlled via rewriting. At the same time you require extra work to make simple examples.

Later in the book, section 5.7.1, we document the (almost the) real definition of iterated operations. In the first chapter we give a simplified version, that is more natural (and computes) but is less "robust" when you do proofs. It is a general pattern in the book, we gave ourselves the freedom to hide details in part 1.

[SnarkBoojum]

I'm on the second reading, and I don't remember anything about unlock anywhere...

I'll report here when I'll have reached section 5.7.1 too ; perhaps it does answer my question.

[SnarkBoojum]

Indeed reading 5.7 I could get things going with:

Lemma somme n: \sum_ (0 <= i < 5) (i ^ 2) == n.
Proof.
rewrite unlock //=.
compute.

Which leaves me to try to basically prove 30 == n ; which shows the result.

Thanks!