# Linear-arithmetic-with-complex-coefficients

Some books for reasoning about arithmetic expressions with complex coefficients

# Linear Reasoning and Complex Coefficients

Per the following comment from the ACL2 sources, ACL2's built-in
linear arithmetic decision procedure linear-arithmetic is not
applied to polys with complex coefficients.

; Note that in Multiplication by Positive Preserves Inequality we require the
; positive to be rational. Multiplication by a 'positive' complex rational
; does not preserve the inequality. For example, the following evaluates
; to nil:
; (let ((c #c(1 -10))
; (x #c(1 1))
; (y #c(2 -2)))
; (implies (and ; (rationalp c) ; omit the rationalp hyp
; (< 0 c))
; (iff (< x y) ; t
; (< (* c x) (* c y))))) ; nil
; Thus, the coefficients in our polys must be rational.

If you are in the admittedly unusal situation of needing to perform
linear reasoning over such expressions, you may find the following
books helpful. It is also possible that these books would prove
useful for reasoning about theorems involving complex numbers in
general.

## Linearize Complex Polys

(include-book "coi/util/linearize-complex-polys" :dir :system)

The 'linearize-complex-polys' book introduces the nullary
function (imaginary) and rules, such as those below, that transform
complex expressions into expressions in terms of (imaginary). In
particular, the product rule rationalizes the coefficients of complex
polys so that they can be processed by ACL2's linear decision
procedure.

(defthm complex-to-imaginary
(equal (complex real imag)
(+ (rfix real) (* (rfix imag) (imaginary)))))

(defthm reduce-complex-coefficient
(implies
(and
(syntaxp (quotep c))
(complex-rationalp c))
(equal (* c x)
(+ (* (realpart c) x) (* (imagpart c) (imaginary) x)))))

## Eliminate Complex Polys

(include-book "coi/util/eliminate-complex-polys" :dir :system)

The 'eliminate-complex-polys' book aggressively reduces
linear expressions involving complex coefficients into linear
expressions with rational coefficients.