fp2 - ACL2 Book

Included Books

ihs-definitions ihs-lemmas non-linear inverted-factor e0-ordinal

other

(in-package "ACL2")

local

(local (include-book "../../../ihs/ihs-definitions"))

local

(local (include-book "../../../ihs/ihs-lemmas"))

local

(local (include-book "../../../ihs/ihs-lemmas"))

local

(local (progn (in-theory nil)
    (in-theory (enable basic-boot-strap
        ihs-math
        quotient-remainder-rules
        logops-lemmas-theory))))

local

(local (in-theory (enable logops-definitions-theory)))

a1theorem

(defthm a1 (equal (+ x (+ y z)) (+ y (+ x z))))

a2theorem

(defthm a2 (equal (- x) (* -1 x)))

local

(local (in-theory (disable functional-commutativity-of-minus-*-right
      functional-commutativity-of-minus-*-left)))

a3theorem

(defthm a3
  (and (implies (syntaxp (and (quotep c1) (quotep c2)))
      (and (equal (+ (* c1 x) (* c2 x)) (* (+ c1 c2) x))
        (equal (+ (* c1 x) (+ (* c2 x) y)) (+ (* (+ c1 c2) x) y))))
    (implies (syntaxp (quotep c2))
      (and (equal (+ x (* c2 x)) (* (+ 1 c2) x))
        (equal (+ x (+ (* c2 x) y1)) (+ (* (+ 1 c2) x) y1))
        (equal (+ x (+ y1 (* c2 x))) (+ (* (+ 1 c2) x) y1))
        (equal (+ x (+ y1 (+ (* c2 x) y2)))
          (+ (* (+ 1 c2) x) y1 y2))
        (equal (+ x (+ y1 (+ y2 (* c2 x))))
          (+ (* (+ 1 c2) x) y1 y2))
        (equal (+ x (+ y1 (+ y2 (+ y3 (* c2 x)))))
          (+ (* (+ 1 c2) x) y1 y2 y3))
        (equal (+ x (+ y1 (+ y2 (+ (* c2 x) y3))))
          (+ (* (+ 1 c2) x) y1 y2 y3))))
    (and (equal (+ x x) (* 2 x))
      (equal (+ x (+ x y1)) (+ (* 2 x) y1)))))

a4theorem

(defthm a4
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (equal (+ c1 (+ c2 y1)) (+ (+ c1 c2) y1))))

a5theorem

(defthm a5
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (equal (* c1 (* c2 y1)) (* (* c1 c2) y1))))

a6theorem

(defthm a6 (equal (/ (/ x)) (fix x)))

a7theorem

(defthm a7 (equal (/ (* x y)) (* (/ x) (/ y))))

a8theorem

(defthm a8
  (implies (and (case-split (acl2-numberp x))
      (case-split (not (equal x 0))))
    (and (equal (* x (* (/ x) y)) (fix y))
      (equal (* x (/ x)) 1)))
  :hints (("Goal" :cases ((acl2-numberp x)))))

in-theory

(in-theory (disable inverse-of-*))

a9theorem

(defthm a9
  (and (equal (* 0 x) 0)
    (equal (* x (* y z)) (* y (* x z)))
    (equal (* x (+ y z)) (+ (* x y) (* x z)))
    (equal (* (+ y z) x) (+ (* y x) (* z x)))))

local

