Major Section: ACL2-BUILT-INS
Examples: (complex x 3) ; x + 3i, where i is the principal square root of -1 (complex x y) ; x + yi (complex x 0) ; same as x, for rational numbers xThe function
complextakes two rational number arguments and returns an ACL2 number. This number will be of type
(complex rational)[as defined in the Common Lisp language], except that if the second argument is zero, then
complexreturns its first argument. The function
complex-rationalpis a recognizer for complex rational numbers, i.e. for ACL2 numbers that are not rational numbers.
The reader macro
#C (which is the same as
#c) provides a convenient
way for typing in complex numbers. For explicit rational numbers
#C(x y) is read to the same value as
(complex x y).
imagpart return the real and imaginary
parts (respectively) of a complex (possibly rational) number. So
(realpart #C(3 4)) = 3,
(imagpart #C(3 4)) = 4,
(realpart 3/4) = 3/4, and
(imagpart 3/4) = 0.
The following built-in axiom may be useful for reasoning about complex numbers.
(defaxiom complex-definition (implies (and (real/rationalp x) (real/rationalp y)) (equal (complex x y) (+ x (* #c(0 1) y)))) :rule-classes nil)
A completion axiom that shows what
complex returns on arguments
violating its guard (which says that both arguments are rational
numbers) is the following, named
(equal (complex x y) (complex (if (rationalp x) x 0) (if (rationalp y) y 0)))