The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Hi all,

Another question: Say I define natural numbers as usual, and also an
inductive definition which represents the proposition that two numbers
are not equal. Now, I want to define a list which will be associate a
natural number with a value of type ElemKind. In addition, I want to
define the list so that the cons requires that the new index is not
already in the list. It's easy to define notOcc as another inductive
definition, the problem being that the two definitions (List and
notOcc) depend on each other and Coq doesn't allow that (notice the
commented out part in the cons constructor). Anyone have experience or
thoughts on how to achieve this?

Inductive Nat : Set  := zero : Nat
                      | succ : Nat -> Nat.

Inductive notNatEq : Nat -> Nat -> Prop
   := zsucc : (n:Nat) (notNatEq zero (succ n))
   |  succz : (n:Nat) (notNatEq (succ n) zero)
   |  succsucc : (n,m:Nat) (notNatEq n m)->(notNatEq (succ n) (succ
m)).

Hypothesis ElemKind : Set.

Inductive List : Set
   := nil : List
   |  cons : (i:Nat; t:ElemKind; l:List (*; p:(notOcc i l)*)) List.

Inductive notOcc  : Nat -> List -> Kind
   := base : (n:Nat) (notOcc n nil)
   |  step : (n,i:Nat; t:Omega; l:List)
    (notOcc n l) ->
    (notNatEq n i) ->
    (notOcc n (cons i t l)).


Thanks for your suggestions,

--- nadeem