(local (encapsulate nil
    (local (include-book "../../../arithmetic-2/meta/non-linear"))
    (defthm *-weakly-monotonic-alt
      (implies (and (<= y y+) (<= 0 x) (rationalp x))
        (<= (* x y) (* x y+)))
      :hints (("Goal" :cases ((equal x 0))))
      :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
        (:forward-chaining :trigger-terms ((* y x) (* y+ x))
          :corollary (implies (and (<= y y+) (<= 0 x) (rationalp x))
            (<= (* y x) (* y+ x))))
        (:linear :corollary (implies (and (<= y y+) (rationalp x) (<= 0 x))
            (<= (* y x) (* y+ x))))))
    (defthm *-strongly-monotonic-alt
      (implies (and (< y y+) (rationalp x) (< 0 x))
        (< (* x y) (* x y+)))
      :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
        (:forward-chaining :trigger-terms ((* y x) (* y+ x))
          :corollary (implies (and (< y y+) (rationalp x) (< 0 x))
            (< (* y x) (* y+ x))))
        (:linear :corollary (implies (and (< y y+) (rationalp x) (< 0 x))
            (< (* y x) (* y+ x))))))
    (defthm *-weakly-monotonic-negative-multiplier-alt
      (implies (and (<= y y+) (rationalp x) (< x 0))
        (<= (* x y+) (* x y)))
      :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
        (:forward-chaining :trigger-terms ((* y x) (* y+ x))
          :corollary (implies (and (<= y y+) (rationalp x) (< x 0))
            (<= (* y+ x) (* y x))))
        (:linear :corollary (implies (and (<= y y+) (rationalp x) (< x 0))
            (<= (* y+ x) (* y x))))))
    (defthm *-strongly-monotonic-negative-multiplier-alt
      (implies (and (< y y+) (rationalp x) (< x 0))
        (< (* x y+) (* x y)))
      :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
        (:forward-chaining :trigger-terms ((* y x) (* y+ x))
          :corollary (implies (and (< y y+) (rationalp x) (< x 0))
            (< (* y+ x) (* y x))))
        (:linear :corollary (implies (and (< y y+) (rationalp x) (< x 0))
            (< (* y+ x) (* y x))))))
    (defthm /-weakly-monotonic-alt
      (implies (and (<= y y+) (rationalp y) (rationalp y+) (< 0 y))
        (<= (/ y+) (/ y)))
      :rule-classes ((:forward-chaining :trigger-terms ((/ y+) (/ y))) :linear))
    (defthm /-strongly-monotonic-alt
      (implies (and (< y y+) (rationalp y) (rationalp y+) (< 0 y))
        (< (/ y+) (/ y)))
      :rule-classes ((:forward-chaining :trigger-terms ((/ y+) (/ y))) :linear))))

/-weakly-monotonictheorem

(defthm /-weakly-monotonic
  (implies (and (<= y y+)
      (< 0 y)
      (case-split (rationalp y))
      (case-split (rationalp y+)))
    (<= (/ y+) (/ y)))
  :hints (("Goal" :use (/-weakly-monotonic-alt)))
  :rule-classes ((:forward-chaining :trigger-terms ((/ y+) (/ y))) :linear))

/-strongly-monotonictheorem

(defthm /-strongly-monotonic
  (implies (and (< y y+)
      (< 0 y)
      (case-split (rationalp y))
      (case-split (rationalp y+)))
    (< (/ y+) (/ y)))
  :hints (("Goal" :use (/-strongly-monotonic-alt)))
  :rule-classes ((:forward-chaining :trigger-terms ((/ y+) (/ y))) :linear))

*-weakly-monotonictheorem

