more-floor-mod - ACL2 Book

Included Books

top floor-mod floor-mod-basic if-normalization forcing-types

other

(in-package "ACL2")

include-book

(include-book "../basic-ops/top")

include-book

(include-book "floor-mod")

include-book

(include-book "floor-mod-basic")

include-book

(include-book "if-normalization")

include-book

(include-book "forcing-types")

other

(table acl2-defaults-table :state-ok t)

other

(set-default-hints '((nonlinearp-default-hint++ id
     stable-under-simplificationp
     hist
     nil)))

local

(local (in-theory (disable not-integerp-type-set-rules
      integerp-mod-1
      integerp-mod-2
      integerp-mod-3)))

|(* 2 (floor x y))|theorem

(defthm |(* 2 (floor x y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x y)))
    (equal (* 2 (floor x y))
      (if (integerp (* 1/2 (floor (* 2 x) y)))
        (floor (* 2 x) y)
        (+ -1 (floor (* 2 x) y)))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (integerp (* 1/2 (floor (* 2 x) y))))
        (equal (* 2 (floor x y)) (floor (* 2 x) y))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (not (integerp (* 1/2 (floor (* 2 x) y)))))
        (equal (* 2 (floor x y)) (+ -1 (floor (* 2 x) y)))))))

ugly-unhide-hackfunction

(defun ugly-unhide-hack (x) x)

in-theory

(in-theory (disable ugly-unhide-hack))

ugly-unhide-hack-fnfunction

