The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Mon, 29 Oct 2007 17:40:19 +0100 (CET), Marko Malikoviæ
<marko AT ffri.hr>
 a écrit:
> On the end of my proof I have to prove that 5<=x but I don't know how. I
> try to build-up this on the start of my function:

Your function has to work (ie terminate) for ANY value of x y. It seems
that yours do not terminate for y >=6. So you have to test somewhere
that y is below 6 and return someting in this case.

> Function funkcija (x y : nat) {measure decrease_function y} : Prop :=
>   if x>5 then False else

You probably need more something like y<5 (actually le_lt_dec y 5).

>     ...
> 
> but I have this error message:
> 
> Error: The term "x > 5" has type "Prop" which is not a (co-)inductive type
> I don't see about what (co-)inductive type is system talking about.

The > operator is not a function (it is an inductive relation), use
the le_lt_dec function instead (Require Export Compare_dec).

Hope this helps.
Pierre Courtieu