Chinese Remainder Theorem (Higher Order)
-------------------------

------
Summary:
Needs many lemmas (some of whose proofs are also challenging)
An Existential Witness has to be Provided
Higher Order
------

Definitions:

all 
---

nat -> nat -> (nat -> bool) -> bool 

(all X 0 P) = (P 0)
((s Y) < X) -> (all X (s Y) P) = true
(not ((s Y) < X)) -> (all X (s Y) P) = (P (s Y)) and (all X Y P)


leq
---

nat -> nat -> bool 

(leq 0 Y) = true
(leq (s X) 0) = false 
(leq (s X) (s Y)) = (leq X Y) 

mod 
---

nat -> nat -> nat 

                                     (mod X 0) = 0
((X < Y) and (not (Y = 0))) -> (mod X Y) = X
((not (X < Y)) and (not (Y = 0))) -> (mod X Y) = (mod (X - Y) Y)

prod
----
nat -> nat -> (nat -> nat) -> nat 

(prod X 0 F) = (F 0) 
((s Y) < X) -> (prod X (s Y) F) = (s 0) 
(not ((s Y) < X)) -> (prod X (s Y) F) = ((F (s Y)) * (prod X Y F)

quot 
----

nat -> nat -> nat 

                                     (quot X 0) = 0
((X < Y) and (not (Y = 0))) -> (quot X Y) = 0
((not (X < Y)) and (not (Y = 0))) -> (quot X Y) = (s (quot (X - Y) Y)) 

rprime
------ 

nat -> nat -> bool

(rprime X Y) = (primefac X Z) and (primefac Y W) -> (not (eq Z W))

------
Theorem:

forall m,a:(nat -> nat). forall n,u1,u2,v1,v2:nat. exists x:nat.
(all 0 n [i\ (0 < (m i))])
and (leq 0 u1) and (leq u1 n)
and (leq 0 u2) and (leq u2 n)
and (not (eq u1 u2))
and ((primefac v1 (m u1))
     and (primefac v2 (m u2))
     -> (not (eq v1 v2)))
-> (all 0 n [i\ (eq x (mod (a i) (m i)))])

forall m,a:(nat -> nat). forall n,u1,u2,v1,v2,x1,x2:nat.
(all 0 n [i\ (0 < (m i))])
and (leq 0 u1) and (leq u1 n)
and (leq 0 u2) and (leq u2 n)
and (not (eq u1 u2))
and ((primefac v1 (m u1))
     and (primefac v2 (m u2))
     -> (not (eq v1 v2)))
and (all 0 n [i\ (eq x1 (mod (a i) (m i)))])
and (all 0 n [i\ (eq x2 (mod (a i) (m i)))])
-> (eq (mod x1 (prod 0 n m)) (mod x2 (prod 0 n m)))

Comments
--------
Actually two proofs, existance and uniqueness.

First Order version proved in RRL by Zhang and Hua (See IWC008a.txt).

As far as I'm aware no one has really looked at proving the higher
order version of this.

Source
------

Jeremy Gow