Verified Computer Algebra in ACL2 - Artificial Intelligence and Symbolic Computation - page 176

(and (equal p q) (k-polynomialp p))
(and (k-polynomialp p)
(<-> p (elt2 (first proof)) (first proof) F)
(<->* (elt2 (first proof)) q (rest proof) F))))

→ F

→ F ), by
a function called ->* (in this case, we also check that all proof steps are direct).
The following theorems establish that the congruence

Inthesameway,wedefinetherelation (the transitive closure of

≡ F is equal to the

equivalence closure ∗

↔ F . This result is crucial to connect the results about re-
duction relations to polynomial ideals.

(defthm |p =<F> q => p <->F* q|
(let ((proof (|p =<F> q => p <->F* q|-proof p q F)))
(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F)
(=<> p q F))
(<->* p q proof F)))

(defthm |p <->F* q => p =<F> q|
(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F)
(<->* p q proof F))
(=<> p q F)))

These two theorems establish that it is possible to obtain a sequence of proof
steps justifying that p

∗
↔ F q from a list of coecients justifying that p−q ∈F

,
and vice versa. The expression (|p =<F> q => p <->F* q|-proof p q F) ex-
plicitly computes such proof, in a recursive way. This is typical in our develop-
ment: in many subsequent Acl2 theorems, the proof argument in <->* or ->*
will be locally-bound (through a let or let* form) to a function computing
the necessary proof steps. As these functions are rather technical and it would
take long to explain them, we will omit their definitions. But it is important to
remark this constructive aspect of our formalization.
Next, we proceed to prove the Noetherianity of the reduction relation. In the
sequel, < represents the polynomial ordering whose well-foundedness was proved
in [9] 5 . This ordering can be used to state the Noetherianity of the polynomial
reduction. For this purpose, it suces to prove that the application of a valid
operator to a polynomial produces a smaller polynomial with respect to this
well-founded relation:

(defthm |validp(p, o, F) => reduction(p, o) < p|
(implies (and (k-polynomialp p) (k-polynomialsp F))
(implies (validp p o F) (< (reduction p o) p))))

As a consequence of Noetherianity we can define the notion of normal form.

Definition 5. A polynomial p is in normal form or is irreducible w.r.t. → F if

there is no q such that p → F q .Otherwise, p is said to be reducible. A polynomial
q is a normal form of p w.r.t. if p → F q and q is irreducible w.r.t.

→ F → F .

5 As it is customary in Acl2, this is proved by means of an ordinal embedding into 0 .