The Coq mailing list

[Fabien Renaud <Fabien.Renaud AT inria.fr>]

I know that in my example the property is not true in general.

I would like to know if there is a way to restrict the statement on
NList_ which have been created by NList (for which the statement is true).

On Thu, Oct 3, 2013 at 1:32 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

But I'm able to disprove your assertion.

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

Proof.

intro H1.

pose proof (H1 nat) as H2.

pose proof (H2 (cons 0 nil)) as H3.

pose proof (H3 0) as H4.

pose proof @Base as H5.

pose proof (H5 nat) as H6.

pose proof (H6 (cons 0 nil)) as H7.

pose proof (H4 H7) as H8.

simpl in H8.

discriminate H8.

Defined.

On Thu, Oct 3, 2013 at 12:17 PM, Fabien Renaud <Fabien.Renaud AT inria.fr> wrote:

This is an illustration of my problem and in my case I cannot change it.

On Thu, Oct 3, 2013 at 12:44 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

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