The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le vendredi 20 juillet 2012 à 22:10 +0200, 
hugoccomp AT gmail.com
 a écrit :
> Hello club.
> 
> In an attempt to use Coq for solving Project Euler problems (and quickly
> realising Peano naturals wouldn't cut it) i've unsuccessfully tried to use 
> the
> BigN naturals from the standard library.

To complement Thomas' answer:

1. If you wish to effectively compute inside Coq, you should always
strip your functions of proof terms, since Coq will try to normalize
them along the way, thus wasting time.

2. Use vm_compute rather than compute, especially for bigN numbers.

Below is a variant of your code, but without using any of the high-level
commands (Program Fixpoint, Function), so that everything is explicit.
It uses the same guard as in Thomas' reply. The pred_val function is
tailored specially for your example: it tests the equality to 0 (with
eq_bool) and then returns the predecessor and an opaque proof suitable
for performing the next recursive call. Hopefully, the fib_iter function
should be readable.

Best regards,

Guillaume


Require Recdef.
Require Import BigN.
Import BigN.
Open Scope bigN_scope.

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

Definition infinite := guard 50 lt_wf_0.

Definition pred_val i :
  { p : bigN | [p] = [pred i] /\ p < i } + { [i] = [0] }.
generalize (spec_eq_bool_aux i 0).
case eq_bool ; intro H.
now right.
left.
exists (pred i).
split.
apply refl_equal.
now apply lt_pred_l.
Defined.

Notation next acc decr := (match acc with Acc_intro n => n _ decr end).

Fixpoint fib_iter (tn_1 tn i : bigN) (acc : Acc lt i) { struct acc } : bigN :=
  match pred_val i with
  | inleft (exist pred_i (conj _ decr)) =>
    fib_iter tn (tn_1 + tn) pred_i (next acc decr)
  | inright _ => tn
  end.

Eval vm_compute in fib_iter 1 0 1000 (infinite _).