The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Agnishom,

I wish to define the function described in this Haskell program, and I have tried three different approaches.

Approach 1(Method1.v) : This uses the mentioned proof-pearl. In this case, the _expression_ refuses to reduce.

You can only reduce a Fixpoint by reducing its structural argument. In your case, this is an accessibility

proof. Usually, accessibility proofs are Opaque (because in Prop) and thus do not reduce. You can open them

(Defined) but they almost certainly contain opaque proofs internally which also need to be opened and then

your start rewriting all the standard library...

A first possible workaround is the use of Acc based fuel (I think first due to Gonthier but I am not sure) which 

consists in pilling up Acc_intro constructors in front of your accessibility proofs, allowing depth limited reduction

but possibly enough for simpl to get you where you want.

Another possibly which we favor in "The Braga Method"  

https://github.com/DmxLarchey/The-Braga-Method

is to write fully specified Fixpoints such as

Fixpoint f x y (d : Acc R (x,y)) { struct d } : { o | Gf x y o } := ...

where Gf : X -> Y -> Z -> Prop describes, as an *inductive* predicate, the computational rules of your recursive

function. Then, by showing that Gf is functional relation (on its output), you get your fixpoint equations for free.

Best,

Dominique