From 22093b97bb5e9a9912caadbf9e4a783dd00a0549 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 1 May 2025 14:07:35 +0900 Subject: [PATCH 1/2] expe lemmas Co-authored-by: Reynald Affeldt Co-authored-by: Jairo Miguel Marulanda-Giraldo --- CHANGELOG_UNRELEASED.md | 2 ++ reals/constructive_ereal.v | 21 +++++++++++++++++++++ 2 files changed, 23 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6638a5a47a..3025d70f92 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,8 @@ + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`, `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`, `ereal_sup_real`, `ereal_inf_real` +- in `constructive_ereal.v`: + + lemmas `expe_ge0`, `expe_eq0`, `expe_gt0` ### Changed diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 560f65caed..9fb3c0aa2d 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -3538,6 +3538,27 @@ Proof. by case: x => [x|//|//]; rewrite !qualifE/=. Qed. End sqrte. +Section expe. +Variable R : numDomainType. +Implicit Types x : \bar R. +Implicit Types n : nat. + +Lemma expe_eq0 x n : (x ^+ n == 0) = (n > 0)%N && (x == 0). +Proof. +by elim: n => [|n IHn]; [rewrite gt_eqF|rewrite expeS mule_eq0 IHn andKb]. +Qed. + +Lemma expe_gt0 x n : 0 < x -> 0 < x ^+ n. +Proof. by elim: n => //n ih /[dup] /ih xn0 x0; rewrite expeS mule_gt0. Qed. + +Lemma expe_ge0 x n : 0 <= x -> 0 <= x ^+ n. +Proof. +by rewrite le_eqVlt => /orP[/eqP <-|]; + [case: n => //n; rewrite expeS mul0e | move/expe_gt0/ltW]. +Qed. + +End expe. + Module DualAddTheory. Export DualAddTheoryNumDomain. Export DualAddTheoryRealDomain. From d3882975ca4962c91716089b821ecbd5165c4b4a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 May 2025 17:49:06 +0900 Subject: [PATCH 2/2] one liners Co-authored-by: Jairo Miguel Marulanda-Giraldo --- reals/constructive_ereal.v | 30 +++++++++--------------------- 1 file changed, 9 insertions(+), 21 deletions(-) diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 9fb3c0aa2d..511405b036 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -1394,6 +1394,15 @@ Qed. Lemma lte0_abs x : x < 0 -> `|x| = - x. Proof. by move=> /ltW/lee0_abs. Qed. +Lemma expe_eq0 x n : (x ^+ n == 0) = (n > 0)%N && (x == 0). +Proof. by elim: n => [|n ih]; rewrite ?expeS ?mule_eq0 ?ih ?andKb// gt_eqF. Qed. + +Lemma expe_gt0 x n : 0 < x -> 0 < x ^+ n. +Proof. by elim: n => //n ih /[dup] /ih xn0 x0; rewrite expeS mule_gt0. Qed. + +Lemma expe_ge0 x n : 0 <= x -> 0 <= x ^+ n. +Proof. by elim: n => // n ih x0; rewrite expeS mule_ge0// ih. Qed. + End ERealArithTh_numDomainType. Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope. Notation "x +? y" := (adde_def x y) : ereal_scope. @@ -3538,27 +3547,6 @@ Proof. by case: x => [x|//|//]; rewrite !qualifE/=. Qed. End sqrte. -Section expe. -Variable R : numDomainType. -Implicit Types x : \bar R. -Implicit Types n : nat. - -Lemma expe_eq0 x n : (x ^+ n == 0) = (n > 0)%N && (x == 0). -Proof. -by elim: n => [|n IHn]; [rewrite gt_eqF|rewrite expeS mule_eq0 IHn andKb]. -Qed. - -Lemma expe_gt0 x n : 0 < x -> 0 < x ^+ n. -Proof. by elim: n => //n ih /[dup] /ih xn0 x0; rewrite expeS mule_gt0. Qed. - -Lemma expe_ge0 x n : 0 <= x -> 0 <= x ^+ n. -Proof. -by rewrite le_eqVlt => /orP[/eqP <-|]; - [case: n => //n; rewrite expeS mul0e | move/expe_gt0/ltW]. -Qed. - -End expe. - Module DualAddTheory. Export DualAddTheoryNumDomain. Export DualAddTheoryRealDomain.