First Order Version of the Arithmetic/Geometric Mean ---------------------------------------------------- ------ Summary: Unusual Induction Scheme Needs Lemmata and extra functions Presents challenges to Rippling ------ ------ Definitions: * (times) --------- nat -> nat -> nat (X * 0) = 0 (X * (s Y)) = ((X * Y) + X) exp --- nat -> nat -> nat (exp X 0) = 0 (exp X (s Y)) = ((exp X Y) * X) len --- (list nat) -> nat (len nil) = 0 (len (H::T)) = (s (len T)) leq --- nat -> nat -> bool (leq 0 Y) = true (leq (s X) 0) = false (leq (s X) (s Y)) = (leq X Y) sum (first order) --- nat -> (list nat) -> nat (sum 0 L) = 0 (sum n nil) = 0 (sum (s Y) (H::T)) = h + sum(n, T) prod (first order) ---- nat -> (list nat) -> nat (prod 0 L) = 1 (prod N nil) = 1 (prod (s Y) (H::T)) = h * (prod Y T) ------ Theorem: forall n:nat,a:(list nat). (n = (len n)) -> (leq ((exp n n) * (prod n a)) (exp (sum n a) n)) ------ Comments: The main challenge here is finding the appropriate induction scheme. In the example we have there are two base cases (0 and 1) and two step cases (P(n) -> P(2.n)) and (P(s(n)) -> P(n)). NB. There is a proof of the higher order version of this theorem that uses the scheme (forall m. (m < n) -> P(m)) -> P(n)) - which is more usual. I don't know if this scheme could also be used here. However the step cases require a number of lemmata to solve involving several lemmata (including the introduction of a new functions). New functions are called oddlist, evenlist sumlist, timeslist, ctimeslist, explist and are for respectively getting a list of the odd numbered elements of a list, the even numbered elements of a list, pairwise summation of all the elements of two lists, pairwise multiplication of two list, multiply every element of a list by a constant and raising every element of a list by a given exponent. oddlist: (oddlist nil) = nil (oddlist (H::nil) = (H::nil) (oddlist (H1::H2::T)) = (H1::(oddlist T)) evenlist: (evenlist nil) = nil (evenlist (H::nil) = nil (evenlist (H1::H2::T)) = (H2::(evenlist T)) sumlist: (sumlist nil L) = L (sumlist L nil) = L (sumlist (H1::T1) (H2::T2)) = (H1 + H2)::(sumlist T1 T2) timeslist: (timeslist nil L) = L (timeslist L nil) = L (timeslist (H1::T1) (H2::T2)) = (H1 * H2)::(timeslist T1 T2) ctimeslist: (ctimeslist m nil) = nil (ctimeslist m (H::T)) = (m * H)::(ctimeslist M T) explist (explist nil M) = nil (explist (H::T) M) = (exp H M)::(explist T M) Lemmata used in the sample proof are: (exp (x * y) z) = (exp x z) * (exp y z) ((x * y) * z) = y * (x * z) (prod N (ctimeslist X L)) = ((exp X N) * (prod N L)) (sum (2 * N) L) = (sum N (sumlist (oddlist L) (evenlist L))) (prod (2 * N) L) = (prod N (prodlist (oddlist L) (evenlist L))) (exp X (Y * Z)) = (exp (exp X Y) Z) (prod N (explist L M)) = (exp (prod N L) M) (sum N (sumlist L M)) = (sum N L) + (sum N M) (sumlist L (ctimeslist N L)) = (ctimeslist (s N) L) (sum N (ctimeslist M L)) = M * (sum N L) (prod N (ctimeslist M L)) = (exp M N) * (prod N L) (leq (X * Z) (X * Y)) => (leq Z Y) (exp X (s N)) = X * (exp X N) Even with these lemmata the rewriting involved presents several challenges to rippling (e.g. sinks need to be proved equal) and rippling has to take place in the induction hypothesis for the second step case. I don't know how these might effect other theorem provers - Louise Dennis ------ Source: Toby Walsh Edinburgh MRG Group Blue Book Note 828