The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

Hi David,

Making your well-foundedness lemma transparent is not necessarily
sufficient, since it may itself depend on some opaque lemma which may
have to be unfolded. If I'm not mistaken, the well-foundedness proof
needs to be transparent enough so that it can be reduced to
head-normal form. Making sure of this, and keeping track of which
proofs should be transparent and which should not, is just a headache
as far as I am concerned so I systematically use the 2^n trick that
you hinted at. Actually I see no reason why not to do this, since it
is probably faster than reducing the wf proof anyway and I like it
best when everything computational is transparent, and everything
logical is opaque.

Also, this is unrelated but for those cases where my recursive
function is in Function's fragment, I prefer Function over Program
Fixpoint because the lemmas and induction principles it generates make
it easier to reason on the definition afterwards. Just a matter of
taste, maybe.

Stéphane

On Fri, Jul 1, 2011 at 7:46 PM, David Pereira 
<dpereira AT liacc.up.pt>
 wrote:
> 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.
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06