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

We have formalized polynomial reductions in the framework of abstract re-
ductions developed in [11]. This approach will allow us to export, by functional
instantiation, well-known properties of abstract reductions (for example, New-
man's lemma) to the case of polynomial reductions, avoiding the need to prove
them from scratch.
In [11], instead of defining reductions as binary relations, they are defined as
the action of operators on elements, obtaining reduced elements. More precisely,
the representation of a reduction relation requires defining three functions:

1. A unary predicate specifying the domain where the reduction is defined. In
our case, polynomials, as defined by the function k-polynomialp .
2. A binary function, reduction , computing the application of an operator to
a polynomial. In our case, operators are represented by structures m, c, f

consisting of the monomials m and c , and the polynomial f appearing in the

definition of the polynomial reduction relation (Def. 4).
3. A binary predicate checking whether the application of a given operator to
a given object is valid . The application of an operator

m, c, f to p is valid

if p is a polynomial containing the monomial m , f = 0 is a polynomial in

F −m/ lm ( f ). Notice that the last requirement implies that lm ( f )

must divide m . This validity predicate is implemented by a function validp .

and c =

These functions are just what we need to define in Acl2 all the concepts
related to polynomial reductions. Let us begin defining ↔ F (the symmetric clo-

sure of → F ). We need the notion of proof step to represent the connection of

two polynomials by the reduction relation, in either direction (direct or inverse).
Each proof step is a structure consisting of four fields: a boolean field mark-
ing the step direction, the operator applied, and the elements connected ( elt1 ,
elt2 ). A proof step is valid if one of its elements is obtained by a valid applica-
tion of its operator to the other element in the specified direction. The function
valid-proof-stepp (omitted here), checks the validity of a proof step.
The following function formalizes in Acl2 the relation ↔ F . Note that due

to the absence of existential quantification, the step argument is needed to
explicitly introduce the proof step justifying that p ↔ F q .

(defun <-> (p q step F)
(and (valid-proof-stepp step F)
(equal p (elt1 step)) (equal q (elt2 step))))
Next, we define ∗ → F ). This can be described

by means of a sequence of concatenated proof steps, which we call a proof 4 .Note
that again due to the absence of existential quantification, the proof argument
explicitly introduces the proof steps justifying that p

↔ F (the equivalence closure of

∗
↔ F q .

(defun <->* (p q proof F)
(if (endp proof)
4 Notice that the meaning of the word “proof” here is different than in the expression
“Acl2 proof”. This proof is just a sequence of reduction steps. In fact, we are
formalizing an algebraic proof system inside Acl2.