The Coq mailing list

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

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.

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.

(I am trying something like this:

intros.
unfold decrease_function.
destruct (le_lt_dec y 5).
omega.
absurd (v=C).
discriminate.
rewrite <- anonymous2.
rewrite nth_overflow;auto.
rewrite nth_overflow;[simpl;omega|rewrite H_lista;simpl].

And what now? Or something is missing in Function statement?)

Thank you very much,

Marko Malikoviæ