(defthm *-weakly-monotonic
  (implies (and (<= y y+) (<= 0 x) (case-split (rationalp x)))
    (<= (* x y) (* x y+)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
    (:forward-chaining :trigger-terms ((* y x) (* y+ x))
      :corollary (implies (and (<= y y+) (<= 0 x) (case-split (rationalp x)))
        (<= (* y x) (* y+ x))))
    (:linear :corollary (implies (and (<= y y+) (<= 0 x) (case-split (rationalp x)))
        (<= (* y x) (* y+ x))))))

*-strongly-monotonictheorem

(defthm *-strongly-monotonic
  (implies (and (< y y+) (< 0 x) (case-split (rationalp x)))
    (< (* x y) (* x y+)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
    (:forward-chaining :trigger-terms ((* y x) (* y+ x))
      :corollary (implies (and (< y y+) (< 0 x) (case-split (rationalp x)))
        (< (* y x) (* y+ x))))
    (:linear :corollary (implies (and (< y y+) (< 0 x) (case-split (rationalp x)))
        (< (* y x) (* y+ x))))))

*-weakly-monotonic-negative-multipliertheorem

(defthm *-weakly-monotonic-negative-multiplier
  (implies (and (<= y y+) (< x 0) (case-split (rationalp x)))
    (<= (* x y+) (* x y)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
    (:forward-chaining :trigger-terms ((* y x) (* y+ x))
      :corollary (implies (and (<= y y+) (< x 0) (case-split (rationalp x)))
        (<= (* y+ x) (* y x))))
    (:linear :corollary (implies (and (<= y y+) (< x 0) (case-split (rationalp x)))
        (<= (* y+ x) (* y x))))))

*-strongly-monotonic-negative-multipliertheorem

(defthm *-strongly-monotonic-negative-multiplier
  (implies (and (< y y+) (< x 0) (case-split (rationalp x)))
    (< (* x y+) (* x y)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x y) (* x y+))) (:linear)
    (:forward-chaining :trigger-terms ((* y x) (* y+ x))
      :corollary (implies (and (< y y+) (< x 0) (case-split (rationalp x)))
        (< (* y+ x) (* y x))))
    (:linear :corollary (implies (and (< y y+) (< x 0) (case-split (rationalp x)))
        (< (* y+ x) (* y x))))))

abs*nonneg-openencapsulate

(encapsulate nil
  (local (defthm renaming
      (implies (and (rationalp a)
          (rationalp xmax)
          (rationalp b)
          (rationalp bmax)
          (< (- xmax) a)
          (<= a xmax)
          (< 0 xmax)
          (<= 0 b)
          (< b bmax))
        (and (< (- (* xmax bmax)) (* a b))
          (< (* a b) (* xmax bmax))))
      :hints (("Goal" :cases ((equal b 0))))))
  (defthm abs*nonneg-open
    (implies (and (rationalp a)
        (rationalp amax)
        (rationalp b)
        (rationalp bmax)
        (< (- amax) a)
        (<= a amax)
        (< 0 amax)
        (<= 0 b)
        (< b bmax))
      (and (< (- (* amax bmax)) (* a b))
        (< (* a b) (* amax bmax))))
    :hints (("Goal" :by renaming))
    :rule-classes nil))

abs*nonneg-closedtheorem

(defthm abs*nonneg-closed
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (< (- amax) a)
      (< a amax)
      (< 0 amax)
      (<= 0 b)
      (<= b bmax)
      (< 0 bmax))
    (and (< (- (* amax bmax)) (* a b))
      (< (* a b) (* amax bmax))))
  :hints (("Goal" :cases ((equal b 0))))
  :rule-classes nil)

nonneg-closed*abstheorem

(defthm nonneg-closed*abs
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (< (- amax) a)
      (< a amax)
      (< 0 amax)
      (<= 0 b)
      (<= b bmax)
      (< 0 bmax))
    (and (< (- (* amax bmax)) (* b a))
      (< (* b a) (* amax bmax))))
  :hints (("Goal" :use abs*nonneg-closed))
  :rule-classes nil)

nonneg-open*abstheorem

(defthm nonneg-open*abs
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (< (- amax) a)
      (<= a amax)
      (< 0 amax)
      (<= 0 b)
      (< b bmax))
    (and (< (- (* bmax amax)) (* a b))
      (< (* a b) (* bmax amax))))
  :hints (("Goal" :use abs*nonneg-open))
  :rule-classes nil)

nonneg-open*nonneg-closedtheorem

(defthm nonneg-open*nonneg-closed
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (<= 0 a)
      (< a amax)
      (<= 0 b)
      (<= b bmax)
      (< 0 bmax))
    (and (<= 0 (* a b)) (< (* a b) (* amax bmax))))
  :hints (("Goal" :use abs*nonneg-closed))
  :rule-classes nil)

nonneg-open*nonneg-opentheorem

(defthm nonneg-open*nonneg-open
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (<= 0 a)
      (< a amax)
      (<= 0 b)
      (< b bmax))
    (and (<= 0 (* a b)) (< (* a b) (* amax bmax))))
  :hints (("Goal" :use abs*nonneg-open))
  :rule-classes nil)

nonneg-closed*nonneg-opentheorem

(defthm nonneg-closed*nonneg-open
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (<= 0 a)
      (< a amax)
      (<= 0 b)
      (<= b bmax)
      (< 0 bmax))
    (and (<= 0 (* b a)) (< (* b a) (* amax bmax))))
  :hints (("Goal" :use nonneg-open*nonneg-closed))
  :rule-classes nil)

nonneg-closed*nonneg-closedtheorem

