arith-equiv-defs

(in-package "ACL2")

(defsection arith-equivs
  :parents (arithmetic std/basic)
  :short "Definitions for congruence reasoning about integers/naturals/bits."
  :long "<p>Note: to use this book at full strength, do:</p>

@({
    (include-book "std/basic/arith-equivs" :dir :system)
    (local (in-theory (enable* arith-equiv-forwarding)))
})

<p>You can also load just the definitions and bare-minimum theorems using</p>

@({
    (include-book "std/basic/arith-equiv-defs" :dir :system)
})")

(defsection int-equiv
  :parents (arith-equivs)
  :short "Equivalence under @(see ifix), i.e., integer equivalence."
  (in-theory (enable int-equiv))
  (defcong int-equiv equal (zip a) 1))

(defsection nat-equiv
  :parents (arith-equivs)
  :short "Equivalence under @(see nfix), i.e., natural number equivalence."
  (in-theory (enable nat-equiv))
  (defrefinement int-equiv
    nat-equiv
    :hints (("Goal" :in-theory (enable int-equiv))))
  (defcong nat-equiv equal (zp a) 1))

(defsection bit-equiv
  :parents (arith-equivs)
  :short "Equivalence under @(see bfix), i.e., bit equivalence."
  (in-theory (enable bit-equiv))
  (defrefinement nat-equiv bit-equiv)
  (defcong bit-equiv equal (zbp a) 1))

(defsection bool->bit
  :parents (arith-equivs)
  :short "Coerce a Boolean into a @(see bitp)."
  (defund-inline bool->bit
    (x)
    (declare (xargs :guard t))
    (if x
      1
      0))
  (defthmd bitp-of-bool->bit (bitp (bool->bit x))))

(defsection bit->bool
  :parents (arith-equivs)
  :short "Coerce a bit into a Boolean."
  :long "<p>This is just @('(equal 1 x)').  However, using a function for this
allows us to use congruences and to control case-splitting.  For example, if we
have
@({
  (equal (equal 1 (foo x))
         (equal 1 (bar y)))
})
this will case split into:
@({
  (if (equal 1 (foo x))
      (equal 1 (bar y))
    (not (equal 1 (bar y))))
})
whereas
@({
 (equal (bit->bool (foo x)) (bit->bool (bar y)))
})
will not.</p>

<p>Because a bunch of libraries were written under the assumption that
@('(equal 1 x)') was the way to tell if a bit was true or false, we leave this
enabled by default.</p>"
  (defun-inline bit->bool
    (x)
    (declare (xargs :guard t))
    (equal 1 x))
  (defcong bit-equiv equal (bit->bool a) 1))

(defsection negp
  :parents (arith-equivs)
  :short "Recognizer for negative integers."
  (defund negp
    (x)
    (declare (xargs :guard t))
    (and (integerp x) (< x 0)))
  (defthm negp-compound-recognizer
    (equal (negp x) (and (integerp x) (< x 0)))
    :hints (("Goal" :in-theory (enable negp)))
    :rule-classes :compound-recognizer))