The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

This is really nice to see that there are a few people trying to solve
Project Euler problems.

Here are some remarks:
- I would use Z or N rather than BigN in 8.3, but in 8.4 BigN would
probably be more efficient, and there should be the same lemmas
provided for everything (thanks to Numbers). Yet, it is harder to do
structural operations on them.

- If you cannot use structural recursion, you should use well-founded
induction (this is the Wf stuff that you saw). And there is one trick
to know, that makes it possible to compute efficiently the result of a
function defined using well-founded induction in Coq: one is advised
to stack (lazily) a big number of Acc constructors in front of the
actual proof that the element you are starting with is accessible (in
a nutshell: this proof may be big, and long to compute).

Here is a quick draft of a definition of fib (there are a lot of
caveats, here), but I hope this helps.

Require Import ZArith NArith Program.
Open Scope N_scope.

(** Trick to compute with well-founded recursions: lazily add 2^n
Acc_intro constructors in front of
  a well_foundedness proof, so that the actual proof is never reached
in practise *)
Fixpoint guard A (R : A -> A -> Prop) (n : nat) (wfR : well_founded R)
{struct n}: well_founded R :=
 match n with
   | 0 => wfR
   | S n => fun x => Acc_intro x (fun y _ => guard A R n (guard A R n wfR) y)
 end%nat.


Program Fixpoint fib (n : N) {wf N.lt n}: (N * N) :=
  match  N.ltb 1 n with true =>
           let (a,b) := fib (n - 1) in
             (b, a+b)%N
       | false =>
    if N.eqb n 0%N
    then (0,1)%N
    else  (1,1)end.
Next Obligation.
  assert (1 < n). admit.
  (* could not find the proper lemma browsing Numbers in less than 2
minutes...  *)
  zify. omega.
Qed.
Next Obligation.
  apply (guard _ _ 100).
  apply N.lt_wf_0.
Defined.                        (* this must be defined, not qed *)

Eval vm_compute in fib 100.

> Also, can someone tell me if i'm the right path here? As in, is this the 
> right
> module to use for the Project Euler problems? Or should i be using something
> else entirely?

I would be delighted if we could craft the right set of modules and
recipes to tackle Project Euler problems. Stephane Lescuyer did some
of the problems a long time ago, and we tried to port this to Coq 8.4,
and do more problems together, but it turns out we did not finish/made
significant progress. If I get some time soon, I would love to come
back to this, and if other people are interested, we could do some
community effort.

BTW, computing is nice, but proving that the result you get is the
right one may turn out to be complicated : just phrasing what it is
for a result to be correct may be a challenge by itself on some
problems ;).

Hope that helps
Thomas