The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

Here is a relatively standard trick that allows to lazily stack an
arbitrary number of Acc constructors in front of the real
accessibility proof (hence, this accessibility proof can contain
opaque theorems). The only minor disagrement is that as soon as you
have depleted all the constructors in front of the proof, you will
start to evaluate it and eventually get stuck.

thomas


(** Trick to compute with well-founded recursions: lazily add 2^n
Acc_intro constructors in front of
   a well_foundedness proof, so that the actual proof is never reached
in practise *)
Fixpoint guard A (R : A -> A -> Prop) (n : nat) (wfR : well_founded R)
{struct n}: well_founded R :=
  match n with
    | 0 => wfR
    | S n => fun x => Acc_intro x (fun y _ => guard A R n (guard A R n wfR) y)
  end.

Definition ackermann (nm : { n : nat & nat }) : nat :=
 Acc_rect _
    (fun nm H =>
       match nm return (forall nm', arg_lt nm' nm -> nat) -> nat with
       | existT 0 n => fun ackermann
         => S n
       | existT (S m') 0 => fun ackermann
           => ackermann (existT _ m' 1) (left_lex _ _ _ _ _ _ _ _ (le_n (S 
m')))
       | existT (S m') (S n') => fun ackermann
           => ackermann (existT _ m' (ackermann (existT _ (S m') n')
                                                (right_lex  _ _ _ _ (S
m') _ _ (le_n (S n')))))
                        (left_lex _ _ _ _ _ _ _ _ (le_n (S m')))
              end)
   ( (guard _ _ 100 (arg_lt_wf)) nm).

(* Computation yields 3 *)
Eval compute in ackermann (existT _ 1 1).