Number Theory

This section describes briefly an example development of some theorems of number theory using the library. This development contains some 200 theorems, we just give some of the more important definitions and state the theorems proved. The files are held in a directory called number_theory.

First we need some more facts about integers. We define an elimination rule for the integers and an induction principle.

zedrecd = ... : {C:int.1->Type}(C zero_zed)->({x:int.1}(C x)->
     C (plus_zed one_zed x))->({x:int.1}(C x)->
     C (plus_zed minus_one_zed x))->{a:int.1}C (a.1,a.2)
zedind = ... : {phi:int.1->Prop}(phi zero_zed)->
     ({x:int.1}(phi x)->phi (plus_zed one_zed x))->
     ({x:int.1}(phi x)->phi (plus_zed minus_one_zed x))->
     {a:int.1}phi (a.1,a.2)

We need some more operations on integers.

abs_zed = [a:int.1](abs_nat a,zero) : int.1->int.1
square_zed = [a:int.1]times_zed a a : int.1->int.1
power_zed = [a:int.1]nat_iter one_zed (times_zed a) : int.1->nat->int.1

We work towards defining primeness--the four definitions given are all proved equivalent so whichever is the most convenient for a given proof can be used.

Associate = [a,b:int.1]and (Divides a b) (Divides b a) : int.1->int.1->P
Coprime2 = [m,n:int.1]{a:int.1}(Divides a m)->(Divides a n)->
     Associate a one_zed : int.1->int.1->Prop
Prime1 = [p:int.1]and (Lt_zed one_zed p) 
     ({a:int.1}or (Divides p a) (Coprime p a)) 
     : int.1->Prop
Prime2 = [p:int.1]and (Lt_zed one_zed p) 
     ({a,b:int.1}(Divides p (times_zed a b))->
     or (Divides p a) (Divides p b)) : int.1->Prop
Prime3 = [p:int.1]and (Lt_zed one_zed p) ({t:int.1}(Divides t p)->
     or (Associate t one_zed) (Associate t p)) : int.1->Prop
Prime4 = [p:int.1]and (Lt_zed one_zed p) 
     ({a:int.1}or (Divides p a) (Coprime2 p a)) 
     : int.1->Prop

Some more definitions--we define integers modulo some constant as a quotient type.

Eq_mod = [n|int.1][a,b:int.1]Mod n a b : int.1->int.1->int.1->Prop
modulo = [n|int.1]QU (Eq_mod|n) : int.1->Type(0)
zero_mod == QU_class Eq_mod zero_zed:modulo;
one_mod  == QU_class Eq_mod one_zed :modulo;
power_mod == [aa:modulo]nat_iter one_mod (times_mod aa);
power_div = [p:int.1][n:nat][x:int.1]
     ((decide_Divides (power_zed p n) x)).1 
     : int.1->nat->int.1->bool
power_in = [p,x:int.1]nat_iter zero 
     ([a:nat]if (power_div p (suc a) x) (suc a) a) (abs_nat x) 
     : int.1->int.1->nat
repre == [n:int.1]Ex[x:int.1]Ex[y:int.1]
     eq n (plus_zed (square_zed x) (square_zed y))

And finally the theorems.

pigeon_hole = ... : {n|int.1}(Lt_zed zero_zed n)->
     [m=abs_nat n]{l:list (modulo|n)}(Distin l)->Le (length l) m
Fermat_Theorem = ... : {p:int.1}(Prime1 p)->
     {aa:modulo|p}(not (Eq aa (zero_mod|p)))->
     [pp=abs_nat p]Eq (power_mod aa (pred pp)) (one_mod|p)
Lagrange_Theorem = ... : {n:int.1}(Lt_zed zero_zed n)->
     iff (repre n) ({p:int.1}(Prime1 p)->
     (Eq_mod|four_zed p three_zed)->Even (power_in p n))