The Coq mailing list

[Vilhelm Sj�berg <vilhelm AT cis.upenn.edu>]

Hello Coq-club,

For our programming language theory course done in Coq, we wanted to show the
students a simple parser written in Coq and let them experiment with it.

However, I have run into a problem. Programs defined using well-founded
recursion will not evaluate completely, because the accessibility proof they
recurse on may contain opaque theorems. Below is a simple example, where the
program gets stuck on the opaque theorem wf_lexprod.

For proving things about the function this is not an issue, but here we just
wanted to let the students experiment by running the function on example
inputs. 

Is there anyway around this (short of reimplementing the Coq standard
library...)?

Thanks,
   Vilhelm Sjoberg

Require Import Relations.
Require Import Wellfounded.
Require Import Wf_nat.
Require Import Lt.

Definition arg_lt : {n : nat & nat} -> {m : nat & nat} -> Prop :=
  lexprod nat (fun _ => nat) lt (fun _ => lt).

Lemma arg_lt_wf : well_founded arg_lt.
  apply wf_lexprod; [ | intros] ; apply lt_wf.
Defined.

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)
    (arg_lt_wf nm).

(* Computation gets stuck on opaque wf_lexprod. *)
Eval compute in ackermann (existT _ 1 1).