The Coq mailing list

["Lehner Hermann" <hermann.lehner AT inf.ethz.ch>]

Dear Coq-Club

It seems that i've simplified my example a little bit too much. Here is a 
different version, from which i derived the latter example:

I've got three inductive definitions that depend on each other. I choose to 
define two of them together by using 'with', and to define a third one later 
in the development and pass it as parameter v outside section 'sec'. 

Coq claims that  Ind2 is not used strictly positive. 

I'd be very grateful for any explanations of this behavior. Thanks!


Section sec.

Variable v : Prop.

Inductive Ind1 : Prop :=
| a:  v -> Ind1
| b: Ind3 -> Ind1
with Ind3 : Prop :=
| c: Ind1 -> Ind3.

End sec.

Inductive Ind2: Prop :=
| d: Ind1 Ind2 -> Ind2.






-----Original Message-----
From: Hermann Lehner 
[mailto:hermann.lehner AT inf.ethz.ch]
Sent: Fri 22.01.2010 14:40
To: Coq Club
Subject: [Coq-Club] Inductive Definitions and Positive Occurrences (again)
 
Dear all,

There were already some discussions about similar issues, however, I 
can't explain the following.

I'm aware that the example doesn't make sense, but it shows the essence 
of a problem that i've got in a development of mine of a much larger scale.

(* The following doesn't work (Coq 8.2pl1) *)

Inductive i1 (t : Type) :=
      with i2 (t : Type) :=.
Inductive i3 :=
| def: i1 i3 -> i3.


Here, I get a "Non strictly positive occurence" Error.


The following similar constructs work fine, and I can't see the 
conceptual difference.

(* This works *)
Inductive i1 (t : Type) := .

Inductive i3 :=
| def: i1 i3 -> i3.


(* This works too *)
Inductive i1 :=
with      i2 :=
with      i3 :=
| d: i1 -> i3.



Anyone a clue? Thank!

Hermann

-- 
http://www.pm.inf.ethz.ch/people/lehnerh