inequalities

other

(in-package "ACL2")

local

(local (include-book "basic-arithmetic"))

fcmacro

(defmacro fc (x) x)

local

(local (defthm iff-equal
    (equal (equal (< w x) (< y z)) (iff (< w x) (< y z)))))

/-preserves-positivetheorem

(defthm /-preserves-positive
  (implies (real/rationalp x) (equal (< 0 (/ x)) (< 0 x))))

/-preserves-negativetheorem

(defthm /-preserves-negative
  (implies (real/rationalp x) (equal (< (/ x) 0) (< x 0))))

<-0-minustheorem

(defthm <-0-minus (equal (< 0 (- x)) (< x 0)))

<-minus-zerotheorem

(defthm <-minus-zero (equal (< (- x) 0) (< 0 x)))

<-minus-minustheorem

(defthm <-minus-minus (equal (< (- x) (- y)) (< y x)))

<-0-+-negative-1theorem

(defthm <-0-+-negative-1 (equal (< 0 (+ (- y) x)) (< y x)))

<-0-+-negative-2theorem

(defthm <-0-+-negative-2 (equal (< 0 (+ x (- y))) (< y x)))

<-+-negative-0-1theorem

(defthm <-+-negative-0-1 (equal (< (+ (- y) x) 0) (< x y)))

<-+-negative-0-2theorem

(defthm <-+-negative-0-2 (equal (< (+ x (- y)) 0) (< x y)))

<-*-0theorem

(defthm <-*-0
  (implies (and (real/rationalp x) (real/rationalp y))
    (equal (< (* x y) 0)
      (and (not (equal x 0))
        (not (equal y 0))
        (iff (< x 0) (< 0 y))))))

0-<-*theorem

(defthm 0-<-*
  (implies (and (real/rationalp x) (real/rationalp y))
    (equal (< 0 (* x y))
      (and (not (equal x 0))
        (not (equal y 0))
        (iff (< 0 x) (< 0 y))))))

<-*-right-canceltheorem

(defthm <-*-right-cancel
  (implies (and (fc (real/rationalp x))
      (fc (real/rationalp y))
      (fc (real/rationalp z)))
    (equal (< (* x z) (* y z))
      (cond ((< 0 z) (< x y))
        ((< z 0) (< y x))
        ((equal z 0) nil)
        (t nil))))
  :hints (("Goal" :use ((:instance (:theorem (implies (and (real/rationalp a) (< 0 a) (real/rationalp b) (< 0 b))
            (< 0 (* a b))))
        (a (abs (- y x)))
        (b (abs z))))
     :in-theory (disable 0-<-*))))

<-*-left-canceltheorem

(defthm <-*-left-cancel
  (implies (and (fc (real/rationalp x))
      (fc (real/rationalp y))
      (fc (real/rationalp z)))
    (equal (< (* z x) (* z y))
      (cond ((< 0 z) (< x y))
        ((< z 0) (< y x))
        ((equal z 0) nil)
        (t nil)))))

<-*-x-y-ytheorem

(defthm <-*-x-y-y
  (implies (and (fc (real/rationalp x)) (fc (real/rationalp y)))
    (equal (< (* x y) y)
      (cond ((< 0 y) (< x 1))
        ((< y 0) (< 1 x))
        ((equal y 0) nil)
        (t nil))))
  :hints (("Goal" :use ((:instance <-*-right-cancel (x x) (y 1) (z y))))))

<-*-y-x-ytheorem

(defthm <-*-y-x-y
  (implies (and (fc (real/rationalp x)) (fc (real/rationalp y)))
    (equal (< (* y x) y)
      (cond ((< 0 y) (< x 1))
        ((< y 0) (< 1 x))
        ((equal y 0) nil)
        (t nil)))))

<-y-*-x-ytheorem

(defthm <-y-*-x-y
  (implies (and (fc (real/rationalp x)) (fc (real/rationalp y)))
    (equal (< y (* x y))
      (cond ((< 0 y) (< 1 x))
        ((< y 0) (< x 1))
        ((equal y 0) nil)
        (t nil))))
  :hints (("Goal" :use ((:instance <-*-right-cancel (x 1) (y x) (z y))))))

<-y-*-y-xtheorem

(defthm <-y-*-y-x
  (implies (and (fc (real/rationalp x)) (fc (real/rationalp y)))
    (equal (< y (* y x))
      (cond ((< 0 y) (< 1 x))
        ((< y 0) (< x 1))
        ((equal y 0) nil)
        (t nil)))))

Included Books