The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Hi,

(n=m) is of type "Prop", which is not Inductive, so doing "Cases" on it 
has no point -- the "True" in your expression below would be taken to be 
a variable, not the name of a constructor, and so would "False", hence 
it is redundant. What you really want is:

Require EqNat.
...
Cases (beq_nat n m) of true => ... | false => ... end.


Note, (beq_nat) is of type "nat -> nat -> bool" where "bool" which is 
inductively defined:

Coq < Print bool.
Inductive bool  : Set :=  true : bool | false : bool


See the "EqNat" standard library for converting also proofs from 
"(beq_nat n m)=true" to "n=m".

--- nadeem



Jean-Yves Vion-Dury wrote:

> Dear all,
>
> I'm learning Coq (v7.4), and have a problem with a  "Cases" statement:
>
> Cases (n=m) of True => ...  |  False => ... end.
>
> The problem is with the False => ... branch, that triggers an error 
> message:
>
> >  This clause is redundant
>
> I supect a problem with the "void" definition of False, but how can I 
> do an equivalent
> statement ?
>
> Any help appreciated, and thank to the team and contributors for the 
> great job they
> accomplished.
>
> --
> Jean-Yves Vion-Dury 
> <http://www.xrce.xerox.com/people/vion-dury/home.html>   Research 
> Scientist     	Xerox Research Centre Europe
> INRIA (sabbatical)
> 655 avenue de l'Europe,
> 38334 Montbonnot (FRANCE)
> Jean-Yves.Vion-Dury AT inrialpes.fr 
> <mailto:Jean-Yves.Vion-Dury AT inrialpes.fr> 	from France:   0 4 76 61 53 83
> from abroad: +33 4 76 61 53 83
> you may have a look at the Circus Transformation Language? 
> www.alphaAve.com <http://www.alphaAve.com>