fl-proofs - ACL2 Book

Included Books

numerator denominator nniq arith2 ground-zero floor integerp rationalp unary-divide common-factor negative-syntaxp

other

(in-package "ACL2")

local

(local (include-book "numerator"))

local

(local (include-book "denominator"))

local

(local (include-book "nniq"))

local

(local (include-book "arith2"))

local

(local (include-book "ground-zero"))

local

(local (include-book "floor"))

local

(local (include-book "integerp"))

local

(local (include-book "rationalp"))

local

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

local

(local (include-book "common-factor"))

flfunction

(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

integerp-<-non-integerptheorem

(defthm integerp-<-non-integerp
  (implies (and (and (syntaxp (quotep x)))
      (not (integerp x))
      (integerp n)
      (case-split (rationalp x)))
    (equal (< n x) (<= n (fl x))))
  :hints (("Goal" :in-theory (enable fl))))

non-integerp-<-integerptheorem

(defthm non-integerp-<-integerp
  (implies (and (and (syntaxp (quotep x)))
      (not (integerp x))
      (integerp n)
      (case-split (rationalp x)))
    (equal (< x n) (< (fl x) n)))
  :hints (("Goal" :in-theory (enable fl))))

a10theorem

(defthm a10
  (and (implies (integerp i) (equal (fl i) i))
    (implies (and (integerp i) (case-split (rationalp x1)))
      (and (equal (fl (+ i x1)) (+ i (fl x1)))
        (equal (fl (+ x1 i)) (+ i (fl x1)))))
    (implies (and (integerp i)
        (case-split (rationalp x1))
        (case-split (rationalp x2)))
      (and (equal (fl (+ x1 (+ i x2))) (+ i (fl (+ x1 x2))))
        (equal (fl (+ x1 (+ x2 i))) (+ i (fl (+ x1 x2))))))
    (implies (and (integerp i)
        (case-split (rationalp x1))
        (case-split (rationalp x2))
        (case-split (rationalp x3)))
      (and (equal (fl (+ x1 (+ x2 (+ i x3)))) (+ i (fl (+ x1 x2 x3))))
        (equal (fl (+ x1 (+ x2 (+ x3 i)))) (+ i (fl (+ x1 x2 x3))))))
    (implies (and (integerp i)
        (case-split (rationalp x1))
        (case-split (rationalp x2))
        (case-split (rationalp x3))
        (case-split (rationalp x4)))
      (and (equal (fl (+ x1 (+ x2 (+ x3 (+ i x4)))))
          (+ i (fl (+ x1 x2 x3 x4))))
        (equal (fl (+ x1 (+ x2 (+ x3 (+ x4 i)))))
          (+ i (fl (+ x1 x2 x3 x4)))))))
  :hints (("Goal" :in-theory (enable fl))))

a12theorem

(defthm a12
  (implies (and (integerp i) (integerp j) (< 1 j) (< j i))
    (and (< (acl2-count (fl (/ i j))) (acl2-count i))
      (< (acl2-count (fl (* (/ j) i))) (acl2-count i))))
  :hints (("Goal" :in-theory (enable fl)))
  :rule-classes :linear)

fl-def-linear-part-1theorem

(defthm fl-def-linear-part-1
  (implies (case-split (not (complex-rationalp x)))
    (<= (fl x) x))
  :hints (("goal" :in-theory (enable fl floor)))
  :rule-classes (:rewrite (:linear :trigger-terms ((fl x)))))

fl-def-linear-part-2theorem

(defthm fl-def-linear-part-2
  (implies (case-split (not (complex-rationalp x)))
    (< x (1+ (fl x))))
  :hints (("goal" :in-theory (enable fl floor)))
  :rule-classes (:rewrite (:linear :trigger-terms ((fl x)))))

a13theorem

(defthmd a13
  (implies (case-split (rationalp x))
    (and (< (1- x) (fl x)) (<= (fl x) x)))
  :hints (("Goal" :in-theory (enable fl)))
  :rule-classes :linear)

fl-def-lineartheorem

(defthmd fl-def-linear
  (implies (case-split (rationalp x))
    (and (<= (fl x) x) (< x (1+ (fl x)))))
  :rule-classes :linear)

fl-weakly-monotonictheorem

(defthm fl-weakly-monotonic
  (implies (and (<= y y+)
      (case-split (rationalp y))
      (case-split (rationalp y+)))
    (<= (fl y) (fl y+)))
  :hints (("Goal" :in-theory (enable fl)))
  :rule-classes ((:forward-chaining :trigger-terms ((fl y) (fl y+))) (:linear)
    (:forward-chaining :trigger-terms ((fl y) (fl y+))
      :corollary (implies (and (< y y+)
          (case-split (rationalp y))
          (case-split (rationalp y+)))
        (<= (fl y) (fl y+))))
    (:linear :corollary (implies (and (< y y+)
          (case-split (rationalp y))
          (case-split (rationalp y+)))
        (<= (fl y) (fl y+))))))

fl-of-non-rationaltheorem

(defthm fl-of-non-rational
  (implies (not (rationalp x)) (equal (fl x) 0))
  :hints (("Goal" :in-theory (enable fl))))

fl-minustheorem

(defthmd fl-minus
  (implies (rationalp x)
    (equal (fl (* -1 x))
      (if (integerp x)
        (* -1 x)
        (1- (* -1 (fl x)))))))

fl-monotone-lineartheorem

(defthm fl-monotone-linear
  (implies (and (<= x y) (rationalp x) (rationalp y))
    (<= (fl x) (fl y)))
  :rule-classes :linear)

n<=fl-lineartheorem

(defthm n<=fl-linear
  (implies (and (<= n x) (rationalp x) (integerp n))
    (<= n (fl x)))
  :rule-classes :linear)

fl+int-rewritetheorem

(defthm fl+int-rewrite
  (implies (and (integerp n) (rationalp x))
    (equal (fl (+ x n)) (+ (fl x) n))))

local

(local (defthm fl/int-1
    (implies (and (rationalp x) (integerp n) (<= 0 n))
      (<= (fl (/ (fl x) n)) (fl (/ x n))))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable fl-def-linear-part-1 fl-def-linear-part-2)
       :use ((:instance fl-def-linear))))))

