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