From e971e696882910179fb963447530580c44e0d090 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 28 Dec 2021 11:52:36 +0900 Subject: [PATCH] changelog v0.3.12 --- CHANGELOG.md | 182 +++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 181 --------------------------------------- INSTALL.md | 2 +- Makefile.common | 7 +- theories/boolp.v | 109 ++++++++++++------------ theories/derive.v | 2 +- 6 files changed, 243 insertions(+), 240 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e39ef430e..5927e80bc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,186 @@ # Changelog -Last releases: [[0.3.10] - 2021-08-11](#0310---2021-08-11) and [[0.3.11] - 2021-11-14](#0311---2021-11-14) +Last releases: [[0.3.11] - 2021-11-14](#0311---2021-11-14) and [[0.3.12] - 2021-12-29](#0312---2021-12-29) + +## [0.3.12] - 2012-12-29 + +### Added + +- in `boolp.v`: + + lemmas `not_True`, `not_False` +- in `classical_sets.v`: + + lemma `setDIr` + + lemmas `setMT`, `setTM`, `setMI` + + lemmas `setSM`, `setM_bigcupr`, `setM_bigcupl` + + lemmas `cover_restr`, `eqcover_r` + + lemma `notin_set` +- in `reals.v`: + + lemma `has_ub_lbN` +- in `ereal.v`: + + lemma `onee_eq0` + + lemma `EFinB` + + lemmas `mule_eq0`, `mule_lt0_lt0`, `mule_gt0_lt0`, `mule_lt0_gt0`, + `pmule_rge0`, `pmule_lge0`, `nmule_lge0`, `nmule_rge0`, + `pmule_rgt0`, `pmule_lgt0`, `nmule_lgt0`, `nmule_rgt0` + + lemmas `muleBr`, `muleBl` + + lemma `eqe_absl` + + lemma `lee_pmul` + + lemmas `fin_numElt`, `fin_numPlt` +- in `topology.v` + + lemmas `cstE`, `compE`, `opprfunE`, `addrfunE`, `mulrfunE`, `scalrfunE`, `exprfunE` + + multi-rule `fctE` + + lemmas `within_interior`, `within_subset,` `withinE`, `fmap_within_eq` + + definitions `subspace`, `incl_subspace`. + + canonical instances of `pointedType`, `filterType`, `topologicalType`, + `uniformType` and `pseudoMetricType` on `subspace`. + + lemmas `nbhs_subspaceP`, `nbhs_subspace_in`, `nbhs_subspace_out`, `subspace_cvgP`, + `subspace_continuousP`, `subspace_eq_continuous`, `nbhs_subspace_interior`, + `nbhs_subspace_ex`, `incl_subspace_continuous`, `open_subspace1out`, + `open_subspace_out`, `open_subspaceT`, `open_subspaceIT`, `open_subspaceTI`, + `closed_subspaceT`, `open_subspaceP`, `open_subspaceW`, `subspace_hausdorff`, + and `compact_subspaceIP`. +- in `normedtype.v` + + lemmas `continuous_shift`, `continuous_withinNshiftx` + + lemmas `bounded_fun_has_ubound`, `bounded_funN`, `bounded_fun_has_lbound`, + `bounded_funD` +- in `derive.v` + + lemmas `derive1_comp`, `derivable_cst`, `derivable_id`, trigger_derive` + + instances `is_derive_id`, `is_derive_Nid` +- in `sequences.v`: + + lemmas `cvg_series_bounded`, `cvg_to_0_linear`, `lim_cvg_to_0_linear`. + + lemma `cvg_sub0` + + lemma `cvg_zero` + + lemmas `ereal_cvg_abs0`, `ereal_cvg_sub0`, `ereal_squeeze` + + lemma `ereal_is_cvgD` +- in `measure.v`: + + hints for `measurable0` and `measurableT` +- file `realfun.v`: + + lemma `is_derive1_caratheodory`, `is_derive_0_is_cst` + + instance `is_derive1_comp` + + lemmas `is_deriveV`, `is_derive_inverse` +- new file `nsatz_realType` +- new file `exp.v` + + lemma `normr_nneg` (hint) + + definitions `pseries`, `pseries_diffs` + + facts `is_cvg_pseries_inside_norm`, `is_cvg_pseries_inside` + + lemmas `pseries_diffsN`, `pseries_diffs_inv_fact`, `pseries_diffs_sumE`, + `pseries_diffs_equiv`, `is_cvg_pseries_diffs_equiv`, + `pseries_snd_diffs` + + lemmas `expR0`, `expR_ge1Dx`, `exp_coeffE`, `expRE` + + instance `is_derive_expR` + + lemmas `derivable_expR`, `continuous_expR`, `expRxDyMexpx`, `expRxMexpNx_1` + + lemmas `pexpR_gt1`, `expR_gt0`, `expRN`, `expRD`, `expRMm` + + lemmas `expR_gt1`, `expR_lt1`, `expRB`, `ltr_expR`, `ler_expR`, `expR_inj`, + `expR_total_gt1`, `expR_total` + + definition `ln` + + fact `ln0` + + lemmas `expK`, `lnK`, `ln1`, `lnM`, `ln_inj`, `lnV`, `ln_div`, `ltr_ln`, `ler_ln`, `lnX` + + lemmas `le_ln1Dx`, `ln_sublinear`, `ln_ge0`, `ln_gt0` + + lemma `continuous_ln` + + instance `is_derive1_ln` + + definition `exp_fun`, notation `` `^ `` + + lemmas `exp_fun_gt0`, `exp_funr1`, `exp_funr0`, `exp_fun1`, `ler_exp_fun`, + `exp_funD`, `exp_fun_inv`, `exp_fun_mulrn` + + definition `riemannR`, lemmas `riemannR_gt0`, `dvg_riemannR` +- new file `trigo.v` + + lemmas `sqrtvR`, `eqr_div`, `big_nat_mul`, `cvg_series_cvg_series_group`, + `lt_sum_lim_series` + + definitions `periodic`, `alternating` + + lemmas `periodicn`, `alternatingn` + + definition `sin_coeff` + + lemmas `sin_coeffE`, `sin_coeff_even`, `is_cvg_series_sin_coeff` + + definition `sin` + + lemmas `sinE` + + definition `sin_coeff'` + + lemmas `sin_coeff'E`, `cvg_sin_coeff'`, `diffs_sin`, `series_sin_coeff0`, `sin0` + + definition `cos_coeff` + + lemmas `cos_ceff_2_0`, `cos_coeff_2_2`, `cos_coeff_2_4`, `cos_coeffE`, `is_cvg_series_cos_coeff` + + definition `cos` + + lemma `cosE` + + definition `cos_coeff'` + + lemmas `cos_coeff'E`, `cvg_cos_coeff'`, `diffs_cos`, `series_cos_coeff0`, `cos0` + + instance `is_derive_sin` + + lemmas `derivable_sin`, `continuous_sin`, `is_derive_cos`, `derivable_cos`, `continuous_cos` + + lemmas `cos2Dsin2`, `cos_max`, `cos_geN1`, `cos_le1`, `sin_max`, `sin_geN1`, `sin_le1` + + fact `sinD_cosD` + + lemmas `sinD`, `cosD` + + lemmas `sin2cos2`, `cos2sin2`, `sin_mulr2n`, `cos_mulr2n` + + fact `sinN_cosN` + + lemmas `sinN`, `cosN` + + lemmas `sin_sg`, `cos_sg`, `cosB`, `sinB` + + lemmas `norm_cos_eq1`, `norm_sin_eq1`, `cos1sin0`, `sin0cos1`, `cos_norm` + + definition `pi` + + lemmas `pihalfE`, `cos2_lt0`, `cos_exists` + + lemmas `sin2_gt0`, `cos_pihalf_uniq`, `pihalf_02_cos_pihalf`, `pihalf_02`, `pi_gt0`, `pi_ge0` + + lemmas `sin_gt0_pihalf`, `cos_gt0_pihalf`, `cos_pihalf`, `sin_pihalf`, `cos_ge0_pihalf`, `cospi`, `sinpi` + + lemmas `cos2pi`, `sin2pi`, `sinDpi`, `cosDpi`, `sinD2pi`, `cosD2pi` + + lemmas `cosDpihalf`, `cosBpihalf`, `sinDpihalf`, `sinBpihalf`, `sin_ge0_pi` + + lemmas `ltr_cos`, `ltr_sin`, `cos_inj`, `sin_inj` + + definition `tan` + + lemmas `tan0`, `tanpi`, `tanN`, `tanD`, `tan_mulr2n`, `cos2_tan2` + + lemmas `tan_pihalf`, `tan_piquarter`, `tanDpi`, `continuous_tan` + + lemmas `is_derive_tan`, `derivable_tan`, `ltr_tan`, `tan_inj` + + definition `acos` + + lemmas `acos_def`, `acos_ge0`, `acos_lepi`, `acosK`, `acos_gt0`, `acos_ltpi` + + lemmas `cosK`, `sin_acos`, `continuous_acos`, `is_derive1_acos` + + definition `asin` + + lemmas `asin_def`, `asin_geNpi2`, `asin_lepi2`, `asinK`, `asin_ltpi2`, `asin_gtNpi2` + + lemmas `sinK`, `cos_asin`, `continuous_asin`, `is_derive1_asin` + + definition `atan` + + lemmas `atan_def`, `atan_gtNpi2`, `atan_ltpi2`, `atanK`, `tanK` + + lemmas `continuous_atan`, `cos_atan` + + instance `is_derive1_atan` + +### Changed + +- in `normedtype.v`: + + `nbhs_minfty_lt` renamed to `nbhs_ninfty_lt_pos` and changed to not use `{posnum R}` + + `nbhs_minfty_le` renamed to `nbhs_ninfty_le_pos` and changed to not use `{posnum R}` +- in `sequences.v`: + + lemma `is_cvg_ereal_nneg_natsum`: remove superfluous `P` parameter + + statements of lemmas `nondecreasing_cvg`, `nondecreasing_is_cvg`, + `nonincreasing_cvg`, `nonincreasing_is_cvg` use `has_{l,u}bound` + predicates instead of requiring an additional variable + + statement of lemma `S1_sup` use `ubound` instead of requiring an + additional variable + +### Renamed + +- in `normedtype.v`: + + `nbhs_minfty_lt_real` -> `nbhs_ninfty_lt` + + `nbhs_minfty_le_real` -> `nbhs_ninfty_le` +- in `sequences.v`: + + `cvgNminfty` -> `cvgNninfty` + + `cvgPminfty` -> `cvgPninfty` + + `ler_cvg_minfty` -> `ler_cvg_ninfty` + + `nondecreasing_seq_ereal_cvg` -> `ereal_nondecreasing_cvg` +- in `normedtype.v`: + + `nbhs_pinfty_gt` -> `nbhs_pinfty_gt_pos` + + `nbhs_pinfty_ge` -> `nbhs_pinfty_ge_pos` + + `nbhs_pinfty_gt_real` -> `nbhs_pinfty_gt` + + `nbhs_pinfty_ge_real` -> `nbhs_pinfty_ge` +- in `measure.v`: + + `measure_bigcup` -> `measure_bigsetU` +- in `ereal.v`: + + `mulrEDr` -> `muleDr` + + `mulrEDl` -> `muleDl` + + `dmulrEDr` -> `dmuleDr` + + `dmulrEDl` -> `dmuleDl` + + `NEFin` -> `EFinN` + + `addEFin` -> `EFinD` + + `mulEFun` -> `EFinM` + + `daddEFin` -> `dEFinD` + + `dsubEFin` -> `dEFinB` + +### Removed + +- in `ereal.v`: + + lemma `subEFin` + +### Infrastructure + +- in `Makefile.common` + + add `doc` and `doc-clean` targets ## [0.3.11] - 2021-11-14 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2377d4f52..c1ee5bdc8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,193 +4,12 @@ ### Added -- in `classical_sets.v`: - + lemma `setDIr` - + lemmas `setMT`, `setTM`, `setMI` - + lemmas `setSM`, `setM_bigcupr`, `setM_bigcupl` -- in `ereal.v`: - + lemma `onee_eq0` - + lemma `EFinB` - + lemmas `mule_eq0`, `mule_lt0_lt0`, `mule_gt0_lt0`, `mule_lt0_gt0`, - `pmule_rge0`, `pmule_lge0`, `nmule_lge0`, `nmule_rge0`, - `pmule_rgt0`, `pmule_lgt0`, `nmule_lgt0`, `nmule_rgt0` -- in `measure.v`: - + hints for `measurable0` and `measurableT` -- in `ereal.v`: - + lemmas `muleBr`, `muleBl` - + lemma `eqe_absl` - + lemma `lee_pmul` - + lemmas `cover_restr`, `eqcover_r` -- in `topology.v` : - + lemmas `cstE`, `compE`, `opprfunE`, `addrfunE`, `mulrfunE`, `scalrfunE`, `exprfunE` - + multi-rule `fctE` -- in `normedtype.v` - + lemmas `continuous_shift`, `continuous_withinNshiftx` -- in `derive.v` - + lemmas `derive1_comp`, `derivable_cst`, `derivable_id`, trigger_derive` - + instances `is_derive_id`, `is_derive_Nid` -- in `sequences.v`: - + lemmas `cvg_series_bounded`, `cvg_to_0_linear`, `lim_cvg_to_0_linear`. - + lemma `cvg_sub0` - + lemma `cvg_zero` -- file `realfun.v`: - + lemma `is_derive1_caratheodory`, `is_derive_0_is_cst` - + instance `is_derive1_comp` - + lemmas `is_deriveV`, `is_derive_inverse` -- new file `nsatz_realType` -- new file `exp.v` - + lemma `normr_nneg` (hint) - + definitions `pseries`, `pseries_diffs` - + facts `is_cvg_pseries_inside_norm`, `is_cvg_pseries_inside` - + lemmas `pseries_diffsN`, `pseries_diffs_inv_fact`, `pseries_diffs_sumE`, - `pseries_diffs_equiv`, `is_cvg_pseries_diffs_equiv`, - `pseries_snd_diffs` - + lemmas `expR0`, `expR_ge1Dx`, `exp_coeffE`, `expRE` - + instance `is_derive_expR` - + lemmas `derivable_expR`, `continuous_expR`, `expRxDyMexpx`, `expRxMexpNx_1` - + lemmas `pexpR_gt1`, `expR_gt0`, `expRN`, `expRD`, `expRMm` - + lemmas `expR_gt1`, `expR_lt1`, `expRB`, `ltr_expR`, `ler_expR`, `expR_inj`, - `expR_total_gt1`, `expR_total` - + definition `ln` - + fact `ln0` - + lemmas `expK`, `lnK`, `ln1`, `lnM`, `ln_inj`, `lnV`, `ln_div`, `ltr_ln`, `ler_ln`, `lnX` - + lemmas `le_ln1Dx`, `ln_sublinear`, `ln_ge0`, `ln_gt0` - + lemma `continuous_ln` - + instance `is_derive1_ln` - + definition `exp_fun`, notation `` `^ `` - + lemmas `exp_fun_gt0`, `exp_funr1`, `exp_funr0`, `exp_fun1`, `ler_exp_fun`, - `exp_funD`, `exp_fun_inv`, `exp_fun_mulrn` - + definition `riemannR`, lemmas `riemannR_gt0`, `dvg_riemannR` -- new file `trigo.v` - + lemmas `sqrtvR`, `eqr_div`, `big_nat_mul`, `cvg_series_cvg_series_group`, - `lt_sum_lim_series` - + definitions `periodic`, `alternating` - + lemmas `periodicn`, `alternatingn` - + definition `sin_coeff` - + lemmas `sin_coeffE`, `sin_coeff_even`, `is_cvg_series_sin_coeff` - + definition `sin` - + lemmas `sinE` - + definition `sin_coeff'` - + lemmas `sin_coeff'E`, `cvg_sin_coeff'`, `diffs_sin`, `series_sin_coeff0`, `sin0` - + definition `cos_coeff` - + lemmas `cos_ceff_2_0`, `cos_coeff_2_2`, `cos_coeff_2_4`, `cos_coeffE`, `is_cvg_series_cos_coeff` - + definition `cos` - + lemma `cosE` - + definition `cos_coeff'` - + lemmas `cos_coeff'E`, `cvg_cos_coeff'`, `diffs_cos`, `series_cos_coeff0`, `cos0` - + instance `is_derive_sin` - + lemmas `derivable_sin`, `continuous_sin`, `is_derive_cos`, `derivable_cos`, `continuous_cos` - + lemmas `cos2Dsin2`, `cos_max`, `cos_geN1`, `cos_le1`, `sin_max`, `sin_geN1`, `sin_le1` - + fact `sinD_cosD` - + lemmas `sinD`, `cosD` - + lemmas `sin2cos2`, `cos2sin2`, `sin_mulr2n`, `cos_mulr2n` - + fact `sinN_cosN` - + lemmas `sinN`, `cosN` - + lemmas `sin_sg`, `cos_sg`, `cosB`, `sinB` - + lemmas `norm_cos_eq1`, `norm_sin_eq1`, `cos1sin0`, `sin0cos1`, `cos_norm` - + definition `pi` - + lemmas `pihalfE`, `cos2_lt0`, `cos_exists` - + lemmas `sin2_gt0`, `cos_pihalf_uniq`, `pihalf_02_cos_pihalf`, `pihalf_02`, `pi_gt0`, `pi_ge0` - + lemmas `sin_gt0_pihalf`, `cos_gt0_pihalf`, `cos_pihalf`, `sin_pihalf`, `cos_ge0_pihalf`, `cospi`, `sinpi` - + lemmas `cos2pi`, `sin2pi`, `sinDpi`, `cosDpi`, `sinD2pi`, `cosD2pi` - + lemmas `cosDpihalf`, `cosBpihalf`, `sinDpihalf`, `sinBpihalf`, `sin_ge0_pi` - + lemmas `ltr_cos`, `ltr_sin`, `cos_inj`, `sin_inj` - + definition `tan` - + lemmas `tan0`, `tanpi`, `tanN`, `tanD`, `tan_mulr2n`, `cos2_tan2` - + lemmas `tan_pihalf`, `tan_piquarter`, `tanDpi`, `continuous_tan` - + lemmas `is_derive_tan`, `derivable_tan`, `ltr_tan`, `tan_inj` - + definition `acos` - + lemmas `acos_def`, `acos_ge0`, `acos_lepi`, `acosK`, `acos_gt0`, `acos_ltpi` - + lemmas `cosK`, `sin_acos`, `continuous_acos`, `is_derive1_acos` - + definition `asin` - + lemmas `asin_def`, `asin_geNpi2`, `asin_lepi2`, `asinK`, `asin_ltpi2`, `asin_gtNpi2` - + lemmas `sinK`, `cos_asin`, `continuous_asin`, `is_derive1_asin` - + definition `atan` - + lemmas `atan_def`, `atan_gtNpi2`, `atan_ltpi2`, `atanK`, `tanK` - + lemmas `continuous_atan`, `cos_atan` - + instance `is_derive1_atan` - + lemmas `fin_numElt`, `fin_numPlt` -- in `sequences.v`: - + `ereal_cvg_abs0`, `ereal_cvg_sub0`, `ereal_squeeze` - ### Changed -- in `normedtype.v`: - + `nbhs_minfty_lt` renamed to `nbhs_ninfty_lt_pos` and changed to not use `{posnum R}` - + `nbhs_minfty_le` renamed to `nbhs_ninfty_le_pos` and changed to not use `{posnum R}` -- in `sequences.v`: - + lemma `is_cvg_ereal_nneg_natsum`: remove superfluous `P` parameter - + lemma `notin_set` -- in `boolp.v`: - + lemmas `not_True`, `not_False` -- in `topology.v` - + lemmas `within_interior`, `within_subset,` `withinE`, `fmap_within_eq` - + definitions `subspace`, `incl_subspace`. - + canonical instances of `pointedType`, `filterType`, `topologicalType`, - `uniformType` and `pseudoMetricType` on `subspace`. - + lemmas `nbhs_subspaceP`, `nbhs_subspace_in`, `nbhs_subspace_out`, `subspace_cvgP`, - `subspace_continuousP`, `subspace_eq_continuous`, `nbhs_subspace_interior`, - `nbhs_subspace_ex`, `incl_subspace_continuous`, `open_subspace1out`, - `open_subspace_out`, `open_subspaceT`, `open_subspaceIT`, `open_subspaceTI`, - `closed_subspaceT`, `open_subspaceP`, `open_subspaceW`, `subspace_hausdorff`, - and `compact_subspaceIP`. - ### Renamed -- in `normedtype.v`: - + `nbhs_minfty_lt_real` -> `nbhs_ninfty_lt` - + `nbhs_minfty_le_real` -> `nbhs_ninfty_le` -- in `sequences.v`: - + `cvgNminfty` -> `cvgNninfty` - + `cvgPminfty` -> `cvgPninfty` - + `ler_cvg_minfty` -> `ler_cvg_ninfty` -- in `normedtype.v`: - + `nbhs_pinfty_gt` -> `nbhs_pinfty_gt_pos` - + `nbhs_pinfty_ge` -> `nbhs_pinfty_ge_pos` - + `nbhs_pinfty_gt_real` -> `nbhs_pinfty_gt` - + `nbhs_pinfty_ge_real` -> `nbhs_pinfty_ge` -- in `measure.v`: - + `measure_bigcup` -> `measure_bigsetU` -- in `ereal.v`: - + `mulrEDr` -> `muleDr` - + `mulrEDl` -> `muleDl` - + `dmulrEDr` -> `dmuleDr` - + `dmulrEDl` -> `dmuleDl` - + `NEFin` -> `EFinN` - + `addEFin` -> `EFinD` - + `mulEFun` -> `EFinM` - + `daddEFin` -> `dEFinD` - + `dsubEFin` -> `dEFinB` -- in `normedtype.v`: - + lemmas `bounded_fun_has_ubound`, `bounded_funN`, `bounded_fun_has_lbound`, - `bounded_funD` -- in `reals.v`: - + lemma `has_ub_lbN` -- in `sequences.v`: - + lemma `ereal_is_cvgD` - -### Changed - -- in `sequences.v`: - + statements of lemmas `nondecreasing_cvg`, `nondecreasing_is_cvg`, - `nonincreasing_cvg`, `nonincreasing_is_cvg` use `has_{l,u}bound` - predicates instead of requiring an additional variable - + statement of lemma `S1_sup` use `ubound` instead of requiring an - additional variable - -### Renamed - -- in `sequences.v`: - + `nondecreasing_seq_ereal_cvg` -> `ereal_nondecreasing_cvg` - ### Removed -- in `ereal.v`: - + lemma `subEFin` - ### Infrastructure -- in `Makefile.common` - + add `doc` and `doc-clean` targets - ### Misc diff --git a/INSTALL.md b/INSTALL.md index f66c54502..e7f2ce490 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.3.11 +$ opam install coq-mathcomp-analysis.0.3.12 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/Makefile.common b/Makefile.common index 9acb5d9f5..b9161da0a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -98,8 +98,11 @@ endif %.vo: __always__ Makefile.coq +$(COQMAKE) $@ -# the doc targets are essentially copied from the Mathematical Components repository -# the location of the math-comp git repository is hard-wired to avoid copying scripts +# the doc targets doc and doc-clean are essentially copied from the Mathematical +# Components repository +# we reuse the scripts from the math-comp git repo (which is hard wired) +# modulo one fix: we change builddoc_lib.sh:l.18 to s/\(\*{5,}+\)//g; + MATHCOMP = ../math-comp/ doc: __always__ Makefile.coq diff --git a/theories/boolp.v b/theories/boolp.v index 61578e554..72a074e40 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -692,81 +692,82 @@ Lemma xchoosebP {T : choiceType} (P : pred T) (h : `[exists x, P x]) : Proof. exact/xchooseP. Qed. (* -------------------------------------------------------------------- *) -(* Notation "'exists_ view" := (existsPP (fun _ => view)) *) -(* (at level 4, right associativity, format "''exists_' view"). *) -(* Notation "'forall_ view" := (forallPP (fun _ => view)) *) -(* (at level 4, right associativity, format "''forall_' view"). *) +(* Notation "'exists_ view" := (existsPP (fun _ => view)) + (at level 4, right associativity, format "''exists_' view"). +Notation "'forall_ view" := (forallPP (fun _ => view)) + (at level 4, right associativity, format "''forall_' view"). -(* Section Quantifiers. *) -(* Variables (T : Type) (rT : T -> eqType). *) -(* Implicit Type (D P : rset T) (f : forall x, rT x). *) +Section Quantifiers. -(* Lemma forallP P : reflect (forall x, P x) [forall x, P x]. *) -(* Proof. *) -(* About forallPP. *) -(* have:= (forallPP (fun x => (asboolP (P x)))). *) -(* exact: 'forall_asboolP. Qed. *) +Variables (T : Type) (rT : T -> eqType). +Implicit Type (D P : rset T) (f : forall x, rT x). -(* Lemma eqfunP f1 f2 : reflect (forall x, f1 x = f2 x) [forall x, f1 x == f2 x]. *) -(* Proof. exact: 'forall_eqP. Qed. *) +Lemma forallP P : reflect (forall x, P x) [forall x, P x]. +Proof. +About forallPP. +have:= (forallPP (fun x => (asboolP (P x)))). +exact: 'forall_asboolP. Qed. + +Lemma eqfunP f1 f2 : reflect (forall x, f1 x = f2 x) [forall x, f1 x == f2 x]. +Proof. exact: 'forall_eqP. Qed. -(* Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x]. *) -(* Proof. exact: 'forall_implyP. Qed. *) +Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x]. +Proof. exact: 'forall_implyP. Qed. -(* Lemma eqfun_inP D f1 f2 : *) -(* reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x]. *) -(* Proof. by apply: (iffP 'forall_implyP) => eq_f12 x Dx; apply/eqP/eq_f12. Qed. *) +Lemma eqfun_inP D f1 f2 : + reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x]. +Proof. by apply: (iffP 'forall_implyP) => eq_f12 x Dx; apply/eqP/eq_f12. Qed. -(* Lemma existsP P : reflect (exists x, P x) [exists x, P x]. *) -(* Proof. exact: 'exists_idP. Qed. *) +Lemma existsP P : reflect (exists x, P x) [exists x, P x]. +Proof. exact: 'exists_idP. Qed. -(* Lemma exists_eqP f1 f2 : *) -(* reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x]. *) +Lemma exists_eqP f1 f2 : + reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x]. -(* Proof. exact: 'exists_eqP. Qed. *) +Proof. exact: 'exists_eqP. Qed. -(* Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x]. *) -(* Proof. by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x. Qed. *) +Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x]. +Proof. by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x. Qed. -(* Lemma exists_eq_inP D f1 f2 : *) -(* reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x]. *) -(* Proof. by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x. Qed. *) +Lemma exists_eq_inP D f1 f2 : + reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x]. +Proof. by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x. Qed. -(* Lemma eq_existsb P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x]. *) -(* Proof. by move=> eqP12; congr (_ != 0); apply: eq_card. Qed. *) +Lemma eq_existsb P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x]. +Proof. by move=> eqP12; congr (_ != 0); apply: eq_card. Qed. -(* Lemma eq_existsb_in D P1 P2 : *) -(* (forall x, D x -> P1 x = P2 x) -> *) -(* [exists (x | D x), P1 x] = [exists (x | D x), P2 x]. *) -(* Proof. by move=> eqP12; apply: eq_existsb => x; apply: andb_id2l => /eqP12. Qed. *) +Lemma eq_existsb_in D P1 P2 : + (forall x, D x -> P1 x = P2 x) -> + [exists (x | D x), P1 x] = [exists (x | D x), P2 x]. +Proof. by move=> eqP12; apply: eq_existsb => x; apply: andb_id2l => /eqP12. Qed. -(* Lemma eq_forallb P1 P2 : P1 =1 P2 -> [forall x, P1 x] = [forall x, P2 x]. *) -(* Proof. by move=> eqP12; apply/negb_inj/eq_existsb=> /= x; rewrite eqP12. Qed. *) +Lemma eq_forallb P1 P2 : P1 =1 P2 -> [forall x, P1 x] = [forall x, P2 x]. +Proof. by move=> eqP12; apply/negb_inj/eq_existsb=> /= x; rewrite eqP12. Qed. -(* Lemma eq_forallb_in D P1 P2 : *) -(* (forall x, D x -> P1 x = P2 x) -> *) -(* [forall (x | D x), P1 x] = [forall (x | D x), P2 x]. *) -(* Proof. *) -(* by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12. *) -(* Qed. *) +Lemma eq_forallb_in D P1 P2 : + (forall x, D x -> P1 x = P2 x) -> + [forall (x | D x), P1 x] = [forall (x | D x), P2 x]. +Proof. +by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12. +Qed. -(* Lemma negb_forall P : ~~ [forall x, P x] = [exists x, ~~ P x]. *) -(* Proof. by []. Qed. *) +Lemma negb_forall P : ~~ [forall x, P x] = [exists x, ~~ P x]. +Proof. by []. Qed. -(* Lemma negb_forall_in D P : *) -(* ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x]. *) -(* Proof. by apply: eq_existsb => x; rewrite negb_imply. Qed. *) +Lemma negb_forall_in D P : + ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x]. +Proof. by apply: eq_existsb => x; rewrite negb_imply. Qed. -(* Lemma negb_exists P : ~~ [exists x, P x] = [forall x, ~~ P x]. *) -(* Proof. by apply/negbLR/esym/eq_existsb=> x; apply: negbK. Qed. *) +Lemma negb_exists P : ~~ [exists x, P x] = [forall x, ~~ P x]. +Proof. by apply/negbLR/esym/eq_existsb=> x; apply: negbK. Qed. -(* Lemma negb_exists_in D P : *) -(* ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x]. *) -(* Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed. *) +Lemma negb_exists_in D P : + ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x]. +Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed. -(* End Quantifiers. *) +End Quantifiers. *) (* -------------------------------------------------------------------- *) (* FIXME: to be moved *) diff --git a/theories/derive.v b/theories/derive.v index 3a3f5e35e..427729f2a 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -8,7 +8,7 @@ Require Import normedtype landau forms. (******************************************************************************) (* This file provides a theory of differentiation. It includes the standard *) (* rules of differentiation (differential of a sum, of a product, of *) -(* exponentiation, of the inverse, etc.) as well standard theorems (the *) +(* exponentiation, of the inverse, etc.) as well as standard theorems (the *) (* Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem). *) (* *) (* Parsable notations (in all of the following, f is not supposed to be *)