The Coq mailing list

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

Dear Coq users and developers,

I have strange problem. If I define environment using nat type and
recursive function using command "Function" then is everything OK, but if
I create analogous case but with enumerated inductive type then tactic
compute get into infinite loop (I think it is infinite loop because Coq
stop without any information).

So, the cases are:

Good case:

Require Import List.

Definition list_A :=
(1 :: 2 :: 3 :: 3 :: nil) ::
(4 :: 1 :: 2 :: 1 :: nil) ::
(1 :: 1 :: 5 :: 2 :: nil) ::
(3 :: 2 :: 4 :: 1 :: nil) ::
(5 :: 5 :: 4 :: 1 :: nil) ::
nil.

Require Import Recdef.
Definition mes (x:nat) : nat := 3-x.
Require Import Arith.
Require Import Omega.

Function problem (x y:nat) {measure mes x} : Prop :=
if eq_nat_dec (nth y (nth x list_A nil) 0) 1 then
     if eq_nat_dec (nth (y+1) (nth (x+1) list_A nil) 0) 5 then True
       else
         if eq_nat_dec (nth (y+1) (nth (x+1) list_A nil) 0) 1 then
                if eq_nat_dec x 3 then False
                  else if eq_nat_dec y 3 then False
                    else problem (S x) (S y)
           else False
     else False.

After proof that each recursive call is actually decreasing, then for
example:

Goal problem 0 0.
compute.

is work well.

But, this analogous case does not work well:

Inductive for_list : Set := a | b | c | d.

Require Import List.

Definition list_B :=
(a :: b :: a :: a :: nil) ::
(c :: a :: a :: b :: nil) ::
(a :: c :: a :: a :: nil) ::
(c :: b :: c :: c :: nil) ::
(a :: c :: b :: a :: nil) ::
nil.

Require Import Recdef.
Definition mes (x:nat) : nat := 3-x.
Require Import Arith.
Require Import Omega.

Lemma eq_list_B : forall x y:for_list, {x=y}+{~x=y}.
decide equality.
Qed.

Function problem (x y:nat) {measure mes x} : Prop :=
if eq_list_B (nth y (nth x list_B nil) d) a then
     if eq_list_B (nth (y+1) (nth (x+1) list_B nil) d) c then True
       else
         if eq_list_B (nth (y+1) (nth (x+1) list_B nil) d) a then
                if eq_nat_dec x 3 then False
                  else if eq_nat_dec y 3 then False
                    else problem (S x) (S y)
           else False
     else False.
intros; unfold mes; subst.
destruct (le_lt_dec x 3).
omega.
absurd (d=a).
discriminate.
rewrite <- anonymous1.
rewrite nth_overflow; auto.
rewrite nth_overflow; simpl; try omega.
Qed.

Goal problem 1 1.
compute.

get into infinite loop (I repeat: I just think it is infinite loop).

I am doing something wrong or this is a bug?

Thank you very much,

Marko Malikoviæ
Faculty of Arts and Sciences
Rijeka, Croatia