(defun ugly-unhide-hack-fn
  (x)
  (case-match x
    ((('lambda ('x 'y) ('binary-* ''1/2 ('floor 'x 'y))) u v) (list (cons 'y `(binary-* '1/2 (floor ,U ,V)))))
    ((('lambda ('y 'x) ('binary-* ''1/2 ('floor 'x 'y))) u v) (list (cons 'y `(binary-* '1/2 (floor ,V ,U)))))
    (& nil)))

ugly-unhide-hack-thm-1theorem

(defthm ugly-unhide-hack-thm-1
  (implies (and (bind-free (ugly-unhide-hack-fn x) (y))
      (force (equal x y)))
    (equal (ugly-unhide-hack (hide x)) y))
  :hints (("Goal" :in-theory (enable ugly-unhide-hack)
     :expand ((hide x)))))

ugly-unhide-hack-thm-2theorem

(defthm ugly-unhide-hack-thm-2
  (implies (syntaxp (not (consp (car x))))
    (equal (ugly-unhide-hack (hide x)) x))
  :hints (("Goal" :in-theory (enable ugly-unhide-hack)
     :expand ((hide x)))))

ugly-unhide-hack-loop-stopper-1function

(defun ugly-unhide-hack-loop-stopper-1
  (bad-term clause n)
  (declare (xargs :guard (true-listp clause)))
  (cond ((or (not (integerp n)) (<= n 0)) (or (and (eq (fn-symb (car clause)) 'not)
          (equal bad-term (arg1 (car clause))))
        (equal bad-term (car clause))))
    (t (ugly-unhide-hack-loop-stopper-1 bad-term
        (cdr clause)
        (+ -1 n)))))

ugly-unhide-hack-loop-stopperfunction

(defun ugly-unhide-hack-loop-stopper
  (x y mfc state)
  (declare (ignore state))
  (ugly-unhide-hack-loop-stopper-1 `(integerp (binary-* '1/2 (floor ,X ,Y)))
    (mfc-clause mfc)
    (car (access rewrite-constant
        (access metafunction-context mfc :rcnst)
        :pt))))

|(* 1/2 (floor x y))|theorem

(defthm |(* 1/2 (floor x y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (not (ugly-unhide-hack-loop-stopper x y mfc state)))
      (real/rationalp (/ x y)))
    (equal (* 1/2 (floor x y))
      (if (integerp (ugly-unhide-hack (hide (* 1/2 (floor x y)))))
        (floor (* 1/2 x) y)
        (+ 1/2 (floor (* 1/2 x) y)))))
  :hints (("Goal" :in-theory (enable ugly-unhide-hack)
     :expand ((hide (* 1/2 (floor x y))))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (integerp (ugly-unhide-hack (hide (* 1/2 (floor x y))))))
        (equal (* 1/2 (floor x y)) (floor (* 1/2 x) y))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (not (integerp (ugly-unhide-hack (hide (* 1/2 (floor x y)))))))
        (equal (* 1/2 (floor x y)) (+ 1/2 (floor (* 1/2 x) y)))))))

local

(local (defthm extra-intp-thm-1
    (implies (and (integerp (* (/ i) (/ j) x))
        (real/rationalp x)
        (integerp i)
        (integerp j)
        (not (equal j 0)))
      (integerp (* (/ i) x)))
    :hints (("Goal" :use (:instance (:theorem (implies (and (integerp x) (integerp y)) (integerp (* x y))))
         (x (* (/ i) (/ j) x))
         (y j))))))

local

(local (defthm extra-intp-thm-3
    (implies (and (integerp (* (/ i) (/ j) x))
        (real/rationalp x)
        (integerp i)
        (integerp j))
      (integerp (* (/ j) (floor x i))))
    :hints (("Goal" :cases ((equal j 0))))))

|(floor (+ x r) i)|theorem

(defthm |(floor (+ x r) i)|
  (implies (and (integerp x)
      (real/rationalp r)
      (<= 0 r)
      (< r 1)
      (integerp i)
      (< 0 i))
    (equal (floor (+ x r) i) (floor x i))))

mod-x-i*jtheorem

(defthm mod-x-i*j
  (implies (and (< 0 j)
      (integerp i)
      (integerp j)
      (real/rationalp x)
      (integerp (* (/ j) (floor x i))))
    (equal (mod x (* i j)) (mod x i))))

mod-x-i*j-v2theorem

(defthm mod-x-i*j-v2
  (implies (and (integerp i)
      (integerp j)
      (real/rationalp x)
      (< j 0)
      (not (integerp (* (/ i) (/ j) x)))
      (integerp (* (/ j) (floor x i))))
    (equal (mod x (* i j)) (+ (* i j) (mod x i)))))

mod-x-i*j-x-2theorem

(defthmd mod-x-i*j-x-2
  (implies (and (force (integerp i))
      (force (integerp j))
      (force (real/rationalp x)))
    (equal (mod x (* i j))
      (cond ((and (< j 0)
           (not (integerp (* (/ i) (/ j) x)))
           (integerp (* (/ j) (floor x i)))) (+ (* i j) (mod x i)))
        (t (+ (mod x i) (* i (mod (floor x i) j))))))))

mod-x+i*k-i*jtheorem

(defthm mod-x+i*k-i*j
  (implies (and (force (real/rationalp x))
      (force (rationalp i))
      (force (integerp j))
      (force (integerp k))
      (< 0 i)
      (< 0 j)
      (<= 0 x)
      (< x i))
    (equal (mod (+ x (* i k)) (* i j)) (+ x (* i (mod k j))))))

floor-x+i*k-i*jtheorem

(defthm floor-x+i*k-i*j
  (implies (and (force (real/rationalp x))
      (force (rationalp i))
      (force (integerp j))
      (force (integerp k))
      (< 0 i)
      (< 0 j)
      (<= 0 x)
      (< x i))
    (equal (floor (+ x (* i k)) (* i j)) (floor k j))))

floor-equal-i-over-j-rewritetheorem

(defthm floor-equal-i-over-j-rewrite
  (implies (and (case-split (not (equal j 0)))
      (case-split (real/rationalp i))
      (case-split (real/rationalp j)))
    (equal (equal (* j (floor i j)) i) (integerp (* i (/ j))))))

mod-plus-mod-ntheorem

(defthm mod-plus-mod-n
  (implies (and (integerp a) (integerp b) (integerp n))
    (iff (= (mod (+ a b) n) (mod a n)) (= (mod b n) 0)))
  :rule-classes nil)

mod-mult-ntheorem

(defthmd mod-mult-n (equal (mod (* a n) n) (* n (mod a 1))))

mod-theorem-one-atheorem

(defthm mod-theorem-one-a
  (implies (and (real/rationalp a)
      (integerp b)
      (real/rationalp n)
      (not (equal n 0)))
    (equal (mod (* (mod a n) b) n) (mod (* a b) n))))

mod-theorem-one-btheorem

(defthm mod-theorem-one-b
  (implies (and (real/rationalp a)
      (integerp b)
      (real/rationalp n)
      (not (equal n 0)))
    (equal (mod (* b (mod a n)) n) (mod (* a b) n))))

mod-theorem-twoencapsulate

(encapsulate nil
  (local (defun ind-fn
      (i)
      (if (zp i)
        t
        (ind-fn (+ -1 i)))))
  (local (in-theory (enable integerp-mod-1 integerp-mod-2 integerp-mod-3)))
  (local (scatter-exponents))
  (local (encapsulate nil
      (local (in-theory (disable (:rewrite mod-x-y-=-x-y . 1)
            (:rewrite mod-x-y-=-x+y . 1)
            expt-type-prescription-nonpositive-base-odd-exponent
            expt-type-prescription-nonpositive-base-even-exponent
            expt-type-prescription-negative-base-odd-exponent
            expt-type-prescription-negative-base-even-exponent
            expt-type-prescription-integerp-base
            expt-type-prescription-positive-base
            expt-type-prescription-integerp-base-b
            expt-type-prescription-integerp-base-a
            (:type-prescription mod-zero . 4)
            (:rewrite mod-x-y-=-x . 3)
            (:rewrite mod-x-y-=-x . 4)
            (:meta meta-integerp-correct)
            (:rewrite simplify-products-scatter-exponents-<)
            (:rewrite mod-zero . 4)
            (:type-prescription integerp-mod-2)
            (:rewrite default-times-2)
            (:rewrite default-times-1)
            (:type-prescription mod-zero . 3)
            (:type-prescription mod-zero . 2)
            (:type-prescription mod-zero . 1)
            (:type-prescription mod-positive . 2)
            (:type-prescription mod-positive . 1)
            (:type-prescription mod-negative . 2)
            (:type-prescription mod-negative . 1)
            (:rewrite mod-x-y-=-x+y . 3)
            (:rewrite mod-x-y-=-x-y . 3)
            (:rewrite |(integerp (expt x n))|)
            (:rewrite mod-x-y-=-x-y . 2)
            (:rewrite default-mod-ratio)
            (:rewrite simplify-products-scatter-exponents-equal)
            (:rewrite mod-x-y-=-x+y . 2)
            (:rewrite normalize-factors-scatter-exponents)
            (:rewrite default-plus-2)
            (:rewrite prefer-positive-exponents-scatter-exponents-equal)
            (:rewrite prefer-positive-exponents-scatter-exponents-<)
            (:rewrite default-less-than-2)
            (:rewrite default-less-than-1)
            (:rewrite default-plus-1)
            (:rewrite integerp-/)
            (:rewrite |(< c (- x))|)
            (:rewrite bubble-down-*-match-1)
            (:rewrite |(< (- x) c)|)
            (:rewrite |(* (expt x m) (expt x n))|)
            (:rewrite integerp-minus-x)
            (:rewrite |(< (- x) (- y))|)
            (:rewrite |(< 0 (/ x))|)
            (:rewrite reduce-rational-multiplicative-constant-<)
            (:rewrite reduce-multiplicative-constant-<)
            (:rewrite reduce-additive-constant-<)
            (:rewrite |(< c (/ x)) positive c --- present in goal|)
            (:rewrite |(< c (/ x)) positive c --- obj t or nil|)
            (:rewrite |(< c (/ x)) negative c --- present in goal|)
            (:rewrite |(< c (/ x)) negative c --- obj t or nil|)
            (:rewrite |(< (/ x) c) positive c --- present in goal|)
            (:rewrite |(< (/ x) c) positive c --- obj t or nil|)
            (:rewrite |(< (/ x) c) negative c --- present in goal|)
            (:rewrite |(< (/ x) c) negative c --- obj t or nil|)
            (:rewrite |(< (/ x) (/ y))|)
            (:rewrite remove-strict-inequalities)
            (:rewrite integerp-<-constant)
            (:rewrite constant-<-integerp)
            (:rewrite mod-x-y-=-x . 2)
            (:rewrite |(mod (+ x (mod a b)) y)|)
            (:rewrite |(mod (+ x (- (mod a b))) y)|)
            (:rewrite default-divide)
            (:rewrite normalize-terms-such-as-1/ax+bx)
            (:rewrite default-minus)
            (:rewrite |(equal (- x) c)|)
            (:linear expt-is-weakly-increasing-for-base->-1)
            (:linear expt-is-weakly-decreasing-for-pos-base-<-1)
            (:linear expt-is-increasing-for-base->-1)
            (:linear expt-is-decreasing-for-pos-base-<-1)
            (:linear expt->=-1-one)
            (:rewrite default-mod-1)
            (:type-prescription rationalp-expt-type-prescription)
            (:rewrite |(equal (- x) (- y))|)
            (:rewrite |(* c (* d x))|)
            (:rewrite mod-cancel-*-rewriting-goal-literal)
            (:rewrite mod-cancel-*-const)
            (:rewrite |(equal (/ x) c)|)
            (:rewrite |(mod x (* y (/ z))) rewriting-goal-literal|)
            (:rewrite |(mod (* x (/ y)) z) rewriting-goal-literal|)
            (:rewrite |(< 0 (* x y))|)
            (:rewrite bubble-down-*-bubble-down)
            (:linear expt-x->=-x)
            (:linear expt-x->-x)
            (:linear expt->=-1-two)
            (:linear expt->-1-two)
            (:linear expt->-1-one)
            (:linear expt-<=-1-two)
            (:linear expt-<=-1-one)
            (:linear expt-<-1-two)
            (:linear expt-<-1-one)
            (:rewrite reduce-multiplicative-constant-equal)
            (:rewrite reduce-additive-constant-equal)
            (:rewrite |(equal c (/ x))|)
            (:rewrite |(equal (/ x) (/ y))|)
            (:rewrite |(equal c (- x))|)
            (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-remainder)
            (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-common)
            (:rewrite |(< (/ x) 0)|)
            (:rewrite |(< (* x y) 0)|)
            (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-remainder)
            (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-common)
            (:rewrite equal-of-predicates-rewrite)
            (:type-prescription bubble-down)
            (:rewrite |(* x (if a b c))|)
            (:linear expt-linear-upper-<=)
            (:linear expt-linear-upper-<)
            (:linear expt-linear-lower-<=)
            (:linear expt-linear-lower-<)
            (:rewrite |arith (* c (* d x))|)
            (:rewrite simplify-terms-such-as-ax+bx-=-0)
            (:rewrite |(equal (mod (+ x y) z) x)|))))
      (defthm mod-theorem-two-helper-helper
        (implies (and (not (zp i))
            (equal (mod (expt a i) n) (mod (expt (mod a n) i) n))
            (integerp a)
            (integerp b)
            (integerp n)
            (not (equal n 0)))
          (equal (mod (* b (expt (mod a n) i)) n)
            (mod (* b (expt a i)) n)))
        :hints (("Goal" :induct (ind-fn b))))))
  (local (defthm mod-theorem-two-helper
      (implies (and (not (zp i))
          (equal (mod (expt a i) n) (mod (expt (mod a n) i) n))
          (integerp a)
          (integerp n)
          (not (equal n 0)))
        (equal (mod (expt (mod a n) (+ 1 i)) n)
          (mod (expt a (+ 1 i)) n)))))
  (local (gather-exponents))
  (defthm mod-theorem-two
    (implies (and (integerp a)
        (integerp i)
        (<= 0 i)
        (integerp n)
        (not (equal n 0)))
      (equal (mod (expt (mod a n) i) n) (mod (expt a i) n)))
    :hints (("Goal" :induct (ind-fn i) :do-not '(generalize)) ("Subgoal *1/2''" :cases ((equal i 1)))
      ("Subgoal *1/2.2" :use (:instance mod-theorem-two-helper (i (+ -1 i)))
        :in-theory (disable mod-theorem-two-helper)))))

two-xxxtheorem

(defthm two-xxx
  (implies (and (integerp x)
      (< 0 x)
      (integerp n)
      (<= 0 n)
      (not (integerp (* 1/2 x))))
    (equal (+ 1 (* 2 (mod (floor x 2) (expt 2 n))))
      (mod x (expt 2 (+ 1 n)))))
  :hints (("Goal" :do-not '(generalize) :do-not-induct t))
  :otf-flg t)

mod-theorem-threetheorem

(defthm mod-theorem-three
  (implies (and (integerp a)
      (integerp i)
      (<= 0 i)
      (integerp n)
      (not (equal n 0))
      (integerp x))
    (equal (mod (* x (expt (mod a n) i)) n)
      (mod (* x (expt a i)) n)))
  :hints (("Goal" :use ((:instance mod-theorem-one-a (a (expt (mod a n) i)) (b x)) (:instance mod-theorem-one-a (a (expt a i)) (b x)))
     :in-theory (disable mod-theorem-one-a mod-theorem-one-b))))

mod-mult-2theorem

(defthm mod-mult-2
  (implies (integerp a) (equal (mod (* a n) n) 0))
  :hints (("Goal" :cases ((equal n 0)))))

mod-prodtheorem

(defthm mod-prod
  (implies (and (real/rationalp m)
      (real/rationalp n)
      (real/rationalp k))
    (equal (mod (* k m) (* k n)) (* k (mod m n))))
  :otf-flg t)

mod-multtheorem

(defthm mod-mult
  (implies (and (integerp a) (real/rationalp m) (real/rationalp n))
    (equal (mod (+ m (* a n)) n) (mod m n))))

mod-sums-cancel-1theorem

(defthm mod-sums-cancel-1
  (implies (and (case-split (<= 0 y))
      (case-split (real/rationalp k))
      (case-split (real/rationalp y))
      (case-split (real/rationalp x1))
      (case-split (real/rationalp x2)))
    (equal (equal (mod (+ k x1) y) (mod (+ k x2) y))
      (equal (mod x1 y) (mod x2 y)))))

|(equal (mod a n) (mod b n))|theorem

(defthm |(equal (mod a n) (mod b n))|
  (implies (and (integerp (+ (* a (/ n)) (- (* b (/ n)))))
      (real/rationalp a)
      (real/rationalp b)
      (real/rationalp n)
      (not (equal n 0)))
    (equal (equal (mod a n) (mod b n)) t))
  :hints (("Goal" :use (:instance mod-zero (x (+ a (- b))) (y n))
     :in-theory (e/d nil (mod-zero)))))

find-nasty-floor-addend-1function

(defun find-nasty-floor-addend-1
  (x ans)
  (declare (xargs :mode :program))
  (cond ((variablep x) ans)
    ((fquotep x) ans)
    ((eq (ffn-symb x) 'floor) (if (term-order ans x)
        x
        ans))
    ((eq (ffn-symb x) 'binary-+) (find-nasty-floor-addend-1 (arg2 x)
        (find-nasty-floor-addend-1 (arg1 x) ans)))
    (t ans)))

find-nasty-floor-addendfunction

(defun find-nasty-floor-addend
  (x)
  (declare (xargs :mode :program))
  (let ((ans (find-nasty-floor-addend-1 x nil)))
    (if ans
      (list (cons 'a (arg1 ans))
        (cons 'b (arg2 ans))
        (cons 'c `(unary-- ,ANS)))
      nil)))

the-floor-abovetheorem

(defthm the-floor-above
  (implies (and (syntaxp (in-term-order-+ x mfc state))
      (bind-free (find-nasty-floor-addend x) (a b c))
      (integerp x)
      (integerp y)
      (real/rationalp (* a (/ b)))
      (equal c (- (floor a b))))
    (equal (< x y) (< (+ (* a (/ b)) c x) y))))

the-floor-belowtheorem

(defthm the-floor-below
  (implies (and (syntaxp (in-term-order-+ y mfc state))
      (bind-free (find-nasty-floor-addend y) (a b c))
      (integerp x)
      (integerp y)
      (real/rationalp (* a (/ b)))
      (equal c (- (floor a b)))
      (not (equal x y)))
    (equal (< x y) (< x (+ (* a (/ b)) c y)))))