The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Sep 01, 2005 at 03:56:06PM +0200, Lionel Elie Mamane wrote:

> m   : nat
> v   : vec Prop (S m)
> IHm : vec Prop (m) -> Prop
> ==================
> Prop
> 
> I'd like to destruct v into vcons a v', in order to do:
>  exact (a -> (IHm v')).
 
> But then I get this anomaly:

>> destruct v.
>> ^^^^^^^^^^
> Anomaly: Cannot take the successor of a non variable universes:

I noticed (helped by Pierre Courtieu) that the problem is more
subtle. Here is a minimal script that reproduces it:

Set Implicit Arguments.

Inductive vec : Type -> nat -> Type :=
  | vnil  : forall A:Type, vec A 0
  | vcons : forall A:Type, forall n:nat, A -> vec A n -> vec A (S n).

Definition vmap : forall A B:Type, forall f:A->B, forall n:nat, vec A n -> 
vec B n.
induction n.
intros; exact (vnil B).

intros va.
inversion va.
rewrite H in X0; rewrite H1 in X0; rewrite H in X.
rename A into a; rename X0 into va'.
clear H H1.
exact (vcons (f X) (IHn va')).
Defined.

Lemma f : forall m   : nat,
  forall v   : vec Prop (S m),
  forall IHm : vec Prop (m) -> Prop, Prop.
intros.
destruct v.


Note that:

1) Removing vmap: No anomaly

2) Adding "Reset vmap." before "Lemma f": Still anomaly!

3) If I define vect, vmap, then do "Reset Initial." then re-define
   vec, but not vmap, I still get the anomaly.

So it seems that the definition of vmap irremediably "clobbers" the
state of Coq in a way that is _not_ cancelled by Reset! Naively, I'd
call this a "Reset" bug... Defining something and then resetting it is
not equivalent to not defining it, which it is supposed to be, isn't
it?

-- 
Lionel