abs package:sbv

Compute the floating point absolute value.

Absolute value.

A number divides another exactly when it also divides its absolute value. While this property seems obvious, I was unable to get z3 to prove it. Even CVC5 needs a bit of help to guide it through the case split on b.

Proof

>>> runTP dvdAbs
Lemma: dvdAbs_l2r
Step: 1 (2 way case split)
Step: 1.1                           Q.E.D.
Step: 1.2                           Q.E.D.
Step: 1.Completeness                Q.E.D.
Result:                               Q.E.D.
Lemma: dvdAbs_r2l
Step: 1 (2 way case split)
Step: 1.1                           Q.E.D.
Step: 1.2                           Q.E.D.
Step: 1.Completeness                Q.E.D.
Result:                               Q.E.D.
Lemma: dvdAbs                           Q.E.D.
[Proven] dvdAbs :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool