Stream: math-comp users

Topic: Computing on code that uses views


view this post on Zulip Valentin Robert (Mar 19 2024 at 00:32):

If I write the following:

From mathcomp Require Import ssreflect tuple.

Definition Bits n := n.-tuple bool.
Definition getLo : Bits 2 -> Bits 1.
  case /tupleP => _.
  case /tupleP => a _.
  exact ([tuple a]).
Defined.

Definition v : list bool := tval (getLo [tuple false;true]).

Eval compute in v.

The result at the end does not reduce to a canonical form of a list bool.

Is there something I can do, either by defining getLo differently, or by invoking computation differently, so that I end up with a fully-computable result at the end?

view this post on Zulip Pierre Roux (Mar 19 2024 at 08:25):

That's because tupleP is opaque (it's designed to write proofs more than programs), not using it works fine:

From mathcomp Require Import ssreflect tuple.

Definition Bits n := n.-tuple bool.

Definition getLo : Bits 2 -> Bits 1.
move=> [[//| _ [//| a _]] _]; exact: [tuple a].
Defined.

Definition v : list bool := tval (getLo [tuple false;true]).

Eval compute in v.

view this post on Zulip Karl Palmskog (Mar 19 2024 at 08:49):

I think it's becoming standard advice at this point: if you want to compute with MathComp definitions and can't get away from some opaque/locked constant, best to first refine them to a compute-friendly representation via something like CoqEAL or (more experiementally) Trocq.


Last updated: Jul 23 2024 at 20:01 UTC