local

(local (defthm fl/int-2
    (implies (and (rationalp x) (integerp n) (> n 0))
      (>= (fl (/ (fl x) n)) (fl (/ x n))))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable fl-def-linear-part-1 fl-def-linear-part-2)
       :use ((:instance fl-def-linear) (:instance n<=fl-linear (n (* n (fl (/ x n)))))
         (:instance n<=fl-linear (n (fl (/ x n))) (x (/ (fl x) n)))
         (:instance fl-def-linear (x (/ x n)))
         (:instance fl-def-linear (x (/ (fl x) n))))))))

fl/int-rewritetheorem

(defthm fl/int-rewrite
  (implies (and (integerp n) (<= 0 n) (rationalp x))
    (equal (fl (/ (fl x) n)) (fl (/ x n))))
  :hints (("Goal" :use ((:instance fl/int-1) (:instance fl/int-2)))))

fl/int-rewrite-alttheorem

(defthm fl/int-rewrite-alt
  (implies (and (integerp n) (<= 0 n) (rationalp x))
    (equal (fl (* (/ n) (fl x))) (fl (/ x n))))
  :hints (("Goal" :in-theory (disable fl/int-rewrite)
     :use (fl/int-rewrite))))

fl-integer-typetheorem

(defthm fl-integer-type
  (integerp (fl x))
  :rule-classes (:type-prescription))

in-theory

(in-theory (disable (:type-prescription fl)))

fl-inttheorem

(defthm fl-int (implies (integerp x) (equal (fl x) x)))

fl-integerptheorem

(defthm fl-integerp (equal (equal (fl x) x) (integerp x)))

fl-uniquetheorem

(defthm fl-unique
  (implies (and (rationalp x) (integerp n) (<= n x) (< x (1+ n)))
    (equal (fl x) n))
  :rule-classes nil)

fl-rationaltheorem

(defthm fl-rational (rationalp (fl x)))

fl-integertheorem

(defthm fl-integer (integerp (fl x)))

fl-non-negative-integer-type-prescriptiontheorem

(defthm fl-non-negative-integer-type-prescription
  (implies (<= 0 x) (and (<= 0 (fl x)) (integerp (fl x))))
  :rule-classes (:type-prescription))

fl-less-than-zerotheorem

(defthm fl-less-than-zero
  (implies (case-split (rationalp x))
    (equal (< (fl x) 0) (< x 0)))
  :hints (("Goal" :in-theory (enable fl))))

fl-non-negative-lineartheorem

(defthm fl-non-negative-linear
  (implies (<= 0 x) (<= 0 (fl x)))
  :rule-classes (:linear))

pull-constant-out-of-fltheorem

