The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Hi all

Adam Koprowski wrote:

>    Hello everybody,
>
>  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? I tried all varations of discriminate, 
> injection etc. I could think of. Or is this equality not valid 
> intuitionistically? Any indications why? Any help appreciated!


If this is a one-off problem, then some sort of induction will do 
nicely. If you want to do this sort of thing a lot, and especially if 
your cycle length gets longer than 1, eg disproving a = Pair b (Pair a 
c), you can prove a once-per-datatype 'no cycles' theorem following the 
scheme in 'A Few Constructions on Constructors' by myself, Healf Goguen 
and James McKinna, in proceedings of TYPES 2004.

Basically, the idea is that given some x = t, compute the tuple of 
proofs that x is not equal to any of the constructor-guarded subterms of 
t. In your case, given the above, you would get a tuple containing 'a is 
not a', which is quite useful.

Hope this helps

Conor

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.