diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | CONTRIBUTING.md | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 78 |
3 files changed, 85 insertions, 8 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0693252..eb39d33 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,6 +20,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added +- in `ssrnum.v`, new lemmas: + + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW` + + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`, + `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl` + ### Changed ### Renamed diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6313d01..19ab0e5 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -124,7 +124,9 @@ Abbreviations are in the header of the file which introduces them. We list here - `g` -- a group argument. - `I` -- left/right injectivity, as in `addbI : right_injective addb.` -- alternatively predicate or set intersection, as in `predI.` - - `l` -- the left-hand of an operation, as in `andb_orl : left_distributive andb orb.` + - `l` -- the left-hand of an operation, as in + + `andb_orl : left_distributive andb orb.` + + ``ltr_norml x y : (`|x| < y) = (- y < x < y).`` - `L` -- the left-hand of a relation, as in `ltn_subrL : n - m < n = (0 < m) && (0 < n).` - `LR` -- moving an operator from the left-hand to the right-hand of an relation, as in `leq_subLR : (m - n <= p) = (m <= n + p).` - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.` @@ -132,8 +134,10 @@ Abbreviations are in the header of the file which introduces them. We list here - `N` -- alternatively ring negation, as in `mulNr : (- x) * y = - (x * y).` - `P` -- a characteristic property, often a reflection lemma, as in `andP : reflect (a /\ b) (a && b)`. - - `r` -- a right-hand operation, as `orb_andr : right_distributive orb andb.` - -- alternatively, it is a ring argument. + - `r` -- a right-hand operation, as in + + `orb_andr : right_distributive orb andb.` + + ``ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).`` + + alternatively, it is a ring argument. - `R` -- the right-hand of a relation, as in `ltn_subrR : n < n - m = false`. - `RL` -- moving an operator from the right-hand to the left-hand of an relation, as in `ltn_subRL : (n < p - m) = (m + n < p).` - `T` or `t` -- boolean truth, as in `andbT: right_id true andb.` diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index e1e5992..95c40cd 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2894,7 +2894,19 @@ rewrite real_ltNge ?real_ler_norml // negb_and -?real_ltNge ?realN //. by rewrite orbC ltr_oppr. Qed. -Definition real_lter_normr := (real_ler_normr, real_ltr_normr). +Definition real_lter_normr := (real_ler_normr, real_ltr_normr). + +Lemma real_ltr_normlW x y : x \is real -> `|x| < y -> x < y. +Proof. by move=> ?; case/real_ltr_normlP. Qed. + +Lemma real_ltrNnormlW x y : x \is real -> `|x| < y -> - y < x. +Proof. by move=> ?; case/real_ltr_normlP => //; rewrite ltr_oppl. Qed. + +Lemma real_ler_normlW x y : x \is real -> `|x| <= y -> x <= y. +Proof. by move=> ?; case/real_ler_normlP. Qed. + +Lemma real_lerNnormlW x y : x \is real -> `|x| <= y -> - y <= x. +Proof. by move=> ?; case/real_ler_normlP => //; rewrite ler_oppl. Qed. Lemma real_ler_distl x y e : x - y \is real -> (`|x - y| <= e) = (y - e <= x <= y + e). @@ -2906,6 +2918,30 @@ Proof. by move=> Rxy; rewrite real_lter_norml // !lter_sub_addl. Qed. Definition real_lter_distl := (real_ler_distl, real_ltr_distl). +Lemma real_ltr_distl_addr x y e : x - y \is real -> `|x - y| < e -> x < y + e. +Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed. + +Lemma real_ler_distl_addr x y e : x - y \is real -> `|x - y| <= e -> x <= y + e. +Proof. by move=> ?; rewrite real_ler_distl // => /andP[]. Qed. + +Lemma real_ltr_distlC_addr x y e : x - y \is real -> `|x - y| < e -> y < x + e. +Proof. by rewrite realBC (distrC x) => ? /real_ltr_distl_addr; apply. Qed. + +Lemma real_ler_distlC_addr x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. +Proof. by rewrite realBC distrC => ? /real_ler_distl_addr; apply. Qed. + +Lemma real_ltr_distl_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y. +Proof. by move/real_ltr_distl_addr; rewrite ltr_sub_addr; apply. Qed. + +Lemma real_ler_distl_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y. +Proof. by move/real_ler_distl_addr; rewrite ler_sub_addr; apply. Qed. + +Lemma real_ltr_distlC_subl x y e : x - y \is real -> `|x - y| < e -> y - e < x. +Proof. by rewrite realBC distrC => ? /real_ltr_distl_subl; apply. Qed. + +Lemma real_ler_distlC_subl x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. +Proof. by rewrite realBC distrC => ? /real_ler_distl_subl; apply. Qed. + (* GG: pointless duplication }-( *) Lemma eqr_norm_id x : (`|x| == x) = (0 <= x). Proof. by rewrite ger0_def. Qed. Lemma eqr_normN x : (`|x| == - x) = (x <= 0). Proof. by rewrite ler0_def. Qed. @@ -3738,22 +3774,54 @@ Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y). Proof. exact: real_ltr_normlP. Qed. Arguments ltr_normlP {x y}. +Lemma ltr_normlW x y : `|x| < y -> x < y. Proof. exact: real_ltr_normlW. Qed. + +Lemma ltrNnormlW x y : `|x| < y -> - y < x. Proof. exact: real_ltrNnormlW. Qed. + +Lemma ler_normlW x y : `|x| <= y -> x <= y. Proof. exact: real_ler_normlW. Qed. + +Lemma lerNnormlW x y : `|x| <= y -> - y <= x. Proof. exact: real_lerNnormlW. Qed. + Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y). -Proof. by rewrite leNgt ltr_norml negb_and -!leNgt orbC ler_oppr. Qed. +Proof. exact: real_ler_normr. Qed. Lemma ltr_normr x y : (x < `|y|) = (x < y) || (x < - y). -Proof. by rewrite ltNge ler_norml negb_and -!ltNge orbC ltr_oppr. Qed. +Proof. exact: real_ltr_normr. Qed. Definition lter_normr := (ler_normr, ltr_normr). Lemma ler_distl x y e : (`|x - y| <= e) = (y - e <= x <= y + e). -Proof. by rewrite lter_norml !lter_sub_addl. Qed. +Proof. exact: real_ler_distl. Qed. Lemma ltr_distl x y e : (`|x - y| < e) = (y - e < x < y + e). -Proof. by rewrite lter_norml !lter_sub_addl. Qed. +Proof. exact: real_ltr_distl. Qed. Definition lter_distl := (ler_distl, ltr_distl). +Lemma ltr_distl_addr x y e : `|x - y| < e -> x < y + e. +Proof. exact: real_ltr_distl_addr. Qed. + +Lemma ler_distl_addr x y e : `|x - y| <= e -> x <= y + e. +Proof. exact: real_ler_distl_addr. Qed. + +Lemma ltr_distlC_addr x y e : `|x - y| < e -> y < x + e. +Proof. exact: real_ltr_distlC_addr. Qed. + +Lemma ler_distlC_addr x y e : `|x - y| <= e -> y <= x + e. +Proof. exact: real_ler_distlC_addr. Qed. + +Lemma ltr_distl_subl x y e : `|x - y| < e -> x - e < y. +Proof. exact: real_ltr_distl_subl. Qed. + +Lemma ler_distl_subl x y e : `|x - y| <= e -> x - e <= y. +Proof. exact: real_ler_distl_subl. Qed. + +Lemma ltr_distlC_subl x y e : `|x - y| < e -> y - e < x. +Proof. exact: real_ltr_distlC_subl. Qed. + +Lemma ler_distlC_subr x y e : `|x - y| <= e -> y - e <= x. +Proof. exact: real_ler_distlC_subl. Qed. + Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. |