Hello, here is a simplified version of the types and functions I would like to design:

```
Inductive buffer (A : Type) : nat -> Type :=
| B0 : buffer A 0
| B1 : A -> buffer A 1.
Arguments B0 {A}.
Arguments B1 {A}.
Inductive decompose (A : Type) : nat -> nat -> Type :=
| F {size : nat} : buffer A size -> decompose A 0 size.
Arguments F {A size}.
Equations decompose_buffer {A : Type} {size : nat} :
buffer A size -> decompose A (size / 2) (size mod 2) :=
decompose_buffer B0 := F B0;
decompose_buffer (B1 a) := F (B1 a).
Equations test {A : Type} {size : nat} : buffer A size -> nat :=
test b with decompose_buffer b => { | F _ := 0 }.
```

Buffers are lists parametrized with their size. The decompose type is used to decompose sizes of buffers into their half and their parity.

Unfortunately, the `test`

function is not accepted, the following error is returned:

Unable to build a covering for with subprogram:

test A size b refine

In context:

A : Type size : nat b : buffer A size refine : decompose A (size / 2) (size mod 2)

And clauses: {A} {size} b (F _wildcard _wildcard0) := 0

Is there a way to overcome this issue ?

You have "green slime" in your indices, e.g. to match (size / 2) with 0 (from the constructor F) there is no obvious solution. One way is to rephrase `F {size size'} : size'= 0 -> buffer A size -> decompose A size' size`

so that matching always succeeds (because it's size', a variable, is matched agains (size / 2) now). Now you could rewrite with your equality.

I see, thank you !

Last updated: Oct 13 2024 at 01:02 UTC