Prefer-*-to-/
A small theory of lemmas that eliminate / in favor of *.
This is a small theory of rules that eliminate / from equalites and
inequalities in favor of *, e.g., x < y/z is rewritten to x*y < z
for positive z. This theory is compatible with the ALGEBRA theories, i.e.,
it should not cause looping.
These rules are not included in rationalp-algebra because it is not
clear that we should prefer x*y < z to x < y/z, or x*y = z to
x = y/z. In the case of the lemma normalize-equal-/-to-*, there
is no reason to suspect that `y' is a better term than `x'; in fact, the
whole point of the proofs using these libraries may have to do with a
representation involving /. So, unless someone provides a convincing reason
to the contrary, these rules will remain separate from the rationalp-algebra theory.
Note, however, that in certain cases this theory is just the thing that
needs to be ENABLEd to make the proofs work. Keep it in mind.
Subtopics
- Normalize-<-/-to-*-3
- Rewrite: Replace x < y/z and x > y/z with x*z < y or
x*z > y, depending on the sign of z.
- Normalize-<-/-to-*
- Rewrite: Replace x < 1/y with x*y < 1 or x*y > 1,
based on the sign of y.
- Normalize-equal-/-to-*
- Rewrite: Replace x = y/z with x*z = y.
