# 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).
Local Notation "a ²" := (a * a) (at level 5, no associativity, format "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 ²).
Sqrt and addition
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

Local Notation "a ²" := (a * a) (at level 5, no associativity, format "a ²").
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.
Local Notation "√° a" := (sqrt_up a) (at level 6, no associativity).
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
Instance sqrt_up_wd : Proper (eq ==> eq) sqrt_up.
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.
Links between sqrt and sqrt_up
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.
Lemma sqrt_up_mul_above : forall a b, 0<= a -> 0<= b -> √°( a * b ) <= √° a * √° b.
Lemma sqrt_up_mul_below : forall a b, 0< a -> 0< b -> ( P √° a )*( P √° b ) < √°( a * b ).
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

Lemma sqrt_up_succ_le : forall a, 0<= a -> √°( S a ) <= S (√° a).
Lemma sqrt_up_succ_or : forall a, 0<= a -> √°( S a ) == S (√° a) \/ √°( S a ) == √° a.
Lemma sqrt_up_eq_succ_iff_square : forall a, 0<= a ->
(√°( S a ) == S (√° a) <-> exists b , 0<= b /\ a == b ²).
sqrt_up and addition
Lemma sqrt_up_add_le : forall a b, √°( a + b ) <= √° a + √° b.
Convexity-like inequality for sqrt_up: sqrt_up of middle is above middle of square roots. We cannot say more, for instance take a=b=2, then 2+2 <= S 3
Lemma add_sqrt_up_le : forall a b, 0<= a -> 0<= b -> √° a + √° b <= S √°(2*( a + b ) ).
End NZSqrtUpProp.