Library Stdlib.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

#[global]
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

#[global]
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.