The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

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.

Paul Tarau

On Mon, Apr 12, 2010 at 5:18 PM, Taral 
<taralx AT gmail.com>
 wrote:
> On Sat, Apr 10, 2010 at 4:47 PM, 
> �<paul.tarau AT gmail.com>
>  wrote:
>> -- successor
>> s E = A E E
>> s (A x y) = s0 x y
>>
>> s0 E y = A (s x) z where A x z = s y
>> s0 (A a b) y = A E (A (p0 a b) y)
>>
>> p0 E E = E
>> p0 E (A x y) = A (s x) y
>> p0 (A a b) y = A E (p0 (p0 a b) y)
>>
>> -- predecessor
>> p (A x y) = p0 x y
>
> First prove to me (informally) that this mess _always_ terminates.
>
> --
> Taral 
>Â <taralx AT gmail.com>
> "Please let me know if there's any further trouble I can give you."
>    -- Unknown
>