## Stream: Coq users

### Topic: Recursive functions

#### Rafael Garcia Leiva (Jul 30 2020 at 09:19):

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

#### GTR (Jun 27 2022 at 18:48):

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

But I have this error

The term "get_nth_col r c l n M col ++ " 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.

#### Karl Palmskog (Jun 27 2022 at 18:56):

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)

#### Pierre Castéran (Jun 27 2022 at 19:37):

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

#### Karl Palmskog (Jun 27 2022 at 19:40):

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

#### GTR (Jun 27 2022 at 20:18):

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: Oct 03 2023 at 19:01 UTC