The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Hi list members,

I am currently implementing a decision procedure whose termination  is 
based on a well-founded relation. I am using the Program Fixpoint 
command to implement such procedure. The code goes as follows:
<<<
Program Fixpoint dec(sh : set re * set re)(sig:set A)(h:dec_p sh)
      {wf RAlg sh }:set re :=
        match one_iter sh sig with
          | (nv,l) as H0 =>
            match l with
              | Terminate => fst nv
              | Continue  => dec nv sig (hhh (fst sh) (snd sh) sig
                (eee sh h) (fst nv) (snd nv) (refl_equal H0))
            end
        end.
 (* Obligations proved and made transparent with Defined *)
>>>

The type [set re] is the type of finite sets of the Containers library 
by Lescuyer, the functions [hhh] and [eee] are defined transparently, 
the well-foundness proofs for [RAlg] where also made transparent,  and 
the type [dec_p] is just the following Record:
<<<
Record dec_p(sh:set re * set re) : Type := {
      H1 : fst sh[<=]PD r ;
      H2 : snd sh[<=]PD r ;
      D  : \./ sh
    }.

Definition hhh : forall s1 s2 sig,
   dec_p (s1, s2) -> forall s s0, (s, s0, Continue) = one_iter (s1, s2) 
sig ->  dec_p (s,s0).

Definition eee : forall sh, dec_p sh -> dec_p (fst sh,snd sh).

 Inductive DisjP(p:set re * set re) : Type :=
  | DisjP_0 : inter (fst p) (snd p) === {}%set -> DisjP p.

  Notation "\./ p" := (DisjP p).
>>>

Everything went fine when developing all this stuff, but when it was 
time to execute [dec] within Coq, i.e, using Eval vm_compute in dec sh 
sig h, the evaluation simply seems to go on forever. I am pretty sure 
that it is due to well-foundness term used for the recursion. So, my 
question is : is there any standard tricks for enabling such a 
computation based on well-foundness when using Program Fixpoint? I know 
of a trick used by Thomas Braibant and Damien Pous that adds 2^n  
Acc_intro constructors in front of a well_foundedness proof, in order to 
keep the actual proof unreachable. Is this the standard trick, or there 
is any other one?

Sorry if the message is confusing. Also I was not able to isolate the 
problem ir order to provide a script.

Best regards to all,
    David Pereira.