#!/usr/bin/env python
"""
Task2, LUP, 2025.

You need the Python wrapper for Z3. You can install it, for example, by

pip install z3-solver

A tutorial Z3 API in Python is available at (but there is no need to go through it):

https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

For details, see https://z3prover.github.io/api/html/index.html

Note that you may get different counterexamples!
"""

from z3 import * # We want to experiment...

def mean(x, y):
    """
    The function returns the mean of ``x`` and ``y``.
    """
    return (x + y) / 2

# Define two reals.
x, y = Reals("x y")


# We want to prove that mean(x, y) < x or mean(x, y) < y
#
# For prove, see
# https://z3prover.github.io/api/html/namespacez3py.html#afe5063009623290e15bf3f15183bbd50

prove(Or(mean(x, y) < x, mean(x, y) < y))
# counterexample
# [y = 0, x = 0]


# Ok, so assume that x < y

prove(Implies(x < y, Or(mean(x, y) < x, mean(x, y) < y)))
# proved


# Is it still the case if x and y are floats?

x_fp, y_fp, mean_fp = FPs("x_fp y_fp mean_fp", Float32())
prove(Implies(And(x_fp < y_fp, mean(x_fp, y_fp) == mean_fp), Or(mean_fp < x_fp, mean_fp < y_fp)))
# counterexample
# [y_fp = -1.5156190395355224609375*(2**-115),
#  mean_fp = -1.5156190395355224609375*(2**-115),
#  x_fp = -1.51561915874481201171875*(2**-115)]


# Say we want to show that
#
# if 1 < x and 1 < y then mean(x, y) != sqrt(x)
#
# Do not use Sqrt(x) from Z3, or add Sqrt(x) * Sqrt(x) == x among your conditions...

sqrt_x = Real("sqrt_x")
prove(Implies(And(1 < x, 1 < y, 0 < sqrt_x, sqrt_x * sqrt_x == x), mean(x, y) != sqrt_x))
# proved

######################
# Task2 starts here. #
######################

def heron(x, init=1, iters=6):
    """
    It computes the approximation of sqrt(x) using Heron's method
    where ``init`` is the initial estimate. The number of iterations
    is in ``iters``.
    
    https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Heron's_method
    """
    res = init
    for _ in range(iters):
        res = (x / res + res) / 2
    return res


# 1) Let x be a real number such that 0 < x < 100.
# - Find a counterexample for |heron(x, init=1, iters=6) - sqrt(x)| < 0.01.
# - Prove |heron(x, init=1, iters=7) - sqrt(x)| < 0.01.
#
# (there exists a function Abs)
#
# (5 points.)


# 2) Let x and b be real numbers such that 0 < x and 0 < b.
# - Find a counterexample for
# |heron(x, init=b, iters=1) - sqrt(x)| > |heron(x, init=b, iters=2) - sqrt(x)|.
# - Prove that the previous holds if b != sqrt(x).
# - If b != sqrt(x), find (experimentally) the maximal real number c for which you can prove
# |heron(x, init=b, iters=1) - sqrt(x)| > c*|heron(x, init=b, iters=3) - sqrt(x)|.
#
# (7 points.)


# 3) Let x, b1, and b2 be real numbers such that 0 < x and 0 < b1 < b2. Moreover,
#
# | sqrt(x) - b1| == | sqrt(x) - b2|.
#
# Is heron(x, iters=1, init=b1) or heron(x, iters=1, init=b2) a better
# approximation of sqrt(x)? Prove your claim!
#
# (3 points.)