The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

If you're willing to change "Base l: NList_ 0 l" to "Base: NList_ 0 nil", you can do it like so:

Goal forall A l n, @NList_ A n l -> length l = n.

Proof. induction 1. reflexivity. subst. reflexivity. Defined.

On Thu, Oct 3, 2013 at 11:01 AM, Fabien Renaud <Fabien.Renaud AT inria.fr> wrote:

Hello,

The subject of my question is not very clear but my problem yes:

For the illustration, suppose I have this (weird) inductive:

Inductive NList_ {A : Type} : nat -> list A -> Type :=
| Base l: NList_ 0 l
| Cons n l a: NList_ n l -> NList_ (S n) (a::l).

Now I want to start building NList_ such that the first argument is always the length of the list:

Definition NList {A : Type} (l : list A) := NList_ (length l) l.

Is there a way to state properties about NList_ created by NList like

forall l n, NList_ n l -> length l = n?

Thanks,

Fabien