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?

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

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