The Coq mailing list

[Théo Zim <theo.zim AT free.fr>]

Hi,

One difference between the two definitions (with or without parameter) would be the form of the induction principle which you can check by doing

Check list1_ind.

In the parametrized case, the induction principle is simpler.

About the loss of information, I think that the manual is trying to say that the type (list A) itself has an inductive definition, exactly as if you had defined it like that:

Section lists.

  Variable A : Type.

  Inductive listA : Type :=

    | nilA : listA

    | consA : A -> listA -> listA.

End lists.

Whereas it would not be the case with a type that cannot be parametrized such as "lists of length n" :

Inductive listN : nat -> Type :=

  | nilN : listN 0

  | consN : forall (n : nat), nat -> listN n -> listN (S n)

(here I have assumed that the lists contained integers).

Hope that this clarifies,

Theo

Le lun. 27 avr. 2015 à 12:44, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> a écrit :

Hi,

I am reading the Reference Manual
(Section 4.5.1 : Representing an inductive definition)
(subsection : Inductive definitions with parameters)
https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#sec190

I would like to ask a question concerning this passage:

        "Generally one want consider lists of elements of different types.
         ...
         One possible way to do that would be to define the type List inductively
         as being an inductive family of type Set → Set:

           Ind()(List : Set → Set := nil : (∀ A : Set, List A), cons : (∀ A : Set, A → List A → List A))

         There are drawbacks to this point of view.
         The information which says that for any A, (List A) is an inductively defined Set *has be lost*.
        "

The last sentence is used as a motivation for the need to discriminate between parameters and arguments.
I am not sure if I understand the argument.

If I consider a concrete example (corresponding to the above definition):

        Inductive list1 : Type -> Type :=
        | nil1 : forall A : Type, list1 A
        | cons1 : forall A : Type, A -> list1 A -> list1 A.

I fail to see what is "lost".

I can construct values of this type:

        Check nil1 nat.
        Check cons1 nat 5 (nil1 nat).

I can work with those values normally.
E.g.:

        Definition is_empty (A:Type) (l : list1 A) :=
          match l with
          | nil1 _ => true
          | cons1 _ _ _ => false
          end.

        Compute is_empty nat (nil1 nat).
        Compute is_empty nat (cons1 nat 5 (nil1 nat)).


I am curious, why is "list1" as defined above inferior to "list" as it appears in the standard library?