simple-equalities-and-inequalities-helper

(local (include-book "../../support/top"))

(local (defun rationalp-guard-fn
    (args)
    (if (endp (cdr args))
      `((rationalp ,(CAR ARGS)))
      (cons `(rationalp ,(CAR ARGS))
        (rationalp-guard-fn (cdr args))))))

(local (defmacro rationalp-guard
    (&rest args)
    (if (endp (cdr args))
      `(rationalp ,(CAR ARGS))
      (cons 'and (rationalp-guard-fn args)))))

(local (defun real/rationalp-guard-fn
    (args)
    (if (endp (cdr args))
      `((real/rationalp ,(CAR ARGS)))
      (cons `(real/rationalp ,(CAR ARGS))
        (real/rationalp-guard-fn (cdr args))))))

(local (defmacro real/rationalp-guard
    (&rest args)
    (if (endp (cdr args))
      `(real/rationalp ,(CAR ARGS))
      (cons 'and (real/rationalp-guard-fn args)))))

(local (defthm niq-bounds
    (implies (and (integerp i) (<= 0 i) (integerp j) (< 0 j))
      (and (<= (nonnegative-integer-quotient i j) (/ i j))
        (< (+ (/ i j) -1) (nonnegative-integer-quotient i j))))
    :hints (("Subgoal *1/1''" :in-theory (enable normalize-<-/-to-*-3-3)))
    :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))))

(local (defthm floor-bounds-1
    (implies (real/rationalp-guard x y)
      (and (< (+ (/ x y) -1) (floor x y))
        (<= (floor x y) (/ x y))))
    :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))

(local (defthm floor-bounds-2
    (implies (and (real/rationalp-guard x y) (integerp (/ x y)))
      (equal (floor x y) (/ x y)))
    :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))

(local (defthm floor-bounds-3
    (implies (and (real/rationalp-guard x y) (not (integerp (/ x y))))
      (< (floor x y) (/ x y)))
    :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))

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