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