fl - ACL2 Book

other

(in-package "ACL2")

include-book

(include-book "negative-syntaxp")

local

(local (include-book "fl-proofs"))

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)))))

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))))

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))))))))

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))))
  :rule-classes :linear)

fl-def-linear-part-1theorem

(defthm fl-def-linear-part-1
  (implies (case-split (not (complex-rationalp x)))
    (<= (fl x) x))
  :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))))
  :rule-classes (:rewrite (:linear :trigger-terms ((fl x)))))

a13theorem

(defthmd a13
  (implies (case-split (rationalp x))
    (and (< (1- x) (fl x)) (<= (fl x) x)))
  :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+)))
  :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)))

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))))

fl/int-rewritetheorem

(defthm fl/int-rewrite
  (implies (and (integerp n) (<= 0 n) (rationalp x))
    (equal (fl (* (fl x) (/ n))) (fl (/ x n)))))

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)))))

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))))

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))))))

fl-minus-factortheorem

(defthmd 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))))))))

floor-fltheorem

(defthm floor-fl (equal (floor m n) (fl (/ m n))))

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

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

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))))

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

(defthmd 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))))))

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))))))

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))))))

y-is-oddtheorem

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

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))))))))

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)))))

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)))))

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)))))

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+1theorem

(defthm fl-m+1
  (implies (and (integerp m) (integerp n) (>= m 0) (> n 0))
    (= (fl (- (/ (1+ m) n))) (1- (- (fl (/ m n))))))
  :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))))))

fl-boundtheorem

(defthm fl-bound
  (implies (and (< 0 y) (rationalp x) (rationalp y))
    (<= (* y (fl (* x (/ y)))) x)))

quot-bndtheorem

(defthm quot-bnd
  (implies (and (<= 0 x) (<= 0 y) (rationalp x) (rationalp y))
    (<= (* y (fl (/ x y))) x))
  :rule-classes :linear)

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))))))

fl

Included Books