Information Technology Reference

In-Depth Information

(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
.

Search WWH ::

Custom Search