Stream: Coq users

Topic: locks in mathcomp


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip 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)).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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].

view this post on Zulip Janno (Jul 01 2021 at 09:10):

Yeah that looks good!


Last updated: Jan 29 2023 at 01:02 UTC