The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 1, 2018 at 9:35 AM Li-yao Xia 
<lysxia AT gmail.com>
 wrote:
>
> 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.

Or, to put a bit of monad-type synactic sugar around it:

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)
  {Y : Type} (f : X -> fuelled Y) :
  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).

Definition recursive_call {X:Type} (x : fuelled X) :
  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