11919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 242e3b607cbfe96be2006a4ef702d8d296d13d0e5Stefan Krah; Copyright (c) 2008-2016 Stefan Krah. All rights reserved. 31919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 41919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; Redistribution and use in source and binary forms, with or without 51919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; modification, are permitted provided that the following conditions 61919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; are met: 71919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 81919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 1. Redistributions of source code must retain the above copyright 91919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; notice, this list of conditions and the following disclaimer. 101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 2. Redistributions in binary form must reproduce the above copyright 121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; notice, this list of conditions and the following disclaimer in the 131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; documentation and/or other materials provided with the distribution. 141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND 161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE 191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL 201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY 241919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF 251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; SUCH DAMAGE. 261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; 271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(in-package "ACL2") 301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(include-book "arithmetic/top-with-meta" :dir :system) 321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(include-book "arithmetic-2/floor-mod/floor-mod" :dir :system) 331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ===================================================================== 361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; Proofs for several functions in umodarith.h 371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ===================================================================== 381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ===================================================================== 421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; Helper theorems 431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ===================================================================== 441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm elim-mod-m461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (<= m x) 471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< x (* 2 m)) 481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp x) (rationalp m)) 491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod x m) 501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ x (- m))))) 511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm modaux-1a 531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< x m) (< 0 x) (< 0 m) 541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp x) (rationalp m)) 551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (- x) m) 561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (- x) m)))) 571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm modaux-1b 591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< (- x) m) (< x 0) (< 0 m) 601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp x) (rationalp m)) 611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod x m) 621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ x m))) 631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :use ((:instance modaux-1a 641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (- x))))))) 651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm modaux-1c 671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< x m) (< 0 x) (< 0 m) 681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp x) (rationalp m)) 691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod x m) 701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah x))) 711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm modaux-2a 731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 b) (< b m) 741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) (natp m) 751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (mod (+ b x) m) b)) 761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ (- m) b x) m) 771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (- m) b (mod x m))))) 781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm modaux-2b 801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 b) (< b m) 811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) (natp m) 821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (mod (+ b x) m) b)) 831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ b x) m) 841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (- m) b (mod x m)))) 851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :use (modaux-2a)))) 861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm linear-mod-1 881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< x m) (< b m) 891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) 901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp m)) 911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (< x (mod (+ (- b) x) m)) 921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< x b))) 931919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :use ((:instance modaux-1a 941919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ b (- x)))))))) 951919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 961919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm linear-mod-2 971919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 b) (< b m) 981919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) 991919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m)) 1001919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (< (mod x m) 1011919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ (- b) x) m)) 1021919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (mod x m) b)))) 1031919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1041919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm linear-mod-3 1051919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< x m) (< b m) 1061919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) 1071919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp m)) 1081919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (<= b (mod (+ b x) m)) 1091919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (+ b x) m))) 1101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :use ((:instance elim-mod-m 1111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ b x))))))) 1121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm modaux-2c 1141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 b) (< b m) 1151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) (natp m) 1161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (<= b (mod (+ b x) m))) 1171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ b x) m) 1181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ b (mod x m)))) 1191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Subgoal *1/8''" :use (linear-mod-3)))) 1201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd modaux-2d 1221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< x m) (< 0 x) (< 0 m) 1231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (- m) b) (< b 0) (rationalp m) 1241919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (<= x (mod (+ b x) m)) 1251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp x) (rationalp b)) 1261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (+ (- m) (mod (+ b x) m)) 1271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ b x))) 1281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((<= 0 (+ b x)))) 1291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 2'" :use ((:instance modaux-1b 1301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ b x))))))) 1311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-m-b 1331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 x) (< 0 b) (< 0 m) 1341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< x b) (< b m) 1351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (natp b) (natp m)) 1361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ (mod (- x) m) b) m) 1371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- x) b)))) 1381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ===================================================================== 1411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; addmod, submod 1421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ===================================================================== 1431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun addmod (a b m base) 1451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((s (mod (+ a b) base)) 1461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (s (if (< s a) (mod (- s m) base) s)) 1471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (s (if (>= s m) (mod (- s m) base) s))) 1481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah s)) 1491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd addmod-correct 1511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 1521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< a m) (<= b m) 1531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 1541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp a) (natp b)) 1551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (addmod a b m base) 1561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ a b) m))) 1571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((<= base (+ a b)))) 1581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 2.1'" :use ((:instance elim-mod-m 1591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ a b))))))) 1601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun submod (a b m base) 1621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((d (mod (- a b) base)) 1631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (if (< a d) (mod (+ d m) base) d))) 1641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah d)) 1651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd submod-aux1 1671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< a (mod (+ a (- b)) base)) 1681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< 0 base) (< a base) (<= b base) 1691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp base) (natp a) (natp b)) 1701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< a b)) 1711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :rule-classes :forward-chaining) 1721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd submod-aux2 1741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (<= (mod (+ a (- b)) base) a) 1751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< 0 base) (< a base) (< b base) 1761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp base) (natp a) (natp b)) 1771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (<= b a)) 1781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :rule-classes :forward-chaining) 1791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd submod-correct 1811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 1821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< a m) (<= b m) 1831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 1841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp a) (natp b)) 1851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (submod a b m base) 1861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- a b) m))) 1871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((<= base (+ a b)))) 1881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 2.2" :use ((:instance submod-aux1))) 1891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 2.2'''" :cases ((and (< 0 (+ a (- b) m)) 1901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (+ a (- b) m) m)))) 1911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 2.1" :use ((:instance submod-aux2))) 1921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2" :use ((:instance submod-aux1))) 1931919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1" :use ((:instance submod-aux2))))) 1941919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1951919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 1961919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun submod-2 (a b m base) 1971919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((d (mod (- a b) base)) 1981919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (if (< a b) (mod (+ d m) base) d))) 1991919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah d)) 2001919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2011919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm submod-2-correct 2021919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 2031919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< a m) (<= b m) 2041919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 2051919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp a) (natp b)) 2061919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (submod-2 a b m base) 2071919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- a b) m))) 2081919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Subgoal 2'" :cases ((and (< 0 (+ a (- b) m)) 2091919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (+ a (- b) m) m)))))) 2101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 2131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ext-submod is correct 2141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 2151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; a < 2*m, b < 2*m 2171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun ext-submod (a b m base) 2181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((a (if (>= a m) (- a m) a)) 2191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (if (>= b m) (- b m) b)) 2201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (mod (- a b) base)) 2211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (if (< a b) (mod (+ d m) base) d))) 2221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah d)) 2231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2241919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; a < 2*m, b < 2*m 2251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun ext-submod-2 (a b m base) 2261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((a (mod a m)) 2271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (mod b m)) 2281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (mod (- a b) base)) 2291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (if (< a b) (mod (+ d m) base) d))) 2301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah d)) 2311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd ext-submod-ext-submod-2-equal 2331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 2341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< a (* 2 m)) (< b (* 2 m)) 2351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 2361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp a) (natp b)) 2371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (ext-submod a b m base) 2381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (ext-submod-2 a b m base)))) 2391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd ext-submod-2-correct 2411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 2421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< a (* 2 m)) (< b (* 2 m)) 2431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 2441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp a) (natp b)) 2451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (ext-submod-2 a b m base) 2461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- a b) m)))) 2471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 2501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; dw-reduce is correct 2511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 2521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun dw-reduce (hi lo m base) 2541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((r1 (mod hi m)) 2551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (r2 (mod (+ (* r1 base) lo) m))) 2561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah r2)) 2571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd dw-reduce-correct 2591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 2601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< hi base) (< lo base) 2611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 2621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 2631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (dw-reduce hi lo m base) 2641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ (* hi base) lo) m)))) 2651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd <=-multiply-both-sides-by-z 2671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (rationalp x) (rationalp y) 2681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< 0 z) (rationalp z)) 2691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (<= x y) 2701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (<= (* z x) (* z y))))) 2711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd dw-reduce-aux1 2731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 2741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 2751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo base) (natp lo) 2761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< x m) (natp x)) 2771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (+ lo (* base x)) (* base m))) 2781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((<= (+ x 1) m))) 2791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1''" :cases ((<= (* base (+ x 1)) (* base m)))) 2801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("subgoal 1.2" :use ((:instance <=-multiply-both-sides-by-z 2811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ 1 x)) 2821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y m) 2831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (z base)))))) 2841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm dw-reduce-aux2 2861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< x (* base m)) 2871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< 0 m) (< m base) 2881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) (natp x)) 2891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (floor x m) base))) 2901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 2911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; This is the necessary condition for using _mpd_div_words(). 2921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd dw-reduce-second-quotient-fits-in-single-word 2931919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 2941919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< hi base) (< lo base) 2951919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 2961919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo) 2971919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal r1 (mod hi m))) 2981919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (floor (+ (* r1 base) lo) m) 2991919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah base)) 3001919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((< r1 m))) 3011919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m)))) 3021919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2" :use ((:instance dw-reduce-aux1 3031919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (mod hi m))))))) 3041919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3051919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3061919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 3071919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; dw-submod is correct 3081919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 3091919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun dw-submod (a hi lo m base) 3111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((r (dw-reduce hi lo m base)) 3121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (mod (- a r) base)) 3131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (d (if (< a r) (mod (+ d m) base) d))) 3141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah d)) 3151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd dw-submod-aux1 3171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (natp a) (< 0 m) (natp m) 3181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp x) (equal r (mod x m))) 3191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (- a x) m) 3201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- a r) m)))) 3211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd dw-submod-correct 3231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 m) (< m base) 324752bfb71d8cdcdd355e8efcaf7c3eba434573f05Stefan Krah (natp a) (< a m) 3251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< hi base) (< lo base) 3261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp m) (natp base) 3271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 3281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (dw-submod a hi lo m base) 3291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- a (+ (* base hi) lo)) m))) 3301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :in-theory (disable dw-reduce) 3311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :use ((:instance dw-submod-aux1 3321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ lo (* base hi))) 3331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (r (dw-reduce hi lo m base))) 3341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (:instance dw-reduce-correct))))) 3351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 3381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ANSI C arithmetic for uint64_t 3391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ========================================================================= 3401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun add (a b) 3421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ a b) 3431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 64))) 3441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun sub (a b) 3461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (- a b) 3471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 64))) 3481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun << (w n) 3501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (* w (expt 2 n)) 3511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 64))) 3521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun >> (w n) 3541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (floor w (expt 2 n))) 3551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; join upper and lower half of a double word, yielding a 128 bit number 3571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun join (hi lo) 3581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (expt 2 64) hi) lo)) 3591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ============================================================================= 3621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; Fast modular reduction 3631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; ============================================================================= 3641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; These are the three primes used in the Number Theoretic Transform. 3661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; A fast modular reduction scheme exists for all of them. 3671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defmacro p1 () 3681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (expt 2 64) (- (expt 2 32)) 1)) 3691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defmacro p2 () 3711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (expt 2 64) (- (expt 2 34)) 1)) 3721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defmacro p3 () 3741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (expt 2 64) (- (expt 2 40)) 1)) 3751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; reduce the double word number hi*2**64 + lo (mod p1) 3781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun simple-mod-reduce-p1 (hi lo) 3791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (expt 2 32) hi) (- hi) lo)) 3801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; reduce the double word number hi*2**64 + lo (mod p2) 3821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun simple-mod-reduce-p2 (hi lo) 3831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (expt 2 34) hi) (- hi) lo)) 3841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; reduce the double word number hi*2**64 + lo (mod p3) 3861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun simple-mod-reduce-p3 (hi lo) 3871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (expt 2 40) hi) (- hi) lo)) 3881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ---------------------------------------------------------- 3911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; The modular reductions given above are correct 3921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ---------------------------------------------------------- 3931919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 3941919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd congruence-p1-aux 3951919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (* (expt 2 64) hi) 3961919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (p1) hi) 3971919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (* (expt 2 32) hi) 3981919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (- hi)))) 3991919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4001919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd congruence-p2-aux 4011919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (* (expt 2 64) hi) 4021919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (p2) hi) 4031919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (* (expt 2 34) hi) 4041919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (- hi)))) 4051919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4061919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd congruence-p3-aux 4071919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (* (expt 2 64) hi) 4081919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* (p3) hi) 4091919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (* (expt 2 40) hi) 4101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (- hi)))) 4111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd mod-augment 4131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (rationalp x) 4141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp y) 4151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (rationalp m)) 4161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ x y) m) 4171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ x (mod y m)) m)))) 4181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p1-congruent 4201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (integerp hi) 4211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (integerp lo)) 4221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (simple-mod-reduce-p1 hi lo) (p1)) 4231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (join hi lo) (p1)))) 4241919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal''" :use ((:instance congruence-p1-aux) 4251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (:instance mod-augment 4261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (p1)) 4271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ (- hi) lo (* (expt 2 32) hi))) 4281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y (* (p1) hi))))))) 4291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p2-congruent 4311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (integerp hi) 4321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (integerp lo)) 4331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (simple-mod-reduce-p2 hi lo) (p2)) 4341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (join hi lo) (p2)))) 4351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal''" :use ((:instance congruence-p2-aux) 4361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (:instance mod-augment 4371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (p2)) 4381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ (- hi) lo (* (expt 2 34) hi))) 4391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y (* (p2) hi))))))) 4401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p3-congruent 4421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (integerp hi) 4431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (integerp lo)) 4441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (simple-mod-reduce-p3 hi lo) (p3)) 4451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (join hi lo) (p3)))) 4461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal''" :use ((:instance congruence-p3-aux) 4471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (:instance mod-augment 4481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (p3)) 4491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ (- hi) lo (* (expt 2 40) hi))) 4501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y (* (p3) hi))))))) 4511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; --------------------------------------------------------------------- 4541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; We need a number less than 2*p, so that we can use the trick from 4551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; elim-mod-m<x<2*m for the final reduction. 4561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; For p1, two modular reductions are sufficient, for p2 and p3 three. 4571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; --------------------------------------------------------------------- 4581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p1: the first reduction is less than 2**96 4601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p1-<-2**96 4611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 4621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 4631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 4641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p1 hi lo) 4651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 96)))) 4661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p1: the second reduction is less than 2*p1 4681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p1-<-2*p1 4691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 4701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 4711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (join hi lo) (expt 2 96)) 4721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 4731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p1 hi lo) 4741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (* 2 (p1))))) 4751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p2: the first reduction is less than 2**98 4781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p2-<-2**98 4791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 4801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 4811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 4821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p2 hi lo) 4831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 98)))) 4841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p2: the second reduction is less than 2**69 4861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p2-<-2*69 4871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 4881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 4891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (join hi lo) (expt 2 98)) 4901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 4911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p2 hi lo) 4921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 69)))) 4931919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 4941919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p3: the third reduction is less than 2*p2 4951919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p2-<-2*p2 4961919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 4971919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 4981919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (join hi lo) (expt 2 69)) 4991919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 5001919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p2 hi lo) 5011919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (* 2 (p2))))) 5021919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5031919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5041919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p3: the first reduction is less than 2**104 5051919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p3-<-2**104 5061919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 5071919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 5081919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 5091919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p3 hi lo) 5101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 104)))) 5111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p3: the second reduction is less than 2**81 5131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p3-<-2**81 5141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 5151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 5161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (join hi lo) (expt 2 104)) 5171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 5181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p3 hi lo) 5191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (expt 2 81)))) 5201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah;; p3: the third reduction is less than 2*p3 5221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthmd simple-mod-reduce-p3-<-2*p3 5231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 5241919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 5251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (join hi lo) (expt 2 81)) 5261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 5271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (simple-mod-reduce-p3 hi lo) 5281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (* 2 (p3))))) 5291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ------------------------------------------------------------------------- 5321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; The simple modular reductions, adapted for compiler friendly C 5331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ------------------------------------------------------------------------- 5341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun mod-reduce-p1 (hi lo) 5361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((y hi) 5371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x y) 5381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (>> hi 32)) 5391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (sub lo x)) 5401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (if (> x lo) (+ hi -1) hi)) 5411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y (<< y 32)) 5421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (lo (add y x)) 5431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (if (< lo y) (+ hi 1) hi))) 5441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* hi (expt 2 64)) lo))) 5451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun mod-reduce-p2 (hi lo) 5471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((y hi) 5481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x y) 5491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (>> hi 30)) 5501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (sub lo x)) 5511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (if (> x lo) (+ hi -1) hi)) 5521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y (<< y 34)) 5531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (lo (add y x)) 5541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (if (< lo y) (+ hi 1) hi))) 5551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* hi (expt 2 64)) lo))) 5561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defun mod-reduce-p3 (hi lo) 5581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (let* ((y hi) 5591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x y) 5601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (>> hi 24)) 5611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (sub lo x)) 5621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (if (> x lo) (+ hi -1) hi)) 5631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (y (<< y 40)) 5641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (lo (add y x)) 5651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (hi (if (< lo y) (+ hi 1) hi))) 5661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ (* hi (expt 2 64)) lo))) 5671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ------------------------------------------------------------------------- 5701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; The compiler friendly versions are equal to the simple versions 5711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah; ------------------------------------------------------------------------- 5721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-aux1 5741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (<= 0 a) (natp a) (natp m) 5751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (- m) b) (<= b 0) 5761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (integerp b) 5771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (mod (+ b a) m) 5781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod a m))) 5791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ b a) m) 5801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ b (mod a m)))) 5811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Subgoal 2" :use ((:instance modaux-1b 5821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x (+ a b))))))) 5831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-aux2 5851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (<= 0 a) (natp a) (natp m) 5861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< b m) (natp b) 5871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (mod (+ b a) m) 5881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod a m))) 5891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (+ m (mod (+ b a) m)) 5901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ b (mod a m))))) 5911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 5931919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-aux3 5941919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 a) (natp a) (natp m) 5951919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< (- m) b) (< b 0) 5961919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (integerp b) 5971919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (<= (mod a m) 5981919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ b a) m))) 5991919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (+ (- m) (mod (+ b a) m)) 6001919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ b (mod a m)))) 6011919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Subgoal 1.2'" :use ((:instance modaux-1b 6021919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x b)))) 6031919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1''" :use ((:instance modaux-2d 6041919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (x I)))))) 6051919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6061919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6071919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-aux4 6081919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< 0 a) (natp a) (natp m) 6091919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< b m) (natp b) 6101919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (<= (mod a m) 6111919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (mod (+ b a) m))) 6121919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod (+ b a) m) 6131919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (+ b (mod a m))))) 6141919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6151919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6161919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-p1==simple-mod-reduce-p1 6171919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 6181919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 6191919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 6201919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod-reduce-p1 hi lo) 6211919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (simple-mod-reduce-p1 hi lo))) 6221919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :in-theory (disable expt) 6231919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :cases ((< 0 hi))) 6241919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 6251919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6261919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6271919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 32) hi))))) 6281919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 6291919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6301919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6311919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 32) hi))))) 6321919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 6331919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6341919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6351919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 32) hi))))) 6361919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 6371919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6381919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6391919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 32) hi))))))) 6401919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6411919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6421919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-p2==simple-mod-reduce-p2 6431919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 6441919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 6451919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 6461919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod-reduce-p2 hi lo) 6471919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (simple-mod-reduce-p2 hi lo))) 6481919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((< 0 hi))) 6491919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 6501919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6511919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6521919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 34) hi))))) 6531919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 6541919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6551919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6561919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 34) hi))))) 6571919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 6581919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6591919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6601919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 34) hi))))) 6611919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 6621919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6631919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6641919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 34) hi))))))) 6651919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6661919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6671919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah(defthm mod-reduce-p3==simple-mod-reduce-p3 6681919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (implies (and (< hi (expt 2 64)) 6691919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (< lo (expt 2 64)) 6701919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (natp hi) (natp lo)) 6711919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (equal (mod-reduce-p3 hi lo) 6721919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (simple-mod-reduce-p3 hi lo))) 6731919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah :hints (("Goal" :cases ((< 0 hi))) 6741919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 6751919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6761919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6771919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 40) hi))))) 6781919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 6791919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6801919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6811919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 40) hi))))) 6821919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 6831919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6841919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6851919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 40) hi))))) 6861919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 6871919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (m (expt 2 64)) 6881919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (b (+ (- HI) LO)) 6891919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah (a (* (expt 2 40) hi))))))) 6901919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6911919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 6921919b7e72bc43315b32f38a6f5f01e8c717907f4Stefan Krah 693