Is it possible to define in Coq the set of all prefix-free partial recursive functions? Thanks.

Hi all,

I have a recursive function defined as follows (I simplified it here, but a complete version does terminate)

Inductive vec A : nat -> Type :=

| vnil : vec A O

| vcons {n} (x : A) (xs : vec A n): vec A (S n).

Definition mtx (A:Type) (r c : nat) : Type := vec (vec A c) r.

In this setting, I am trying to define a function similar to the following.

Fixpoint get_nth_col {r c l: nat} (n : nat) (M: mtx nat r c)

(col : vec nat l) : vec nat (l+1) := get_nth_col n M col ++ [1].

But I have this error

The term "get_nth_col r c l n M col ++ [1]" has type "vec nat (l + 1 + 1)"while it is expected to have type "vec nat (l + 1)".

I am not sure how to fix this. I appreciate any help here.

it looks like you are getting stuck with dependent pattern matching. The default community answer is to use Equations to define the function: https://github.com/mattam82/Coq-Equations (also part of the Coq Platform)

Maybe you have simplified your function too much. I cannot guess any decreasing argument.

If you declare that `get_nth_col n M col`

is a vector of length `l+1`

, then your function body returns a vector of length `l+1+1`

. But this contradicts the header ...

right, it may be best to define an explicit well-founded relation and use it via Equations (`Equations ... : ... by wf ...`

)

Pierre Castéran said:

Maybe you have simplified your function too much. I cannot guess any decreasing argument.

If you declare that`get_nth_col n M col`

is a vector of length`l+1`

, then your function body returns a vector of length`l+1+1`

. But this contradicts the header ...

I see the problem now. I might have to use equations as Karl Palmskog suggested. I never used them and will start working on it.

Last updated: Jan 29 2023 at 04:05 UTC