The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

You mean "forall A (a : A) l, NList l <-> NList (a :: l)"?

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

Let me rephrase my question.

I have an inductive datastructure for which a property is not true.
However, for some elements (whose shape is given by some definition), the property is true and preserved by all the rules of the inductive.

Now I would like to state this and prove it.

In my previous example this means that all the nodes NList_ n l of a derivation tree starting from NList satisfy the property that (length l = n).

How can I state this?

On Thu, Oct 3, 2013 at 1:54 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 10/03/2013 01:49 PM, Robbert Krebbers wrote:

The best result you well get in this case is:

   Goal forall A (l : list A) n, NList_ n l -> n <= length l.
   Proof. induction 1; simpl; auto with arith. Qed.

... because

Goal forall A (l : list A) n, n <= length l -> NList_ n l.
Proof.
  intros A l n; revert l. induction n as [|n]; [constructor|].
  intros [|??]; simpl; [omega|]. constructor; auto with arith.
Qed.