nniq - ACL2 Book

Included Books

ground-zero fp2 denominator numerator predicate unary-divide product integerp arith rationals idiv top-with-meta

other

(in-package "ACL2")

include-book

(include-book "ground-zero")

local

(local (include-book "fp2"))

local

(local (include-book "denominator"))

local

(local (include-book "numerator"))

local

(local (include-book "predicate"))

local

(local (include-book "unary-divide"))

local

(local (include-book "product"))

local

(local (include-book "integerp"))

local

(local (include-book "arith"))

nonnegative-integer-quotient-with-a-non-integer-argtheorem

(defthm nonnegative-integer-quotient-with-a-non-integer-arg
  (implies (not (integerp i))
    (equal (nonnegative-integer-quotient i j) 0))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-with-a-non-integer-arg-2theorem

(defthm nonnegative-integer-quotient-with-a-non-integer-arg-2
  (implies (not (integerp j))
    (equal (nonnegative-integer-quotient i j) 0))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-with-a-non-positive-argtheorem

(defthm nonnegative-integer-quotient-with-a-non-positive-arg
  (implies (<= i 0)
    (equal (nonnegative-integer-quotient i j) 0))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-with-a-non-positive-arg-2theorem

(defthm nonnegative-integer-quotient-with-a-non-positive-arg-2
  (implies (<= j 0)
    (equal (nonnegative-integer-quotient i j) 0))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-upper-bound-rewritetheorem

(defthm nonnegative-integer-quotient-upper-bound-rewrite
  (implies (and (case-split (<= 0 i))
      (case-split (<= 0 j))
      (case-split (rationalp j)))
    (<= (nonnegative-integer-quotient i j) (/ i j)))
  :hints (("Goal" :cases ((rationalp i))
     :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-upper-bound-lineartheorem

(defthm nonnegative-integer-quotient-upper-bound-linear
  (implies (and (case-split (<= 0 i))
      (case-split (<= 0 j))
      (case-split (rationalp j)))
    (<= (nonnegative-integer-quotient i j) (/ i j)))
  :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j)))))

nonnegative-integer-quotient-max-value-rewritetheorem

(defthm nonnegative-integer-quotient-max-value-rewrite
  (implies (and (case-split (<= 0 i))
      (case-split (<= 0 j))
      (case-split (integerp i))
      (case-split (integerp j)))
    (equal (equal (nonnegative-integer-quotient i j) (/ i j))
      (integerp (/ i j))))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-lower-bound-rewritetheorem

(defthm nonnegative-integer-quotient-lower-bound-rewrite
  (implies (and (case-split (integerp i))
      (case-split (integerp j))
      (case-split (<= 0 i))
      (case-split (<= 0 j)))
    (< (+ -1 (/ i j)) (nonnegative-integer-quotient i j)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-lower-bound-lineartheorem

(defthm nonnegative-integer-quotient-lower-bound-linear
  (implies (and (case-split (integerp i))
      (case-split (integerp j))
      (case-split (<= 0 i))
      (case-split (<= 0 j)))
    (< (+ -1 (/ i j)) (nonnegative-integer-quotient i j)))
  :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j)))))

nonnegative-integer-quotient-upper-bound-linear-strongertheorem

(defthm nonnegative-integer-quotient-upper-bound-linear-stronger
  (implies (and (case-split (<= 0 i))
      (case-split (<= 0 j))
      (not (integerp (* i (/ j))))
      (case-split (acl2-numberp i))
      (case-split (rationalp j))
      (case-split (rationalp k))
      (case-split (< 0 k)))
    (< (* k (nonnegative-integer-quotient i j)) (* k (/ i j))))
  :hints (("Goal" :cases ((rationalp i))
     :in-theory (enable nonnegative-integer-quotient)))
  :rule-classes ((:linear :trigger-terms ((* k (nonnegative-integer-quotient i j))))))

nonnegative-integer-quotient-when-j-is-0theorem

(defthm nonnegative-integer-quotient-when-j-is-0
  (equal (nonnegative-integer-quotient i 0) 0))

nniq-no-rounding-to-doencapsulate

(encapsulate nil
  (local (defthm nniq-no-rounding-to-do-all-but-j=0
      (implies (and (integerp (* i (/ j)))
          (integerp i)
          (>= i 0)
          (integerp j)
          (> j 0))
        (equal (nonnegative-integer-quotient i j) (/ i j)))))
  (defthm nniq-no-rounding-to-do
    (implies (and (integerp (* i (/ j)))
        (case-split (integerp i))
        (case-split (<= 0 i))
        (case-split (integerp j))
        (case-split (<= 0 j)))
      (equal (nonnegative-integer-quotient i j) (/ i j)))))

denom-1-means-num-is-alltheorem

(defthm denom-1-means-num-is-all
  (implies (and (rationalp x) (equal (denominator x) 1))
    (equal (numerator x) x))
  :hints (("Goal" :in-theory (disable rational-implies2)
     :use rational-implies2)))

nonnegative-integer-quotient-by-1theorem

(defthm nonnegative-integer-quotient-by-1
  (implies (and (integerp x) (<= 0 x))
    (equal (nonnegative-integer-quotient x 1) x)))

division-by-zero-yields-zerotheorem

(defthm division-by-zero-yields-zero (equal (/ m 0) 0))

fraction-less-than-1theorem

(defthm fraction-less-than-1
  (implies (and (< (abs m) (abs n)) (rationalp m) (rationalp n))
    (<= (* m (/ n)) 1))
  :hints (("Goal" :cases ((> n 0) (= n 0)))))

nniq-inttheorem

(defthm nniq-int
  (implies (and (integerp x) (case-split (<= 0 x)))
    (equal (nonnegative-integer-quotient (numerator x) (denominator x))
      x)))

quotient-numer-denomencapsulate

(encapsulate nil
  (local (include-book "../../../arithmetic/rationals"))
  (local (include-book "../../../arithmetic/idiv"))
  (defthm quotient-numer-denom
    (implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
      (equal (nonnegative-integer-quotient (numerator (/ x y))
          (denominator (/ x y)))
        (nonnegative-integer-quotient x y))))
  (defthm numerator-minus
    (equal (numerator (- i)) (- (numerator i))))
  (defthm denominator-unary-minus
    (implies (rationalp x)
      (equal (denominator (- x)) (denominator x))))
  (defthm denominator-plus
    (implies (and (rationalp r) (integerp i))
      (equal (denominator (+ i r)) (denominator r))))
  (defthm denominator-plus-2
    (implies (and (rationalp r) (integerp i))
      (equal (denominator (+ r i)) (denominator r))))
  (defthm numerator-plus
    (implies (and (rationalp x) (integerp i))
      (equal (numerator (+ x i))
        (+ (* i (denominator x)) (numerator x))))
    :hints (("Goal" :in-theory (disable rational-implies2)
       :use (:instance rational-implies2 (x (+ x i)))))))

numerator-plus-alttheorem

(defthm numerator-plus-alt
  (implies (and (rationalp x) (integerp i))
    (equal (numerator (+ i x))
      (+ (* i (denominator x)) (numerator x))))
  :hints (("Goal" :in-theory (disable numerator-plus)
     :use (:instance numerator-plus))))

numerator-minus-erictheorem

(defthm numerator-minus-eric
  (equal (numerator (* -1 i)) (* -1 (numerator i)))
  :hints (("Goal" :in-theory (disable numerator-minus)
     :use numerator-minus)))

denominator-unary-minus-erictheorem

(defthm denominator-unary-minus-eric
  (implies (rationalp x)
    (equal (denominator (* -1 x)) (denominator x)))
  :hints (("Goal" :in-theory (disable denominator-unary-minus)
     :use denominator-unary-minus)))

nonnegative-integer-quotient-sum-on-top-gen-both-casesencapsulate

(encapsulate nil
  (local (defthm nonnegative-integer-quotient-sum-on-top
      (implies (and (integerp x) (>= x 0) (integerp y) (> y 0))
        (equal (nonnegative-integer-quotient (+ x y) y)
          (+ 1 (nonnegative-integer-quotient x y))))))
  (local (defun nniq-induct
      (x y a)
      (if (zp a)
        1
        (* x y (nniq-induct x y (- a 1))))))
  (local (defthm nonnegative-integer-quotient-sum-on-top-gen
      (implies (and (integerp x)
          (>= x 0)
          (integerp a)
          (integerp y)
          (> y 0)
          (>= a 0))
        (equal (nonnegative-integer-quotient (+ x (* a y)) y)
          (+ a (nonnegative-integer-quotient x y))))
      :hints (("subgoal *1/2" :in-theory (disable nonnegative-integer-quotient-sum-on-top)
         :use ((:instance nonnegative-integer-quotient-sum-on-top
            (x (+ x (* (- a 1) y)))))) ("Goal" :do-not '(generalize) :induct (nniq-induct x y a)))))
  (local (defthm nonnegative-integer-quotient-sum-on-top-back
      (implies (and (integerp x)
          (>= x 0)
          (integerp y)
          (> y 0)
          (>= (+ x (- y)) 0))
        (equal (nonnegative-integer-quotient (+ x (* -1 y)) y)
          (+ -1 (nonnegative-integer-quotient x y))))))
  (local (defun nniq-induct-2
      (x y a)
      (if (or (not (integerp a)) (>= a 0))
        1
        (* x y (nniq-induct-2 x y (+ a 1))))))
  (local (defthm nonnegative-integer-quotient-sum-on-top-gen-back
      (implies (and (integerp x)
          (>= x 0)
          (integerp a)
          (integerp y)
          (> y 0)
          (< a 0)
          (<= 0 (+ x (* a y))))
        (equal (nonnegative-integer-quotient (+ x (* a y)) y)
          (+ a (nonnegative-integer-quotient x y))))
      :otf-flg t
      :hints (("subgoal *1/" :in-theory (disable nonnegative-integer-quotient-sum-on-top-back)
         :use ((:instance nonnegative-integer-quotient-sum-on-top-back
            (x (+ x (* (+ a 1) y)))))) ("Goal" :do-not '(generalize) :induct (nniq-induct-2 x y a)))))
  (defthm nonnegative-integer-quotient-sum-on-top-gen-both-cases
    (implies (and (integerp x)
        (>= x 0)
        (integerp a)
        (integerp j)
        (> j 0)
        (<= 0 (+ x (* a j))))
      (equal (nonnegative-integer-quotient (+ x (* a j)) j)
        (+ a (nonnegative-integer-quotient x j))))
    :hints (("Goal" :cases ((>= a 0))))))

nniq-eric-1encapsulate

(encapsulate nil
  (local (include-book "../../../arithmetic/idiv"))
  (local (include-book "../../../arithmetic/top-with-meta"))
  (defthm nniq-eric-1
    (implies (and (rationalp x) (not (integerp x)))
      (> (+ 1
          (nonnegative-integer-quotient (numerator x) (denominator x)))
        x))
    :hints (("Goal" :in-theory (disable quotient-upper-bound nonnegative-integer-quotient)
       :use (:instance quotient-upper-bound
         (x (numerator x))
         (y (denominator x)))))))

nniq-eric-2theorem

(defthm nniq-eric-2
  (implies (and (rationalp x) (not (integerp x)))
    (> (+ (denominator x)
        (* (denominator x)
          (nonnegative-integer-quotient (numerator x) (denominator x))))
      (numerator x)))
  :hints (("Goal" :in-theory (disable nniq-eric-1 rational-implies2)
     :use (nniq-eric-1 rational-implies2))))

nniq-eric-3theorem

(defthm nniq-eric-3
  (implies (and (rationalp x) (not (integerp x)))
    (>= (+ (denominator x)
        (* (denominator x)
          (nonnegative-integer-quotient (numerator x) (denominator x))))
      (+ 1 (numerator x))))
  :hints (("Goal" :in-theory (disable nniq-eric-2) :use (nniq-eric-2))))

nniq-eric-4theorem

(defthm nniq-eric-4
  (implies (and (rationalp x) (not (integerp x)))
    (>= (+ 1
        (nonnegative-integer-quotient (numerator x) (denominator x)))
      (+ (/ (numerator x) (denominator x)) (/ (denominator x)))))
  :hints (("Goal" :in-theory (disable nniq-eric-3 rational-implies2)
     :use (nniq-eric-3))))

nniq-lower-bound-non-integer-casetheorem

(defthm nniq-lower-bound-non-integer-case
  (implies (and (rationalp x) (not (integerp x)))
    (>= (+ 1
        (nonnegative-integer-quotient (numerator x) (denominator x)))
      (+ x (/ (denominator x)))))
  :hints (("Goal" :in-theory (disable nniq-eric-3 nniq-eric-4)
     :use (nniq-eric-4))))

in-theory

(in-theory (disable nniq-eric-1 nniq-eric-2 nniq-eric-3 nniq-eric-4))

nniq-eric-5theorem

(defthm nniq-eric-5
  (implies (and (integerp p)
      (integerp q)
      (not (integerp (/ p q)))
      (< 0 p)
      (< 0 q))
    (< (nonnegative-integer-quotient p q) (/ p q)))
  :hints (("Goal" :in-theory (disable nniq-eric-1 rational-implies2)
     :use (nniq-eric-1 rational-implies2))))

nniq-eric-6theorem

(defthm nniq-eric-6
  (implies (and (integerp p)
      (integerp q)
      (not (integerp (/ p q)))
      (< 0 p)
      (< 0 q))
    (< (* q (nonnegative-integer-quotient p q)) p))
  :hints (("Goal" :in-theory (disable nonnegative-integer-quotient nniq-eric-5)
     :use (nniq-eric-5))))

nniq-eric-7theorem

(defthm nniq-eric-7
  (implies (and (integerp p)
      (integerp q)
      (not (integerp (/ p q)))
      (< 0 p)
      (< 0 q))
    (<= (+ 1 (* q (nonnegative-integer-quotient p q))) p))
  :hints (("Goal" :in-theory (disable nonnegative-integer-quotient nniq-eric-6)
     :use (nniq-eric-6))))

nniq-eric-8theorem

(defthm nniq-eric-8
  (implies (and (integerp p)
      (integerp q)
      (not (integerp (/ p q)))
      (< 0 p)
      (< 0 q))
    (<= (+ (/ q) (nonnegative-integer-quotient p q)) (/ p q)))
  :hints (("Goal" :in-theory (disable nonnegative-integer-quotient nniq-eric-7)
     :use (nniq-eric-7))))

in-theory

(in-theory (disable nniq-eric-5 nniq-eric-6 nniq-eric-7 nniq-eric-8))