Has-square-root?-satisfies-pfield-squarep
Show how pfield-squarep can be refined into has-square-root?
pfield-squarep is a nonexecutable specification of what it means to
check that a field element is a square of another field element.
primes::has-square-root? is an executable specification that uses Euler's
Criterion to determine if the field element has a square root.
In order to use apt::simplify to refine a use of pfield-squarep
to has-square-root?, we must show that they are equivalent under
appropriate hypotheses that limit the domain. That is the purpose of
this definition.
Implementation notes:
Use residue-meaning-backwards to turn has-square-root? into dm::residue,open it up to expose dm::find-root, use the theorem about dm::find-root to obtainthat the square of dm::find-root is a, and finally use that as witness toconclude pfield-squarep.
There is a case split on whether a is 0 or not,due to the definition of dm::residue. The enablement of mul is so thatpfield-squarep is phrased as (mod (* ... ...) p), and enablement offep because some of the theorems used have natp and < p as hyps.
Definitions and Theorems
Theorem: has-square-root?-satisfies-pfield-squarep
(defthm has-square-root?-satisfies-pfield-squarep
(implies (and (dm::primep p)
(not (equal p 2))
(fep a p)
(primes::has-square-root? a p))
(pfield-squarep a p)))