(defthm nonneg-closed*nonneg-closed
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (<= 0 a)
      (<= a amax)
      (< 0 amax)
      (<= 0 b)
      (<= b bmax)
      (< 0 bmax))
    (and (<= 0 (* a b)) (<= (* a b) (* amax bmax))))
  :rule-classes nil)

abs*abstheorem

(defthm abs*abs
  (implies (and (rationalp a)
      (rationalp amax)
      (rationalp b)
      (rationalp bmax)
      (< (- amax) a)
      (< a amax)
      (< 0 amax)
      (< (- bmax) b)
      (<= b bmax)
      (< 0 bmax))
    (and (< (- (* amax bmax)) (* a b))
      (< (* a b) (* amax bmax))))
  :hints (("Goal" :cases ((< b 0) (> b 0))))
  :rule-classes nil)

rearrange-negative-coefs-<theorem

(defthm rearrange-negative-coefs-<
  (and (equal (< (* (- c) x) z) (< 0 (+ (* c x) z)))
    (equal (< (+ (* (- c) x) y) z) (< y (+ (* c x) z)))
    (equal (< (+ y (* (- c) x)) z) (< y (+ (* c x) z)))
    (equal (< (+ y1 y2 (* (- c) x)) z)
      (< (+ y1 y2) (+ (* c x) z)))
    (equal (< (+ y1 y2 y3 (* (- c) x)) z)
      (< (+ y1 y2 y3) (+ (* c x) z)))
    (equal (< z (+ (* (- c) x) y)) (< (+ (* c x) z) y))
    (equal (< z (+ y (* (- c) x))) (< (+ (* c x) z) y))
    (equal (< z (+ y1 y2 (* (- c) x)))
      (< (+ (* c x) z) (+ y1 y2)))
    (equal (< z (+ y1 y2 y3 (* (- c) x)))
      (< (+ (* c x) z) (+ y1 y2 y3)))))

rearrange-negative-coefs-equaltheorem

(defthm rearrange-negative-coefs-equal
  (and (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp z)))
      (equal (equal (* (- c) x) z) (equal 0 (+ (* c x) z))))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y))
        (case-split (rationalp z)))
      (equal (equal (+ (* (- c) x) y) z) (equal y (+ (* c x) z))))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y))
        (case-split (rationalp z)))
      (equal (equal (+ y (* (- c) x)) z) (equal y (+ (* c x) z))))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y1))
        (case-split (rationalp y2))
        (case-split (rationalp z)))
      (equal (equal (+ y1 y2 (* (- c) x)) z)
        (equal (+ y1 y2) (+ (* c x) z))))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y1))
        (case-split (rationalp y2))
        (case-split (rationalp y3))
        (case-split (rationalp z)))
      (equal (equal (+ y1 y2 y3 (* (- c) x)) z)
        (equal (+ y1 y2 y3) (+ (* c x) z))))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y))
        (case-split (rationalp z)))
      (equal (equal z (+ (* (- c) x) y)) (equal (+ (* c x) z) y)))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y))
        (case-split (rationalp z)))
      (equal (equal z (+ y (* (- c) x))) (equal (+ (* c x) z) y)))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y1))
        (case-split (rationalp y2))
        (case-split (rationalp z)))
      (equal (equal z (+ y1 y2 (* (- c) x)))
        (equal (+ (* c x) z) (+ y1 y2))))
    (implies (and (case-split (rationalp c))
        (case-split (rationalp x))
        (case-split (rationalp y1))
        (case-split (rationalp y2))
        (case-split (rationalp y3))
        (case-split (rationalp z)))
      (equal (equal z (+ y1 y2 y3 (* (- c) x)))
        (equal (+ (* c x) z) (+ y1 y2 y3))))))

include-book

(include-book "inverted-factor")

equal-multiply-through-by-inverted-factor-from-left-hand-sidetheorem

(defthm equal-multiply-through-by-inverted-factor-from-left-hand-side
  (implies (and (bind-free (find-inverted-factor lhs) (k))
      (syntaxp (not (is-a-factor k lhs)))
      (syntaxp (sum-of-products-syntaxp lhs))
      (syntaxp (sum-of-products-syntaxp rhs))
      (syntaxp (not (quotep lhs)))
      (case-split (not (equal k 0)))
      (case-split (acl2-numberp k))
      (case-split (acl2-numberp lhs))
      (case-split (acl2-numberp rhs)))
    (equal (equal lhs rhs) (equal (* lhs k) (* rhs k)))))

