## Stream: Coq users

### Topic: locks in mathcomp

#### Jérôme Leroux (Jun 29 2021 at 09:25):

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 ?

#### Pierre Roux (Jun 29 2021 at 09:57):

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.

#### Jérôme Leroux (Jun 29 2021 at 10:57):

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.

#### Christian Doczkal (Jun 29 2021 at 11:30):

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 *)


#### Janno (Jun 29 2021 at 14:23):

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)).


#### Jérôme Leroux (Jul 01 2021 at 08:57):

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.

#### Janno (Jul 01 2021 at 08:58):

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.

#### Janno (Jul 01 2021 at 08:59):

In fact, the best solution is probably to do this in a loop until the second compute step doesn't make progress anymore.

#### Jérôme Leroux (Jul 01 2021 at 09:07):

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].


#### Janno (Jul 01 2021 at 09:10):

Yeah that looks good!

Last updated: Oct 03 2023 at 04:02 UTC