The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear list

I'm trying to write a inductive in Prop (bigger than the one shown
below), but I can't match on one of the parameter:

<<<<<<
Variables A B: Type.
Variable PA: A -> Prop.
Variable PB : B -> Prop.

Inductive either : Type :=
| EA (a: A)
| EB (b: B).

Inductive P (e: either) : Prop :=
|P_intro:
  match e with
    | EA a => PA a
    | EB b => PB b
  end -> P e.

>>>>>>
leads to : Error: A parameter or name of an inductive type e must not
be used as a bound variable in the type of its constructor.


But if I write :

<<<<<<
Inductive P : either -> Prop :=
|P_intro: forall e,
  match e with
    | EA a => PA a
    | EB b => PB b
  end -> P e.
>>>>>>

or more strangely

<<<<<<
Inductive P (e: either) : Prop :=
|P_intro:
  match id e with
    | EA a => PA a
    | EB b => PB b
  end -> P e.
>>>>>>

where id is the identity function, everything works fine.

Is there a reason for such a limitation ?

Alexandre Pilkiewicz