Stream: Coq users

Topic: Function dependent on list value

Julin Shaji (Nov 20 2023 at 13:24):

I had been trying to make function whose return type is dependent on a list.

Like this:

Require Import List.
Import ListNotations.

Inductive enum (A: Type): list A -> Type :=
| Zero: forall ls:list A,
    enum A ls
| More: forall (ls:list A) (a:A),
    enum A (a::ls).

Fixpoint foo (n:nat): forall ls:list nat, enum nat ls :=
  match n with
  | O => fun ls => Zero _ ls
  | S n' => fun ls => (* More _ ls n' *)
  end.
(*
In environment
foo : nat -> forall ls : list nat, enum nat ls
n : nat
n' : nat
ls : list nat
The term "More nat ls n'" has type "enum nat (n' :: ls)"
while it is expected to have type "enum nat ls".
*)

But couldn't do it.

How can such a function be defined?

The return type is dependent on a list which won't be same for all possible constructors.

Kenji Maillard (Nov 20 2023 at 13:49):

The return type of foo states that it will return an enum for any n: nat and ls : list nat, while your comment seem to indicate that you have a specific list in mind (possibly defined using n : nat). Is this really the type you want to inhabit ?

Andrey Klaus (Nov 20 2023 at 13:54):

this foo compiles.. but I'm not sure it is what you would like to have in result.

Fixpoint foo (n:nat): forall ls:list nat,
    match n with O => enum nat ls | S n' => enum nat (n'::ls) end
      :=
  match n with
  | O => fun ls => Zero _ ls
  | S n' => fun ls => More _ ls n'
  end.

Julin Shaji (Nov 20 2023 at 16:48):

Kenji Maillard said:

Is this really the type you want to inhabit ?

I wasn't sure if that's how the type should be stated, to be honest..

I have a type depedent on a list. While values of this type are being built, the list changes. And this causes a type mismatch.

I wanted to skirt around this problem.

That's what I wanted to show with this example. Not sure how well I expressed it..

Julin Shaji (Nov 20 2023 at 16:49):

Andrey Klaus said:

this foo compiles.. but I'm not sure it is what you would like to have in result.

Fixpoint foo (n:nat): forall ls:list nat,
    match n with O => enum nat ls | S n' => enum nat (n'::ls) end
      :=
  match n with
  | O => fun ls => Zero _ ls
  | S n' => fun ls => More _ ls n'
  end.

Is it possible to use the foo as a recursive call inside the first match as well?

Andrey Klaus (Nov 20 2023 at 21:11):

Julin Shaji said:

Is it possible to use the foo as a recursive call inside the first match as well?

I do not think so. What problem do you try to solve?

Kenji Maillard (Nov 21 2023 at 09:36):

You cannot use foo in its own type but you could first define the list employed in the type of foo by induction on n:nat and then implement a variant of foo:

Fixpoint downToZero (n : nat) : list nat :=
  match n with
  | 0 => []
  | S n => n :: downToZero n
  end.

Definition foo (n : nat) : enum nat (downToZero n) :=
  match n as k return enum nat (downToZero k) with
  | 0 => Zero nat []
  | S n => More nat (downToZero n) n
  end.

By the way, if you want enum to actually enumerate/frame a prefix of your list, you should probably have a recursive occurence in the constructor More, e.g.:

Inductive enum (A: Type): list A -> Type :=
| Zero: forall ls:list A,
    enum A ls
| More: forall (ls:list A) (a:A), enum A ls ->
    enum A (a::ls).

Last updated: Oct 13 2024 at 01:02 UTC