Some proofs of validity using Z3 SMT 2.0 online

0
votes

Lemma: forall x : R, x <> 0 -> (x / x) = 1.

Proof:

(declare-const x Real)
(push)
(assert (or (> x 0) (< x 0)))
(assert (not (= (/ x x) 1)))
(check-sat)

and the output is : 

unsat

Qed.

Lemma: forall x y : R, x <> 0, y <> 0 -> (x / x + y / y) = 2.

Proof:

(declare-const x Real)
(declare-const y Real)
(push)
(assert (or (> x 0) (< x 0)))
(assert (or (> y 0) (< y 0)))
(assert (not (= (+ (/ x x) (/ y y)) 2)))
(check-sat)

and the output is:

unsat

Qed.

Lemma: forall x y : R, x <> 0, y <> 0 -> (x / x + x / y) = ((x + y) / y).

Proof:

(declare-const x Real)
(declare-const y Real)
(push)
(assert (or (> x 0) (< x 0)))
(assert (or (> y 0) (< y 0)))
(assert (not (= (+ (/ x x) (/ x y)) (/ (+ x y) y))))
(check-sat)

and the output is:

unsat

Qed.

These lemmas were proved using Coq + Maple at

http://coq.inria.fr/V8.2pl1/contribs/MapleMode.Examples.html

and using Z3Py online at

Some proofs of validity using Z3Py online and a strategy proposed by Nikolaj Bjorner

Please let me know if my proofs with Z3 SMT 2.0 are correct and if you know a more direct form to prove them using Z3 SMT 2.0. Many thanks.

1
z3

1 Answers

2
votes

There is nothing wrong with your encodings. You may also consider the following encoding that is closer to the lemmas you are trying to prove (also available online here):

(assert (not (forall ((x Real)) (=> (not (= x 0)) (= (/ x x) 1)))))
(check-sat)

(reset)
(assert (not (forall ((x Real) (y Real)) (=> (and (not (= x 0))
                                                  (not (= y 0)))
                                             (= (+ (/ x x) (/ y y)) 2)))))
(check-sat)

(reset)
(assert (not (forall ((x Real) (y Real)) (=> (and (not (= x 0))
                                                  (not (= y 0)))
                                             (= (+ (/ x x) (/ x y)) (/ (+ x y) y))))))
(check-sat)