The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi David,

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

Le 1 juil. 2011 à 10:46, David Pereira a écrit :

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