Support simple functions such as `sqrt` and `abs`

[JC-Chen1]

Support for Abs, available in https://github.com/yangky11/lean-smt/commit/6edb4d8b48380f52750d58751cf8cdbec3791ef8

Specifically, I add correct translating process for Abs.

Example,

theorem amc12_2000_p5 (x p : ℝ) (h₀ : x < 2) (h₁ : abs (x - 2) = p) : x - p = 2 - 2 * p := by
  smt!

query:
(declare-const p Real)
(declare-const x Real)
(assert (= (abs (+ x (- 2))) p))
(assert (< x 2))
(assert (not (= (+ x (- p)) (+ 2 (- (* 2 p))))))
(check-sat)

result: unsat

[JC-Chen1]

Support for Real.sqrt, available in https://github.com/yangky11/lean-smt/commit/dbd4668c1eb45a800589ba92e02854c91d72d04c

My goal is to self-define Real.sqrt and then provide sufficient properties corresponding to it. More specifically, I want to encode Real.sqrt in the following format.

(declare-fun Real.sqrt (Real) Real)
(assert (forall ((__sqrt_x Real)) (= (Real.sqrt (^ __sqrt_x 2)) (abs __sqrt_x))))
(assert (forall ((__sqrt_x Real)) (=> (>= __sqrt_x 0) (and (>= (Real.sqrt __sqrt_x) 0) (= (^ (Real.sqrt __sqrt_x) 2) __sqrt_x)))))

For implementation details, I modified the Query.lean file, which play a key role in building dependency graph. I defined some special dependency operation when detecting Real.sqrt.

Example,

theorem algebra_amgm_sqrtxymulxmyeqxpy_xpygeq4 (x y : ℝ) (h₀ : 0 < x ∧ 0 < y) (h₁ : y ≤ x)
    (h₂ : Real.sqrt (x * y) * (x - y) = x + y) : x + y ≥ 4 := by smt!

(declare-fun Real.sqrt (Real) Real)
(assert (forall ((__sqrt_x Real)) (= (Real.sqrt (^ __sqrt_x 2)) (abs __sqrt_x))))
(assert (forall ((__sqrt_x Real)) (=> (>= __sqrt_x 0) (and (>= (Real.sqrt __sqrt_x) 0) (= (^ (Real.sqrt __sqrt_x) 2) __sqrt_x)))))
(declare-const y Real)
(declare-const x Real)
(assert (= (* (Real.sqrt (* x y)) (+ x (- y))) (+ x y)))
(assert (<= y x))
(assert (and (< 0 x) (< 0 y)))
(assert (not (>= (+ x y) 4)))
(check-sat)

result: unsat

More, We can also support sqrt in the following way,

Real.sqrt 2 -> define z : Real, z * z == 2

I found that this method is more powerful, but the encoding process could be more difficult to implement. So I make some compromises.

[JC-Chen1]

Next step, I plan to encode other simple oprations like Int.floor and Int.ceil.

Meanwhile, I will try to find a way to support sqrt in the more powerful strategy.

[yangky11]

abs is a built-in function supported by SMT solvers?

[JC-Chen1]

yes

[yangky11]

this method is more powerful, but the encoding process could be more difficult to implement

What's the difficulty here? Is it because we have to introduce new variables into the local context?

[JC-Chen1]

Yes, we have to introduce new variables in this way.

[yangky11]

I see. You can try to do that first, and we can discuss more tomorrow.

[yangky11]

BTW, why do you think this encoding strategy is more powerful than the current way of handling sqrt? Do you have an example that cannot be handled by the current way but can be handled by the new encoding strategy?

[JC-Chen1]

Yes, I found a theorem that can be resolved by z * z == 2 but not in the self-define way.

theorem imo_2006_p6 (a b c : ℝ) :
    a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2) ≤
      9 * Real.sqrt 2 / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2 := by smt!

When using self-define strategy, smt solvers output result: unknown

But when using z * z == 2 strategy, smt solvers will be able to resolve it.

I didn't have the accurate number of this kind of phenomenon. But I think this just occupy a small portion based on my current obsearvation.

[yangky11]

OK, then it makes sense to try the new strategy.

[JC-Chen1]

Yes, z * z == 2 would be a better way.