Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Records and Inductive definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Records and Inductive definitions


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Records and Inductive definitions
  • Date: Thu, 1 Oct 2015 15:22:13 +0200

On 01/10/2015 15:12, Petar Maksimovic wrote:
> I think that the length condition that I had (length lT = 1) is
> causing the issue, but I don't quite understand why.

Indeed, the problem is that the length mentions the type T, and not in a
strictly positive fashion, because length is essentially a fixpoint. The
manual describes what it means to be strictly positive here:

https://coq.inria.fr/refman/Reference-Manual006.html#sec199

As you can see, it is a syntactical approximation to ensure
productivity, and in particular it is only an under-approximation. Your
use case is perfectly sound semantically but not syntactically positive.

In your use case, you can workaround this limitation by using vectors
(which won't lack an occasion to make you regret to use them), in the
following way:

Require Vector.

Inductive T : Type :=
| T_main : Vector.t T 1 -> T.

The Vector.t type encodes in a positive fashion what you were looking
for. Yet, you're probably going to suffer if you wish to write dependent
programs.

Good luck,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page