The Coq Standard Library

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.

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 ²").

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

Lemma sqrt_nonneg : forall a, 0<=√a.

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

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

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.

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

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

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

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

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

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

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.

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).

Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²").

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 )².

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

Instance sqrt_up_wd : Proper (eq ==>eq) sqrt_up.

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

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

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

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 ²).

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

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

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

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 ²).

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

Library Coq.Numbers.NatInt.NZSqrt

sqrt_up : a square root that rounds up instead of down