The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

>  During my work in Coq I encountered something that looks rather as an
> elementary problem but I got stucked on it nevertheless. Here is the
> relevant snippet:
>
> Variable A: Set.
> Inductive Test: Set :=
> | Elem: A -> Test
> | Pair: Test -> Test -> Test.
>
> Fact discr: forall a b, ~a = Pair a b.
> Proof. ?
>
>   How can one prove discr?

By induction over a, followed by equality-related tactics (I'm quite
fond of "congruence" myself).

> I tried all varations of discriminate,
> injection etc. I could think of. Or is this equality not valid
> intuitionistically?

It is, but only because your type Test is inductive (all values of
type Test are finite trees): if it were coinductive, you could
construct an a such that a = Pair a b.  So, it is not surprising that
you need to use induction to prove a property that depends crucially
on the inductive nature of your data type.

Hope this helps,

- Xavier Leroy