equal-multiply-through-by-inverted-factor-from-right-hand-sidetheorem

(defthm equal-multiply-through-by-inverted-factor-from-right-hand-side
  (implies (and (bind-free (find-inverted-factor rhs) (k))
      (syntaxp (not (is-a-factor k rhs)))
      (syntaxp (sum-of-products-syntaxp lhs))
      (syntaxp (sum-of-products-syntaxp rhs))
      (syntaxp (not (quotep rhs)))
      (case-split (not (equal k 0)))
      (case-split (acl2-numberp k))
      (case-split (acl2-numberp lhs))
      (case-split (acl2-numberp rhs)))
    (equal (equal lhs rhs) (equal (* lhs k) (* rhs k)))))

less-than-multiply-through-by-inverted-factor-from-left-hand-sidetheorem

(defthm less-than-multiply-through-by-inverted-factor-from-left-hand-side
  (implies (and (bind-free (find-inverted-factor lhs) (k))
      (syntaxp (not (is-a-factor k lhs)))
      (syntaxp (sum-of-products-syntaxp lhs))
      (syntaxp (sum-of-products-syntaxp rhs))
      (case-split (not (equal k 0)))
      (case-split (rationalp k)))
    (equal (< lhs rhs)
      (if (<= 0 k)
        (< (* lhs k) (* rhs k))
        (< (* rhs k) (* lhs k))))))

less-than-multiply-through-by-inverted-factor-from-right-hand-sidetheorem

(defthm less-than-multiply-through-by-inverted-factor-from-right-hand-side
  (implies (and (bind-free (find-inverted-factor rhs) (k))
      (syntaxp (not (is-a-factor k rhs)))
      (syntaxp (sum-of-products-syntaxp lhs))
      (syntaxp (sum-of-products-syntaxp rhs))
      (case-split (not (equal k 0)))
      (case-split (rationalp k)))
    (equal (< lhs rhs)
      (if (<= 0 k)
        (< (* lhs k) (* rhs k))
        (< (* rhs k) (* lhs k))))))

x*/y=1->x=ytheorem

(defthm x*/y=1->x=y
  (implies (and (rationalp x)
      (rationalp y)
      (not (equal x 0))
      (not (equal y 0)))
    (equal (equal (* x (/ y)) 1) (equal x y)))
  :rule-classes nil)

point-right-measurefunction

(defun point-right-measure
  (x)
  (floor (if (and (rationalp x) (< 0 x))
      (/ x)
      0)
    1))

point-left-measurefunction

(defun point-left-measure
  (x)
  (floor (if (and (rationalp x) (> x 0))
      x
      0)
    1))

include-book

(include-book "../../../ordinals/e0-ordinal")

recursion-by-point-righttheorem

(defthm recursion-by-point-right
  (and (e0-ordinalp (point-right-measure x))
    (implies (and (rationalp x) (< 0 x) (< x 1))
      (e0-ord-< (point-right-measure (* 2 x))
        (point-right-measure x)))))

recursion-by-point-lefttheorem

(defthm recursion-by-point-left
  (and (e0-ordinalp (point-left-measure x))
    (implies (and (rationalp x) (>= x 2))
      (e0-ord-< (point-left-measure (* 1/2 x))
        (point-left-measure x)))))

in-theory

(in-theory (disable point-right-measure point-left-measure))

x<x*y<->1<ytheorem

(defthm x<x*y<->1<y
  (implies (and (rationalp x) (< 0 x) (rationalp y))
    (equal (< x (* x y)) (< 1 y)))
  :rule-classes nil)

cancel-equal-*theorem

(defthm cancel-equal-*
  (implies (and (rationalp r)
      (rationalp s)
      (rationalp a)
      (not (equal a 0)))
    (equal (equal (* a r) (* a s)) (equal r s)))
  :rule-classes nil)

cancel-<-*theorem

(defthm cancel-<-*
  (implies (and (rationalp r) (rationalp s) (rationalp a) (< 0 a))
    (equal (< (* a r) (* a s)) (< r s)))
  :rule-classes nil)