The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Well, nothing is really "lost". If I am not wrong, you can still write an isomorphism between list1 and list.

That is: you can build two functions "f:∀ A, list1 A → list A" and "g:∀ A, list A → list1 A" such that you can prove in Coq:

"I1 : ∀ A (l:list A), f(g l) = l"

"I2 : ∀ A (l:list1 A), g(f l) = l".

But the induction principle is not as convenient in list1 than it is in list:

list1_ind : ∀ (P : ∀ A, list A  → Prop),

              (∀ A, P A (nil1 A)) →

              (∀ A l a, P A l → P A (cons1 A a l)) →

              ∀ l, P l.

list_ind : ∀ A (P : list A  → Prop),

             (P (nil A)) →

             (∀ l a, P l → P (cons A a l)) →

             ∀ l, P l.

Thus quantification over A is not at the same place.

Now imagine that you use "list1" instead of "list", and that you have proven "Q (nil1 X)" and "∀ x l, Q l → Q (cons1 X x l)" for given X and P. You think you can easily prove that "∀ l, Q l".

The truth is "yes, you can do it quite easily", but not as easily as if you were directly using "list" instead of "list1".

Indeed, in your concrete example, Q has not the "∀ A, list1 A → Prop" type, but "list1 X → Type".

Thus you will have to define something like:
"Let P A l := ∀ (H:X=A), Q (match H in _=a return list a with eq_refl => l end)."

And then use it with list1_ind, to get:

"Aux: ∀ l, P l" which can then be used to prove your theorem by "fun l => Aux X l (eq_refl X)".

2015-04-27 12:44 GMT+02:00 Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>:

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?