[TYPES] Eliminators in type theory

Sergei SOLOVIEV soloviev at irit.fr
Mon Mar 20 11:30:41 EST 2006

(I have already sent it to Yong Luo)

it can be done using more simple coding of pairs <x,y> = (x+y)(x+y+1)/2 +y 
and corresponding projections p1 and p2
(about their definitions I'll speak below).

Assume that <x, y> and p1, p2 are already defined using Elim_Nat. Then we 
may define the function F(x) = <fib(x), fib(x+1)>
using Elim_Nat because F(x+1) = <fib(x+1), fib(x+2)> = <fib(x+1), fib(x)+ 
fib(x+1)>= <p2(F(x)), p1(F(x))+p2(F(x))>
and fib(x) will be p1(F(x)).

Concerning the definitions of <...>, p1, p2, I will not go into definition 
of multiplication *, division (integer) by 2, call it
div2, substraction (where we pose n-m=0 if m>=n) using Elim_Nat (this is 
easy - but it will take space). Plus + you have already defined. I already 
defined pred.

<x, y> = (div2 ((x+y)*(x+y+1)))+y

To define projections we define

d = Elim_Nat(S0)(\p:Nat.\r:Nat.0)      (dn =1 if n=0 and 0 otherwise)

d' = Elim_Nat(0)(\p:Nat.\r:Nat.S0)     (d'n =0 if n=0 and 1 otherwise)

k=  Elim_Nat 0 (\p:Nat\r:Nat. (r+(d((Sr)*(SSr)- 2*(Sp)))))    (enumeration 
of pairs, if you put them on the plan xy is done along
the diagonals y= -x+kn and kn is the number of a diagonal where the pair of 
number n is placed)

for the pair number 0 k0 =0,
for the pairs 1 and 2 k1=k2=1,
k3=k4=k5 = 2 etc


p1 = Elim_Nat 0 (\p:Nat\r:Nat. (((dr)*(S(kp)))+((d'r)*(pred r))))

p2 = \n:Nat.(kn - (p1)n)

I copied these definitions from our old text with David Chemouil, there may 
be some small
arithmetical errors, but essentially it is like this.

soloviev at irit.fr

More information about the Types-list mailing list