The Coq mailing list

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

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.