Hi All,

I am trying (as a training exercise) to make the following computation in Coq, but I did not get the final answer. It seems that I need to unlock bigop. In a Lemma, I think that I now how to do that, but in a Compute command, I did not manage to do it. Here it is the simple code:

```
From mathcomp Require Import all_ssreflect.
Compute
\sum_( 1 <= i < 10) i.
```

What is the right way to get the full computation ?

The following (from @Erik Martin-Dorel ) works

```
From mathcomp Require Import all_ssreflect.
Ltac reduce e :=
let e := eval hnf in e in
match e with
| context B [BigOp.bigop] =>
let t := context B [reducebig] in
reduce t
| ?failure => exact failure
end.
Definition example := \sum_(1 <= i < 10) i.
Eval compute in ltac:(reduce example).
```

but bigop are designed for proofs, not for actual computations.

Thanks, it works. I am wondering if there is a variant solution using something like `rewrite !unlock`

on `example`

before evaluating it that avoid an explicit transformation of `BigOp.bigop`

into `reducebig`

.

As far as I know, you cannot do this using the `Compute`

command. However, you an do something like this:

```
Lemma foo : exists n, \sum_( 1 <= i < 10) i = n.
eexists.
rewrite unlock.
cbv. (* goal is 45 = ?n *)
```

This here might be a tad shorter (especially if you keep the tactic notation somewhere in a utilities library):

```
From mathcomp Require Import all_ssreflect.
Tactic Notation "unlock" open_constr(x) :=
let n := open_constr:(_ : _) in
assert (x = n);[rewrite !unlock; compute; reflexivity|exact n].
Compute ltac:(unlock (\sum_( 1 <= i < 10) i)).
```

When I replace in the solution of @Janno the last line by `Compute ltac:(unlock example).`

with `example`

previously defined as `Definition example := \sum_(1 <= i < 10) i.`

I got the error

```
The LHS of unlock
(unlocked _)
does not match any subterm of the goal
```

I did not see why.

Because the locked term is hidden behind a definition (`example`

) and rewrite only works on the surface of the term. You could always throw in a another `compute`

before the `rewrite`

step.

In fact, the best solution is probably to do this in a loop until the second `compute`

step doesn't make progress anymore.

Do you mean something like that ?

```
Tactic Notation "unlock" open_constr(x) :=
let n := open_constr:(_ : _) in
assert (x = n);[repeat progress (compute;rewrite !unlock); compute; reflexivity|exact n].
```

Yeah that looks good!

Last updated: Oct 03 2023 at 04:02 UTC