The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Hi,

On 08/20/2010 12:34 PM, Evgeny Makarov wrote:
> I don't have the solution, but this does look strange. If there are
> two snippets of code of which only one works and which differ only in
> "match e with" and "match id e with", then it looks like Coq does not
> have the subject reduction property...

Coq does fail to enjoy the subject reduction property, but not for that 
reason. (Search in this mailing list archive about coinductive types...)


On 08/18/2010 06:04 PM, Alexandre Pilkiewicz wrote:
> <<<<<<
> 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.
>

Expressions like  match e with ... end
are not pure CIC expressions: they need elaboration, for instance to 
determine the "elimination predicate" (the P variable in the either_rect 
constant) or the return clause of the match.

When you do a match on a variable (as opposed to (id e)), it is 
understood as  match e as e return Q(e) with ... end
where Q(e) is the return type, abstracted over e to express the 
dependency, and the system does its best to guess Q.

As you see, the interface is adding for you a binder with name e. In 
general this is a bad thing when a binder shadows a parameter in a 
constructor type, because this might prevent you from writing any 
instance of your inductive type under that binder (inductive P must be 
applied to parameter e, but e is now bound to something else).

This is too defensive here since we don't need to invoke P, and in fact 
positivity prevents you from using P in that position! So the error 
should at most be a warning, but since the binder is not introduced by 
the user, it should be accepted silently.


>
> 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.
>>>>>>>

Accepted because you don't hide a parameter.

>
> 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.
>>>>>>>

Accepted because the system does not create a binder with name e.

> Is there a reason for such a limitation ?

No good reason, besides the explanation above.
You could report this to coq-bugs so that it eventually gets fixed. 
Meanwhile, you can force Coq to choose another name for the binder:
match e as e' with ... end

Hope this helps,

Bruno Barras.