The Coq mailing list

[Taral <taralx AT gmail.com>]

On Mon, Apr 12, 2010 at 8:52 PM, Paul Tarau 
<paul.tarau AT gmail.com>
 wrote:
> Interpret (bijectively, with function i : T -> nat)
>
> i E = 0
> i (A x y) = 2^(i x)*(2*(i y)+1)
>
> Then i (s x) = (i x) + 1, a formula in Peano arithmetic,
> would show that s works like the successor function on nat,
> which obviously terminates.
>
> Still, my hope was that given this bijection, a direct
> inductive proof that "the mess" implements the equivalent
> of the successor function could be found using Coq.

Sure can. Define that function and then use the {measure f x}
termination annotation to Program Fixpoint.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown