The Coq mailing list

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

Dear Matthieu and Stephane,

Thanks for your hints.

I was still not able to find what is blocking the computation of my function, and I guess it will be hard to do it (I should have thought earlier about these problems :)), so I guess I will try to apply the 2^n Acc_intros trick.

By the way, does anyone in the list can point me to some simple examples where this trick used?

Best regards,
    David

---

Matthieu Sozeau July 6, 2011 5:32 PM

Hi David,

you can use [Print Opaque Dependencies dec] to find out which opaque lemmas
are used in the term.
-- Matthieu

---

David Pereira July 1, 2011 6:46 PM

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.