diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-18 14:40:10 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-18 14:40:10 +0000 |
commit | 57ef3e2c400d0be06b7a9a2c5f07e5f34240fe64 (patch) | |
tree | ff61bb65ecfac97b7d2851b47ac636d692324a6f /theories/Numbers/NatInt | |
parent | 503d92f75b520e88864649306f5a70058ff73990 (diff) |
NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrt
Some more results about sqrt. Similar results for sqrt_up.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13649 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r-- | theories/Numbers/NatInt/NZLog.v | 2 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 466 |
2 files changed, 446 insertions, 22 deletions
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index db7c1fa53..6e1c2b3a1 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -335,7 +335,7 @@ Lemma log2_succ_or : forall a, log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a. Proof. intros. - destruct (le_gt_cases (log2 (S a)) (log2 a)). + destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. left. apply le_succ_l in H. generalize (log2_succ_le a); order. Qed. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 4cdf322fd..414770d18 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -17,7 +17,7 @@ Module Type Sqrt (Import A : Typ). End Sqrt. Module Type SqrtNotation (A : Typ)(Import B : Sqrt A). - Notation "√ x" := (sqrt x) (at level 25). + Notation "√ x" := (sqrt x) (at level 6). End SqrtNotation. Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A. @@ -37,15 +37,17 @@ Module Type NZSqrtProp (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 a b, - b*b <= a < S b * S b -> 0 <= b. +Lemma sqrt_spec_nonneg : forall b, + b² < (S b)² -> 0 <= b. Proof. - intros a b (LE,LT). + intros b LT. destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso. - assert (S b * S b < b * b). - rewrite mul_succ_l, <- (add_0_r (b*b)). + assert ((S b)² < b²). + rewrite mul_succ_l, <- (add_0_r b²). apply add_lt_le_mono. apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. now apply le_succ_l. @@ -56,16 +58,16 @@ Lemma sqrt_nonneg : forall a, 0<=√a. Proof. intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. now rewrite (sqrt_neg _ Ha). - now apply (sqrt_spec_nonneg a), sqrt_spec. + apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. (** The spec of sqrt indeed determines it *) -Lemma sqrt_unique : forall a b, b*b <= a < S b * S b -> √a == b. +Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b. Proof. intros a b (LEb,LTb). - assert (Ha : 0<=a) by (transitivity (b*b); trivial using square_nonneg). - assert (Hb : 0<=b) by (apply (sqrt_spec_nonneg a); now split). + assert (Ha : 0<=a) by (transitivity b²; trivial using square_nonneg). + assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order). assert (Ha': 0<=√a) by now apply sqrt_nonneg. destruct (sqrt_spec a Ha) as (LEa,LTa). assert (b <= √a). @@ -91,7 +93,7 @@ Qed. (** An alternate specification *) Lemma sqrt_spec_alt : forall a, 0<=a -> exists r, - a == √a * √a + r /\ 0 <= r <= 2*√a. + a == (√a)² + r /\ 0 <= r <= 2*√a. Proof. intros a Ha. destruct (sqrt_spec _ Ha) as (LE,LT). @@ -99,13 +101,13 @@ Proof. exists r. split. now rewrite add_comm. split. trivial. - apply (add_le_mono_r _ _ (√a * √a)). + apply (add_le_mono_r _ _ (√a)²). rewrite <- Hr, add_comm. generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc. Qed. Lemma sqrt_unique' : forall a b c, 0<=c<=2*b -> - a == b*b + c -> sqrt a == b. + a == b² + c -> √a == b. Proof. intros a b c (Hc,H) EQ. apply sqrt_unique. @@ -119,13 +121,31 @@ Qed. (** Sqrt is exact on squares *) -Lemma sqrt_square : forall a, 0<=a -> √(a*a) == a. +Lemma sqrt_square : forall a, 0<=a -> √(a²) == a. Proof. intros a Ha. apply sqrt_unique' with 0. split. order. apply mul_nonneg_nonneg; order'. now nzsimpl. Qed. +(** Sqrt and predecessors of squares *) + +Lemma sqrt_pred_square : forall a, 0<a -> √(P a²) == P a. +Proof. + intros a Ha. + apply sqrt_unique. + assert (EQ := lt_succ_pred 0 a Ha). + rewrite EQ. split. + apply lt_succ_r. + rewrite (lt_succ_pred 0). + assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ). + assert (P a < a) by (now rewrite <- le_succ_l, EQ). + apply mul_lt_mono_nonneg; trivial. + now apply mul_pos_pos. + apply le_succ_l. + rewrite (lt_succ_pred 0). reflexivity. now apply mul_pos_pos. +Qed. + (** Sqrt is a monotone function (but not a strict one) *) Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b. @@ -152,7 +172,7 @@ Proof. destruct (sqrt_spec a Ha) as (_,LT). destruct (sqrt_spec b Hb) as (LE,_). apply le_succ_l in H. - assert (S (√a) * S (√a) <= √b * √b). + assert ((S (√a))² <= (√b)²). apply mul_le_mono_nonneg; trivial. now apply lt_le_incl, lt_succ_r, sqrt_nonneg. now apply lt_le_incl, lt_succ_r, sqrt_nonneg. @@ -161,19 +181,19 @@ Qed. (** When left side is a square, we have an equivalence for <= *) -Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b*b<=a <-> b <= √a). +Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a). Proof. intros a b Ha Hb. split; intros H. rewrite <- (sqrt_square b); trivial. now apply sqrt_le_mono. destruct (sqrt_spec a Ha) as (LE,LT). - transitivity (√a * √a); trivial. + transitivity (√a)²; trivial. now apply mul_le_mono_nonneg. Qed. (** When right side is a square, we have an equivalence for < *) -Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b*b <-> √a < b). +Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b). Proof. intros a b Ha Hb. split; intros H. destruct (sqrt_spec a Ha) as (LE,_). @@ -199,6 +219,13 @@ Proof. apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'. Qed. +Lemma sqrt_pos : forall a, 0 < √a <-> 0 < a. +Proof. + intros a. split; intros Ha. apply sqrt_lt_cancel. now rewrite sqrt_0. + rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono. + now rewrite one_succ, le_succ_l. +Qed. + Lemma sqrt_lt_lin : forall a, 1<a -> √a<a. Proof. intros a Ha. rewrite <- sqrt_lt_square; try order'. @@ -252,10 +279,56 @@ Qed. (** 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*c-1, - then √(a*b) = c*c -1 while S √a = S √b = c + - 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). +Proof. + intros a Ha. + apply lt_succ_r. + apply sqrt_lt_square. + now apply le_le_succ_r. + apply le_le_succ_r, le_le_succ_r, sqrt_nonneg. + rewrite <- (add_1_l (S (√a))). + apply lt_le_trans with (1²+(S (√a))²). + rewrite mul_1_l, add_1_l, <- succ_lt_mono. + now apply sqrt_spec. + apply add_square_le. order'. apply le_le_succ_r, sqrt_nonneg. +Qed. + +Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a. +Proof. + intros a Ha. + destruct (le_gt_cases (√(S a)) (√a)) as [H|H]. + right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order. + left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order. +Qed. + +Lemma sqrt_eq_succ_iff_square : forall a, 0<=a -> + (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²). +Proof. + intros a Ha. split. + intros EQ. exists (S (√a)). + split. apply lt_succ_r, sqrt_nonneg. + generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l. + assert (Ha' : 0 <= S a) by now apply le_le_succ_r. + generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order. + intros (b & Hb & H). + rewrite H. rewrite sqrt_square; try order. + symmetry. + rewrite <- (lt_succ_pred 0 b Hb). apply succ_wd. + rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H. + now rewrite H, sqrt_pred_square. + now apply mul_pos_pos. +Qed. + (** Sqrt and addition *) Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b. @@ -301,10 +374,361 @@ Proof. apply sqrt_le_square. apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg. now apply add_nonneg_nonneg. - transitivity (2*(√a*√a + √b*√b)). + transitivity (2*((√a)² + (√b)²)). now apply square_add_le. apply mul_le_mono_nonneg_l. order'. apply add_le_mono; now apply sqrt_spec. Qed. 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. +Proof. + intros a Ha. unfold sqrt_up. case compare_spec; try order. +Qed. + +Lemma sqrt_up_eqn : forall a, 0<a -> √°a == S √(P a). +Proof. + intros a Ha. unfold sqrt_up. case compare_spec; try order. +Qed. + +Lemma sqrt_up_spec : forall a, 0<a -> (P √°a)² < a <= (√°a)². +Proof. + intros a Ha. + rewrite sqrt_up_eqn, pred_succ; trivial. + assert (Ha' := lt_succ_pred 0 a Ha). + rewrite <- Ha' at 3 4. + rewrite le_succ_l, lt_succ_r. + apply sqrt_spec. + now rewrite <- lt_succ_r, Ha'. +Qed. + +(** First, [sqrt_up] is non-negative *) + +Lemma sqrt_up_nonneg : forall a, 0<=√°a. +Proof. + intros. destruct (le_gt_cases a 0) as [Ha|Ha]. + now rewrite sqrt_up_eqn0. + rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. +Qed. + +(** [sqrt_up] is a morphism *) + +Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up. +Proof. + assert (Proper (eq==>eq==>Logic.eq) compare). + intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. + intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx. +Qed. + +(** The spec of [sqrt_up] indeed determines it *) + +Lemma sqrt_up_unique : forall a b, 0<b -> (P b)² < a <= b² -> √°a == b. +Proof. + intros a b Hb (LEb,LTb). + assert (Ha : 0<a) + by (apply le_lt_trans with (P b)²; trivial using square_nonneg). + rewrite sqrt_up_eqn; trivial. + assert (Hb' := lt_succ_pred 0 b Hb). + rewrite <- Hb'. apply succ_wd. apply sqrt_unique. + rewrite <- le_succ_l, <- lt_succ_r, Hb'. + rewrite (lt_succ_pred 0 a Ha). now split. +Qed. + +(** [sqrt_up] is exact on squares *) + +Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a. +Proof. + intros a Ha. + apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + rewrite sqrt_up_eqn by (now apply mul_pos_pos). + rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. + rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. +Qed. + +(** [sqrt_up] and successors of squares *) + +Lemma sqrt_up_succ_square : forall a, 0<=a -> √°(S a²) == S a. +Proof. + intros a Ha. + rewrite sqrt_up_eqn by (now apply lt_succ_r, mul_nonneg_nonneg). + now rewrite pred_succ, sqrt_square. +Qed. + +(** Basic constants *) + +Lemma sqrt_up_0 : √°0 == 0. +Proof. + rewrite <- (mul_0_l 0) at 1. now apply sqrt_up_square. +Qed. + +Lemma sqrt_up_1 : √°1 == 1. +Proof. + rewrite <- (mul_1_l 1) at 1. apply sqrt_up_square. order'. +Qed. + +Lemma sqrt_up_2 : √°2 == 2. +Proof. + rewrite sqrt_up_eqn by order'. + now rewrite two_succ, pred_succ, sqrt_1. +Qed. + +(** Links between sqrt and [sqrt_up] *) + +Lemma le_sqrt_sqrt_up : forall a, √a <= √°a. +Proof. + intros a. unfold sqrt_up. case compare_spec; intros H. + rewrite <- H, sqrt_0. order. + rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le. + apply lt_succ_r. now rewrite (lt_succ_pred 0 a H). + now rewrite sqrt_neg. +Qed. + +Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a). +Proof. + intros a. unfold sqrt_up. + case compare_spec; intros H; try apply le_le_succ_r, sqrt_nonneg. + rewrite <- succ_le_mono. apply sqrt_le_mono. + rewrite <- (lt_succ_pred 0 a H) at 2. apply le_succ_diag_r. +Qed. + +Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)². +Proof. + intros a H. split. + now apply sqrt_spec. + rewrite le_lteq in H. destruct H as [H|H]. + now apply sqrt_up_spec. + now rewrite <-H, sqrt_up_0, mul_0_l. +Qed. + +Lemma sqrt_sqrt_up_exact : + forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). +Proof. + intros a Ha. + split. intros. exists √a. + split. apply sqrt_nonneg. + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. + intros (b & Hb & Hb'). rewrite Hb'. + now rewrite sqrt_square, sqrt_up_square. +Qed. + +(** [sqrt_up] is a monotone function (but not a strict one) *) + +Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b. +Proof. + intros a b H. + destruct (le_gt_cases a 0) as [Ha|Ha]. + rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg. + rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono. + apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order. +Qed. + +(** No reverse result for <=, consider for instance √°3 <= √°2 *) + +Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b. +Proof. + intros a b H. + destruct (le_gt_cases b 0) as [Hb|Hb]. + rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order. + destruct (le_gt_cases a 0) as [Ha|Ha]; [order|]. + rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono. + apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn. +Qed. + +(** 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). +Proof. + intros a b Ha Hb. split; intros H. + destruct (sqrt_up_spec a) as (LE,LT). + apply le_lt_trans with b²; trivial using square_nonneg. + apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg. + apply sqrt_up_lt_cancel. now rewrite sqrt_up_square. +Qed. + +(** 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). +Proof. + intros a b Ha Hb. split; intros H. + rewrite <- (sqrt_up_square b Hb). + now apply sqrt_up_le_mono. + apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg]. + transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec. +Qed. + +Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a. +Proof. + intros a. split; intros Ha. apply sqrt_up_lt_cancel. now rewrite sqrt_up_0. + rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono. + now rewrite one_succ, le_succ_l. +Qed. + +Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a. +Proof. + intros a Ha. + rewrite sqrt_up_eqn by order'. + assert (Ha' := lt_succ_pred 2 a Ha). + rewrite <- Ha' at 2. rewrite <- succ_lt_mono. + apply sqrt_lt_lin. rewrite succ_lt_mono. now rewrite Ha', <- two_succ. +Qed. + +Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a. +Proof. + intros a Ha. + apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + rewrite sqrt_up_eqn; trivial. apply le_succ_l. + apply le_lt_trans with (P a). apply sqrt_le_lin. + now rewrite <- lt_succ_r, (lt_succ_pred 0). + rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r. + now rewrite <- Ha, sqrt_up_0. +Qed. + +(** [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. +Proof. + intros a b Ha Hb. + apply sqrt_up_le_square. + now apply mul_nonneg_nonneg. + apply mul_nonneg_nonneg; apply sqrt_up_nonneg. + rewrite mul_shuffle1. + apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec. +Qed. + +Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b). +Proof. + intros a b Ha Hb. + apply sqrt_up_lt_square. + apply mul_nonneg_nonneg; order. + apply mul_nonneg_nonneg; apply lt_succ_r. + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + rewrite mul_shuffle1. + apply mul_lt_mono_nonneg; trivial using square_nonneg; + now apply sqrt_up_spec. +Qed. + +(** 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). +Proof. + intros a Ha. + apply sqrt_up_le_square. + now apply le_le_succ_r. + apply le_le_succ_r, sqrt_up_nonneg. + rewrite <- (add_1_l (√°a)). + apply le_trans with (1²+(√°a)²). + rewrite mul_1_l, add_1_l, <- succ_le_mono. + now apply sqrt_sqrt_up_spec. + apply add_square_le. order'. apply sqrt_up_nonneg. +Qed. + +Lemma sqrt_up_succ_or : forall a, 0<=a -> √°(S a) == S (√°a) \/ √°(S a) == √°a. +Proof. + intros a Ha. + destruct (le_gt_cases (√°(S a)) (√°a)) as [H|H]. + right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order. + left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order. +Qed. + +Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a -> + (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²). +Proof. + intros a Ha. split. + intros EQ. + apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + exists (√°a). split. apply sqrt_up_nonneg. + generalize (proj2 (sqrt_up_spec a Ha)). + assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). + generalize (proj1 (sqrt_up_spec (S a) Ha')). + rewrite EQ, pred_succ, lt_succ_r. order. + exists 0. nzsimpl. now split. + intros (b & Hb & H). + now rewrite H, sqrt_up_succ_square, sqrt_up_square. +Qed. + +(** [sqrt_up] and addition *) + +Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b. +Proof. + assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b). + intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl. + apply sqrt_up_le_mono. + rewrite <- (add_0_l b) at 2. + apply add_le_mono_r; order. + intros a b. + destruct (le_gt_cases a 0) as [Ha|Ha]. now apply AUX. + destruct (le_gt_cases b 0) as [Hb|Hb]. + rewrite (add_comm a), (add_comm (√°a)); now apply AUX. + rewrite 2 sqrt_up_eqn; trivial. + nzsimpl. rewrite <- succ_le_mono. + transitivity (√(P a) + √b). + rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le. + apply add_le_mono_l. + apply le_sqrt_sqrt_up. + now apply add_pos_pos. +Qed. + +(** 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)). +Proof. + intros a b Ha Hb. + apply le_lteq in Ha; destruct Ha as [Ha|Ha]. + apply le_lteq in Hb; destruct Hb as [Hb|Hb]. + rewrite 3 sqrt_up_eqn; trivial. + nzsimpl. rewrite <- 2 succ_le_mono. + etransitivity; [eapply add_sqrt_le|]. + apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha). + apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). + apply sqrt_le_mono. + apply lt_succ_r. rewrite (lt_succ_pred 0). + apply mul_lt_mono_pos_l. order'. + apply add_lt_mono. + apply le_succ_l. now rewrite (lt_succ_pred 0). + apply le_succ_l. now rewrite (lt_succ_pred 0). + apply mul_pos_pos. order'. now apply add_pos_pos. + apply mul_pos_pos. order'. now apply add_pos_pos. + rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. + rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'. + rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. + rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'. +Qed. + +End NZSqrtUpProp. |