coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sylvain Boulme <Sylvain.Boulme AT imag.fr>
- To: S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>
- Cc: Coq <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Strange error message during inductive definition
- Date: Wed, 19 Nov 2003 17:40:50 +0100 (MET)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello.
Inductive types have syntactical restrictions to avoid paradoxes (see "A
Tutorial on Recursive Types in Coq" by Eduardo Giménez in the
documentation part of http://coq.inria.fr). For instance, assuming the
following (well-known) definition :
Inductive Absurd: Type :=
| cons_absurd: (Absurd -> False) -> Absurd.
we can build a proof of False :
Definition delta: Absurd -> False
:= [a:Absurd]Cases a of (cons_absurd f) => (f (cons_absurd f)) end.
Definition omega: False := (delta (cons_absurd delta)).
Fortunatly, this inductive definition is not syntactically correct.
The strange "_UNBOUND_REL_6" of your inductive definition may come from an
occurrence of "term s" as an implicit argument. With your inductive
definition, it is seems possible to replay the paradox above (in "delta"
definition, use "s" such "forall f. (arity s f)=O", and take a list of
size 1 for "l").
Yours.
S.
On Wed, 19 Nov 2003, Sébastien Hinderer wrote:
> Dear Coq users,
>
> Assume we have the following definitions :
>
> Inductive variable : Set := V : nat -> variable.
> Inductive function : Set := F : nat -> function.
> Definition signature := function -> nat.
> Definition arity := [s:signature;f:function] (s f).
>
> Then the following declaration is not accepted by Coq :
>
> Inductive term [s:signature] : Set :=
> | Var : variable -> (term s)
> | Fun :
> (f:function) (l:(list (term s))) (H:(length l)=(arity s f)) (term s).
>
> Coq 7.4 returns the following error message :
>
> Error: Non strictly positive occurrence of _UNBOUND_REL_6 in
> (f:function; l:(list (term s)))(length l)=(arity s f)->(term s)
>
> Does someone have an idea about what is wrong with the definition of term ?
>
> Thanks in advance,
> Sébastien.
> --------------------------------------------------------
> 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
>
______________________________________________________________________
BOULME Sylvain, ENSIMAG-LSR | e-mail :
Sylvain.Boulme AT imag.fr
BP-72 38402 St-MARTIN D'HERES | tel : 04-76-82-72-89, 06-86-24-41-70
- [Coq-Club] Strange error message during inductive definition, Sébastien Hinderer
- Re: [Coq-Club] Strange error message during inductive definition, Sylvain Boulme
- Re: [Coq-Club] Strange error message during inductive definition, Sylvain Boulme
- Re: [Coq-Club] Strange error message during inductive definition, Russell O'Connor
- Re: [Coq-Club] Strange error message during inductive definition, Sylvain Boulme
Archive powered by MhonArc 2.6.16.