[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
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
More information about the Types-list
mailing list