(defthm pull-constant-out-of-fl
  (implies (and (syntaxp (and (quotep c1) (>= (abs (cadr c1)) 1)))
      (rationalp c1)
      (rationalp x))
    (equal (fl (+ c1 x))
      (+ (truncate c1 1) (fl (+ (rem c1 1) x)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable rem) '(truncate)))))

fl-minus-factortheorem

(defthm fl-minus-factor
  (implies (and (syntaxp (quotep k))
      (< k 0)
      (rationalp k)
      (rationalp x))
    (equal (fl (* k x))
      (if (integerp (* k x))
        (* -1 (fl (* (- k) x)))
        (+ -1 (- (fl (* (- k) x))))))))

fl-<-integertheorem

(defthm fl-<-integer
  (implies (and (integerp y) (case-split (rationalp x)))
    (equal (< (fl x) y) (< x y))))

fl->-integertheorem

(defthm fl->-integer
  (implies (and (integerp y) (case-split (rationalp x)))
    (equal (< y (fl x)) (<= (+ 1 y) x))))

fl-equal-0theorem

(defthm fl-equal-0
  (implies (case-split (rationalp x))
    (equal (equal (fl x) 0) (and (<= 0 x) (< x 1)))))

fl-equal-0-alttheorem

(defthmd fl-equal-0-alt
  (implies (and (< x 1) (<= 0 x) (case-split (rationalp x)))
    (equal (fl x) 0)))

fl-strong-monotonetheorem

(defthm fl-strong-monotone
  (implies (and (< x y) (rationalp x) (rationalp y))
    (< (fl x) y)))

fl-weak-monotonetheorem

(defthm fl-weak-monotone
  (implies (and (<= x y) (rationalp x) (rationalp y))
    (<= (fl x) y)))

fl-def-linear-quotienttheorem

(defthm fl-def-linear-quotient
  (implies (and (< 0 y)
      (case-split (rationalp x))
      (case-split (rationalp y)))
    (and (not (< x (* y (fl (* x (/ y))))))
      (not (< x (* y (fl (* (/ y) x)))))))
  :hints (("Goal" :in-theory (disable fl-strong-monotone
       fl-weak-monotone
       fl-def-linear-part-1)
     :use (:instance fl-def-linear-part-1 (x (/ x y))))))

floor-fltheorem

(defthm floor-fl
  (equal (floor m n) (fl (/ m n)))
  :hints (("goal" :in-theory (e/d (fl) (rationalp-product))
     :cases ((rationalp m)))))

other

(theory-invariant (incompatible (:rewrite floor-fl) (:definition fl))
  :key floor-fl--and--fl--conflict)

fl-of-odd/2theorem

(defthm fl-of-odd/2
  (implies (and (integerp x) (not (integerp (* 1/2 x))))
    (equal (fl (* 1/2 x)) (- (* 1/2 x) 1/2))))

fl-of-even/2theorem

(defthm fl-of-even/2
  (implies (and (integerp (* x (/ 2))))
    (equal (fl (* 1/2 x)) (* 1/2 x))))

fl-force-to-0theorem

(defthm fl-force-to-0
  (implies (case-split (rationalp x))
    (equal (equal 0 (fl x)) (and (<= 0 x) (< x 1)))))

in-theory

(in-theory (disable fl-force-to-0))

fl-factor-out-integer-boundtheorem

(defthm fl-factor-out-integer-bound
  (implies (and (integerp n) (> n 0) (rationalp x))
    (<= (* n (fl x)) (fl (* n x)))))

fl-factor-out-integer-bound-2theorem

(defthm fl-factor-out-integer-bound-2
  (implies (and (integerp n) (> n 0) (rationalp m))
    (<= (* n (fl (* m (/ n)))) (fl m))))

fl-plus-integer-erictheorem

(defthm fl-plus-integer-eric
  (implies (and (integerp n) (case-split (rationalp x)))
    (equal (fl (+ x n)) (+ n (fl x)))))

local

(local (in-theory (disable floor-fl)))

quotient-numer-denom-erictheorem

(defthm quotient-numer-denom-eric
  (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)))
  :hints (("Goal" :cases ((and (= x 0) (= y 0)) (and (not (= x 0)) (= y 0))
       (and (= x 0) (not (= y 0)))))))

fl-claim-rewrite-to-integerp-claim-gentheorem

(defthm fl-claim-rewrite-to-integerp-claim-gen
  (implies (and (equal k-inverse (/ k))
      (case-split (acl2-numberp k))
      (case-split (not (equal k 0)))
      (case-split (acl2-numberp x)))
    (and (equal (equal (* k (fl (* k-inverse x))) x)
        (integerp (* k-inverse x)))
      (equal (equal (* k (fl (* x k-inverse))) x)
        (integerp (* k-inverse x)))))
  :hints (("Goal" :in-theory (disable fl-integerp)
     :use (:instance fl-integerp (x (* k-inverse x))))))

in-theory

(in-theory (disable fl-claim-rewrite-to-integerp-claim-gen))

fl-claim-rewrite-to-integerp-claim-gen-2theorem

(defthm fl-claim-rewrite-to-integerp-claim-gen-2
  (implies (and (equal k-inverse (/ k))
      (case-split (acl2-numberp k))
      (case-split (not (equal k 0)))
      (case-split (acl2-numberp x))
      (case-split (acl2-numberp y)))
    (and (equal (equal (* k (fl (* k-inverse x y))) (* x y))
        (integerp (* k-inverse x y)))
      (equal (equal (* k (fl (* x k-inverse y))) (* x y))
        (integerp (* k-inverse x y)))
      (equal (equal (* k (fl (* x y k-inverse))) (* x y))
        (integerp (* k-inverse x y)))))
  :hints (("Goal" :in-theory (disable fl-integerp)
     :use (:instance fl-claim-rewrite-to-integerp-claim-gen
       (x (* x y))))))

fl-claim-rewrite-to-integerp-claimtheorem

(defthm fl-claim-rewrite-to-integerp-claim
  (implies (and (syntaxp (and (quotep k-inverse) (quotep k)))
      (equal k-inverse (/ k))
      (case-split (acl2-numberp k))
      (case-split (not (equal k 0)))
      (case-split (acl2-numberp x)))
    (and (equal (equal (* k (fl (* k-inverse x))) x)
        (integerp (* k-inverse x)))
      (equal (equal (* k (fl (* x k-inverse))) x)
        (integerp (* k-inverse x)))))
  :hints (("Goal" :in-theory (disable fl-integerp)
     :use (:instance fl-integerp (x (* k-inverse x))))))

y-is-oddtheorem

(defthm y-is-odd
  (equal (equal y (+ 1 (* 2 (fl (* 1/2 y)))))
    (and (integerp y) (not (integerp (* 1/2 y))))))

include-book

(include-book "negative-syntaxp")

fl-minus-gentheorem

(defthm fl-minus-gen
  (implies (and (syntaxp (negative-syntaxp x))
      (case-split (rationalp x)))
    (equal (fl x)
      (if (integerp x)
        (* -1 (fl (* -1 x)))
        (+ -1 (- (fl (* -1 x))))))))

in-theory

(in-theory (disable fl-minus-factor))

fl-of-fraction-max-change-case-1theorem

(defthmd fl-of-fraction-max-change-case-1
  (implies (and (not (integerp (/ p q)))
      (integerp p)
      (integerp q)
      (< 0 q))
    (>= (+ 1 (fl (/ p q))) (+ (/ p q) (/ q))))
  :otf-flg t
  :hints (("Goal" :in-theory (set-difference-theories (enable fl floor) '(floor-fl))
     :use ((:instance <=-transitive
        (a (+ (/ q) (* p (/ q))))
        (b (+ (* p (/ q)) (/ (denominator (* p (/ q))))))
        (c (+ 1
            (nonnegative-integer-quotient (numerator (* p (/ q)))
              (denominator (* p (/ q))))))) (:instance nniq-eric-8 (p (- p)))
       (:instance quotient-numer-denom (x (- p)) (y q))
       (:instance nniq-lower-bound-non-integer-case (x (/ p q)))))))

fl-of-fraction-max-change-case-2theorem

(defthmd fl-of-fraction-max-change-case-2
  (implies (and (integerp (/ p q)) (integerp p) (integerp q) (< 0 q))
    (>= (+ 1 (fl (/ p q))) (+ (/ p q) (/ q))))
  :otf-flg t
  :hints (("Goal" :use (:instance (:instance mult-both-sides-of-<-by-positive
         (a 1)
         (b (/ q))
         (c q))))))

fl-of-fraction-max-changetheorem

(defthm fl-of-fraction-max-change
  (implies (and (< 0 q) (integerp p) (integerp q))
    (>= (+ 1 (fl (/ p q))) (+ (/ p q) (/ q))))
  :otf-flg t
  :hints (("Goal" :use (fl-of-fraction-max-change-case-2 fl-of-fraction-max-change-case-1))))

int-uniquetheorem

(defthm int-unique
  (implies (and (integerp i)
      (integerp j)
      (rationalp x)
      (rationalp y)
      (<= x y)
      (< x i)
      (<= i y)
      (< x j)
      (<= j y)
      (<= (- y x) 1))
    (equal i j))
  :rule-classes nil)

fl-unique-2theorem

(defthm fl-unique-2
  (implies (rationalp x)
    (equal (and (integerp n) (<= n x) (< x (1+ n)))
      (equal (fl x) n)))
  :rule-classes nil)

fl-m+1encapsulate

(encapsulate nil
  (local (defthm fl-m+1-1
      (implies (and (integerp m)
          (integerp n)
          (>= m 0)
          (> n 0)
          (integerp (+ (/ n) (* m (/ n)))))
        (= (fl (- (/ (1+ m) n))) (1- (- (fl (/ m n))))))
      :hints (("Goal" :use (:instance fl-unique
           (x (* m (/ n)))
           (n (/ (+ 1 (- n) m) n)))))
      :rule-classes nil))
  (local (defthm fl-m+1-2
      (implies (and (integerp m)
          (integerp n)
          (>= m 0)
          (> n 0)
          (not (integerp (+ (/ n) (* m (/ n))))))
        (= (fl (- (/ (1+ m) n))) (1- (- (fl (/ m n))))))
      :otf-flg t
      :rule-classes nil
      :hints (("Goal" :in-theory (disable fl-integer-type
           fl-non-negative-integer-type-prescription
           fl-def-linear-part-2)
         :use ((:instance fl-def-linear (x (+ (/ n) (* m (/ n))))) (:instance fl-of-fraction-max-change (p m) (q n))
           (:instance fl-unique-2
             (x (* m (/ n)))
             (n (+ -1 (/ n) (* m (/ n)))))
           (:instance int-unique
             (i (fl (+ (/ n) (* m (/ n)))))
             (j (fl (* m (/ n))))
             (x (+ (/ m n) (/ n) -1))
             (y (+ (/ m n) (/ n)))))))))
  (defthm fl-m+1
    (implies (and (integerp m) (integerp n) (>= m 0) (> n 0))
      (= (fl (- (/ (1+ m) n))) (1- (- (fl (/ m n))))))
    :hints (("Goal" :use (fl-m+1-1 fl-m+1-2)))
    :rule-classes nil))

fl-of-fraction-min-changetheorem

(defthmd fl-of-fraction-min-change
  (implies (and (not (integerp (/ p q))) (integerp p) (integerp q))
    (<= (/ q) (- (/ p q) (fl (/ p q)))))
  :otf-flg t
  :hints (("Goal" :do-not-induct t
     :in-theory (set-difference-theories (enable fl floor)
       '(nniq-eric-8 fl-of-fraction-max-change))
     :use ((:instance fl-of-fraction-max-change (p (- p))) (:instance fl-of-fraction-max-change (q (- q)))))))

fl-boundtheorem

(defthm fl-bound
  (implies (and (< 0 y) (rationalp x) (rationalp y))
    (<= (* y (fl (* x (/ y)))) x))
  :hints (("Goal" :use (:instance floor-upper-bound (i x) (j y))
     :in-theory (e/d (fl) (floor-upper-bound)))))

quot-bndtheorem

(defthm quot-bnd
  (implies (and (<= 0 x) (<= 0 y) (rationalp x) (rationalp y))
    (<= (* y (fl (/ x y))) x))
  :rule-classes :linear :hints (("Goal" :in-theory (disable fl-weak-monotone fl-def-linear-part-1)
     :use (:instance fl-def-linear-part-1 (x (/ x y))))))

x-times-something>=1theorem

(defthmd x-times-something>=1
  (implies (and (case-split (<= 1 y))
      (case-split (rationalp y))
      (case-split (rationalp x))
      (case-split (<= 0 x)))
    (<= x (* x y)))
  :rule-classes :linear)

fl-<=-ytheorem

(defthm fl-<=-y
  (implies (and (<= x y) (case-split (not (complex-rationalp x))))
    (<= (fl x) y)))

fl-equal-rewritetheorem

(defthmd fl-equal-rewrite
  (implies (and (rationalp x) (integerp n))
    (equal (equal (fl x) n) (and (<= n x) (< x (+ 1 n))))))