The Coq mailing list

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

Le Mon, 17 Sep 2007 08:35:15 +0200 (CEST), Marko Malikoviæ
<marko AT ffri.hr>
 a écrit:
> 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?

Yes :-)

If you put "Defined" instead of "Qed" when saving eq_list_B and at the
end of you termination proof, it will work. This makes transparent
(i.e. unfoldable) enough things for compute to work.

Another way of doing this is to only make transparent eq_list_B and use
the fixpoint equation that is generated by Function (named
<function name>_equation, see second script below). It may happen
that this second method is easier to use in proofs.

Best regards,
Pierre Courtieu

------------------------------8X----------------------------------

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

Goal problem 3 3.
compute.

-----------------------------8X--------------------------------

(* ... Same start ... *)

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. (* Proof remains opaque*)

Goal problem 3 3.
rewrite problem_equation;simpl. (* use of fixpoint equation *)