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

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: Apr 19 2024 at 21:01 UTC