The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Consider the following two ways of defining the same relation:

(this relation is the parametricity translation of list)

Fixpoint list_RF (A A₂ : Type) (A_R : A -> A₂ -> Type) 

                                  (l : list A) (l₂ : list A₂) {struct l} :

   Type :=

   match l with

   | nil =>

       match l₂ with

       | nil => True

       | cons _ _ => False

       end

   | cons h tl =>

       match l₂ with

       | nil  => False

       | cons h₂ tl₂ =>

           A_R h h₂ * list_RF A A₂ A_R tl tl₂

       end

   end.

Inductive list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) : list A₁ -> list A₂ -> Type :=

| nil_R : list_R A₁ A₂ A_R nil nil

| cons_R : forall (h : A₁) (h₂ : A₂),

    A_R h h₂ ->

    forall (tl : list A₁) (tl₂ : list A₂),

    list_R A₁ A₂ A_R tl tl₂ -> list_R A₁ A₂ A_R (cons h tl) (cons h₂ tl₂).

Template Polymorphism works better for the latter definition:

Fail Check  ((list_RF nat nat (fun _ _ => True) nil nil):Set).

Check  ((list_R nat nat (fun _ _ => True) nil nil):Set).

Is there a way to make the first Check succeed?

Is there a theoretical problem in making the Check succeed, or just something that hasn't been implemented yet?

Although this is a simple example, in case of indexed inductives, I find the 

first style (using Fixpoint instead of Inductive) much easier to use.

Is there some documentation for template polymorphism?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/