The Coq mailing list

[Brian Emre Aydemir <baydemir AT cis.upenn.edu>]

Hi,

So if n and m have type nat, I'd like to be able to write something like

  if (n < m) then X else Y

and be able to reduce/simplify that down to either X or Y somehow.  
However, what I wrote doesn't work since (n < m) has type Prop.  So 
instead, I could write (lt_ge_dec n m).

Then my question is: how do I simplify (if (lt_ge_dec n m) then X else 
Y) down to X or Y?  For example, I'm guessing I need to do a case 
analysis on (n < m \/ n >= m), but how do I prove that assertion.  And 
then once I'm assuming one of the cases, say (n < m), how do I proceed 
to simplify the expression?  Perhaps lt_ge_dec is not the way to go, 
but then I haven't been able to find anything else that works.  As a 
related question: are there any comparison functions on the natural 
numbers with the type (nat -> nat -> bool)?  Or maybe I should try 
working with the integers instead?

Thanks,
Brian

--
Brian Emre Aydemir
http://www.cis.upenn.edu/~baydemir/