Skip to Content.
Sympa Menu

coq-club - Re: A question on positivity conditions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: A question on positivity conditions


chronological Thread 
  • From: Hugo Herbelin <herbelin AT margaux.inria.fr>
  • To: sacerdot AT students.cs.unibo.it
  • Cc: coqdev AT pauillac.inria.fr
  • Subject: Re: A question on positivity conditions
  • Date: Fri, 28 Jan 2000 18:06:09 +0100 (MET)

  Dear Claudio,

> I have read the description of the positivity conditions required
> for an indutive definition, but I can't understand why in Coq the next
> definition is valid:
>
>  Inductive t : Type := k : (List t) -> t.
>
> where List is defined as usual as
>
>  Inductive List [T:Type] : Type :=
>     nil : (List T)
>   | cons : T -> (List T) -> (List T).
>
> Accordingly to the manual, t should appear only strictly positively in
> (List t), but it doesn't.
>
> Is Coq's implementation different from the theory or have I missed 
> something?

  The manual is late wrt the implementation. The positivity criterium
has been generalized. The up do date definition follows:

                                                  Hugo

-----------------
The constant X _occurs strictly positively_ in T in the
following cases:

-- T=(X t1 ... tn) and X does not occur in any of ti
-- T=(I a1 ... am t1 ... tn) where I is an inductive type not mutually
defined with m parameters and arity of length n, and X does not occur
in any of the ti but each constructor of I satisfies the weak
positivity condition after substituting the parameters by a_1 ...  a_n
-- T=(x:U)V and X does not occur in U but may occur strictly
positively in V.

The constant X _satisfies the weak positivity condition_ in t either
when t=[x:T]u and X occurs strictly positively in T and satisfies the
weak positivity condition in u, or when X satisfies the positivity
condition (defined as before) in t.





Archive powered by MhonArc 2.6.16.

Top of Page