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

`complex`

takes 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 `complex`

returns its first
argument. The function `complex-rationalp`

is 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 `x`

and `y`

, `#C(x y)`

is read to the same value as `(complex x y)`

.

The functions `realpart`

and `imagpart`

return the real and imaginary
parts (respectively) of a complex (possibly rational) number. So
for example, `(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 `completion-of-complex`

.

(equal (complex x y) (complex (if (rationalp x) x 0) (if (rationalp y) y 0)))