The Coq mailing list

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

Here is a simple example inspired by the last question on Coq Club, it's a function returning the list of all possible "shuffles" of two lists:

==================================================

Require Import Wf Recdef.

Require Import List Omega.

Definition seq := list nat.

Definition lt_seq (p q : seq * seq) :=

  length (fst p) + length (snd p) < length (fst q) + length (snd q).

Axiom wf_lt_seq : well_founded lt_seq.

Definition prefix (a : nat) (q : list seq) :=

  List.map (cons a) q.

Fixpoint guard (n : nat) (wf : well_founded lt_seq) : well_founded lt_seq :=

  match n with

    | 0 => wf

    | S n' => fun x => Acc_intro x (fun y _ => guard n' (guard n' wf) y)

  end.

Function shuffle (p : seq * seq) { wf lt_seq } : list seq :=

  match p with

    | (nil, nil) => cons nil nil

    | (l1, nil) => cons l1 nil

    | (nil, l2) => cons l2 nil

    | ((a::u) as l1, (b::v) as l2) =>

      List.app (prefix a (shuffle (u, l2))) 

      (prefix b (shuffle (l1, v)))

  end.

Proof.

  abstract (intros; subst; unfold lt_seq; simpl; omega).

  abstract (intros; subst; unfold lt_seq; simpl; omega).

  exact (guard 100 wf_lt_seq).

Defined.

Eval vm_compute in (shuffle (1::2::3::4::nil, 5::6::7::8::9::nil)).

==================================================

Note that I just admitted the well-foundedness proof but it doesnt prevent computation because the proof I gave at the end of Function was guarded with 2^100 constructors. If instead you write "exact wf_lt_seq", you will see that the computation stops early. If you prove wf_lt_seq, you end up with an axiom-free recursive function whose computation never uses the actual well-foundedness proof.

Hope this helps,

Stéphane

On Tue, Jul 12, 2011 at 12:27 PM, David Pereira <dpereira AT liacc.up.pt> wrote:

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.

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