diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 16 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 561 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 40 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 132 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 5 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 622 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 5 |
10 files changed, 247 insertions, 1158 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 3efe76d..c99ef61 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1075,11 +1075,11 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. Qed. -Notation "@ 'coprimez_expl'" := - (deprecate coprimez_expl coprimezXl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimez_expr'" := - (deprecate coprimez_expr coprimezXr) (at level 10, only parsing) : fun_scope. -Notation coprimez_mull := (deprecate coprimez_mull coprimezMl) (only parsing). -Notation coprimez_mulr := (deprecate coprimez_mulr coprimezMr) (only parsing). -Notation coprimez_expl := (fun k => @coprimez_expl k _ _) (only parsing). -Notation coprimez_expr := (fun k => @coprimez_expr k _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMl instead.")] +Notation coprimez_mull := coprimezMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMr instead.")] +Notation coprimez_mulr := coprimezMr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXl instead.")] +Notation coprimez_expl := coprimezXl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXr instead.")] +Notation coprimez_expr := coprimezXr (only parsing). diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index b6964f1..57d7c3c 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -876,444 +876,197 @@ Proof. exact: itv_splitUeq. Qed. End mc_1_11. -(* Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a *) -(* qualified name.) *) -Local Notation lteif := Order.lteif (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use Order.lteif instead.")] Notation "@ 'lersif'" := - ((fun _ (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b)) - (deprecate lersif lteif)) + (fun (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b)) (at level 10, only parsing). -Notation lersif := (@lersif _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use Order.lteif instead.")] +Notation lersif := (fun x y b => @Order.lteif _ _ x y (~~ b)) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use [_ < _ ?<= if _] instead.")] Notation "x <= y ?< 'if' b" := - ((fun _ => x < y ?<= if ~~ b) (deprecate lersif lteif)) - (at level 70, y at next level, only parsing) : ring_scope. + (x < y ?<= if ~~ b) (at level 70, y at next level, only parsing) : ring_scope. (* LersifPo *) -Notation "@ 'subr_lersifr0'" := - ((fun _ => @mc_1_11.subr_lersifr0) (deprecate subr_lersifr0 subr_lteifr0)) - (at level 10, only parsing). - -Notation subr_lersifr0 := (@subr_lersifr0 _) (only parsing). - -Notation "@ 'subr_lersif0r'" := - ((fun _ => @mc_1_11.subr_lersif0r) (deprecate subr_lersif0r subr_lteif0r)) - (at level 10, only parsing). - -Notation subr_lersif0r := (@subr_lersif0r _) (only parsing). - -Notation subr_lersif0 := - ((fun _ => @mc_1_11.subr_lersif0) (deprecate subr_lersif0 subr_lteif0)) - (only parsing). - -Notation "@ 'lersif_trans'" := - ((fun _ => @mc_1_11.lersif_trans) (deprecate lersif_trans lteif_trans)) - (at level 10, only parsing). - -Notation lersif_trans := (@lersif_trans _ _ _ _ _ _) (only parsing). - -Notation lersif01 := - ((fun _ => @mc_1_11.lersif01) (deprecate lersif01 lteif01)) (only parsing). - -Notation "@ 'lersif_anti'" := - ((fun _ => @mc_1_11.lersif_anti) (deprecate lersif_anti lteif_anti)) - (at level 10, only parsing). - -Notation lersif_anti := (@lersif_anti _) (only parsing). - -Notation "@ 'lersifxx'" := - ((fun _ => @mc_1_11.lersifxx) (deprecate lersifxx lteifxx)) - (at level 10, only parsing). - -Notation lersifxx := (@lersifxx _) (only parsing). - -Notation "@ 'lersifNF'" := - ((fun _ => @mc_1_11.lersifNF) (deprecate lersifNF lteifNF)) - (at level 10, only parsing). - -Notation lersifNF := (@lersifNF _ _ _ _) (only parsing). - -Notation "@ 'lersifS'" := - ((fun _ => @mc_1_11.lersifS) (deprecate lersifS lteifS)) - (at level 10, only parsing). - -Notation lersifS := (@lersifS _ _ _) (only parsing). - -Notation "@ 'lersifT'" := - ((fun _ => @mc_1_11.lersifT) (deprecate lersifT lteifT)) - (at level 10, only parsing). - -Notation lersifT := (@lersifT _) (only parsing). - -Notation "@ 'lersifF'" := - ((fun _ => @mc_1_11.lersifF) (deprecate lersifF lteifF)) - (at level 10, only parsing). - -Notation lersifF := (@lersifF _) (only parsing). - -Notation "@ 'lersif_oppl'" := - ((fun _ => @mc_1_11.lersif_oppl) (deprecate lersif_oppl lteif_oppl)) - (at level 10, only parsing). - -Notation lersif_oppl := (@lersif_oppl _) (only parsing). - -Notation "@ 'lersif_oppr'" := - ((fun _ => @mc_1_11.lersif_oppr) (deprecate lersif_oppr lteif_oppr)) - (at level 10, only parsing). - -Notation lersif_oppr := (@lersif_oppr _) (only parsing). - -Notation "@ 'lersif_0oppr'" := - ((fun _ => @mc_1_11.lersif_0oppr) (deprecate lersif_0oppr lteif_0oppr)) - (at level 10, only parsing). - -Notation lersif_0oppr := (@lersif_0oppr _) (only parsing). - -Notation "@ 'lersif_oppr0'" := - ((fun _ => @mc_1_11.lersif_oppr0) (deprecate lersif_oppr0 lteif_oppr0)) - (at level 10, only parsing). - -Notation lersif_oppr0 := (@lersif_oppr0 _) (only parsing). - -Notation "@ 'lersif_opp2'" := - ((fun _ => @mc_1_11.lersif_opp2) (deprecate lersif_opp2 lteif_opp2)) - (at level 10, only parsing). - -Notation lersif_opp2 := (@lersif_opp2 _) (only parsing). - -Notation lersif_oppE := - ((fun _ => @mc_1_11.lersif_oppE) (deprecate lersif_oppE lteif_oppE)) - (only parsing). - -Notation "@ 'lersif_add2l'" := - ((fun _ => @mc_1_11.lersif_add2l) (deprecate lersif_add2l lteif_add2l)) - (at level 10, only parsing). - -Notation lersif_add2l := (@lersif_add2l _) (only parsing). - -Notation "@ 'lersif_add2r'" := - ((fun _ => @mc_1_11.lersif_add2r) (deprecate lersif_add2r lteif_add2r)) - (at level 10, only parsing). - -Notation lersif_add2r := (@lersif_add2r _) (only parsing). - -Notation lersif_add2 := - ((fun _ => @mc_1_11.lersif_add2) (deprecate lersif_add2 lteif_add2)) - (only parsing). - -Notation "@ 'lersif_subl_addr'" := - ((fun _ => @mc_1_11.lersif_subl_addr) - (deprecate lersif_subl_addr lteif_subl_addr)) - (at level 10, only parsing). - -Notation lersif_subl_addr := (@lersif_subl_addr _) (only parsing). - -Notation "@ 'lersif_subr_addr'" := - ((fun _ => @mc_1_11.lersif_subr_addr) - (deprecate lersif_subr_addr lteif_subr_addr)) - (at level 10, only parsing). - -Notation lersif_subr_addr := (@lersif_subr_addr _) (only parsing). - -Notation lersif_sub_addr := - ((fun _ => @mc_1_11.lersif_sub_addr) - (deprecate lersif_sub_addr lteif_sub_addr)) - (only parsing). - -Notation "@ 'lersif_subl_addl'" := - ((fun _ => @mc_1_11.lersif_subl_addl) - (deprecate lersif_subl_addl lteif_subl_addl)) - (at level 10, only parsing). - -Notation lersif_subl_addl := (@lersif_subl_addl _) (only parsing). - -Notation "@ 'lersif_subr_addl'" := - ((fun _ => @mc_1_11.lersif_subr_addl) - (deprecate lersif_subr_addl lteif_subr_addl)) - (at level 10, only parsing). - -Notation lersif_subr_addl := (@lersif_subr_addl _) (only parsing). - -Notation lersif_sub_addl := - ((fun _ => @mc_1_11.lersif_sub_addl) - (deprecate lersif_sub_addl lteif_sub_addl)) - (only parsing). - -Notation "@ 'lersif_andb'" := - ((fun _ => @mc_1_11.lersif_andb) (deprecate lersif_andb lteif_andb)) - (at level 10, only parsing). - -Notation lersif_andb := (@lersif_andb _) (only parsing). - -Notation "@ 'lersif_orb'" := - ((fun _ => @mc_1_11.lersif_orb) (deprecate lersif_orb lteif_orb)) - (at level 10, only parsing). - -Notation lersif_orb := (@lersif_orb _) (only parsing). - -Notation "@ 'lersif_imply'" := - ((fun _ => @mc_1_11.lersif_imply) (deprecate lersif_imply lteif_imply)) - (at level 10, only parsing). - -Notation lersif_imply := (@lersif_imply _ _ _ _ _) (only parsing). - -Notation "@ 'lersifW'" := - ((fun _ => @mc_1_11.lersifW) (deprecate lersifW lteifW)) - (at level 10, only parsing). - -Notation lersifW := (@lersifW _ _ _ _) (only parsing). - -Notation "@ 'ltrW_lersif'" := - ((fun _ => @mc_1_11.ltrW_lersif) (deprecate ltrW_lersif ltrW_lteif)) - (at level 10, only parsing). - -Notation ltrW_lersif := (@ltrW_lersif _) (only parsing). - -Notation "@ 'lersif_pmul2l'" := - ((fun _ => @mc_1_11.lersif_pmul2l) (deprecate lersif_pmul2l lteif_pmul2l)) - (at level 10, only parsing). - -Notation lersif_pmul2l := (fun b => @lersif_pmul2l _ b _) (only parsing). - -Notation "@ 'lersif_pmul2r'" := - ((fun _ => @mc_1_11.lersif_pmul2r) (deprecate lersif_pmul2r lteif_pmul2r)) - (at level 10, only parsing). - -Notation lersif_pmul2r := (fun b => @lersif_pmul2r _ b _) (only parsing). - -Notation "@ 'lersif_nmul2l'" := - ((fun _ => @mc_1_11.lersif_nmul2l) (deprecate lersif_nmul2l lteif_nmul2l)) - (at level 10, only parsing). - -Notation lersif_nmul2l := (fun b => @lersif_nmul2l _ b _) (only parsing). - -Notation "@ 'lersif_nmul2r'" := - ((fun _ => @mc_1_11.lersif_nmul2r) (deprecate lersif_nmul2r lteif_nmul2r)) - (at level 10, only parsing). - -Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing). - -Notation "@ 'real_lersifN'" := - ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifNE)) - (at level 10, only parsing). - -Notation real_lersifN := (@real_lersifN _ _ _) (only parsing). - -Notation "@ 'real_lersif_norml'" := - ((fun _ => @mc_1_11.real_lersif_norml) - (deprecate real_lersif_norml real_lteif_norml)) - (at level 10, only parsing). - -Notation real_lersif_norml := - (fun b => @real_lersif_norml _ b _) (only parsing). - -Notation "@ 'real_lersif_normr'" := - ((fun _ => @mc_1_11.real_lersif_normr) - (deprecate real_lersif_normr real_lteif_normr)) - (at level 10, only parsing). - -Notation real_lersif_normr := - (fun b x => @real_lersif_normr _ b x _) (only parsing). - -Notation "@ 'lersif_nnormr'" := - ((fun _ => @mc_1_11.lersif_nnormr) (deprecate lersif_nnormr lteif_nnormr)) - (at level 10, only parsing). - -Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteifr0 instead.")] +Notation subr_lersifr0 := mc_1_11.subr_lersifr0 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteif0r instead.")] +Notation subr_lersif0r := mc_1_11.subr_lersif0r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteif0 instead.")] +Notation subr_lersif0 := mc_1_11.subr_lersif0 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_trans instead.")] +Notation lersif_trans := mc_1_11.lersif_trans (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif01 instead.")] +Notation lersif01 := mc_1_11.lersif01 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_anti instead.")] +Notation lersif_anti := mc_1_11.lersif_anti (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifxx instead.")] +Notation lersifxx := mc_1_11.lersifxx (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifNF instead.")] +Notation lersifNF := mc_1_11.lersifNF (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifS instead.")] +Notation lersifS := mc_1_11.lersifS (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifT instead.")] +Notation lersifT := mc_1_11.lersifT (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifF instead.")] +Notation lersifF := mc_1_11.lersifF (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppl instead.")] +Notation lersif_oppl := mc_1_11.lersif_oppl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppr instead.")] +Notation lersif_oppr := mc_1_11.lersif_oppr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_0oppr instead.")] +Notation lersif_0oppr := mc_1_11.lersif_0oppr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppr0 instead.")] +Notation lersif_oppr0 := mc_1_11.lersif_oppr0 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_opp2 instead.")] +Notation lersif_opp2 := mc_1_11.lersif_opp2 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppE instead.")] +Notation lersif_oppE := mc_1_11.lersif_oppE (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2l instead.")] +Notation lersif_add2l := mc_1_11.lersif_add2l (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2r instead.")] +Notation lersif_add2r := mc_1_11.lersif_add2r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2 instead.")] +Notation lersif_add2 := mc_1_11.lersif_add2 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_subl_addr instead.")] +Notation lersif_subl_addr := mc_1_11.lersif_subl_addr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_subr_addr instead.")] +Notation lersif_subr_addr := mc_1_11.lersif_subr_addr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_sub_addr instead.")] +Notation lersif_sub_addr := mc_1_11.lersif_sub_addr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lersif_subl_addl instead.")] +Notation lersif_subl_addl := mc_1_11.lersif_subl_addl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lersif_subr_addl instead.")] +Notation lersif_subr_addl := mc_1_11.lersif_subr_addl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lersif_sub_addl instead.")] +Notation lersif_sub_addl := mc_1_11.lersif_sub_addl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_andb instead.")] +Notation lersif_andb := mc_1_11.lersif_andb (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_orb instead.")] +Notation lersif_orb := mc_1_11.lersif_orb (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_imply instead.")] +Notation lersif_imply := mc_1_11.lersif_imply (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifW instead.")] +Notation lersifW := mc_1_11.lersifW (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use ltrW_lteif instead.")] +Notation ltrW_lersif := mc_1_11.ltrW_lersif (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pmul2l instead.")] +Notation lersif_pmul2l := mc_1_11.lersif_pmul2l (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pmul2r instead.")] +Notation lersif_pmul2r := mc_1_11.lersif_pmul2r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nmul2l instead.")] +Notation lersif_nmul2l := mc_1_11.lersif_nmul2l (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nmul2r instead.")] +Notation lersif_nmul2r := mc_1_11.lersif_nmul2r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use real_lteifNE instead.")] +Notation real_lersifN := mc_1_11.real_lersifN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use real_lteif_norml instead.")] +Notation real_lersif_norml := mc_1_11.real_lersif_norml (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use real_lteif_normr instead.")] +Notation real_lersif_normr := mc_1_11.real_lersif_normr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nnormr instead.")] +Notation lersif_nnormr := mc_1_11.lersif_nnormr (only parsing). (* LersifOrdered *) -Notation "@ 'lersifN'" := - ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifNE)) - (at level 10, only parsing). - -Notation lersifN := (@lersifN _) (only parsing). - -Notation "@ 'lersif_norml'" := - ((fun _ => @mc_1_11.lersif_norml) (deprecate lersif_norml lteif_norml)) - (at level 10, only parsing). - -Notation lersif_norml := (@lersif_norml _) (only parsing). - -Notation "@ 'lersif_normr'" := - ((fun _ => @mc_1_11.lersif_normr) (deprecate lersif_normr lteif_normr)) - (at level 10, only parsing). - -Notation lersif_normr := (@lersif_normr _) (only parsing). - -Notation "@ 'lersif_distl'" := - ((fun _ => @mc_1_11.lersif_distl) (deprecate lersif_distl lteif_distl)) - (at level 10, only parsing). - -Notation lersif_distl := (@lersif_distl _) (only parsing). - -Notation "@ 'lersif_minr'" := - ((fun _ => @mc_1_11.lersif_minr) (deprecate lersif_minr lteif_minr)) - (at level 10, only parsing). - -Notation lersif_minr := (@lersif_minr _) (only parsing). - -Notation "@ 'lersif_minl'" := - ((fun _ => @mc_1_11.lersif_minl) (deprecate lersif_minl lteif_minl)) - (at level 10, only parsing). - -Notation lersif_minl := (@lersif_minl _) (only parsing). - -Notation "@ 'lersif_maxr'" := - ((fun _ => @mc_1_11.lersif_maxr) (deprecate lersif_maxr lteif_maxr)) - (at level 10, only parsing). - -Notation lersif_maxr := (@lersif_maxr _) (only parsing). - -Notation "@ 'lersif_maxl'" := - ((fun _ => @mc_1_11.lersif_maxl) (deprecate lersif_maxl lteif_maxl)) - (at level 10, only parsing). - -Notation lersif_maxl := (@lersif_maxl _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifNE instead.")] +Notation lersifN := mc_1_11.lersifN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_norml instead.")] +Notation lersif_norml := mc_1_11.lersif_norml (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_normr instead.")] +Notation lersif_normr := mc_1_11.lersif_normr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_distl instead.")] +Notation lersif_distl := mc_1_11.lersif_distl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_minr instead.")] +Notation lersif_minr := mc_1_11.lersif_minr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_minl instead.")] +Notation lersif_minl := mc_1_11.lersif_minl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_maxr instead.")] +Notation lersif_maxr := mc_1_11.lersif_maxr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_maxl instead.")] +Notation lersif_maxl := mc_1_11.lersif_maxl (only parsing). (* LersifField *) -Notation "@ 'lersif_pdivl_mulr'" := - ((fun _ => @mc_1_11.lersif_pdivl_mulr) - (deprecate lersif_pdivl_mulr lteif_pdivl_mulr)) - (at level 10, only parsing). - -Notation lersif_pdivl_mulr := - (fun b => @lersif_pdivl_mulr _ b _) (only parsing). - -Notation "@ 'lersif_pdivr_mulr'" := - ((fun _ => @mc_1_11.lersif_pdivr_mulr) - (deprecate lersif_pdivr_mulr lteif_pdivr_mulr)) - (at level 10, only parsing). - -Notation lersif_pdivr_mulr := - (fun b => @lersif_pdivr_mulr _ b _) (only parsing). - -Notation "@ 'lersif_pdivl_mull'" := - ((fun _ => @mc_1_11.lersif_pdivl_mull) - (deprecate lersif_pdivl_mull lteif_pdivl_mull)) - (at level 10, only parsing). - -Notation lersif_pdivl_mull := - (fun b => @lersif_pdivl_mull _ b _) (only parsing). - -Notation "@ 'lersif_pdivr_mull'" := - ((fun _ => @mc_1_11.lersif_pdivr_mull) - (deprecate lersif_pdivr_mull lteif_pdivr_mull)) - (at level 10, only parsing). - -Notation lersif_pdivr_mull := - (fun b => @lersif_pdivr_mull _ b _) (only parsing). - -Notation "@ 'lersif_ndivl_mulr'" := - ((fun _ => @mc_1_11.lersif_ndivl_mulr) - (deprecate lersif_ndivl_mulr lteif_ndivl_mulr)) - (at level 10, only parsing). - -Notation lersif_ndivl_mulr := - (fun b => @lersif_ndivl_mulr _ b _) (only parsing). - -Notation "@ 'lersif_ndivr_mulr'" := - ((fun _ => @mc_1_11.lersif_ndivr_mulr) - (deprecate lersif_ndivr_mulr lteif_ndivr_mulr)) - (at level 10, only parsing). - -Notation lersif_ndivr_mulr := - (fun b => @lersif_ndivr_mulr _ b _) (only parsing). - -Notation "@ 'lersif_ndivl_mull'" := - ((fun _ => @mc_1_11.lersif_ndivl_mull) - (deprecate lersif_ndivl_mull lteif_ndivl_mull)) - (at level 10, only parsing). - -Notation lersif_ndivl_mull := - (fun b => @lersif_ndivl_mull _ b _) (only parsing). - -Notation "@ 'lersif_ndivr_mull'" := - ((fun _ => @mc_1_11.lersif_ndivr_mull) - (deprecate lersif_ndivr_mull lteif_ndivr_mull)) - (at level 10, only parsing). - -Notation lersif_ndivr_mull := - (fun b => @lersif_ndivr_mull _ b _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivl_mulr instead.")] +Notation lersif_pdivl_mulr := mc_1_11.lersif_pdivl_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivr_mulr instead.")] +Notation lersif_pdivr_mulr := mc_1_11.lersif_pdivr_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivl_mull instead.")] +Notation lersif_pdivl_mull := mc_1_11.lersif_pdivl_mull (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivr_mull instead.")] +Notation lersif_pdivr_mull := mc_1_11.lersif_pdivr_mull (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivl_mulr instead.")] +Notation lersif_ndivl_mulr := mc_1_11.lersif_ndivl_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivr_mulr instead.")] +Notation lersif_ndivr_mulr := mc_1_11.lersif_ndivr_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivl_mull instead.")] +Notation lersif_ndivl_mull := mc_1_11.lersif_ndivl_mull (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivr_mull instead.")] +Notation lersif_ndivr_mull := mc_1_11.lersif_ndivr_mull (only parsing). (* IntervalPo *) -Notation "@ 'lersif_in_itv'" := - ((fun _ => @mc_1_11.lersif_in_itv) (deprecate lersif_in_itv lteif_in_itv)) - (at level 10, only parsing). - -Notation lersif_in_itv := (@lersif_in_itv _ _ _ _ _ _) (only parsing). - -Notation "@ 'itv_gte'" := - ((fun _ => @mc_1_11.itv_gte) (deprecate itv_gte itv_ge)) - (at level 10, only parsing). - -Notation itv_gte := (@itv_gte _ _ _ _ _) (only parsing). - -Notation "@ 'ltr_in_itv'" := - ((fun _ => @mc_1_11.ltr_in_itv) (deprecate ltr_in_itv lt_in_itv)) - (at level 10, only parsing). - -Notation ltr_in_itv := (@ltr_in_itv _ _ _ _ _ _) (only parsing). - -Notation "@ 'ler_in_itv'" := - ((fun _ => @mc_1_11.ler_in_itv) (deprecate ler_in_itv lt_in_itv)) - (at level 10, only parsing). - -Notation ler_in_itv := (@ler_in_itv _ _ _ _ _ _) (only parsing). - -Notation "@ 'itv_splitU2'" := - ((fun _ => @mc_1_11.itv_splitU2) (deprecate itv_splitU2 itv_splitUeq)) - (at level 10, only parsing). - -Notation itv_splitU2 := (@itv_splitU2 _ _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_in_itv instead.")] +Notation lersif_in_itv := mc_1_11.lersif_in_itv (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use itv_ge instead.")] +Notation itv_gte := mc_1_11.itv_gte (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lt_in_itv instead.")] +Notation ltr_in_itv := mc_1_11.ltr_in_itv (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lt_in_itv instead.")] +Notation ler_in_itv := @mc_1_11.ler_in_itv (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use itv_splitUeq instead.")] +Notation itv_splitU2 := mc_1_11.itv_splitU2 (only parsing). (* `itv_intersection` accepts any `numDomainType` but `Order.meet` accepts *) -(* only `realDomainType`. Use `Order.meet` instead of `itv_meet`. *) +(* only `realDomainType`. *) +#[deprecated(since="mathcomp 1.12.0", note="Use Order.meet instead.")] Notation "@ 'itv_intersection'" := - ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R]) - (deprecate itv_intersection itv_meet)) + (fun (R : realDomainType) => @Order.meet _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use Order.meet instead.")] +Notation itv_intersection := + (@Order.meet _ [latticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersection := (@itv_intersection _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meet1x instead.")] Notation "@ 'itv_intersection1i'" := - ((fun _ (R : realDomainType) => @meet1x _ [tbLatticeType of interval R]) - (deprecate itv_intersection1i meet1x)) + (fun (R : realDomainType) => @meet1x _ [tbLatticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use meet1x instead.")] +Notation itv_intersection1i := + (@meet1x _ [tbLatticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersection1i := (@itv_intersection1i _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meetx1 instead.")] Notation "@ 'itv_intersectioni1'" := - ((fun _ (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R]) - (deprecate itv_intersectioni1 meetx1)) + (fun (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use meetx1 instead.")] + Notation itv_intersectioni1 := + (@meetx1 _ [tbLatticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersectioni1 := (@itv_intersectioni1 _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meetxx instead.")] Notation "@ 'itv_intersectionii'" := - ((fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R]) - (deprecate itv_intersectionii meetxx)) + (fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. - -Notation itv_intersectionii := (@itv_intersectionii _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use meetxx instead.")] +Notation itv_intersectionii := + (@meetxx _ [latticeType of interval (_ : realDomainType)]) (only parsing). (* IntervalOrdered *) - +#[deprecated(since="mathcomp 1.12.0", note="Use meetC instead.")] Notation "@ 'itv_intersectionC'" := - ((fun _ (R : realDomainType) => @meetC _ [latticeType of interval R]) - (deprecate itv_intersectionC meetC)) + (fun (R : realDomainType) => @meetC _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use meetC instead.")] +Notation itv_intersectionC := + (@meetC _ [latticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersectionC := (@itv_intersectionC _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meetA instead.")] Notation "@ 'itv_intersectionA'" := - ((fun _ (R : realDomainType) => @meetA _ [latticeType of interval R]) - (deprecate itv_intersectionA meetA)) + (fun (R : realDomainType) => @meetA _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. - -Notation itv_intersectionA := (@itv_intersectionA _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use meetA instead.")] +Notation itv_intersectionA := + (@meetA _ [latticeType of interval (_ : realDomainType)]) (only parsing). diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index e7e0e35..bd39654 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -3146,9 +3146,8 @@ Canonical matrix_finAlgType (R : finComRingType) n' := Hint Resolve comm_mx_scalar comm_scalar_mx : core. -Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar) - (at level 10, only parsing) : fun_scope. -Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use comm_mx_scalar instead.")] +Notation scalar_mx_comm := comm_mx_scalar (only parsing). (*****************************************************************************) (********************** Matrix unit ring and inverse matrices ****************) @@ -3685,6 +3684,5 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S) End mxRingOver. End mxOver. -Notation "@ 'map_mx_sub'" := - (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope. -Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use map_mxB instead.")] +Notation map_mx_sub := map_mxB (only parsing). diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index d707905..c23cfb1 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -3068,9 +3068,7 @@ Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. -Notation "@ 'mulsmx_addl'" := - (deprecate mulsmx_addl mulsmxDl) (at level 10, only parsing) : fun_scope. -Notation "@ 'mulsmx_addr'" := - (deprecate mulsmx_addr mulsmxDr) (at level 10, only parsing) : fun_scope. -Notation mulsmx_addl := (@mulsmx_addl _ _ _ _ _) (only parsing). -Notation mulsmx_addr := (@mulsmx_addr _ _ _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mulsmxDl instead.")] +Notation mulsmx_addl := mulsmxDl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mulsmxDr instead.")] +Notation mulsmx_addr := mulsmxDr (only parsing). diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 21e8ada..e74c917 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -2769,27 +2769,19 @@ Qed. End ClosedField. -Notation "@ 'polyC_add'" := - (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_opp'" := - (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_sub'" := - (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_muln'" := - (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_mul'" := - (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_inv'" := - (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope. -Notation "@ 'lead_coef_opp'" := - (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope. -Notation "@ 'derivn_sub'" := - (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope. -Notation polyC_add := (@polyC_add _) (only parsing). -Notation polyC_opp := (@polyC_opp _) (only parsing). -Notation polyC_sub := (@polyC_sub _) (only parsing). -Notation polyC_muln := (@polyC_muln _) (only parsing). -Notation polyC_mul := (@polyC_mul _) (only parsing). -Notation polyC_inv := (@polyC_inv _) (only parsing). -Notation lead_coef_opp := (@lead_coef_opp _) (only parsing). -Notation derivn_sub := (@derivn_sub _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCD instead.")] +Notation polyC_add := polyCD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCN instead.")] +Notation polyC_opp := polyCN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCB instead.")] +Notation polyC_sub := polyCB (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCMn instead.")] +Notation polyC_muln := polyCMn (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCM instead.")] +Notation polyC_mul := polyCM (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCV instead.")] +Notation polyC_inv := polyCV (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lead_coefN instead.")] +Notation lead_coef_opp := lead_coefN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use derivnB instead.")] +Notation derivn_sub := derivnB (only parsing). diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 41147fb..05a9ee3 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -624,17 +624,12 @@ Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed. End MonicDivisor. -Notation "@ 'rdivp_addl'" := - (deprecate rdivp_addl rdivpDl) (at level 10, only parsing) : fun_scope. -Notation "@ 'rdivp_addr'" := - (deprecate rdivp_addr rdivpDr) (at level 10, only parsing) : fun_scope. -Notation "@ 'rmodp_add'" := - (deprecate rmodp_add rmodpD) (at level 10, only parsing) : fun_scope. -Notation rdivp_addl := - (fun d_monic => @rdivp_addl _ _ d_monic _) (only parsing). -Notation rdivp_addr := - (fun d_monic q => @rdivp_addr _ _ d_monic q _) (only parsing). -Notation rmodp_add := (@rmodp_add _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use rdivpDl instead.")] +Notation rdivp_addl := rdivpDl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use rdivpDr instead.")] +Notation rdivp_addr := rdivpDr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use rmodpD instead.")] +Notation rmodp_add := rmodpD (only parsing). End RingMonic. @@ -2358,27 +2353,20 @@ End IDomainPseudoDivision. Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core. Hint Resolve dvdp0 : core. -Notation "@ 'dvdp_scalel'" := - (deprecate dvdp_scalel dvdpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'dvdp_scaler'" := - (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'dvdp_opp'" := - (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_scalel'" := - (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_scaler'" := - (deprecate coprimep_scaler coprimepZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_mull'" := - (deprecate coprimep_mull coprimepMl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_mulr'" := - (deprecate coprimep_mulr coprimepMr) (at level 10, only parsing) : fun_scope. -Notation dvdp_scalel := (@dvdp_scalel _ _) (only parsing). -Notation dvdp_scaler := (@dvdp_scaler _ _) (only parsing). -Notation dvdp_opp := (@dvdp_opp _) (only parsing). -Notation coprimep_scalel := (@coprimep_scalel _ _) (only parsing). -Notation coprimep_scaler := (@coprimep_scaler _ _) (only parsing). -Notation coprimep_mull := (@coprimep_mull _) (only parsing). -Notation coprimep_mulr := (@coprimep_mulr _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use dvdpZl instead.")] +Notation dvdp_scalel := dvdpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use dvdpZr instead.")] +Notation dvdp_scaler := dvdpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use dvdpNr instead.")] +Notation dvdp_opp := dvdpNr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepZl instead.")] +Notation coprimep_scalel := coprimepZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepZr instead.")] +Notation coprimep_scaler := coprimepZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepMl instead.")] +Notation coprimep_mull := coprimepMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepMr instead.")] +Notation coprimep_mulr := coprimepMr (only parsing). End CommonIdomain. @@ -2704,30 +2692,22 @@ Qed. End MoreUnitDivisor. -Notation "@ 'modp_scalel'" := - (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_scaler'" := - (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_opp'" := - (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_add'" := - (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scalel'" := - (deprecate divp_scalel divpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scaler'" := - (deprecate divp_scaler divpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_opp'" := - (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_add'" := - (deprecate divp_add divpD) (at level 10, only parsing) : fun_scope. -Notation modp_scalel := (@modp_scalel _ _) (only parsing). -Notation modp_scaler := (fun d_unit => @modp_scaler _ _ d_unit _) (only parsing). -Notation modp_opp := (@modp_opp _ _) (only parsing). -Notation modp_add := (@modp_add _ _) (only parsing). -Notation divp_scalel := (@divp_scalel _ _) (only parsing). -Notation divp_scaler := (fun d_unit => @divp_scaler _ _ d_unit _) (only parsing). -Notation divp_opp := (@divp_opp _ _) (only parsing). -Notation divp_add := (@divp_add _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZl instead.")] +Notation modp_scalel := modpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZr instead.")] +Notation modp_scaler := modpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpN instead.")] +Notation modp_opp := modpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpD instead.")] +Notation modp_add := modpD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZl instead.")] +Notation divp_scalel := divpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZr instead.")] +Notation divp_scaler := divpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpN instead.")] +Notation divp_opp := divpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpD instead.")] +Notation divp_add := divpD (only parsing). End IdomainUnit. @@ -3192,30 +3172,22 @@ End FieldMap. End FieldDivision. -Notation "@ 'modp_scalel'" := - (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_scaler'" := - (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_opp'" := - (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_add'" := - (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scalel'" := - (deprecate modp_scalel divpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scaler'" := - (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_opp'" := - (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_add'" := - (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope. -Notation modp_scalel := (@modp_scalel _) (only parsing). -Notation modp_scaler := (@modp_scaler _ _) (only parsing). -Notation modp_opp := (@modp_opp _) (only parsing). -Notation modp_add := (@modp_add _) (only parsing). -Notation divp_scalel := (@divp_scalel _) (only parsing). -Notation divp_scaler := (@divp_scaler _ _) (only parsing). -Notation divp_opp := (@divp_opp _) (only parsing). -Notation divp_add := (@divp_add _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZl instead.")] +Notation modp_scalel := modpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZr instead.")] +Notation modp_scaler := modpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpN instead.")] +Notation modp_opp := modpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpD instead.")] +Notation modp_add := modpD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZl instead.")] +Notation divp_scalel := divpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZr instead.")] +Notation divp_scaler := divpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpN instead.")] +Notation divp_opp := divpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpD instead.")] +Notation divp_add := divpD (only parsing). End Field. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index de8b513..a27177d 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -6044,8 +6044,8 @@ Definition imaginary_exists := imaginary_exists. Notation null_fun V := (null_fun V) (only parsing). Notation in_alg A := (in_alg_loc A). -Notation prodrMn := - (fun n A F => deprecate prodrMn prodrMn_const _ n _ A F) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use prodrMn_const instead.")] +Notation prodrMn := prodrMn_const (only parsing). End Theory. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index a51ec47..becacc2 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1778,6 +1778,5 @@ Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. End rpred. -Notation "@ 'polyC_mulrz'" := - (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope. -Notation polyC_mulrz := (@polyC_mulrz _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCMz instead.")] +Notation polyC_mulrz := polyCMz (only parsing). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index dce3ffd..cc04183 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -5395,625 +5395,3 @@ Export Num.NumMixin.Exports Num.RealMixin.Exports. Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports. Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin. - -(* compatibility module *) -Module mc_1_10. -Module Num. -(* If you failed to process the next line in the PG or the CoqIDE, replace *) -(* all the "ssrnum.Num" with "Top.Num" in this module to process them, and *) -(* revert them in order to compile and commit. This problem will be solved *) -(* in Coq 8.10. See also: https://github.com/math-comp/math-comp/pull/270. *) -Export ssrnum.Num. - -Module Import Def. -Export ssrnum.Num.Def. -Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y. -Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x. -End Def. - -Notation min := minr. -Notation max := maxr. - -Module Import Syntax. -Notation "`| x |" := - (@norm _ (@Num.NormedZmodule.numDomain_normedZmodType _) x) : ring_scope. -End Syntax. - -Module Import Theory. -Export ssrnum.Num.Theory. - -Section NumIntegralDomainTheory. -Variable R : numDomainType. -Implicit Types x y z : R. -Definition ltr_def x y : (x < y) = (y != x) && (x <= y) := lt_def x y. -Definition gerE x y : ge x y = (y <= x) := geE x y. -Definition gtrE x y : gt x y = (y < x) := gtE x y. -Definition lerr x : x <= x := lexx x. -Definition ltrr x : x < x = false := ltxx x. -Definition ltrW x y : x < y -> x <= y := @ltW _ _ x y. -Definition ltr_neqAle x y : (x < y) = (x != y) && (x <= y) := lt_neqAle x y. -Definition ler_eqVlt x y : (x <= y) = (x == y) || (x < y) := le_eqVlt x y. -Definition gtr_eqF x y : y < x -> x == y = false := @gt_eqF _ _ x y. -Definition ltr_eqF x y : x < y -> x == y = false := @lt_eqF _ _ x y. -Definition ler_asym : antisymmetric (@ler R) := le_anti. -Definition eqr_le x y : (x == y) = (x <= y <= x) := eq_le x y. -Definition ltr_trans : transitive (@ltr R) := lt_trans. -Definition ler_lt_trans y x z : x <= y -> y < z -> x < z := - @le_lt_trans _ _ y x z. -Definition ltr_le_trans y x z : x < y -> y <= z -> x < z := - @lt_le_trans _ _ y x z. -Definition ler_trans : transitive (@ler R) := le_trans. -Definition lterr := (lerr, ltrr). -Definition lerifP x y C : - reflect (x <= y ?= iff C) (if C then x == y else x < y) := leifP. -Definition ltr_asym x y : x < y < x = false := lt_asym x y. -Definition ler_anti : antisymmetric (@ler R) := le_anti. -Definition ltr_le_asym x y : x < y <= x = false := lt_le_asym x y. -Definition ler_lt_asym x y : x <= y < x = false := le_lt_asym x y. -Definition lter_anti := (=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym). -Definition ltr_geF x y : x < y -> y <= x = false := @lt_geF _ _ x y. -Definition ler_gtF x y : x <= y -> y < x = false := @le_gtF _ _ x y. -Definition ltr_gtF x y : x < y -> y < x = false := @lt_gtF _ _ x y. -Definition normr0 : `|0| = 0 :> R := normr0 _. -Definition normrMn x n : `|x *+ n| = `|x| *+ n := normrMn x n. -Definition normr0P {x} : reflect (`|x| = 0) (x == 0) := normr0P. -Definition normr_eq0 x : (`|x| == 0) = (x == 0) := normr_eq0 x. -Definition normrN x : `|- x| = `|x| := normrN x. -Definition distrC x y : `|x - y| = `|y - x| := distrC x y. -Definition normr_id x : `| `|x| | = `|x| := normr_id x. -Definition normr_ge0 x : 0 <= `|x| := normr_ge0 x. -Definition normr_le0 x : (`|x| <= 0) = (x == 0) := normr_le0 x. -Definition normr_lt0 x : `|x| < 0 = false := normr_lt0 x. -Definition normr_gt0 x : (`|x| > 0) = (x != 0) := normr_gt0 x. -Definition normrE := (normr_id, normr0, @normr1 R, @normrN1 R, normr_ge0, - normr_eq0, normr_lt0, normr_le0, normr_gt0, normrN). -End NumIntegralDomainTheory. - -Section NumIntegralDomainMonotonyTheory. -Variables R R' : numDomainType. -Section AcrossTypes. -Variables (D D' : pred R) (f : R -> R'). -Definition ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y} := - ltW_homo (f := f). -Definition ltrW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y} := - ltW_nhomo (f := f). -Definition inj_homo_ltr : - injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltr : - injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y} := - inj_nhomo_lt (f := f). -Definition incr_inj : {mono f : x y / x <= y} -> injective f := - inc_inj (f := f). -Definition decr_inj : {mono f : x y /~ x <= y} -> injective f := - dec_inj (f := f). -Definition lerW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y} := - leW_mono (f := f). -Definition lerW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y} := - leW_nmono (f := f). -Definition ltrW_homo_in : - {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}} := - ltW_homo_in (f := f). -Definition ltrW_nhomo_in : - {in D & D', {homo f : x y /~ x < y}} -> - {in D & D', {homo f : x y /~ x <= y}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltr_in : - {in D & D', injective f} -> {in D & D', {homo f : x y / x <= y}} -> - {in D & D', {homo f : x y / x < y}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltr_in : - {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} -> - {in D & D', {homo f : x y /~ x < y}} := - inj_nhomo_lt_in (f := f). -Definition incr_inj_in : - {in D &, {mono f : x y / x <= y}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decr_inj_in : - {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition lerW_mono_in : - {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}} := - leW_mono_in (f := f). -Definition lerW_nmono_in : - {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}} := - leW_nmono_in (f := f). -End AcrossTypes. -Section NatToR. -Variables (D D' : pred nat) (f : nat -> R). -Definition ltnrW_homo : - {homo f : m n / (m < n)%N >-> m < n} -> - {homo f : m n / (m <= n)%N >-> m <= n} := - ltW_homo (f := f). -Definition ltnrW_nhomo : - {homo f : m n / (n < m)%N >-> m < n} -> - {homo f : m n / (n <= m)%N >-> m <= n} := - ltW_nhomo (f := f). -Definition inj_homo_ltnr : injective f -> - {homo f : m n / (m <= n)%N >-> m <= n} -> - {homo f : m n / (m < n)%N >-> m < n} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltnr : injective f -> - {homo f : m n / (n <= m)%N >-> m <= n} -> - {homo f : m n / (n < m)%N >-> m < n} := - inj_nhomo_lt (f := f). -Definition incnr_inj : - {mono f : m n / (m <= n)%N >-> m <= n} -> injective f := - inc_inj (f := f). -Definition decnr_inj : - {mono f : m n / (n <= m)%N >-> m <= n} -> injective f := - dec_inj (f := f). -Definition decnr_inj_inj := decnr_inj. -Definition lenrW_mono : {mono f : m n / (m <= n)%N >-> m <= n} -> - {mono f : m n / (m < n)%N >-> m < n} := - leW_mono (f := f). -Definition lenrW_nmono : {mono f : m n / (n <= m)%N >-> m <= n} -> - {mono f : m n / (n < m)%N >-> m < n} := - leW_nmono (f := f). -Definition lenr_mono : {homo f : m n / (m < n)%N >-> m < n} -> - {mono f : m n / (m <= n)%N >-> m <= n} := - le_mono (f := f). -Definition lenr_nmono : - {homo f : m n / (n < m)%N >-> m < n} -> - {mono f : m n / (n <= m)%N >-> m <= n} := - le_nmono (f := f). -Definition ltnrW_homo_in : - {in D & D', {homo f : m n / (m < n)%N >-> m < n}} -> - {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} := - ltW_homo_in (f := f). -Definition ltnrW_nhomo_in : - {in D & D', {homo f : m n / (n < m)%N >-> m < n}} -> - {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltnr_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} -> - {in D & D', {homo f : m n / (m < n)%N >-> m < n}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltnr_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} -> - {in D & D', {homo f : m n / (n < m)%N >-> m < n}} := - inj_nhomo_lt_in (f := f). -Definition incnr_inj_in : - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decnr_inj_in : - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition decnr_inj_inj_in := decnr_inj_in. -Definition lenrW_mono_in : - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> - {in D &, {mono f : m n / (m < n)%N >-> m < n}} := - leW_mono_in (f := f). -Definition lenrW_nmono_in : - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> - {in D &, {mono f : m n / (n < m)%N >-> m < n}} := - leW_nmono_in (f := f). -Definition lenr_mono_in : - {in D &, {homo f : m n / (m < n)%N >-> m < n}} -> - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} := - le_mono_in (f := f). -Definition lenr_nmono_in : - {in D &, {homo f : m n / (n < m)%N >-> m < n}} -> - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} := - le_nmono_in (f := f). -End NatToR. -Section RToNat. -Variables (D D' : pred R) (f : R -> nat). -Definition ltrnW_homo : - {homo f : m n / m < n >-> (m < n)%N} -> - {homo f : m n / m <= n >-> (m <= n)%N} := - ltW_homo (f := f). -Definition ltrnW_nhomo : - {homo f : m n / n < m >-> (m < n)%N} -> - {homo f : m n / n <= m >-> (m <= n)%N} := - ltW_nhomo (f := f). -Definition inj_homo_ltrn : injective f -> - {homo f : m n / m <= n >-> (m <= n)%N} -> - {homo f : m n / m < n >-> (m < n)%N} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltrn : injective f -> - {homo f : m n / n <= m >-> (m <= n)%N} -> - {homo f : m n / n < m >-> (m < n)%N} := - inj_nhomo_lt (f := f). -Definition incrn_inj : {mono f : m n / m <= n >-> (m <= n)%N} -> injective f := - inc_inj (f := f). -Definition decrn_inj : {mono f : m n / n <= m >-> (m <= n)%N} -> injective f := - dec_inj (f := f). -Definition lernW_mono : - {mono f : m n / m <= n >-> (m <= n)%N} -> - {mono f : m n / m < n >-> (m < n)%N} := - leW_mono (f := f). -Definition lernW_nmono : - {mono f : m n / n <= m >-> (m <= n)%N} -> - {mono f : m n / n < m >-> (m < n)%N} := - leW_nmono (f := f). -Definition ltrnW_homo_in : - {in D & D', {homo f : m n / m < n >-> (m < n)%N}} -> - {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} := - ltW_homo_in (f := f). -Definition ltrnW_nhomo_in : - {in D & D', {homo f : m n / n < m >-> (m < n)%N}} -> - {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltrn_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} -> - {in D & D', {homo f : m n / m < n >-> (m < n)%N}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltrn_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} -> - {in D & D', {homo f : m n / n < m >-> (m < n)%N}} := - inj_nhomo_lt_in (f := f). -Definition incrn_inj_in : - {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decrn_inj_in : - {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition lernW_mono_in : - {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> - {in D &, {mono f : m n / m < n >-> (m < n)%N}} := - leW_mono_in (f := f). -Definition lernW_nmono_in : - {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> - {in D &, {mono f : m n / n < m >-> (m < n)%N}} := - leW_nmono_in (f := f). -End RToNat. -End NumIntegralDomainMonotonyTheory. - -Section NumDomainOperationTheory. -Variable R : numDomainType. -Implicit Types x y z t : R. -Definition lerif_refl x C : reflect (x <= x ?= iff C) C := leif_refl. -Definition lerif_trans x1 x2 x3 C12 C23 : - x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23 := - @leif_trans _ _ x1 x2 x3 C12 C23. -Definition lerif_le x y : x <= y -> x <= y ?= iff (x >= y) := @leif_le _ _ x y. -Definition lerif_eq x y : x <= y -> x <= y ?= iff (x == y) := @leif_eq _ _ x y. -Definition ger_lerif x y C : x <= y ?= iff C -> (y <= x) = C := - @ge_leif _ _ x y C. -Definition ltr_lerif x y C : x <= y ?= iff C -> (x < y) = ~~ C := - @lt_leif _ _ x y C. -Definition normr_real x : `|x| \is real := normr_real x. -Definition ler_norm_sum I r (G : I -> R) (P : pred I): - `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i| := - ler_norm_sum r G P. -Definition ler_norm_sub x y : `|x - y| <= `|x| + `|y| := ler_norm_sub x y. -Definition ler_dist_add z x y : `|x - y| <= `|x - z| + `|z - y| := - ler_dist_add z x y. -Definition ler_sub_norm_add x y : `|x| - `|y| <= `|x + y| := - ler_sub_norm_add x y. -Definition ler_sub_dist x y : `|x| - `|y| <= `|x - y| := ler_sub_dist x y. -Definition ler_dist_dist x y : `| `|x| - `|y| | <= `|x - y| := - ler_dist_dist x y. -Definition ler_dist_norm_add x y : `| `|x| - `|y| | <= `|x + y| := - ler_dist_norm_add x y. -Definition ler_nnorml x y : y < 0 -> `|x| <= y = false := @ler_nnorml _ _ x y. -Definition ltr_nnorml x y : y <= 0 -> `|x| < y = false := @ltr_nnorml _ _ x y. -Definition lter_nnormr := (ler_nnorml, ltr_nnorml). -Definition mono_in_lerif (A : pred R) (f : R -> R) C : - {in A &, {mono f : x y / x <= y}} -> - {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)} := - @mono_in_leif _ _ A f C. -Definition mono_lerif (f : R -> R) C : - {mono f : x y / x <= y} -> - forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C) := - @mono_leif _ _ f C. -Definition nmono_in_lerif (A : pred R) (f : R -> R) C : - {in A &, {mono f : x y /~ x <= y}} -> - {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)} := - @nmono_in_leif _ _ A f C. -Definition nmono_lerif (f : R -> R) C : - {mono f : x y /~ x <= y} -> - forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C) := - @nmono_leif _ _ f C. -End NumDomainOperationTheory. - -Section RealDomainTheory. -Variable R : realDomainType. -Implicit Types x y z t : R. -Definition ler_total : total (@ler R) := le_total. -Definition ltr_total x y : x != y -> (x < y) || (y < x) := - @lt_total _ _ x y. -Definition wlog_ler P : - (forall a b, P b a -> P a b) -> (forall a b, a <= b -> P a b) -> - forall a b : R, P a b := - @wlog_le _ _ P. -Definition wlog_ltr P : - (forall a, P a a) -> - (forall a b, (P b a -> P a b)) -> (forall a b, a < b -> P a b) -> - forall a b : R, P a b := - @wlog_lt _ _ P. -Definition ltrNge x y : (x < y) = ~~ (y <= x) := @ltNge _ _ x y. -Definition lerNgt x y : (x <= y) = ~~ (y < x) := @leNgt _ _ x y. -Definition neqr_lt x y : (x != y) = (x < y) || (y < x) := @neq_lt _ _ x y. -Definition eqr_leLR x y z t : - (x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t) := - @eq_leLR _ _ x y z t. -Definition eqr_leRL x y z t : - (x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y) := - @eq_leRL _ _ x y z t. -Definition eqr_ltLR x y z t : - (x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t) := - @eq_ltLR _ _ x y z t. -Definition eqr_ltRL x y z t : - (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y) := - @eq_ltRL _ _ x y z t. -End RealDomainTheory. - -Section RealDomainMonotony. -Variables (R : realDomainType) (R' : numDomainType) (D : pred R). -Variables (f : R -> R') (f' : R -> nat). -Definition ler_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y} := - le_mono (f := f). -Definition homo_mono := ler_mono. -Definition ler_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y} := - le_nmono (f := f). -Definition nhomo_mono := ler_nmono. -Definition ler_mono_in : - {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}} := - le_mono_in (f := f). -Definition homo_mono_in := ler_mono_in. -Definition ler_nmono_in : - {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}} := - le_nmono_in (f := f). -Definition nhomo_mono_in := ler_nmono_in. -Definition lern_mono : - {homo f' : m n / m < n >-> (m < n)%N} -> - {mono f' : m n / m <= n >-> (m <= n)%N} := - le_mono (f := f'). -Definition lern_nmono : - {homo f' : m n / n < m >-> (m < n)%N} -> - {mono f' : m n / n <= m >-> (m <= n)%N} := - le_nmono (f := f'). -Definition lern_mono_in : - {in D &, {homo f' : m n / m < n >-> (m < n)%N}} -> - {in D &, {mono f' : m n / m <= n >-> (m <= n)%N}} := - le_mono_in (f := f'). -Definition lern_nmono_in : - {in D &, {homo f' : m n / n < m >-> (m < n)%N}} -> - {in D &, {mono f' : m n / n <= m >-> (m <= n)%N}} := - le_nmono_in (f := f'). -End RealDomainMonotony. - -Section RealDomainOperations. -Variable R : realDomainType. -Implicit Types x y z : R. -Section MinMax. - -Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.max x y))%type. -Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed. -Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?]. -Ltac mexact x := by mapply x. - -Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed. -Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed. -Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed. -Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed. -Lemma maxrC : @commutative R R max. Proof. mexact @maxC. Qed. -Lemma maxrr : @idempotent R max. Proof. mexact @maxxx. Qed. -Lemma maxr_l x y : y <= x -> max x y = x. Proof. mexact @max_l. Qed. -Lemma maxr_r x y : x <= y -> max x y = y. Proof. mexact @max_r. Qed. - -Lemma minrA x y z : min x (min y z) = min (min x y) z. -Proof. mexact @minA. Qed. - -Lemma minrCA : @left_commutative R R min. Proof. mexact @minCA. Qed. -Lemma minrAC : @right_commutative R R min. Proof. mexact @minAC. Qed. -Lemma maxrA x y z : max x (max y z) = max (max x y) z. -Proof. mexact @maxA. Qed. - -Lemma maxrCA : @left_commutative R R max. Proof. mexact @maxCA. Qed. -Lemma maxrAC : @right_commutative R R max. Proof. mexact @maxAC. Qed. -Lemma eqr_minl x y : (min x y == x) = (x <= y). Proof. mexact @eq_minl. Qed. -Lemma eqr_minr x y : (min x y == y) = (y <= x). Proof. mexact @eq_minr. Qed. -Lemma eqr_maxl x y : (max x y == x) = (y <= x). Proof. mexact @eq_maxl. Qed. -Lemma eqr_maxr x y : (max x y == y) = (x <= y). Proof. mexact @eq_maxr. Qed. - -Lemma ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z). -Proof. mexact @le_minr. Qed. - -Lemma ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x). -Proof. mexact @le_minl. Qed. - -Lemma ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z). -Proof. mexact @le_maxr. Qed. - -Lemma ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x). -Proof. mexact @le_maxl. Qed. - -Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z). -Proof. mexact @lt_minr. Qed. - -Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x). -Proof. mexact @lt_minl. Qed. - -Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z). -Proof. mexact @lt_maxr. Qed. - -Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x). -Proof. mexact @lt_maxl. Qed. - -Definition lter_minr := (ler_minr, ltr_minr). -Definition lter_minl := (ler_minl, ltr_minl). -Definition lter_maxr := (ler_maxr, ltr_maxr). -Definition lter_maxl := (ler_maxl, ltr_maxl). - -Lemma minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed. -Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; mexact @maxKx. Qed. - -Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed. -Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed. -Lemma minr_maxl : @left_distributive R R min max. Proof. mexact @min_maxl. Qed. -Lemma minr_maxr : @right_distributive R R min max. Proof. mexact @min_maxr. Qed. - -Variant minr_spec x y : bool -> bool -> R -> Type := -| Minr_r of x <= y : minr_spec x y true false x -| Minr_l of y < x : minr_spec x y false true y. -Lemma minrP x y : minr_spec x y (x <= y) (y < x) (min x y). -Proof. by rewrite mrE; case: leP; constructor. Qed. - -Variant maxr_spec x y : bool -> bool -> R -> Type := -| Maxr_r of y <= x : maxr_spec x y true false x -| Maxr_l of x < y : maxr_spec x y false true y. -Lemma maxrP x y : maxr_spec x y (y <= x) (x < y) (max x y). -Proof. by rewrite mrE; case: (leP y); constructor. Qed. - -End MinMax. -End RealDomainOperations. - -Arguments lerifP {R x y C}. -Arguments lerif_refl {R x C}. -Arguments mono_in_lerif [R A f C]. -Arguments nmono_in_lerif [R A f C]. -Arguments mono_lerif [R f C]. -Arguments nmono_lerif [R f C]. - -Section RealDomainArgExtremum. - -Context {R : realDomainType} {I : finType} (i0 : I). -Context (P : pred I) (F : I -> R) (Pi0 : P i0). - -Definition arg_minr := extremum <=%R i0 P F. -Definition arg_maxr := extremum >=%R i0 P F. -Definition arg_minrP : extremum_spec <=%R P F arg_minr := arg_minP F Pi0. -Definition arg_maxrP : extremum_spec >=%R P F arg_maxr := arg_maxP F Pi0. - -End RealDomainArgExtremum. - -Notation "@ 'real_lerP'" := - (deprecate real_lerP real_leP) (at level 10, only parsing) : fun_scope. -Notation real_lerP := (@real_lerP _ _ _) (only parsing). -Notation "@ 'real_ltrP'" := - (deprecate real_ltrP real_ltP) (at level 10, only parsing) : fun_scope. -Notation real_ltrP := (@real_ltrP _ _ _) (only parsing). -Notation "@ 'real_ltrNge'" := - (deprecate real_ltrNge real_ltNge) (at level 10, only parsing) : fun_scope. -Notation real_ltrNge := (@real_ltrNge _ _ _) (only parsing). -Notation "@ 'real_lerNgt'" := - (deprecate real_lerNgt real_leNgt) (at level 10, only parsing) : fun_scope. -Notation real_lerNgt := (@real_lerNgt _ _ _) (only parsing). -Notation "@ 'real_ltrgtP'" := - (deprecate real_ltrgtP real_ltgtP) (at level 10, only parsing) : fun_scope. -Notation real_ltrgtP := (@real_ltrgtP _ _ _) (only parsing). -Notation "@ 'real_ger0P'" := - (deprecate real_ger0P real_ge0P) (at level 10, only parsing) : fun_scope. -Notation real_ger0P := (@real_ger0P _ _) (only parsing). -Notation "@ 'real_ltrgt0P'" := - (deprecate real_ltrgt0P real_ltgt0P) (at level 10, only parsing) : fun_scope. -Notation real_ltrgt0P := (@real_ltrgt0P _ _) (only parsing). -Notation lerif_nat := (deprecate lerif_nat leif_nat_r) (only parsing). -Notation "@ 'lerif_subLR'" := - (deprecate lerif_subLR leif_subLR) (at level 10, only parsing) : fun_scope. -Notation lerif_subLR := (@lerif_subLR _) (only parsing). -Notation "@ 'lerif_subRL'" := - (deprecate lerif_subRL leif_subRL) (at level 10, only parsing) : fun_scope. -Notation lerif_subRL := (@lerif_subRL _) (only parsing). -Notation "@ 'lerif_add'" := - (deprecate lerif_add leif_add) (at level 10, only parsing) : fun_scope. -Notation lerif_add := (@lerif_add _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_sum'" := - (deprecate lerif_sum leif_sum) (at level 10, only parsing) : fun_scope. -Notation lerif_sum := (@lerif_sum _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_0_sum'" := - (deprecate lerif_0_sum leif_0_sum) (at level 10, only parsing) : fun_scope. -Notation lerif_0_sum := (@lerif_0_sum _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_norm'" := - (deprecate real_lerif_norm real_leif_norm) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_norm := (@real_lerif_norm _ _) (only parsing). -Notation "@ 'lerif_pmul'" := - (deprecate lerif_pmul leif_pmul) (at level 10, only parsing) : fun_scope. -Notation lerif_pmul := (@lerif_pmul _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_nmul'" := - (deprecate lerif_nmul leif_nmul) (at level 10, only parsing) : fun_scope. -Notation lerif_nmul := (@lerif_nmul _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_pprod'" := - (deprecate lerif_pprod leif_pprod) (at level 10, only parsing) : fun_scope. -Notation lerif_pprod := (@lerif_pprod _ _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_mean_square_scaled'" := - (deprecate real_lerif_mean_square_scaled real_leif_mean_square_scaled) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_mean_square_scaled := - (@real_lerif_mean_square_scaled _ _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_AGM2_scaled'" := - (deprecate real_lerif_AGM2_scaled real_leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_AGM2_scaled := - (@real_lerif_AGM2_scaled _ _ _) (only parsing). -Notation "@ 'lerif_AGM_scaled'" := - (deprecate lerif_AGM_scaled leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_AGM_scaled := (@lerif_AGM_scaled _ _ _ _) (only parsing). -Notation "@ 'real_lerif_mean_square'" := - (deprecate real_lerif_mean_square real_leif_mean_square) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_mean_square := - (@real_lerif_mean_square _ _ _) (only parsing). -Notation "@ 'real_lerif_AGM2'" := - (deprecate real_lerif_AGM2 real_leif_AGM2) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_AGM2 := (@real_lerif_AGM2 _ _ _) (only parsing). -Notation "@ 'lerif_AGM'" := - (deprecate lerif_AGM leif_AGM) (at level 10, only parsing) : fun_scope. -Notation lerif_AGM := (@lerif_AGM _ _ _ _) (only parsing). -Notation "@ 'lerif_mean_square_scaled'" := - (deprecate lerif_mean_square_scaled leif_mean_square_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_mean_square_scaled := - (@lerif_mean_square_scaled _) (only parsing). -Notation "@ 'lerif_AGM2_scaled'" := - (deprecate lerif_AGM2_scaled leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_AGM2_scaled := (@lerif_AGM2_scaled _) (only parsing). -Notation "@ 'lerif_mean_square'" := - (deprecate lerif_mean_square leif_mean_square) - (at level 10, only parsing) : fun_scope. -Notation lerif_mean_square := (@lerif_mean_square _) (only parsing). -Notation "@ 'lerif_AGM2'" := - (deprecate lerif_AGM2 leif_AGM2) (at level 10, only parsing) : fun_scope. -Notation lerif_AGM2 := (@lerif_AGM2 _) (only parsing). -Notation "@ 'lerif_normC_Re_Creal'" := - (deprecate lerif_normC_Re_Creal leif_normC_Re_Creal) - (at level 10, only parsing) : fun_scope. -Notation lerif_normC_Re_Creal := (@lerif_normC_Re_Creal _) (only parsing). -Notation "@ 'lerif_Re_Creal'" := - (deprecate lerif_Re_Creal leif_Re_Creal) - (at level 10, only parsing) : fun_scope. -Notation lerif_Re_Creal := (@lerif_Re_Creal _) (only parsing). -Notation "@ 'lerif_rootC_AGM'" := - (deprecate lerif_rootC_AGM leif_rootC_AGM) - (at level 10, only parsing) : fun_scope. -Notation lerif_rootC_AGM := (@lerif_rootC_AGM _ _ _ _) (only parsing). - -End Theory. - -Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" := - (arg_minr i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 | P ) F ]") : form_scope. - -Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" := - [arg minr_(i < i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]") : form_scope. - -Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" := - (arg_maxr i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 | P ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" := - [arg maxr_(i > i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 ) F ]") : form_scope. - -End Num. -End mc_1_10. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 76bec6f..7875323 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -2049,6 +2049,5 @@ Qed. End Solver. -Notation "@ 'limg_add'" := - (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope. -Notation limg_add := (@limg_add _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use limgD instead.")] +Notation limg_add := limgD (only parsing). |