The Coq mailing list

[Guillaume Dufay <Guillaume.Dufay AT sophia.inria.fr>]

Brian Emre Aydemir a écrit :
> 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?

Hello,

You can simply do a case analysis on (lt_ge_dec n m), which is an
inductive type. You will find below an example of such a use.

Hope this helps.

Regards.

----------

Require Import Lt.
Require Import Bool_nat.

Definition foo (n m:nat) :=
match (lt_ge_dec n m) with
| (left _) => true
| (right _) => false
end.

Lemma bar : forall n m, n < m -> (foo n m) = true.
unfold foo.
intros.
case (lt_ge_dec n m).
reflexivity.
intro H0.
elim (lt_not_le n m H H0).
Qed.

--
Guillaume