The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

So,

I have "list of lists" with name "lista".
My function take two arguments, x and y. With this function I want to get
(y+1)-th element on x-th list and to check it's value. If it's value is A
or B then result of function is True, but vice-versa the function have to
check next y. We have not structurally decreased argument su we must to
use "function" command with decrease function "6-x". But this "x" is just
note: we actualy with decrease function (in measure notation) affect on
argument y. In this case, when y increase from 0 to 5 then 6-y decrease. I
think this is simple and clear.
But another argument x is constant in one calling of function funkcija. On
different calling of this function we can take another x but then in every
recursively calling of (S y) x remain the same.
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:

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

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.

I'm little confused. Can somebody help me?

Thanks in advance,

Marko Malikoviæ

Pierre Courtieu reèe:
> Le Sun, 28 Oct 2007 16:43:02 +0100 (CET), Marko Malikoviæ
>Â <marko AT ffri.hr>
>  a écrit:
>> Greetings,
>>
>> I will be very gratefull if somebody help me to prove the goal on the
>> end
>> of this environment (for the Function command):
>>
>> Section Proba.
>>
>> Require Import List.
>> Require Import Arith.
>> Require Import Recdef.
>> Require Import Omega.
>>
>> Inductive elementi_liste : Set := A | B | C | D | E | F | v.
>>
>> Parameter lista : list (list elementi_liste).
>>
>> Parameter f : elementi_liste.
>>
>> Variable H_lista : lista > (v :: nil) ::
>> (v :: f :: f :: f :: f :: nil) ::
>> (v :: f :: f :: f :: f :: nil) ::
>> (v :: f :: f :: f :: f :: nil) ::
>> (v :: f :: f :: f :: f :: nil) ::
>> nil.
>>
>> Definition decrease_function (x : nat) : nat := 6-x.
>
> Hello,
> I didn't try to make your proof, but be warned that this function
> returns 0 when x >= 6, thus I don't see below how your function
> calls can strictly decrease when y > 5 from the start.
>
> Hope this helps,
> Pierre Courtieu
>
>> Lemma eq_elementi_liste : forall x y : elementi_liste, {x=y}+{~x=y}.
>> decide equality.
>> Qed.
>>
>> Function funkcija (x y : nat) {measure decrease_function y} : Prop :>
>> if eq_nat_dec y 5 then False else
>>     if eq_elementi_liste (nth (y+1) (nth x lista nil) v) A then True
>>       else
>>         if eq_elementi_liste (nth (y+1) (nth x lista nil) v) B then True
>>           else
>>             if eq_elementi_liste (nth (y+1) (nth x lista nil) v) C then
>> funkcija x (S y)
>>               else False.
>