The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 17 Sep 2007, Marko Malikovi? wrote:

> 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.

Replace Qed. with Defined.

> 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.

Here also replace Qed. with Defined.

> Goal problem 1 1.
> compute.
>
> get into infinite loop (I repeat: I just think it is infinite loop).

This isn't a infinite loop, rather Qed makes the eq_list_B symbol opaque, 
which means the definition cannot be unfolded.  Without being able to 
unfold the defintion of eq_list_B, the resulting normal form of problem 1 
1 is very large.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''