The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

Using the boolean datatype is a possible solution. However, I usually
find better to stay at the Prop level. For that, you must use the fact
that equality over nat is decidable :

Coq < Require Arith.

Coq < Check eq_nat_dec.
eq_nat_dec
     : (n,m:nat){n=m}+{n<>m}

so a definition with the shape you want could be

Coq < Definition f := [n,m:nat]
Coq <  Cases (eq_nat_dec n m) of
Coq <  | (left h) => (0)
Coq <  | (right h) => (1)
Coq <  end.
f is defined

The 'h' variables above are proofs of n=m (resp. n<>m), which can be
useful for more complex definitions. Note that such a definition can
be used to compute: 

Coq < Eval Compute in (f (0) (0)).
     = (0)
     : nat

Coq < Eval Compute in (f (0) (1)).
     = (1)
     : nat

Of course, you have to know that 'left' and 'right' are constructors
for { }+{ } which is not very nice, but there is the variant 

Coq < Definition g := [n,m:nat]
Coq <  if (eq_nat_dec n m) then
Coq <   [h](0)
Coq <  else
Coq <   [h](1).
g is defined

for which you don't need anymore to remember constructor names of {
}+{ }.


Hope this helps...






>>>>> "Nadeem" == Nadeem Abdul Hamid 
>>>>>Â <nadeem AT acm.org>
>>>>>  writes:

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

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


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

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


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

    Nadeem> --- nadeem



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

    Nadeem> --------------------------------------------------------
    Nadeem> Bug reports: http://coq.inria.fr/bin/coq-bugs
    Nadeem> Archives: http://pauillac.inria.fr/pipermail/coq-club
    Nadeem>           http://pauillac.inria.fr/bin/wilma/coq-club
    Nadeem> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |