From d3a545dc55d756cd6e508132551287a62a887bb7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 20 Oct 2022 13:26:59 +0200 Subject: [PATCH] Merge mathcomp_extra.v file from theories into classical --- CHANGELOG_UNRELEASED.md | 35 +- _CoqProject | 1 - classical/mathcomp_extra.v | 578 +++++++++++++++++++++++++++++++- theories/Make | 1 - theories/altreals/distr.v | 4 +- theories/altreals/realseq.v | 4 +- theories/altreals/realsum.v | 4 +- theories/constructive_ereal.v | 3 +- theories/derive.v | 4 +- theories/ereal.v | 7 +- theories/esum.v | 7 +- theories/exp.v | 6 +- theories/landau.v | 5 +- theories/lebesgue_integral.v | 7 +- theories/lebesgue_measure.v | 10 +- theories/mathcomp_extra.v | 599 ---------------------------------- theories/measure.v | 7 +- theories/normedtype.v | 7 +- theories/numfun.v | 5 +- theories/realfun.v | 5 +- theories/reals.v | 2 +- theories/sequences.v | 5 +- theories/set_interval.v | 6 +- theories/signed.v | 2 +- theories/topology.v | 4 +- theories/trigo.v | 6 +- 26 files changed, 627 insertions(+), 697 deletions(-) delete mode 100644 theories/mathcomp_extra.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d4e199274..2590b0bc1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -47,16 +47,8 @@ + notation `\;` for the composition of relations - OPAM package `coq-mathcomp-classical` containing `boolp.v` - file `all_classical.v` -- file `classical/mathcomp_extra.v` -- in file `classical/mathcomp_extra.v`: +- in file `mathcomp_extra.v`: + lemmas `pred_oappE` and `pred_oapp_set` (from `classical_sets.v`) - + definition `olift` (from `mathcomp_extra.v`) - + definition `pred_oapp` (from `mathcomp_extra.v`) - + definition `mul_fun` and notation `f \* g` (from `mathcomp_extra.v`) - + lemmas `all_sig2_cond`, `oapp_comp`, `olift_comp`, `compA`, - `can_in_pcan`, `pcan_in_inj`, `ocan_in_comp`, - `eqbRL` (from `mathcomp_extra.v`) - + definition `opp_fun` and notation `\- f` (from `mathcomp_extra.v`) + lemma `sumr_le0` - in file `fsbigop.v`: + lemmas `fsumr_ge0`, `fsumr_le0`, `fsumr_gt0`, `fsumr_lt0`, `pfsumr_eq0`, @@ -83,13 +75,6 @@ `disjoint_neitv`, `neitv_bnd1`, `neitv_bnd2` (from `set_interval.v`) + lemmas `setNK`, `lb_ubN`, `ub_lbN`, `mem_NE`, `nonemptyN`, `opp_set_eq0`, `has_lb_ubN`, `has_ubPn`, `has_lbPn` (from `reals.v`) -- in file `classical/mathcomp_extra.v`: - + coercion `pair_of_interval` (from `mathcomp_extra.v`) - + definition `miditv` (from `mathcomp_extra.v`) - + lemmas `ltBside`, `leBside`, `ltBRight`, `leBRight`, `bnd_simp`, - `itv_splitU1`, `itv_split1U`, `mem_miditv`, `miditv_le_left`, - `miditv_ge_right`, `predC_itvl`, `predC_itvr`, `predC_itv` - (from `mathcomp_extra.v`) - in `classical_sets.v`: + lemma `bigsetU_sup` - in `lebesgue_integral.v`: @@ -179,6 +164,7 @@ + `homo_le_bigmax` -> `le_bigmax2` - in `sequences.v`: + `seqDUE` -> `seqDU_seqD` +- file `theories/mathcomp_extra.v` moved to `classical/mathcomp_extra.v` ### Deprecated @@ -188,15 +174,7 @@ ### Removed - in file `classical_sets.v`: - + lemmas `pred_oappE` and `pred_oapp_set` (moved to `classical/mathcomp_extra.v`) -- in file `mathcomp_extra.v`: - + definition `olift` (moved to `classical/mathcomp_extra.v`) - + definition `pred_oapp` (moved to `classical/mathcomp_extra.v`) - + definition `mul_fun` and notation `f \* g` (moved to `classical/mathcomp_extra.v`) - + lemmas `all_sig2_cond`, `oapp_comp`, `olift_comp`, `compA`, - `can_in_pcan`, `pcan_in_inj`, `ocan_in_comp`, `eqbRL` (moved to - `classical/mathcomp_extra.v`) - + definition `opp_fun` and notation `\- f` (moved to `classical/mathcomp_extra.v`) + + lemmas `pred_oappE` and `pred_oapp_set` (moved to `mathcomp_extra.v`) - in file `fsbigop.v`: + notation `\sum_(_ \in _) _` (moved to `ereal.v`) + lemma `lee_fsum_nneg_subset`, `lee_fsum`, `ge0_mule_fsumr`, @@ -204,13 +182,6 @@ `fsume_lt0`, `pfsume_eq0` (moved to `ereal.v`) + lemma `pair_fsum` (subsumed by `pair_fsbig`) + lemma `exchange_fsum` (subsumed by `exchange_fsbig`) -- in file `mathcomp_extra.v`: - + coercion `pair_of_interval` (moved to `classical/mathcomp_extra.v`) - + definition `miditv` (moved to `classical/mathcomp_extra.v`) - + lemmas `ltBside`, `leBside`, `ltBRight`, `leBRight`, `bnd_simp`, - `itv_splitU1`, `itv_split1U`, `mem_miditv`, `miditv_le_left`, - `miditv_ge_right`, `predC_itvl`, `predC_itvr`, `predC_itv` - (moved to `classical/mathcomp_extra.v`) - in file `reals.v`: + lemmas `setNK`, `lb_ubN`, `ub_lbN`, `mem_NE`, `nonemptyN`, `opp_set_eq0`, `has_lb_ubN`, `has_ubPn`, `has_lbPn` (moved to `classical/set_interval.v`) diff --git a/_CoqProject b/_CoqProject index 8f89a3ebf..c25b2f788 100644 --- a/_CoqProject +++ b/_CoqProject @@ -15,7 +15,6 @@ classical/functions.v classical/cardinality.v classical/fsbigop.v classical/set_interval.v -theories/mathcomp_extra.v theories/constructive_ereal.v theories/ereal.v theories/reals.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 496f5d3ce..069a01369 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,5 +1,12 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect ssralg ssrnum interval. +From mathcomp Require choice. +(* Missing coercion (done before Import to avoid redeclaration error, + thanks to KS for the trick) *) +(* MathComp 1.15 addition *) +Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of. + +From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. +From mathcomp Require Import finset interval. Require Import boolp classical_sets. (***************************) @@ -9,12 +16,14 @@ Require Import boolp classical_sets. (******************************************************************************) (* This files contains lemmas and definitions missing from MathComp. *) (* *) +(* f \max g := fun x => Num.max (f x) (g x) *) (* oflit f := Some \o f *) (* pred_oapp T D := [pred x | oapp (mem D) false x] *) (* f \* g := fun x => f x * g x *) (* \- f := fun x => - f x *) (* lteBSide, bnd_simp == multirule to simplify inequalities between *) (* interval bounds *) +(* miditv i == middle point of interval i *) (* *) (******************************************************************************) @@ -26,6 +35,8 @@ Reserved Notation "f \* g" (at level 40, left associativity). Reserved Notation "f \- g" (at level 50, left associativity). Reserved Notation "\- f" (at level 35, f at level 35). +Reserved Notation "f \max g" (at level 50, left associativity). + Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I) (P Q : I -> T -> Prop) : T -> (forall x : I, D x -> {y : T | P x y & Q x y}) -> @@ -234,12 +245,573 @@ Qed. End itv_porderType. -Import Num.Theory. - Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I -> R) : (forall i, P i -> F i <= 0)%R -> (\sum_(i <- r | P i) F i <= 0)%R. Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_naddl/F0. Qed. +Lemma enum_ord0 : enum 'I_0 = [::]. +Proof. by apply/eqP; rewrite -size_eq0 size_enum_ord. Qed. + +Lemma enum_ordSr n : enum 'I_n.+1 = + rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max. +Proof. +apply: (inj_map val_inj); rewrite val_enum_ord. +rewrite -[in iota _ _]addn1 iotaD/= cats1 map_rcons; congr (rcons _ _). +by rewrite -map_comp/= (@eq_map _ _ _ val) ?val_enum_ord. +Qed. + +Lemma obindEapp {aT rT} (f : aT -> option rT) : obind f = oapp f None. +Proof. by []. Qed. + +Lemma omapEbind {aT rT} (f : aT -> rT) : omap f = obind (olift f). +Proof. by []. Qed. + +Lemma omapEapp {aT rT} (f : aT -> rT) : omap f = oapp (olift f) None. +Proof. by []. Qed. + +Lemma oappEmap {aT rT} (f : aT -> rT) (y0 : rT) x : + oapp f y0 x = odflt y0 (omap f x). +Proof. by case: x. Qed. + +Lemma omap_comp aT rT sT (f : aT -> rT) (g : rT -> sT) : + omap (g \o f) =1 omap g \o omap f. +Proof. by case. Qed. + +Lemma oapp_comp_f {aT rT sT} (f : aT -> rT) (g : rT -> sT) (x : rT) : + oapp (g \o f) (g x) =1 g \o oapp f x. +Proof. by case. Qed. + +Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) + [f : B -> A] [h : C -> B] + [f' : A -> B] [h' : B -> C] : + {homo h : x / x \in D' >-> x \in D} -> + {in D, cancel f f'} -> {in D', cancel h h'} -> + {in D', cancel (f \o h) (h' \o f')}. +Proof. by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed. + +Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) : + {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} -> + {in Q &, injective (f \o h)}. +Proof. +by move=> Pf Qh QP x y xQ yQ xy; apply Qh => //; apply Pf => //; apply QP. +Qed. + +Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) + [f : B -> A] [h : C -> B] + [f' : A -> option B] [h' : B -> option C] : + {homo h : x / x \in D' >-> x \in D} -> + {in D, pcancel f f'} -> {in D', pcancel h h'} -> + {in D', pcancel (f \o h) (obind h' \o f')}. +Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed. + +Lemma ocan_comp [A B C : Type] [f : B -> option A] [h : C -> option B] + [f' : A -> B] [h' : B -> C] : + ocancel f f' -> ocancel h h' -> ocancel (obind f \o h) (h' \o f'). +Proof. +move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=. +by rewrite -[b in RHS]fK; case: (f b) => //=; have := hK c; rewrite hcE. +Qed. + +Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2. +Proof. by move->. Qed. + +Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x). +Notation "f \max g" := (max_fun f g) : ring_scope. +Arguments max_fun {T R} _ _ _ /. + +Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R. +Proof. by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed. + +Lemma le_le_trans {disp : unit} {T : porderType disp} (x y z t : T) : + (z <= x)%O -> (y <= t)%O -> (x <= y)%O -> (z <= t)%O. +Proof. by move=> + /(le_trans _)/[apply]; apply: le_trans. Qed. + +Notation eqLHS := (X in (X == _))%pattern. +Notation eqRHS := (X in (_ == X))%pattern. +Notation leLHS := (X in (X <= _)%O)%pattern. +Notation leRHS := (X in (_ <= X)%O)%pattern. +Notation ltLHS := (X in (X < _)%O)%pattern. +Notation ltRHS := (X in (_ < X)%O)%pattern. +Inductive boxed T := Box of T. + +Lemma eq_bigl_supp [R : eqType] [idx : R] [op : Monoid.law idx] [I : Type] + [r : seq I] [P1 : pred I] (P2 : pred I) (F : I -> R) : + {in [pred x | F x != idx], P1 =1 P2} -> + \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i. +Proof. +move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _. +by case: (eqVneq (F i) idx) => [->|/P12->]; rewrite ?if_same. +Qed. + +Lemma perm_big_supp_cond [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] + [r s : seq I] [P : pred I] (F : I -> R) : + perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] -> + \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. +Proof. +move=> prs; rewrite !(bigID [pred i | F i == idx] P F)/=. +rewrite big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. +rewrite [in RHS]big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. +by rewrite -[in LHS]big_filter -[in RHS]big_filter; apply perm_big. +Qed. + +Lemma perm_big_supp [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] + [r s : seq I] [P : pred I] (F : I -> R) : + perm_eq [seq i <- r | (F i != idx)] [seq i <- s | (F i != idx)] -> + \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. +Proof. +by move=> ?; apply: perm_big_supp_cond; rewrite !filter_predI perm_filter. +Qed. + +Local Open Scope order_scope. +Local Open Scope ring_scope. +Import GRing.Theory Order.TTheory. + +Lemma mulr_ge0_gt0 (R : numDomainType) (x y : R) : 0 <= x -> 0 <= y -> + (0 < x * y) = (0 < x) && (0 < y). +Proof. +rewrite le_eqVlt => /predU1P[<-|x0]; first by rewrite mul0r ltxx. +rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite mulr0 ltxx andbC. +by apply/idP/andP=> [|_]; rewrite pmulr_rgt0. +Qed. + +Section lt_le_gt_ge. +Variable (R : numFieldType). +Implicit Types x y z a b : R. + +Lemma splitr x : x = x / 2%:R + x / 2%:R. +Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed. + +Lemma ler_addgt0Pr x y : reflect (forall e, e > 0 -> x <= y + e) (x <= y). +Proof. +apply/(iffP idP)=> [lexy e e_gt0 | lexye]; first by rewrite ler_paddr// ltW. +have [||ltyx]// := comparable_leP. + rewrite (@comparabler_trans _ (y + 1))// /Order.comparable ?lexye ?ltr01//. + by rewrite ler_addl ler01 orbT. +have /midf_lt [_] := ltyx; rewrite le_gtF//. +rewrite -(@addrK _ y y) addrAC -addrA 2!mulrDl -splitr lexye//. +by rewrite divr_gt0// ?ltr0n// subr_gt0. +Qed. + +Lemma ler_addgt0Pl x y : reflect (forall e, e > 0 -> x <= e + y) (x <= y). +Proof. +by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC. +Qed. + +Lemma in_segment_addgt0Pr x y z : + reflect (forall e, e > 0 -> y \in `[x - e, z + e]) (y \in `[x, z]). +Proof. +apply/(iffP idP)=> [xyz e /[dup] e_gt0 /ltW e_ge0 | xyz_e]. + by rewrite in_itv /= ler_subl_addr !ler_paddr// (itvP xyz). +by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e; + rewrite in_itv /= ler_subl_addr => /andP []. +Qed. + +Lemma in_segment_addgt0Pl x y z : + reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]). +Proof. +apply/(equivP (in_segment_addgt0Pr x y z)). +by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC. +Qed. + +Lemma lt_le a b : (forall x, x < a -> x < b) -> a <= b. +Proof. +move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -ler_subl_addr ltW//. +by rewrite ab // ltr_subl_addr -ltr_subl_addl subrr. +Qed. + +Lemma gt_ge a b : (forall x, b < x -> a < x) -> a <= b. +Proof. +move=> ab; apply/ler_addgt0Pr => e e_gt0. +by rewrite ltW// ab// -ltr_subl_addl subrr. +Qed. + +End lt_le_gt_ge. + (**********************************) (* End of MathComp 1.15 additions *) (**********************************) + +Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R. +Proof. by rewrite GRing.mulrSr. Qed. + +Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R. +Proof. by rewrite GRing.mulrS. Qed. + +(* To be backported to finmap *) + +Lemma fset_nat_maximum (X : choiceType) (A : {fset X}) + (f : X -> nat) : A != fset0 -> + (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat. +Proof. +move=> /fset0Pn[x Ax]. +have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT. +exists (val y); split; first exact: valP. +by move=> z Az; have := mf [` Az]%fset. +Qed. + +Lemma image_nat_maximum n (f : nat -> nat) : + (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N. +Proof. +have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT. +by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn). +Qed. + +Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : + #|` A| = (\sum_(i <- A) 1)%N. +Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed. + +Arguments big_rmcond {R idx op I r} P. +Arguments big_rmcond_in {R idx op I r} P. + +(*******************************) +(* MathComp > 1.15.0 additions *) +(*******************************) + +Section bigminr_maxr. +Import Num.Def. + +Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I -> R) x : + \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. +Proof. +by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. +Qed. +End bigminr_maxr. + +Section SemiGroupProperties. +Variables (R : Type) (op : R -> R -> R). +Hypothesis opA : associative op. + +Section Id. +Variable x : R. +Hypothesis opxx : op x x = x. + +Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x. +Proof. by elim/big_ind : _ => // _ _ -> ->. Qed. + +Lemma big_id_idem I (r : seq I) P F : + op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i. +Proof. by elim/big_rec : _ => // ? ? ?; rewrite -opA => ->. Qed. + +End Id. + +Section Abelian. +Hypothesis opC : commutative op. + +Let opCA : left_commutative op. Proof. by move=> x *; rewrite !opA (opC x). Qed. + +Variable x : R. + +Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r -> + \big[op/x]_(y <- r | P y) F y = + if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y) + else \big[op/x]_(y <- rem z r | P y) F y. +Proof. +elim: r =>// i r ih; rewrite big_cons rem_cons inE =>/predU1P[-> /[!eqxx]//|zr]. +by case: eqP => [-> //|]; rewrite ih// big_cons; case: ifPn; case: ifPn. +Qed. + +Lemma bigD1_AC (I : finType) j (P : pred I) F : P j -> + \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i). +Proof. +rewrite (big_rem_AC _ _ (mem_index_enum j)) => ->. +by rewrite rem_filter ?index_enum_uniq// big_filter_cond big_andbC. +Qed. + +Section Id. +Hypothesis opxx : op x x = x. + +Lemma big_mkcond_idem I r (P : pred I) F : + \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x). +Proof. +elim: r => [|i r]; rewrite ?(big_nil, big_cons)//. +by case: ifPn => Pi ->//; rewrite -[in LHS]big_id_idem. +Qed. + +Lemma big_split_idem I r (P : pred I) F1 F2 : + \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) = + op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i). +Proof. by elim/big_rec3 : _ => [//|i ? ? _ _ ->]; rewrite // opCA -!opA opCA. Qed. + +Lemma big_id_idem_AC I (r : seq I) P F : + \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i. +Proof. by rewrite big_split_idem big_const_idem ?big_id_idem. Qed. + +Lemma bigID_idem I r (a P : pred I) F : + \big[op/x]_(i <- r | P i) F i = + op (\big[op/x]_(i <- r | P i && a i) F i) + (\big[op/x]_(i <- r | P i && ~~ a i) F i). +Proof. +rewrite -big_id_idem_AC big_mkcond_idem !(big_mkcond_idem _ _ F) -big_split_idem. +by apply: eq_bigr => i; case: ifPn => //=; case: ifPn. +Qed. + +End Id. + +End Abelian. + +End SemiGroupProperties. + +Section bigmaxmin. +Local Notation max := Order.max. +Local Notation min := Order.min. +Local Open Scope order_scope. +Variables (d : _) (T : porderType d). +Variables (I : finType) (f : I -> T) (x0 x : T) (P : pred I). + +Lemma bigmax_le : + x0 <= x -> (forall i, P i -> f i <= x) -> \big[max/x0]_(i | P i) f i <= x. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed. + +Lemma bigmax_lt : + x0 < x -> (forall i, P i -> f i < x) -> \big[max/x0]_(i | P i) f i < x. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxElt; case: ifPn. Qed. + +Lemma lt_bigmin : + x < x0 -> (forall i, P i -> x < f i) -> x < \big[min/x0]_(i | P i) f i. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minElt; case: ifPn. Qed. + +Lemma le_bigmin : + x <= x0 -> (forall i, P i -> x <= f i) -> x <= \big[min/x0]_(i | P i) f i. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed. + +End bigmaxmin. + +Section bigmax. +Local Notation max := Order.max. +Local Open Scope order_scope. +Variables (d : unit) (T : orderType d). + +Section bigmax_Type. +Variables (I : Type) (r : seq I) (x : T). +Implicit Types (P a : pred I) (F : I -> T). + +Lemma bigmax_mkcond P F : \big[max/x]_(i <- r | P i) F i = + \big[max/x]_(i <- r) (if P i then F i else x). +Proof. by rewrite big_mkcond_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. + +Lemma bigmax_split P F1 F2 : + \big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) = + max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i). +Proof. by rewrite big_split_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. + +Lemma bigmax_idl P F : + \big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i). +Proof. by rewrite maxC big_id_idem ?maxxx//; exact: maxA. Qed. + +Lemma bigmax_idr P F : + \big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x. +Proof. by rewrite [LHS]bigmax_idl maxC. Qed. + +Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i = + max (\big[max/x]_(i <- r | P i && a i) F i) + (\big[max/x]_(i <- r | P i && ~~ a i) F i). +Proof. by rewrite (bigID_idem maxA maxC _ _ a) ?maxxx. Qed. + +End bigmax_Type. + +Section bigmax_finType. +Variables (I : finType) (x : T). +Implicit Types (P : pred I) (F : I -> T). + +Lemma bigmaxD1 j P F : P j -> + \big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i). +Proof. by move/(bigD1_AC maxA maxC) ->. Qed. + +Lemma le_bigmax_cond j P F : P j -> F j <= \big[max/x]_(i | P i) F i. +Proof. by move=> Pj; rewrite (bigmaxD1 _ Pj) le_maxr lexx. Qed. + +Lemma le_bigmax F j : F j <= \big[max/x]_i F i. +Proof. exact: le_bigmax_cond. Qed. + +(* NB: as of [2022-08-02], bigop.bigmax_sup already exists for nat *) +Lemma bigmax_sup j P m F : P j -> m <= F j -> m <= \big[max/x]_(i | P i) F i. +Proof. by move=> Pj ?; apply: le_trans (le_bigmax_cond _ Pj). Qed. + +Lemma bigmax_leP m P F : reflect (x <= m /\ forall i, P i -> F i <= m) + (\big[max/x]_(i | P i) F i <= m). +Proof. +apply: (iffP idP) => [|[? ?]]; last exact: bigmax_le. +rewrite bigmax_idl le_maxl => /andP[-> leFm]; split=> // i Pi. +by apply: le_trans leFm; exact: le_bigmax_cond. +Qed. + +Lemma bigmax_ltP m P F : + reflect (x < m /\ forall i, P i -> F i < m) (\big[max/x]_(i | P i) F i < m). +Proof. +apply: (iffP idP) => [|[? ?]]; last exact: bigmax_lt. +rewrite bigmax_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi. +by apply: le_lt_trans ltFm; exact: le_bigmax_cond. +Qed. + +Lemma bigmax_eq_arg j P F : P j -> (forall i, P i -> x <= F i) -> + \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i]. +Proof. +move=> Pi0; case: arg_maxP => //= i Pi PF PxF. +apply/eqP; rewrite eq_le le_bigmax_cond // andbT. +by apply/bigmax_leP; split => //; exact: PxF. +Qed. + +Lemma eq_bigmax j P F : P j -> (forall i, P i -> x <= F i) -> + {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}. +Proof. by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists. Qed. + +Lemma le_bigmax2 P F1 F2 : (forall i, P i -> F1 i <= F2 i) -> + \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i. +Proof. +move=> FG; elim/big_ind2 : _ => // a b e f ba fe. +rewrite le_maxr 2!le_maxl ba fe /= andbT; have [//|/= af] := leP f a. +by rewrite (le_trans ba) // (le_trans _ fe) // ltW. +Qed. + +End bigmax_finType. + +End bigmax. +Arguments bigmax_mkcond {d T I r}. +Arguments bigmaxID {d T I r}. +Arguments bigmaxD1 {d T I x} j. +Arguments bigmax_sup {d T I x} j. +Arguments bigmax_eq_arg {d T I} x j. +Arguments eq_bigmax {d T I x} j. + +Section bigmin. +Local Notation min := Order.min. +Local Open Scope order_scope. +Variables (d : _) (T : orderType d). + +Section bigmin_Type. +Variable (I : Type) (r : seq I) (x : T). +Implicit Types (P a : pred I) (F : I -> T). + +Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i = + \big[min/x]_(i <- r) (if P i then F i else x). +Proof. rewrite big_mkcond_idem ?minxx//; [exact: minA|exact: minC]. Qed. + +Lemma bigmin_split P F1 F2 : + \big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) = + min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i). +Proof. rewrite big_split_idem ?minxx//; [exact: minA|exact: minC]. Qed. + +Lemma bigmin_idl P F : + \big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i). +Proof. rewrite minC big_id_idem ?minxx//; exact: minA. Qed. + +Lemma bigmin_idr P F : + \big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x. +Proof. by rewrite [LHS]bigmin_idl minC. Qed. + +Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i = + min (\big[min/x]_(i <- r | P i && a i) F i) + (\big[min/x]_(i <- r | P i && ~~ a i) F i). +Proof. by rewrite (bigID_idem minA minC _ _ a) ?minxx. Qed. + +End bigmin_Type. + +Section bigmin_finType. +Variable (I : finType) (x : T). +Implicit Types (P : pred I) (F : I -> T). + +Lemma bigminD1 j P F : P j -> + \big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i). +Proof. by move/(bigD1_AC minA minC _ _) ->. Qed. + +Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j. +Proof. +have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih. +rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite le_minl lexx. +by case: ifPn => Pj; [rewrite le_minl leminlfi// orbC|exact: leminlfi]. +Qed. + +Lemma bigmin_le j F : \big[min/x]_i F i <= F j. +Proof. exact: bigmin_le_cond. Qed. + +Lemma bigmin_inf j P m F : P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m. +Proof. by move=> Pj ?; apply: le_trans (bigmin_le_cond _ Pj) _. Qed. + +Lemma bigmin_geP m P F : reflect (m <= x /\ forall i, P i -> m <= F i) + (m <= \big[min/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: le_bigmin]. +- by rewrite (le_trans lemFi)// bigmin_idl le_minl lexx. +- by move=> i Pi; rewrite (le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. +Qed. + +Lemma bigmin_gtP m P F : + reflect (m < x /\ forall i, P i -> m < F i) (m < \big[min/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: lt_bigmin]. +- by rewrite (lt_le_trans lemFi)// bigmin_idl le_minl lexx. +- by move=> i Pi; rewrite (lt_le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. +Qed. + +Lemma bigmin_eq_arg j P F : P j -> (forall i, P i -> F i <= x) -> + \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i]. +Proof. +move=> Pi0; case: arg_minP => //= i Pi PF PFx. +apply/eqP; rewrite eq_le bigmin_le_cond //=. +by apply/bigmin_geP; split => //; exact: PFx. +Qed. + +Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) -> + {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}. +Proof. by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists. Qed. + +End bigmin_finType. + +End bigmin. +Arguments bigmin_mkcond {d T I r}. +Arguments bigminID {d T I r}. +Arguments bigminD1 {d T I x} j. +Arguments bigmin_inf {d T I x} j. +Arguments bigmin_eq_arg {d T I} x j. +Arguments eq_bigmin {d T I x} j. + +Reserved Notation "`1- r" (format "`1- r", at level 2). + +Section onem. +Variable R : numDomainType. +Implicit Types r : R. + +Definition onem r := 1 - r. +Local Notation "`1- r" := (onem r). + +Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed. + +Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed. + +Lemma onemK r : `1-(`1-r) = r. +Proof. by rewrite /onem opprB addrCA subrr addr0. Qed. + +Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed. + +Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r. +Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed. + +Lemma onem_le1 r : 0 <= r -> `1-r <= 1. +Proof. by rewrite ler_subl_addr ler_addl. Qed. + +Lemma onem_lt1 r : 0 < r -> `1-r < 1. +Proof. by rewrite ltr_subl_addr ltr_addl. Qed. + +Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n). +Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed. + +Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1. +Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed. + +Lemma onemD r s : `1-(r + s) = `1-r - s. +Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed. + +Lemma onemMr r s : s * `1-r = s - s * r. +Proof. by rewrite /onem mulrBr mulr1. Qed. + +Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. +Proof. +rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA. +by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK. +Qed. + +End onem. +Notation "`1- r" := (onem r) : ring_scope. + +Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. +Proof. by case: a => //= n _; case: b. Qed. diff --git a/theories/Make b/theories/Make index 1adad3c13..f2cd2861b 100644 --- a/theories/Make +++ b/theories/Make @@ -7,7 +7,6 @@ -arg -w -arg -redundant-canonical-projection -arg -w -arg -projection-no-head-constant -mathcomp_extra.v constructive_ereal.v ereal.v reals.v diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v index e3feae68e..ab093e019 100644 --- a/theories/altreals/distr.v +++ b/theories/altreals/distr.v @@ -5,9 +5,9 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import all_ssreflect all_algebra. -From mathcomp.classical Require Import boolp classical_sets . +From mathcomp.classical Require Import boolp classical_sets mathcomp_extra. Require Import xfinmap ereal reals discrete. -Require Import mathcomp_extra topology realseq realsum. +Require Import topology realseq realsum. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v index 79f343518..8857aedb8 100644 --- a/theories/altreals/realseq.v +++ b/theories/altreals/realseq.v @@ -7,8 +7,8 @@ From mathcomp Require Import all_ssreflect all_algebra. Require Import mathcomp.bigenough.bigenough. From mathcomp.classical Require Import boolp classical_sets functions. -Require Import xfinmap ereal reals discrete. -Require Import mathcomp_extra topology. +From mathcomp.classical Require Import mathcomp_extra. +Require Import xfinmap ereal reals discrete topology. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 4a9f9d851..1804e2769 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -7,8 +7,8 @@ From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. Require Import xfinmap ereal reals discrete realseq. -From mathcomp.classical Require Import classical_sets functions. -Require Import mathcomp_extra topology. +From mathcomp.classical Require Import classical_sets functions mathcomp_extra. +Require Import topology. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 0173e0050..1c81024bf 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -10,7 +10,8 @@ incorporate it into mathcomp proper where it could then be used for bounds of intervals*) From mathcomp Require Import all_ssreflect all_algebra finmap. -Require Import mathcomp_extra signed. +From mathcomp.classical Require Import mathcomp_extra. +Require Import signed. (******************************************************************************) (* Extended real numbers *) diff --git a/theories/derive.v b/theories/derive.v index 1e349da5b..2a6260591 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1,8 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval. From mathcomp.classical Require Import boolp classical_sets functions. -Require Import reals mathcomp_extra signed. -Require Import topology prodnormedzmodule normedtype landau forms. +From mathcomp.classical Require Import mathcomp_extra. +Require Import reals signed topology prodnormedzmodule normedtype landau forms. (******************************************************************************) (* This file provides a theory of differentiation. It includes the standard *) diff --git a/theories/ereal.v b/theories/ereal.v index 8b5353192..a2eb4dd8e 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -6,10 +6,9 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import all_ssreflect all_algebra finmap. -From mathcomp.classical Require Import boolp classical_sets functions. -From mathcomp.classical Require Import cardinality fsbigop set_interval. -Require Import mathcomp_extra reals signed. -Require Import topology. +From mathcomp.classical Require Import boolp classical_sets functions fsbigop. +From mathcomp.classical Require Import cardinality set_interval mathcomp_extra. +Require Import reals signed topology. Require Export constructive_ereal. (******************************************************************************) diff --git a/theories/esum.v b/theories/esum.v index 17e40455f..af8f55508 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1,9 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum finmap. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. -Require Import reals mathcomp_extra ereal signed topology. -Require Import sequences normedtype numfun. +From mathcomp.classical Require Import boolp classical_sets functions. +From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra. +Require Import reals ereal signed topology sequences normedtype numfun. (******************************************************************************) (* Summation over classical sets *) diff --git a/theories/exp.v b/theories/exp.v index d8d252a29..6b0f82728 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -2,9 +2,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp.classical Require Import boolp classical_sets functions. -Require Import mathcomp_extra reals ereal nsatz_realtype. -Require Import signed topology normedtype landau sequences derive. -Require Import realfun. +From mathcomp.classical Require Import mathcomp_extra. +Require Import reals ereal nsatz_realtype. +Require Import signed topology normedtype landau sequences derive realfun. (******************************************************************************) (* Theory of exponential/logarithm functions *) diff --git a/theories/landau.v b/theories/landau.v index f5a3855dc..5224d2703 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -1,9 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum. From mathcomp.classical Require Import boolp classical_sets functions. -Require Import ereal reals mathcomp_extra. -Require Import signed topology normedtype. -Require Import prodnormedzmodule. +From mathcomp.classical Require Import mathcomp_extra. +Require Import ereal reals signed topology normedtype prodnormedzmodule. (******************************************************************************) (* BACHMANN-LANDAU NOTATIONS : BIG AND LITTLE O *) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index d2b6c83a0..dceb70ce6 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. -Require Import mathcomp_extra signed. -Require Import reals ereal topology normedtype sequences esum measure. +From mathcomp.classical Require Import boolp classical_sets functions. +From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra. +Require Import signed reals ereal topology normedtype sequences esum measure. Require Import lebesgue_measure numfun. (******************************************************************************) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index c9cad8815..b7b7fbcc2 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1,13 +1,11 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. -Require Import reals ereal signed topology numfun. -Require Import mathcomp_extra normedtype. +From mathcomp.classical Require Import boolp classical_sets functions. +From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra. +Require Import reals ereal signed topology numfun normedtype. From HB Require Import structures. -Require Import sequences esum measure set_interval. -Require Import realfun. +Require Import sequences esum measure set_interval realfun. (******************************************************************************) (* Lebesgue Measure *) diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v deleted file mode 100644 index d0399b90b..000000000 --- a/theories/mathcomp_extra.v +++ /dev/null @@ -1,599 +0,0 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require choice. -(* Missing coercion (done before Import to avoid redeclaration error, - thanks to KS for the trick) *) -(* MathComp 1.15 addition *) -Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. -From mathcomp Require Import finset interval. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Export mathcomp_extra. - -(***************************) -(* MathComp 1.15 additions *) -(***************************) - -(******************************************************************************) -(* This files contains lemmas and definitions missing from MathComp. *) -(* *) -(* f \max g := fun x => Num.max (f x) (g x) *) -(* lteBSide, bnd_simp == multirule to simplify inequalities between *) -(* interval bounds *) -(* miditv i == middle point of interval i *) -(* *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Reserved Notation "f \max g" (at level 50, left associativity). - -Lemma enum_ord0 : enum 'I_0 = [::]. -Proof. by apply/eqP; rewrite -size_eq0 size_enum_ord. Qed. - -Lemma enum_ordSr n : enum 'I_n.+1 = - rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max. -Proof. -apply: (inj_map val_inj); rewrite val_enum_ord. -rewrite -[in iota _ _]addn1 iotaD/= cats1 map_rcons; congr (rcons _ _). -by rewrite -map_comp/= (@eq_map _ _ _ val) ?val_enum_ord. -Qed. - -Lemma obindEapp {aT rT} (f : aT -> option rT) : obind f = oapp f None. -Proof. by []. Qed. - -Lemma omapEbind {aT rT} (f : aT -> rT) : omap f = obind (olift f). -Proof. by []. Qed. - -Lemma omapEapp {aT rT} (f : aT -> rT) : omap f = oapp (olift f) None. -Proof. by []. Qed. - -Lemma oappEmap {aT rT} (f : aT -> rT) (y0 : rT) x : - oapp f y0 x = odflt y0 (omap f x). -Proof. by case: x. Qed. - -Lemma omap_comp aT rT sT (f : aT -> rT) (g : rT -> sT) : - omap (g \o f) =1 omap g \o omap f. -Proof. by case. Qed. - -Lemma oapp_comp_f {aT rT sT} (f : aT -> rT) (g : rT -> sT) (x : rT) : - oapp (g \o f) (g x) =1 g \o oapp f x. -Proof. by case. Qed. - -Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) - [f : B -> A] [h : C -> B] - [f' : A -> B] [h' : B -> C] : - {homo h : x / x \in D' >-> x \in D} -> - {in D, cancel f f'} -> {in D', cancel h h'} -> - {in D', cancel (f \o h) (h' \o f')}. -Proof. by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed. - -Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) : - {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} -> - {in Q &, injective (f \o h)}. -Proof. -by move=> Pf Qh QP x y xQ yQ xy; apply Qh => //; apply Pf => //; apply QP. -Qed. - -Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) - [f : B -> A] [h : C -> B] - [f' : A -> option B] [h' : B -> option C] : - {homo h : x / x \in D' >-> x \in D} -> - {in D, pcancel f f'} -> {in D', pcancel h h'} -> - {in D', pcancel (f \o h) (obind h' \o f')}. -Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed. - -Lemma ocan_comp [A B C : Type] [f : B -> option A] [h : C -> option B] - [f' : A -> B] [h' : B -> C] : - ocancel f f' -> ocancel h h' -> ocancel (obind f \o h) (h' \o f'). -Proof. -move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=. -by rewrite -[b in RHS]fK; case: (f b) => //=; have := hK c; rewrite hcE. -Qed. - -Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2. -Proof. by move->. Qed. - -Import Order.TTheory GRing.Theory Num.Theory. - -Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x). -Notation "f \max g" := (max_fun f g) : ring_scope. -Arguments max_fun {T R} _ _ _ /. - -Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R. -Proof. by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed. - -Lemma le_le_trans {disp : unit} {T : porderType disp} (x y z t : T) : - (z <= x)%O -> (y <= t)%O -> (x <= y)%O -> (z <= t)%O. -Proof. by move=> + /(le_trans _)/[apply]; apply: le_trans. Qed. - -Notation eqLHS := (X in (X == _))%pattern. -Notation eqRHS := (X in (_ == X))%pattern. -Notation leLHS := (X in (X <= _)%O)%pattern. -Notation leRHS := (X in (_ <= X)%O)%pattern. -Notation ltLHS := (X in (X < _)%O)%pattern. -Notation ltRHS := (X in (_ < X)%O)%pattern. -Inductive boxed T := Box of T. - -Lemma eq_bigl_supp [R : eqType] [idx : R] [op : Monoid.law idx] [I : Type] - [r : seq I] [P1 : pred I] (P2 : pred I) (F : I -> R) : - {in [pred x | F x != idx], P1 =1 P2} -> - \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i. -Proof. -move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _. -by case: (eqVneq (F i) idx) => [->|/P12->]; rewrite ?if_same. -Qed. - -Lemma perm_big_supp_cond [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] - [r s : seq I] [P : pred I] (F : I -> R) : - perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] -> - \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. -Proof. -move=> prs; rewrite !(bigID [pred i | F i == idx] P F)/=. -rewrite big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. -rewrite [in RHS]big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. -by rewrite -[in LHS]big_filter -[in RHS]big_filter; apply perm_big. -Qed. - -Lemma perm_big_supp [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] - [r s : seq I] [P : pred I] (F : I -> R) : - perm_eq [seq i <- r | (F i != idx)] [seq i <- s | (F i != idx)] -> - \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. -Proof. -by move=> ?; apply: perm_big_supp_cond; rewrite !filter_predI perm_filter. -Qed. - -Local Open Scope order_scope. -Local Open Scope ring_scope. -Import GRing.Theory Order.TTheory. - -Lemma mulr_ge0_gt0 (R : numDomainType) (x y : R) : 0 <= x -> 0 <= y -> - (0 < x * y) = (0 < x) && (0 < y). -Proof. -rewrite le_eqVlt => /predU1P[<-|x0]; first by rewrite mul0r ltxx. -rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite mulr0 ltxx andbC. -by apply/idP/andP=> [|_]; rewrite pmulr_rgt0. -Qed. - -Section lt_le_gt_ge. -Variable (R : numFieldType). -Implicit Types x y z a b : R. - -Lemma splitr x : x = x / 2%:R + x / 2%:R. -Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed. - -Lemma ler_addgt0Pr x y : reflect (forall e, e > 0 -> x <= y + e) (x <= y). -Proof. -apply/(iffP idP)=> [lexy e e_gt0 | lexye]; first by rewrite ler_paddr// ltW. -have [||ltyx]// := comparable_leP. - rewrite (@comparabler_trans _ (y + 1))// /Order.comparable ?lexye ?ltr01//. - by rewrite ler_addl ler01 orbT. -have /midf_lt [_] := ltyx; rewrite le_gtF//. -rewrite -(@addrK _ y y) addrAC -addrA 2!mulrDl -splitr lexye//. -by rewrite divr_gt0// ?ltr0n// subr_gt0. -Qed. - -Lemma ler_addgt0Pl x y : reflect (forall e, e > 0 -> x <= e + y) (x <= y). -Proof. -by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC. -Qed. - -Lemma in_segment_addgt0Pr x y z : - reflect (forall e, e > 0 -> y \in `[x - e, z + e]) (y \in `[x, z]). -Proof. -apply/(iffP idP)=> [xyz e /[dup] e_gt0 /ltW e_ge0 | xyz_e]. - by rewrite in_itv /= ler_subl_addr !ler_paddr// (itvP xyz). -by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e; - rewrite in_itv /= ler_subl_addr => /andP []. -Qed. - -Lemma in_segment_addgt0Pl x y z : - reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]). -Proof. -apply/(equivP (in_segment_addgt0Pr x y z)). -by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC. -Qed. - -Lemma lt_le a b : (forall x, x < a -> x < b) -> a <= b. -Proof. -move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -ler_subl_addr ltW//. -by rewrite ab // ltr_subl_addr -ltr_subl_addl subrr. -Qed. - -Lemma gt_ge a b : (forall x, b < x -> a < x) -> a <= b. -Proof. -move=> ab; apply/ler_addgt0Pr => e e_gt0. -by rewrite ltW// ab// -ltr_subl_addl subrr. -Qed. - -End lt_le_gt_ge. - -(**********************************) -(* End of MathComp 1.15 additions *) -(**********************************) - -Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R. -Proof. by rewrite GRing.mulrSr. Qed. - -Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R. -Proof. by rewrite GRing.mulrS. Qed. - -(* To be backported to finmap *) - -Lemma fset_nat_maximum (X : choiceType) (A : {fset X}) - (f : X -> nat) : A != fset0 -> - (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat. -Proof. -move=> /fset0Pn[x Ax]. -have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT. -exists (val y); split; first exact: valP. -by move=> z Az; have := mf [` Az]%fset. -Qed. - -Lemma image_nat_maximum n (f : nat -> nat) : - (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N. -Proof. -have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT. -by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn). -Qed. - -Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : - #|` A| = (\sum_(i <- A) 1)%N. -Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed. - -Arguments big_rmcond {R idx op I r} P. -Arguments big_rmcond_in {R idx op I r} P. - -(*******************************) -(* MathComp > 1.15.0 additions *) -(*******************************) - -Section bigminr_maxr. -Import Num.Def. - -Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I -> R) x : - \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. -Proof. -by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. -Qed. -End bigminr_maxr. - -Section SemiGroupProperties. -Variables (R : Type) (op : R -> R -> R). -Hypothesis opA : associative op. - -Section Id. -Variable x : R. -Hypothesis opxx : op x x = x. - -Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x. -Proof. by elim/big_ind : _ => // _ _ -> ->. Qed. - -Lemma big_id_idem I (r : seq I) P F : - op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i. -Proof. by elim/big_rec : _ => // ? ? ?; rewrite -opA => ->. Qed. - -End Id. - -Section Abelian. -Hypothesis opC : commutative op. - -Let opCA : left_commutative op. Proof. by move=> x *; rewrite !opA (opC x). Qed. - -Variable x : R. - -Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r -> - \big[op/x]_(y <- r | P y) F y = - if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y) - else \big[op/x]_(y <- rem z r | P y) F y. -Proof. -elim: r =>// i r ih; rewrite big_cons rem_cons inE =>/predU1P[-> /[!eqxx]//|zr]. -by case: eqP => [-> //|]; rewrite ih// big_cons; case: ifPn; case: ifPn. -Qed. - -Lemma bigD1_AC (I : finType) j (P : pred I) F : P j -> - \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i). -Proof. -rewrite (big_rem_AC _ _ (mem_index_enum j)) => ->. -by rewrite rem_filter ?index_enum_uniq// big_filter_cond big_andbC. -Qed. - -Section Id. -Hypothesis opxx : op x x = x. - -Lemma big_mkcond_idem I r (P : pred I) F : - \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x). -Proof. -elim: r => [|i r]; rewrite ?(big_nil, big_cons)//. -by case: ifPn => Pi ->//; rewrite -[in LHS]big_id_idem. -Qed. - -Lemma big_split_idem I r (P : pred I) F1 F2 : - \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) = - op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i). -Proof. by elim/big_rec3 : _ => [//|i ? ? _ _ ->]; rewrite // opCA -!opA opCA. Qed. - -Lemma big_id_idem_AC I (r : seq I) P F : - \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i. -Proof. by rewrite big_split_idem big_const_idem ?big_id_idem. Qed. - -Lemma bigID_idem I r (a P : pred I) F : - \big[op/x]_(i <- r | P i) F i = - op (\big[op/x]_(i <- r | P i && a i) F i) - (\big[op/x]_(i <- r | P i && ~~ a i) F i). -Proof. -rewrite -big_id_idem_AC big_mkcond_idem !(big_mkcond_idem _ _ F) -big_split_idem. -by apply: eq_bigr => i; case: ifPn => //=; case: ifPn. -Qed. - -End Id. - -End Abelian. - -End SemiGroupProperties. - -Section bigmaxmin. -Local Notation max := Order.max. -Local Notation min := Order.min. -Local Open Scope order_scope. -Variables (d : _) (T : porderType d). -Variables (I : finType) (f : I -> T) (x0 x : T) (P : pred I). - -Lemma bigmax_le : - x0 <= x -> (forall i, P i -> f i <= x) -> \big[max/x0]_(i | P i) f i <= x. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed. - -Lemma bigmax_lt : - x0 < x -> (forall i, P i -> f i < x) -> \big[max/x0]_(i | P i) f i < x. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxElt; case: ifPn. Qed. - -Lemma lt_bigmin : - x < x0 -> (forall i, P i -> x < f i) -> x < \big[min/x0]_(i | P i) f i. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minElt; case: ifPn. Qed. - -Lemma le_bigmin : - x <= x0 -> (forall i, P i -> x <= f i) -> x <= \big[min/x0]_(i | P i) f i. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed. - -End bigmaxmin. - -Section bigmax. -Local Notation max := Order.max. -Local Open Scope order_scope. -Variables (d : unit) (T : orderType d). - -Section bigmax_Type. -Variables (I : Type) (r : seq I) (x : T). -Implicit Types (P a : pred I) (F : I -> T). - -Lemma bigmax_mkcond P F : \big[max/x]_(i <- r | P i) F i = - \big[max/x]_(i <- r) (if P i then F i else x). -Proof. by rewrite big_mkcond_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. - -Lemma bigmax_split P F1 F2 : - \big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) = - max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i). -Proof. by rewrite big_split_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. - -Lemma bigmax_idl P F : - \big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i). -Proof. by rewrite maxC big_id_idem ?maxxx//; exact: maxA. Qed. - -Lemma bigmax_idr P F : - \big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x. -Proof. by rewrite [LHS]bigmax_idl maxC. Qed. - -Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i = - max (\big[max/x]_(i <- r | P i && a i) F i) - (\big[max/x]_(i <- r | P i && ~~ a i) F i). -Proof. by rewrite (bigID_idem maxA maxC _ _ a) ?maxxx. Qed. - -End bigmax_Type. - -Section bigmax_finType. -Variables (I : finType) (x : T). -Implicit Types (P : pred I) (F : I -> T). - -Lemma bigmaxD1 j P F : P j -> - \big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i). -Proof. by move/(bigD1_AC maxA maxC) ->. Qed. - -Lemma le_bigmax_cond j P F : P j -> F j <= \big[max/x]_(i | P i) F i. -Proof. by move=> Pj; rewrite (bigmaxD1 _ Pj) le_maxr lexx. Qed. - -Lemma le_bigmax F j : F j <= \big[max/x]_i F i. -Proof. exact: le_bigmax_cond. Qed. - -(* NB: as of [2022-08-02], bigop.bigmax_sup already exists for nat *) -Lemma bigmax_sup j P m F : P j -> m <= F j -> m <= \big[max/x]_(i | P i) F i. -Proof. by move=> Pj ?; apply: le_trans (le_bigmax_cond _ Pj). Qed. - -Lemma bigmax_leP m P F : reflect (x <= m /\ forall i, P i -> F i <= m) - (\big[max/x]_(i | P i) F i <= m). -Proof. -apply: (iffP idP) => [|[? ?]]; last exact: bigmax_le. -rewrite bigmax_idl le_maxl => /andP[-> leFm]; split=> // i Pi. -by apply: le_trans leFm; exact: le_bigmax_cond. -Qed. - -Lemma bigmax_ltP m P F : - reflect (x < m /\ forall i, P i -> F i < m) (\big[max/x]_(i | P i) F i < m). -Proof. -apply: (iffP idP) => [|[? ?]]; last exact: bigmax_lt. -rewrite bigmax_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi. -by apply: le_lt_trans ltFm; exact: le_bigmax_cond. -Qed. - -Lemma bigmax_eq_arg j P F : P j -> (forall i, P i -> x <= F i) -> - \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i]. -Proof. -move=> Pi0; case: arg_maxP => //= i Pi PF PxF. -apply/eqP; rewrite eq_le le_bigmax_cond // andbT. -by apply/bigmax_leP; split => //; exact: PxF. -Qed. - -Lemma eq_bigmax j P F : P j -> (forall i, P i -> x <= F i) -> - {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}. -Proof. by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists. Qed. - -Lemma le_bigmax2 P F1 F2 : (forall i, P i -> F1 i <= F2 i) -> - \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i. -Proof. -move=> FG; elim/big_ind2 : _ => // a b e f ba fe. -rewrite le_maxr 2!le_maxl ba fe /= andbT; have [//|/= af] := leP f a. -by rewrite (le_trans ba) // (le_trans _ fe) // ltW. -Qed. - -End bigmax_finType. - -End bigmax. -Arguments bigmax_mkcond {d T I r}. -Arguments bigmaxID {d T I r}. -Arguments bigmaxD1 {d T I x} j. -Arguments bigmax_sup {d T I x} j. -Arguments bigmax_eq_arg {d T I} x j. -Arguments eq_bigmax {d T I x} j. - -Section bigmin. -Local Notation min := Order.min. -Local Open Scope order_scope. -Variables (d : _) (T : orderType d). - -Section bigmin_Type. -Variable (I : Type) (r : seq I) (x : T). -Implicit Types (P a : pred I) (F : I -> T). - -Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i = - \big[min/x]_(i <- r) (if P i then F i else x). -Proof. rewrite big_mkcond_idem ?minxx//; [exact: minA|exact: minC]. Qed. - -Lemma bigmin_split P F1 F2 : - \big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) = - min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i). -Proof. rewrite big_split_idem ?minxx//; [exact: minA|exact: minC]. Qed. - -Lemma bigmin_idl P F : - \big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i). -Proof. rewrite minC big_id_idem ?minxx//; exact: minA. Qed. - -Lemma bigmin_idr P F : - \big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x. -Proof. by rewrite [LHS]bigmin_idl minC. Qed. - -Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i = - min (\big[min/x]_(i <- r | P i && a i) F i) - (\big[min/x]_(i <- r | P i && ~~ a i) F i). -Proof. by rewrite (bigID_idem minA minC _ _ a) ?minxx. Qed. - -End bigmin_Type. - -Section bigmin_finType. -Variable (I : finType) (x : T). -Implicit Types (P : pred I) (F : I -> T). - -Lemma bigminD1 j P F : P j -> - \big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i). -Proof. by move/(bigD1_AC minA minC _ _) ->. Qed. - -Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j. -Proof. -have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih. -rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite le_minl lexx. -by case: ifPn => Pj; [rewrite le_minl leminlfi// orbC|exact: leminlfi]. -Qed. - -Lemma bigmin_le j F : \big[min/x]_i F i <= F j. -Proof. exact: bigmin_le_cond. Qed. - -Lemma bigmin_inf j P m F : P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m. -Proof. by move=> Pj ?; apply: le_trans (bigmin_le_cond _ Pj) _. Qed. - -Lemma bigmin_geP m P F : reflect (m <= x /\ forall i, P i -> m <= F i) - (m <= \big[min/x]_(i | P i) F i). -Proof. -apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: le_bigmin]. -- by rewrite (le_trans lemFi)// bigmin_idl le_minl lexx. -- by move=> i Pi; rewrite (le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. -Qed. - -Lemma bigmin_gtP m P F : - reflect (m < x /\ forall i, P i -> m < F i) (m < \big[min/x]_(i | P i) F i). -Proof. -apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: lt_bigmin]. -- by rewrite (lt_le_trans lemFi)// bigmin_idl le_minl lexx. -- by move=> i Pi; rewrite (lt_le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. -Qed. - -Lemma bigmin_eq_arg j P F : P j -> (forall i, P i -> F i <= x) -> - \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i]. -Proof. -move=> Pi0; case: arg_minP => //= i Pi PF PFx. -apply/eqP; rewrite eq_le bigmin_le_cond //=. -by apply/bigmin_geP; split => //; exact: PFx. -Qed. - -Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) -> - {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}. -Proof. by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists. Qed. - -End bigmin_finType. - -End bigmin. -Arguments bigmin_mkcond {d T I r}. -Arguments bigminID {d T I r}. -Arguments bigminD1 {d T I x} j. -Arguments bigmin_inf {d T I x} j. -Arguments bigmin_eq_arg {d T I} x j. -Arguments eq_bigmin {d T I x} j. - -Reserved Notation "`1- r" (format "`1- r", at level 2). - -Section onem. -Variable R : numDomainType. -Implicit Types r : R. - -Definition onem r := 1 - r. -Local Notation "`1- r" := (onem r). - -Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed. - -Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed. - -Lemma onemK r : `1-(`1-r) = r. -Proof. by rewrite /onem opprB addrCA subrr addr0. Qed. - -Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed. - -Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r. -Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed. - -Lemma onem_le1 r : 0 <= r -> `1-r <= 1. -Proof. by rewrite ler_subl_addr ler_addl. Qed. - -Lemma onem_lt1 r : 0 < r -> `1-r < 1. -Proof. by rewrite ltr_subl_addr ltr_addl. Qed. - -Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n). -Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed. - -Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1. -Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed. - -Lemma onemD r s : `1-(r + s) = `1-r - s. -Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed. - -Lemma onemMr r s : s * `1-r = s - s * r. -Proof. by rewrite /onem mulrBr mulr1. Qed. - -Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. -Proof. -rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA. -by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK. -Qed. - -End onem. -Notation "`1- r" := (onem r) : ring_scope. - -Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. -Proof. by case: a => //= n _; case: b. Qed. diff --git a/theories/measure.v b/theories/measure.v index 3517d3b08..185838658 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1,9 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect all_algebra finmap. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. -Require Import mathcomp_extra reals ereal signed. -Require Import topology normedtype sequences esum numfun. +From mathcomp.classical Require Import boolp classical_sets functions. +From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra. +Require Import reals ereal signed topology normedtype sequences esum numfun. From HB Require Import structures. (******************************************************************************) diff --git a/theories/normedtype.v b/theories/normedtype.v index 8aad8655a..c85112948 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import rat interval zmodp vector fieldext falgebra. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality set_interval. -Require Import mathcomp_extra ereal reals. -Require Import signed topology prodnormedzmodule. +From mathcomp.classical Require Import boolp classical_sets functions. +From mathcomp.classical Require Import cardinality set_interval mathcomp_extra. +Require Import ereal reals signed topology prodnormedzmodule. (******************************************************************************) (* This file extends the topological hierarchy with norm-related notions. *) diff --git a/theories/numfun.v b/theories/numfun.v index 30a5fb7f4..08a62d41a 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -3,9 +3,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg ssrnum ssrint interval finmap. From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality. -Require Import mathcomp_extra signed. -Require Import reals ereal topology normedtype sequences. +From mathcomp.classical Require Import functions cardinality mathcomp_extra. +Require Import signed reals ereal topology normedtype sequences. (******************************************************************************) (* This file provides definitions and lemmas about numerical functions. *) diff --git a/theories/realfun.v b/theories/realfun.v index 372ea5e81..5101aa557 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2,9 +2,8 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions cardinality. -Require Import ereal reals mathcomp_extra. -Require Import signed topology prodnormedzmodule. +From mathcomp.classical Require Import functions cardinality mathcomp_extra. +Require Import ereal reals signed topology prodnormedzmodule. Require Import normedtype derive set_interval. From HB Require Import structures. diff --git a/theories/reals.v b/theories/reals.v index 177cdda74..8e303f499 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -37,7 +37,7 @@ From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp classical_sets set_interval. -Require Import mathcomp_extra. +From mathcomp.classical Require Import mathcomp_extra. Require Import Setoid. diff --git a/theories/sequences.v b/theories/sequences.v index d67d5408b..57ab9dd9d 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2,9 +2,8 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Import functions set_interval. -Require Import reals ereal mathcomp_extra signed. -Require Import topology normedtype landau. +From mathcomp.classical Require Import functions set_interval mathcomp_extra. +Require Import reals ereal signed topology normedtype landau. (******************************************************************************) (* Definitions and lemmas about sequences *) diff --git a/theories/set_interval.v b/theories/set_interval.v index eef1ba78b..4dd5a891b 100644 --- a/theories/set_interval.v +++ b/theories/set_interval.v @@ -2,11 +2,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. From mathcomp.classical Require Import boolp classical_sets functions. -From mathcomp.classical Require Export set_interval. -Require Import reals ereal signed topology. -Require Import mathcomp_extra normedtype. +From mathcomp.classical Require Export set_interval mathcomp_extra. From HB Require Import structures. -Require Import sequences. +Require Import reals ereal signed topology normedtype sequences. (******************************************************************************) (* This files contains lemmas about sets and intervals on reals. *) diff --git a/theories/signed.v b/theories/signed.v index 21a4b93d0..5f8d66d66 100644 --- a/theories/signed.v +++ b/theories/signed.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. -Require Import mathcomp_extra. +From mathcomp.classical Require Import mathcomp_extra. (******************************************************************************) (* This file develops tools to make the manipulation of numbers with a known *) diff --git a/theories/topology.v b/theories/topology.v index 6259a9f25..401ce7aec 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1,8 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect all_algebra finmap. From mathcomp.classical Require Import boolp classical_sets functions. -From mathcomp.classical Require Import cardinality. -Require Import mathcomp_extra reals signed. +From mathcomp.classical Require Import cardinality mathcomp_extra. +Require Import reals signed. (******************************************************************************) (* Filters and basic topological notions *) diff --git a/theories/trigo.v b/theories/trigo.v index 4b5291e21..124eb0a9c 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -2,9 +2,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp.classical Require Import boolp classical_sets functions. -Require Import mathcomp_extra reals ereal nsatz_realtype. -Require Import signed topology normedtype landau sequences derive. -Require Import realfun exp. +From mathcomp.classical Require Import mathcomp_extra. +Require Import reals ereal nsatz_realtype signed topology normedtype landau. +Require Import sequences derive realfun exp. (******************************************************************************) (* Theory of trigonometric functions *)