Here is a workaround with a custom proof of well-foundedness using

"Wf_nat.well_founded_lt_compat". The drawback is that the proof of

"lt_wf" thus internally converts to "nat", and thus the computation of

"ackermann" produces a stack overflow even on small inputs. The solution

is to use "lazy" evaluation instead of "cbv".

I also understood why "Solve Obligations" did not work. You need to

start the solving tactic with "program_simplify" (or even

"program_simpl" ?) that cleans the goal a bit. This seems to be done

automatically by "Next Obligation", but not by "Solve Obligations".

Jean-Christophe

Require Import Coq.Numbers.BinNums.

Require Import Coq.NArith.BinNat.

Require Import Program.

Require Import Psatz.

Lemma lt_lt : forall n1 n2, (n1 < n2)%N -> N.to_nat n1 < N.to_nat n2.

Proof. intros; lia.

Qed.

Lemma lt_wf : well_founded N.lt.

Proof.

apply Wf_nat.well_founded_lt_compat with (f:=N.to_nat).

apply lt_lt.

Defined.

Ltac discharge_obligation' :=

program_simplify;

match goal with

| [ H : 0%N <> _ |- _ ] => apply N.lt_pred_l; apply not_eq_sym; exact H

| _ => apply measure_wf; apply lt_wf

end.

Program Fixpoint ackermann_fuel' (fuel : N) (m n : nat) {wf N.lt fuel} :

nat :=

match fuel with

| N0 => 0 (* Default case when out of fuel. *)

| _ =>

match m with

| 0 => S n

| S m' =>

match n with

| 0 => ackermann_fuel' (Npred fuel) m' 1

| S n' => ackermann_fuel' (Npred fuel) m' (ackermann_fuel' (Npred

fuel) m n')

end

end

end.

Solve Obligations with discharge_obligation'.

(* Define ackermann to launch ackermann_fuel' with enough fuel to last

until the end of the universe. *)

Definition ackermann (n m : nat) := ackermann_fuel' (Npow 2 200) n m.

Fail Eval cbv in ackermann 3 3 (* Stack overflow *).

Eval lazy in ackermann 3 3 (* 61 *).

*Post by Peter E Schmidt-Nielsen*Good point Li-yao, I feel really silly for writing "Program Fixpoint"

for the nat-fueled version. I copied it over by analogy from the

BinNat-fueled version I tried to get to work when I saw Klaus's

original suggestion to use fuel. I got stuck on the BinNat version,

and somehow had a moment of silliness and forgot that obviously

Program Fixpoint's features are completely unnecessary with a plain

nat for fuel.

Daniel's sugar for making this easier to write also looks great.

Not to hijack the thread, but I'm really curious if anyone has any

leads on getting the BinNat-fueled version (appearing below the

nat-fueled one in my gist) to work? The great thing about such a

version is that you can just past in some obscene value like 2^200 for

the fuel in every case and never worry about it, while with a nat for

fuel I'm quite constrained on how much fuel I can provide. (I figure

this isn't really thread hijacking, because I think getting a

BinNat-fueled version working would basically practically solve this

issue for OP.)

I looked at the "Type classes for efficient exact real arithmetic in

Coq" paper that was linked, but I'm not sure the laziness suggested

via eta expansion solves this problem, as I'm 98% sure that the output

of Program Fixpoint actually really does need to compute through the

opaque parts of N.lt_pred_l and N.lt_wf_0, although maybe I'm missing

the point.

If there were some generic mechanism that could take an opaque term

and trace all the dependencies Print Opaque Dependencies style and

make a transparent version (or somehow override the opacity) then it

would completely solve the problem...

Thanks,

-snp

*Post by Daniel Schepler**Post by Li-yao Xia*If you're using fuel it is fairly easy to make it structurally

decreasing with a simple Fixpoint because fuel can just decrease by 1,

instead of using a Program and proving decreasingness with respect to lt.

Definition fuelled (X : Type) : Type :=

nat -> option X.

Definition return_ {X : Type} (x : X) : fuelled X :=

fun _ => Some x.

Definition bind {X : Type} (x : fuelled X)

fuelled Y :=

fun fuel => match x fuel with

| Some x0 => match f x0 fuel with

| Some y0 => Some y0

| None => None

end

| None => None

end.

Notation "'do' x0 <- x ; y" := (bind x (fun x0 => y))

(x0 ident, at level 20, right associativity).

fuelled X :=

fun fuel => match fuel with

| S fuel_pred => x fuel_pred

| O => None

end.

Definition ackermann_fuel : nat -> nat -> fuelled nat :=

fix F (m n:nat) (fuel : nat) {struct fuel} : option nat :=

match m with

| O => return_ (S n)

| S m' => match n with

| O => recursive_call (F m' 1)

| S n' =>

do x <- recursive_call (F m n');

recursive_call (F m' x)

end

end fuel.

Definition run_with_fuel {X:Type} (x : fuelled X)

(fuel : nat) :=

x fuel.

Compute (run_with_fuel (ackermann_fuel 3 3) 100)

--

Daniel Schepler