The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

Hello,

In fact, I think that in this example you don't need the Function
facility. You are searching through a list looking for elements that
are equal to D or L. The list decreases in the process, so you can use
regular structural recursion. The fact that the list through which you
are searching is an element in another list (lista) does not change
anything: you first extract the inner list using the nth function and
then search through it.

One reason why your example is problematic is that the double list is
not actually bound to the variable lista; instead there is an axiom
lista = .... Because of this, your term cannot be reduced, for
example, to True, since it has a free variable lista.

Speaking about True, my guess is that you want a function that returns
the type bool, not Prop. If you return Prop then you cannot match the
result against True and False, for example, because Prop is not an
inductive type. In particular, you cannot write "if dd_k 1 1 then 5
else 6", which you can do if you return values of type bool.

Here is my take on your example.

Require Import List.

Inductive elementi_liste : Set := A | B | C | D | E | F | L | O | v | f.

Lemma eq_figure : forall x y : elementi_liste, {x=y}+{~x=y}.
decide equality.
Defined.

(* Note that you have to use Defined instead of Qed here to allow
eq_figure to be replaced by its definition during the reduction. See
6.2.4-5 in the reference manual. Alternatively, you can define "good"
below using match and without  eq_figure. *)

Definition good (x : elementi_liste) :=
if eq_figure x D
then true
else if eq_figure x L
     then true
     else false.

Fixpoint check_nth (n : nat) (l : list elementi_liste) {struct l} :=
match n, l with
| 0, x :: l' => if good x then true else check_nth 0 l'
| S m, x :: t => check_nth m t
| _, nil => false
end.

Definition lista : list (list elementi_liste) :=
(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 main (x y : nat) := check_nth y (nth x lista nil).

Eval compute in main 1 1.

This returns false. If you replace the first "(v :: f :: f :: f :: f
:: nil) ::" line above with "(v :: f :: f :: f :: D :: nil) ::" then
the result will be true.

Evgeny