Merge pull request #887 from proux01/sqrte

Add sqrte

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -63,6 +63,12 @@
   + lemmas `inum_eq`, `inum_le`, `inum_lt`
 - in `measure.v`:
   + lemmas `ae_imply`, `ae_imply2`
+- in `mathcomp_extra.v`
+  + lemma `ler_sqrt`
+- in `constructive_ereal.v`
+  + definition `sqrte`
+  + lemmas `sqrte0`, `sqrte_ge0`, `lee_sqrt`, `sqrteM`, `sqr_sqrte`,
+    `sqrte_sqr`, `sqrte_fin_num`
 
 ### Changed
 

classical/mathcomp_extra.v

@@ -1125,3 +1125,12 @@ End DFunWith.
 Arguments dfwith {I T} f i x.
 
 Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).
+
+Lemma ler_sqrt {R : rcfType} (a b : R) :
+  (0 <= b -> (Num.sqrt a <= Num.sqrt b) = (a <= b))%R.
+Proof.
+have [b_gt0 _|//|<- _] := ltgtP; last first.
+  by rewrite sqrtr0 -sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF.
+have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt.
+by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
+Qed.

theories/constructive_ereal.v

@@ -30,6 +30,7 @@ Require Import signed.
 (*                    r%:E == injects real numbers into \bar R                *)
 (*           +%E, -%E, *%E == addition/opposite/multiplication for extended   *)
 (*                            reals                                           *)
+(*                   sqrte == square root for extended reals                  *)
 (*                `| x |%E == the absolute value of x                         *)
 (*                  x ^+ n == iterated multiplication                         *)
 (*                  x *+ n == iterated addition                               *)
@@ -3063,6 +3064,58 @@ End DualRealFieldType_lemmas.
 
 End DualAddTheoryRealField.
 
+Section sqrte.
+Variable R : rcfType.
+Implicit Types x y : \bar R.
+
+Definition sqrte x :=
+  if x is +oo then +oo else if x is r%:E then (Num.sqrt r)%:E else 0.
+
+Lemma sqrte0 : sqrte 0 = 0 :> \bar R.
+Proof. by rewrite /= sqrtr0. Qed.
+
+Lemma sqrte_ge0 x : 0 <= sqrte x.
+Proof. by case: x => [x|//|]; rewrite /= ?leey// lee_fin sqrtr_ge0. Qed.
+
+Lemma lee_sqrt x y : 0 <= y -> (sqrte x <= sqrte y) = (x <= y).
+Proof.
+case: x y => [x||] [y||] yge0 //=.
+- exact: mathcomp_extra.ler_sqrt.
+- by rewrite !leey.
+- by rewrite leNye lee_fin sqrtr_ge0.
+Qed.
+
+Lemma sqrteM x y : 0 <= x -> sqrte (x * y) = sqrte x * sqrte y.
+Proof.
+case: x y => [x||] [y||] //= age0.
+- by rewrite sqrtrM ?EFinM.
+- move: age0; rewrite le_eqVlt eqe => /predU1P[<-|x0].
+    by rewrite mul0e sqrte0 sqrtr0 mul0e.
+  by rewrite mulry gtr0_sg ?mul1e// mulry gtr0_sg ?mul1e// sqrtr_gt0.
+- move: age0; rewrite mule0 mulrNy lee_fin -sgr_ge0.
+  by case: sgrP; rewrite ?mul0e ?sqrte0// ?mul1e// ler0N1.
+- rewrite !mulyr; case: (sgrP y) => [->||].
+  + by rewrite sqrtr0 sgr0 mul0e sqrte0.
+  + by rewrite mul1e/= -sqrtr_gt0 -sgr_gt0 -lte_fin => /gt0_muley->.
+  + by move=> y0; rewrite EFinN mulN1e/= ltr0_sqrtr// sgr0 mul0e.
+- by rewrite mulyy.
+- by rewrite mulyNy mule0.
+Qed.
+
+Lemma sqr_sqrte x : 0 <= x -> sqrte x ^+ 2 = x.
+Proof.
+case: x => [x||] xge0; rewrite expe2 ?mulyy//.
+by rewrite -sqrteM// -EFinM/= sqrtr_sqr ger0_norm.
+Qed.
+
+Lemma sqrte_sqr x : sqrte (x ^+ 2) = `|x|%E.
+Proof. by case: x => [x||//]; rewrite /expe/= ?sqrtr_sqr// mulyy. Qed.
+
+Lemma sqrte_fin_num x : 0 <= x -> (sqrte x \is a fin_num) = (x \is a fin_num).
+Proof. by case: x => [x|//|//]; rewrite !qualifE/=. Qed.
+
+End sqrte.
+
 Module DualAddTheory.
 Export DualAddTheoryNumDomain.
 Export DualAddTheoryRealDomain.