coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Why can't I use an Inductive definition in a Module to satisfy a Module Type Parameter?

From: "Elie Soubiran" <elie.soubiran AT gmail.com>
To: mulhern <mulhern AT gmail.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Why can't I use an Inductive definition in a Module to satisfy a Module Type Parameter?
Date: Sun, 9 Jul 2006 14:35:09 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=DNCKvgRF63sanOfiWeBvKHCyg7515aBZ8SbetUd1FMrttBTCqQAGIHBKLiEa7KxokhkM8l6t3KUPFjrjUzvz86pmDov/9+M+t2tQBzKotFCDMXLoeatcnl4fO7gfeHk8jVhG8IilZ9Ud2LNnWoUi4yW/jkI1D7UAhOmfqm7q0gE=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

The module subtyping on signatures containing inductive types is less
flexible in the implementation than in the theory. Inductive types
cannot subsume types specified as Parameter due to the difference
between a term representing a constant and a term representing an
inductive.

On 7/8/06, mulhern
<mulhern AT gmail.com>
wrote:

Here is an example:

Module Type MT.
  Parameter A : Set.
  Parameter bp : A -> A -> Prop.
End MT.

Module M <: MT.
  Definition A := option nat.
  Inductive bp : A -> A-> Prop :=
    | BpNone : bp None None
    | BpSome : forall (n n' : nat), n = n' -> bp (Some n) (Some n')
  .
End M.

But I get an error:

User error: Signature components for label bp do not match

I change it thus:

Module Type MT.
  Parameter A : Set.
  Parameter bp : A -> A -> Prop.
End MT.

Module M <: MT.
  Definition A := option nat.
  Inductive bp' : A -> A-> Prop :=
    | BpNone : bp' None None
    | BpSome : forall (n n' : nat), n = n' -> bp' (Some n) (Some n')
  .
  Definition bp := bp'.
End M.

And I get no error.

Why do I need this extra level of assignment?

-mulhern

--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Coq-Club]Why can't I use an Inductive definition in a Module to satisfy a Module Type Parameter?, mulhern
- Re: [Coq-Club]Why can't I use an Inductive definition in a Module to satisfy a Module Type Parameter?, Elie Soubiran