[TYPES] Eliminators in type theory

[Sergei SOLOVIEV]

(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



Now

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
Sergei SOLOVIEV