Newbie question on computing with recursive function

[Mathie-3]

I have defined the following function:

Require Import NArith.
Require Import Recdef.

Open Scope positive_scope.

Function factN (n : positive) {wf Plt n} : positive :=
match n with
| xH => xH
| xO x => n * factN ( Ppred n)
| xI x => n * factN ( Ppred n)
end.

(Proofs have been omitted.)

I'm having a bit of trouble trying to evaluate
factN 4:

Eval compute in (factN 4)

results in a huge expression rather than
a simple number. 

I know I'm missing something but I'm
not sure where to go from here.  Any
help will be greatly appreciated.

[Thomas Braibant-2]

I think that the important point here is that you omitted the proofs.

For example, the following does not work because you end the proof
with Qed, and made the function opaque ...

Function factN (n : positive) {wf Plt n} : positive :=
match n with
| xH => xH
| xO x => n * factN ( Ppred n)
| xI x => n * factN ( Ppred n)
end.
  admit.
  admit.
  admit.
Qed.

Then, if you end the proofs with Defined instead of Qed, you get a not
so huge terms that is blocked on the (fix Ffix x somethinghuge 4
(factN_tcc_admitted1 4)). Here factN_tcc_admitted1 is the proof of
well foundedness of Plt, which is admitted, thus opaque.

If you have provided an actual proof, I guess you can reduce, even if
it can be slow (because you compute the proof of accessibility of the
argument you gave to the fonction)

A nice trick by B. Barras & G. Gonthier some time ago on this list was
to use a "guard"  to the well_foundedness argument, which hides it.

Here is a complete code that reduces :

Require Import NArith.
Require Import Recdef.

Open Scope positive_scope.

Set Implicit Arguments.

Fixpoint guard A (R : A -> A -> Prop) (n : nat) (wfR : well_founded R)
{struct n}: well_founded R :=
  match n with
    | O => wfR
    | S n => fun x => Acc_intro x (fun y _ => guard  n (guard n wfR) y)
  end.

Function factN (n : positive) {wf Plt n} : positive :=
match n with
| xH => xH
| xO x => n * factN ( Ppred n)
| xI x => n * factN ( Ppred n)
end.
  admit.
  admit.
  apply (guard 100).admit.
Defined.


thomas braibant



On Thu, Sep 24, 2009 at 12:43 PM, Mathie <mathie@...> wrote:

> I have defined the following function:
>
> Require Import NArith.
> Require Import Recdef.
>
> Open Scope positive_scope.
>
> Function factN (n : positive) {wf Plt n} : positive :=
> match n with
> | xH => xH
> | xO x => n * factN ( Ppred n)
> | xI x => n * factN ( Ppred n)
> end.
>
> (Proofs have been omitted.)
>
> I'm having a bit of trouble trying to evaluate
> factN 4:
>
> Eval compute in (factN 4)
>
> results in a huge expression rather than
> a simple number.
>
> I know I'm missing something but I'm
> not sure where to go from here.  Any
> help will be greatly appreciated.
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Julien Forest]

Hi,

On Thu, 24 Sep 2009 13:14:49 +0200
Thomas Braibant <thomas.braibant@...> wrote:

> I think that the important point here is that you omitted the proofs.
>
> For example, the following does not work because you end the proof
> with Qed, and made the function opaque ...
>
> Function factN (n : positive) {wf Plt n} : positive :=
> match n with
> | xH => xH
> | xO x => n * factN ( Ppred n)
> | xI x => n * factN ( Ppred n)
> end.
>   admit.
>   admit.
>   admit.
> Qed.
>

This is perfectly true even if not documented (my mistakes sorry).


>
> If you have provided an actual proof, I guess you can reduce, even if
> it can be slow (because you compute the proof of accessibility of the
> argument you gave to the fonction)
>
In fact, you should use the vm_compute strategy instead of the compute one. It should greatly decrease computation time.  

> A nice trick by B. Barras & G. Gonthier some time ago on this list was
> to use a "guard"  to the well_foundedness argument, which hides it.
>
I'm not sure to understand the interest of this trick.
The only way to really prove the termination of the function is to be able to give an upper bound of the number of recursive steps done in guard. In that case, why not use the {measure ....} construction.


Bests,
Julien

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Thomas Braibant-2]

>> A nice trick by B. Barras & G. Gonthier some time ago on this list was
>> to use a "guard"  to the well_foundedness argument, which hides it.
>>
> I'm not sure to understand the interest of this trick.
> The only way to really prove the termination of the function is to be able to give an upper bound of the number of recursive steps done in guard. In that case, why > not use the {measure ....} construction.

But, sometime, the upper bound can be very big, and using measure (or
wf), wouldn't you start by evaluating this upper bound, by computing
the witness of termination, in order to exhibit all the constructors
needed for the recursion? In our case, the function was the
determinisation of NFA, and the bound was 2 to the power of the number
of states of the original automata. Which is quite big.

Here, using this guard, you still need to prove the well-foundedness
of the recursive calls, but you are given 2^n recursion steps, before
trying to compute the witness...

Here is the original post on this list from where this is originated :
http://logical.saclay.inria.fr/coq-puma/messages/7d5a3493009fd0e2

Thomas

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Lescuyer-3]

To add to Thomas' argumentation, sometimes you don't even have a
choice since the integer bound is not computable (typically for
lexicographic orders) and neither is the well-foundedness proof (if it
is classical for instance, as in Guillaume Melquiond's original post).

Stéphane

On Thu, Sep 24, 2009 at 8:34 PM, Thomas Braibant
<thomas.braibant@...> wrote:

>>> A nice trick by B. Barras & G. Gonthier some time ago on this list was
>>> to use a "guard"  to the well_foundedness argument, which hides it.
>>>
>> I'm not sure to understand the interest of this trick.
>> The only way to really prove the termination of the function is to be able to give an upper bound of the number of recursive steps done in guard. In that case, why > not use the {measure ....} construction.
>
> But, sometime, the upper bound can be very big, and using measure (or
> wf), wouldn't you start by evaluating this upper bound, by computing
> the witness of termination, in order to exhibit all the constructors
> needed for the recursion? In our case, the function was the
> determinisation of NFA, and the bound was 2 to the power of the number
> of states of the original automata. Which is quite big.
>
> Here, using this guard, you still need to prove the well-foundedness
> of the recursive calls, but you are given 2^n recursion steps, before
> trying to compute the witness...
>
> Here is the original post on this list from where this is originated :
> http://logical.saclay.inria.fr/coq-puma/messages/7d5a3493009fd0e2
>
> Thomas
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club