Stream: Coq users

Topic: ✔ Strict positivity problem

Stéphane Desarzens (Apr 04 2023 at 06:42):

I'm trying to define a type for arbitrary terms (for universal algebra) and got stuck with the positivity checker.
The following is allowed.

From Coq Require Import Vector.
Inductive tree :=
| tree_ctr (n : nat) (branch : Vector.t tree n).

But the following, which I'd like to do, is not.

Fixpoint Power (A : Type) (n : nat) : Type :=
  match n with
  | O => unit
  | S n =>
      A * Power A n
  end.
Fail Inductive tree :=
| tree_ctr (n : nat) (branch : Power tree n).

And for some reason it is permitted to use Power if n is constant.

Inductive tree :=
| tree_ctr (branch : Power tree 5).

I'm not sure what the problem is, because Power and Vector.t have the same type. Is there some reason for this behavior and/or some workaround?

Stéphane Desarzens (Apr 04 2023 at 06:55):

Found Issue 1433 mentioning this. It seems that this is currently not possible. I think I'll go with the Vector based solution and use the natural bijection between Vector.t A n and Power A n to transform between them.

Notification Bot (Apr 04 2023 at 06:55):

Stéphane Desarzens has marked this topic as resolved.

Last updated: Apr 16 2024 at 19:01 UTC