# Library Coq.Numbers.NatInt.NZSqrt

Square Root Function

Require Import NZAxioms NZMulOrder.

Interface of a sqrt function, then its specification on naturals

Module Type Sqrt (Import A : Typ).
Parameter Inline sqrt : t -> t.
End Sqrt.

Module Type SqrtNotation (A : Typ)(Import B : Sqrt A).
Notation "√ x" := (sqrt x) (at level 6).
End SqrtNotation.

Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.

Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
Axiom sqrt_spec : forall a, 0<=a -> a * a <= a < S (a) * S (a).
Axiom sqrt_neg : forall a, a<0 -> a == 0.
End NZSqrtSpec.

Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A.
Module Type NZSqrt' (A : NZOrdAxiomsSig) := Sqrt' A <+ NZSqrtSpec A.

Derived properties of power

Module Type NZSqrtProp
(Import A : NZOrdAxiomsSig')
(Import B : NZSqrt' A)
(Import C : NZMulOrderProp A).

First, sqrt is non-negative

Lemma sqrt_spec_nonneg : forall b,
b² < (S b -> 0 <= b.

Lemma sqrt_nonneg : forall a, 0<=a.

The spec of sqrt indeed determines it

Lemma sqrt_unique : forall a b, b² <= a < (S b -> a == b.

Hence sqrt is a morphism

Instance sqrt_wd : Proper (eq==>eq) sqrt.

An alternate specification

Lemma sqrt_spec_alt : forall a, 0<=a -> exists r,
a == (a + r /\ 0 <= r <= 2*a.

Lemma sqrt_unique' : forall a b c, 0<=c<=2*b ->
a == b² + c -> a == b.

Sqrt is exact on squares

Lemma sqrt_square : forall a, 0<=a -> √(a²) == a.

Sqrt and predecessors of squares

Lemma sqrt_pred_square : forall a, 0<a -> √(P a²) == P a.

Sqrt is a monotone function (but not a strict one)

Lemma sqrt_le_mono : forall a b, a <= b -> a <= b.

No reverse result for <=, consider for instance √2 <= √1

Lemma sqrt_lt_cancel : forall a b, a < b -> a < b.

When left side is a square, we have an equivalence for <=

Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= a).

When right side is a square, we have an equivalence for <

Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> a < b).

Sqrt and basic constants

Lemma sqrt_0 : 0 == 0.

Lemma sqrt_1 : 1 == 1.

Lemma sqrt_2 : 2 == 1.

Lemma sqrt_pos : forall a, 0 < a <-> 0 < a.

Lemma sqrt_lt_lin : forall a, 1<a -> a<a.

Lemma sqrt_le_lin : forall a, 0<=a -> a<=a.

Sqrt and multiplication.
Due to rounding error, we don't have the usual √(a*b) = √a*√b but only lower and upper bounds.

Lemma sqrt_mul_below : forall a b, a * b <= √(a*b).

Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (a) * S (b).

And we can't find better approximations in general.
• The lower bound is exact for squares
• Concerning the upper bound, for any c>0, take a=b=c²-1, then √(a*b) = c² -1 while S √a = S √b = c
Sqrt and successor :
• the sqrt function climbs by at most 1 at a time
• otherwise it stays at the same value
• the +1 steps occur for squares

Lemma sqrt_succ_le : forall a, 0<=a -> √(S a) <= S (a).

Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (a) \/ √(S a) == a.

Lemma sqrt_eq_succ_iff_square : forall a, 0<=a ->
(√(S a) == S (a) <-> exists b, 0<b /\ S a == b²).

Lemma sqrt_add_le : forall a b, √(a+b) <= a + b.

convexity inequality for sqrt: sqrt of middle is above middle of square roots.

Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> a + b <= √(2*(a+b)).

End NZSqrtProp.

Module Type NZSqrtUpProp
(Import A : NZDecOrdAxiomsSig')
(Import B : NZSqrt' A)
(Import C : NZMulOrderProp A)
(Import D : NZSqrtProp A B C).

# sqrt_up : a square root that rounds up instead of down

For once, we define instead of axiomatizing, thanks to sqrt

Definition sqrt_up a :=
match compare 0 a with
| Lt => S √(P a)
| _ => 0
end.

Lemma sqrt_up_eqn0 : forall a, a<=0 -> √°a == 0.

Lemma sqrt_up_eqn : forall a, 0<a -> √°a == S √(P a).

Lemma sqrt_up_spec : forall a, 0<a -> (P √°a < a <= (√°a.

First, sqrt_up is non-negative

Lemma sqrt_up_nonneg : forall a, 0<=√°a.

sqrt_up is a morphism
The spec of sqrt_up indeed determines it

Lemma sqrt_up_unique : forall a b, 0<b -> (P b < a <= b² -> √°a == b.

sqrt_up is exact on squares

Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a.

sqrt_up and successors of squares

Lemma sqrt_up_succ_square : forall a, 0<=a -> √°(S a²) == S a.

Basic constants

Lemma sqrt_up_0 : √°0 == 0.

Lemma sqrt_up_1 : √°1 == 1.

Lemma sqrt_up_2 : √°2 == 2.

Lemma le_sqrt_sqrt_up : forall a, a <= √°a.

Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (a).

Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (a <= a <= (√°a.

Lemma sqrt_sqrt_up_exact :
forall a, 0<=a -> (a == √°a <-> exists b, 0<=b /\ a == b²).

sqrt_up is a monotone function (but not a strict one)

Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b.

No reverse result for <=, consider for instance √°3 <= √°2

Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b.

When left side is a square, we have an equivalence for <

Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a).

When right side is a square, we have an equivalence for <=

Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b).

Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a.

Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a.

Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a.

sqrt_up and multiplication.
Due to rounding error, we don't have the usual √(a*b) = a*√b but only lower and upper bounds.
And we can't find better approximations in general.
• The upper bound is exact for squares
• Concerning the lower bound, for any c>0, take a=b=c²+1, then √°(a*b) = c²+1 while P √°a = P √°b = c
sqrt_up and successor :
• the sqrt_up function climbs by at most 1 at a time
• otherwise it stays at the same value
• the +1 steps occur after squares