The Coq mailing list

[<hugoccomp AT gmail.com>]

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.

Specifically, i cannot seem to "grok" how to do recursive functions with them,
given that, if you try the usual matching on them, you'll end up crashing
straight into their internal representation.

My best attempt with the induction principles given by the generic Natural
module was thwarted by the fact i needed to prove something involving
Morphisms.Proper, which i believe was the basic fact that my function couldn't
distinguish bewtween different representations of the same natural number.

Below, i've posted my latest attempt at crafting one. This one, i don't even
know why it fails. I'd be glad if anyone could explain.

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?

*Project Euler: http://projecteuler.net/



(*Code starts here!*)

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

Function fib_iter (tn_1 tn i:bigN) {wf lt i} : bigN :=
if eq_dec i 0 then tn else fib_iter tn (tn_1 + tn) (pred i).
Proof. intros. apply lt_pred_l. assumption. apply lt_wf_0. Defined.

Goal fib_iter 0 0 0 = 0.
rewrite fib_iter_equation. auto. Qed.
Goal fib_iter 0 1 5 = 8.
do 6 rewrite fib_iter_equation. auto. Qed.
(*Feel free to test other values and verify this
  function obeys the fibonacci spec.*)

(*All of the following tests run forever on my machine;
  if you must run them, i recommend adding a Timeout
  command to them. Alternatively, replacing "fib_iter"'s
  final Defined command with Qed makes it so that these
  computations get stuck in "fib_iter_terminate".*)
(* Compute fib_iter 0 0 0. *)
(* Compute fib_iter 0 1 5. *)
(* Goal fib_iter 0 0 0 = 0. vm_compute. *)

(*And also, attempting to define "fib_iter" using
  Program Fixpoint results in a obligation with a
  strange typing i can't really explain why, nor prove
  the goal. *)
Require Program.
Program Fixpoint fib_iter' (tn_1 tn i:bigN) {wf lt i} : bigN :=
if eq_dec i 0 then tn else fib_iter' tn (tn_1 + tn) (pred i).
Next Obligation. intros. apply lt_pred_l. assumption. Defined.
Next Obligation.
(*
This is the strange goal:
well_founded
  (Wf.MR lt
     (fun recarg : sigT (fun _ : bigN => sigT (fun _ : bigN => bigN)) =>
      projT2 (projT2 recarg)))
*)