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-NielsenGood 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 ScheplerPost by Li-yao XiaIf 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