diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 443 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 115 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 96 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 43 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 138 |
7 files changed, 697 insertions, 156 deletions
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index e6b0264..b1fa069 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -919,7 +919,7 @@ Proof. by rewrite -(mulr0z x) ler_nmulz2l. Qed. Lemma mulrIz x (hx : x != 0) : injective ( *~%R x). Proof. move=> y z; rewrite -![x *~ _]mulrzr => /(mulfI hx). -by apply: mono_inj y z; apply: ler_pmulz2l. +by apply: incr_inj y z; apply: ler_pmulz2l. Qed. Lemma ler_int m n : (m%:~R <= n%:~R :> R) = (m <= n). @@ -1279,7 +1279,7 @@ Qed. Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) : {in >= 0 &, {mono (exprz x) : x y /~ x <= y}}. Proof. -apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)). +apply: (ler_nmono_in (inj_nhomo_ltr_in _ _)). by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF. by apply: ler_wpiexpz2l; rewrite ?ltrW. Qed. @@ -1291,7 +1291,7 @@ Proof. exact: (lerW_nmono_in (ler_piexpz2l _ _)). Qed. Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) : {in < 0 &, {mono (exprz x) : x y /~ x <= y}}. Proof. -apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)). +apply: (ler_nmono_in (inj_nhomo_ltr_in _ _)). by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF. by apply: ler_wniexpz2l; rewrite ?ltrW. Qed. @@ -1302,7 +1302,7 @@ Proof. exact: (lerW_nmono_in (ler_niexpz2l _ _)). Qed. Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x <= y}. Proof. -apply: (homo_mono (homo_inj_lt _ _)). +apply: (ler_mono (inj_homo_ltr _ _)). by apply: ieexprIz; rewrite ?(ltr_trans ltr01) // gtr_eqF. by apply: ler_weexpz2l; rewrite ?ltrW. Qed. @@ -1348,7 +1348,7 @@ Qed. Lemma ler_pexpz2r n (hn : 0 < n) : {in >= 0 & , {mono ((@exprz R)^~ n) : x y / x <= y}}. Proof. -apply: homo_mono_in (homo_inj_in_lt _ _). +apply: ler_mono_in (inj_homo_ltr_in _ _). by move=> x y hx hy /=; apply: pexpIrz; rewrite // gtr_eqF. by apply: ler_wpexpz2r; rewrite ltrW. Qed. @@ -1360,7 +1360,7 @@ Proof. exact: lerW_mono_in (ler_pexpz2r _). Qed. Lemma ler_nexpz2r n (hn : n < 0) : {in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x <= y}}. Proof. -apply: nhomo_mono_in (nhomo_inj_in_lt _ _); last first. +apply: ler_nmono_in (inj_nhomo_ltr_in _ _); last first. by apply: ler_wnexpz2r; rewrite ltrW. by move=> x y hx hy /=; apply: pexpIrz; rewrite ?[_ \in _]ltrW ?ltr_eqF. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index ec932a1..a16cc45 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -129,6 +129,15 @@ Require Import bigop ssralg finset fingroup zmodp poly. (* e : exterior = in [1, +oo[ or ]1; +oo[ *) (* w : non strict (weak) monotony *) (* *) +(* [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject *) +(* to the condition P (i may appear in P and M), and *) +(* provided P holds for i0. *) +(* [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and *) +(* provided P holds for i0. *) +(* [arg minr_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. *) +(* [arg maxr_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. *) +(* [arg minr_(i < i0) M] == an i : T minimizing M, given i0 : T. *) +(* [arg maxr_(i > i0) M] == an i : T maximizing M, given i0 : T. *) (******************************************************************************) Set Implicit Arguments. @@ -1272,173 +1281,266 @@ Implicit Types m n p : nat. Implicit Types x y z : R. Implicit Types u v w : R'. +(****************************************************************************) +(* This listing of "Let"s factor out the required premices for the *) +(* subsequent lemmas, putting them in the context so that "done" solves the *) +(* goals quickly *) +(****************************************************************************) + +Let leqnn := leqnn. +Let ltnE := ltn_neqAle. +Let ltrE := @ltr_neqAle R. +Let ltr'E := @ltr_neqAle R'. +Let gtnE (m n : nat) : (m > n)%N = (m != n) && (m >= n)%N. +Proof. by rewrite ltn_neqAle eq_sym. Qed. +Let gtrE (x y : R) : (x > y) = (x != y) && (x >= y). +Proof. by rewrite ltr_neqAle eq_sym. Qed. +Let gtr'E (x y : R') : (x > y) = (x != y) && (x >= y). +Proof. by rewrite ltr_neqAle eq_sym. Qed. +Let leq_anti : antisymmetric leq. +Proof. by move=> m n; rewrite -eqn_leq => /eqP. Qed. +Let geq_anti : antisymmetric geq. +Proof. by move=> m n; rewrite -eqn_leq => /eqP. Qed. +Let ler_antiR := @ler_anti R. +Let ler_antiR' := @ler_anti R'. +Let ger_antiR : antisymmetric (>=%R : rel R). +Proof. by move=> ??; rewrite andbC; apply: ler_anti. Qed. +Let ger_antiR' : antisymmetric (>=%R : rel R'). +Proof. by move=> ??; rewrite andbC; apply: ler_anti. Qed. +Let leq_total := leq_total. +Let geq_total : total geq. +Proof. by move=> m n; apply: leq_total. Qed. + Section AcrossTypes. Variable D D' : pred R. Variable (f : R -> R'). Lemma ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}. -Proof. by move=> mf x y /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW]. Qed. +Proof. exact: homoW. Qed. Lemma ltrW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y}. -Proof. by move=> mf x y /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW]. Qed. +Proof. exact: homoW. Qed. -Lemma homo_inj_lt : +Lemma inj_homo_ltr : injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y}. -Proof. -by move=> fI mf x y /= hxy; rewrite ltr_neqAle (inj_eq fI) mf (ltr_eqF, ltrW). -Qed. +Proof. exact: inj_homo. Qed. -Lemma nhomo_inj_lt : +Lemma inj_nhomo_ltr : injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y}. -Proof. -by move=> fI mf x y /= hxy; rewrite ltr_neqAle (inj_eq fI) mf (gtr_eqF, ltrW). -Qed. +Proof. exact: inj_homo. Qed. -Lemma mono_inj : {mono f : x y / x <= y} -> injective f. -Proof. by move=> mf x y /eqP; rewrite eqr_le !mf -eqr_le=> /eqP. Qed. +Lemma incr_inj : {mono f : x y / x <= y} -> injective f. +Proof. exact: mono_inj. Qed. -Lemma nmono_inj : {mono f : x y /~ x <= y} -> injective f. -Proof. by move=> mf x y /eqP; rewrite eqr_le !mf -eqr_le=> /eqP. Qed. +Lemma decr_inj : {mono f : x y /~ x <= y} -> injective f. +Proof. exact: mono_inj. Qed. Lemma lerW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y}. -Proof. -by move=> mf x y /=; rewrite !ltr_neqAle mf inj_eq //; apply: mono_inj. -Qed. +Proof. exact: anti_mono. Qed. Lemma lerW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y}. -Proof. -by move=> mf x y /=; rewrite !ltr_neqAle mf eq_sym inj_eq //; apply: nmono_inj. -Qed. +Proof. exact: anti_mono. Qed. (* Monotony in D D' *) Lemma ltrW_homo_in : {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}}. -Proof. -by move=> mf x y hx hy /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW] //; apply. -Qed. +Proof. exact: homoW_in. Qed. Lemma ltrW_nhomo_in : {in D & D', {homo f : x y /~ x < y}} -> {in D & D', {homo f : x y /~ x <= y}}. -Proof. -by move=> mf x y hx hy /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW] //; apply. -Qed. +Proof. exact: homoW_in. Qed. -Lemma homo_inj_in_lt : +Lemma 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}}. -Proof. -move=> fI mf x y hx hy /= hxy; rewrite ltr_neqAle; apply/andP; split. - by apply: contraTN hxy => /eqP /fI -> //; rewrite ltrr. -by rewrite mf // (ltr_eqF, ltrW). -Qed. +Proof. exact: inj_homo_in. Qed. -Lemma nhomo_inj_in_lt : +Lemma 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}}. -Proof. -move=> fI mf x y hx hy /= hxy; rewrite ltr_neqAle; apply/andP; split. - by apply: contraTN hxy => /eqP /fI -> //; rewrite ltrr. -by rewrite mf // (gtr_eqF, ltrW). -Qed. +Proof. exact: inj_homo_in. Qed. -Lemma mono_inj_in : {in D &, {mono f : x y / x <= y}} -> {in D &, injective f}. -Proof. -by move=> mf x y hx hy /= /eqP; rewrite eqr_le !mf // -eqr_le => /eqP. -Qed. +Lemma incr_inj_in : {in D &, {mono f : x y / x <= y}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. -Lemma nmono_inj_in : +Lemma decr_inj_in : {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f}. -Proof. -by move=> mf x y hx hy /= /eqP; rewrite eqr_le !mf // -eqr_le => /eqP. -Qed. +Proof. exact: mono_inj_in. Qed. Lemma lerW_mono_in : {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}}. -Proof. -move=> mf x y hx hy /=; rewrite !ltr_neqAle mf // (@inj_in_eq _ _ D) //. -exact: mono_inj_in. -Qed. +Proof. exact: anti_mono_in. Qed. Lemma lerW_nmono_in : {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}}. -Proof. -move=> mf x y hx hy /=; rewrite !ltr_neqAle mf // eq_sym (@inj_in_eq _ _ D) //. -exact: nmono_inj_in. -Qed. +Proof. exact: anti_mono_in. Qed. End AcrossTypes. Section NatToR. +Variable D D' : pred nat. Variable (f : nat -> R). -Lemma ltn_ltrW_homo : - {homo f : m n / (m < n)%N >-> m < n} -> +Lemma ltnrW_homo : {homo f : m n / (m < n)%N >-> m < n} -> {homo f : m n / (m <= n)%N >-> m <= n}. -Proof. by move=> mf m n /=; rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW //]. Qed. +Proof. exact: homoW. Qed. -Lemma ltn_ltrW_nhomo : - {homo f : m n / (n < m)%N >-> m < n} -> +Lemma ltnrW_nhomo : {homo f : m n / (n < m)%N >-> m < n} -> {homo f : m n / (n <= m)%N >-> m <= n}. -Proof. by move=> mf m n /=; rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW//]. Qed. +Proof. exact: homoW. Qed. -Lemma homo_inj_ltn_lt : - injective f -> {homo f : m n / (m <= n)%N >-> m <= n} -> +Lemma inj_homo_ltnr : injective f -> + {homo f : m n / (m <= n)%N >-> m <= n} -> {homo f : m n / (m < n)%N >-> m < n}. -Proof. -move=> fI mf m n /= hmn. -by rewrite ltr_neqAle (inj_eq fI) mf ?neq_ltn ?hmn ?orbT // ltnW. -Qed. +Proof. exact: inj_homo. Qed. -Lemma nhomo_inj_ltn_lt : - injective f -> {homo f : m n / (n <= m)%N >-> m <= n} -> +Lemma inj_nhomo_ltnr : injective f -> + {homo f : m n / (n <= m)%N >-> m <= n} -> {homo f : m n / (n < m)%N >-> m < n}. -Proof. -move=> fI mf m n /= hmn; rewrite ltr_def (inj_eq fI). -by rewrite mf ?neq_ltn ?hmn // ltnW. -Qed. +Proof. exact: inj_homo. Qed. -Lemma leq_mono_inj : {mono f : m n / (m <= n)%N >-> m <= n} -> injective f. -Proof. by move=> mf m n /eqP; rewrite eqr_le !mf -eqn_leq => /eqP. Qed. +Lemma incnr_inj : {mono f : m n / (m <= n)%N >-> m <= n} -> injective f. +Proof. exact: mono_inj. Qed. -Lemma leq_nmono_inj : {mono f : m n / (n <= m)%N >-> m <= n} -> injective f. -Proof. by move=> mf m n /eqP; rewrite eqr_le !mf -eqn_leq => /eqP. Qed. +Lemma decnr_inj_inj : {mono f : m n / (n <= m)%N >-> m <= n} -> injective f. +Proof. exact: mono_inj. Qed. -Lemma leq_lerW_mono : - {mono f : m n / (m <= n)%N >-> m <= n} -> +Lemma lenrW_mono : {mono f : m n / (m <= n)%N >-> m <= n} -> {mono f : m n / (m < n)%N >-> m < n}. -Proof. -move=> mf m n /=; rewrite !ltr_neqAle mf inj_eq ?ltn_neqAle 1?eq_sym //. -exact: leq_mono_inj. -Qed. +Proof. exact: anti_mono. Qed. -Lemma leq_lerW_nmono : - {mono f : m n / (n <= m)%N >-> m <= n} -> +Lemma lenrW_nmono : {mono f : m n / (n <= m)%N >-> m <= n} -> {mono f : m n / (n < m)%N >-> m < n}. -Proof. -move=> mf x y /=; rewrite ltr_neqAle mf eq_sym inj_eq ?ltn_neqAle 1?eq_sym //. -exact: leq_nmono_inj. -Qed. +Proof. exact: anti_mono. Qed. -Lemma homo_leq_mono : - {homo f : m n / (m < n)%N >-> m < n} -> +Lemma lenr_mono : {homo f : m n / (m < n)%N >-> m < n} -> {mono f : m n / (m <= n)%N >-> m <= n}. -Proof. -move=> mf m n /=; case: leqP; last by move=> /mf /ltr_geF. -by rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW //]; rewrite lerr. -Qed. +Proof. exact: total_homo_mono. Qed. -Lemma nhomo_leq_mono : - {homo f : m n / (n < m)%N >-> m < n} -> +Lemma lenr_nmono : {homo f : m n / (n < m)%N >-> m < n} -> {mono f : m n / (n <= m)%N >-> m <= n}. -Proof. -move=> mf m n /=; case: leqP; last by move=> /mf /ltr_geF. -by rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW //]; rewrite lerr. -Qed. +Proof. exact: total_homo_mono. Qed. + +Lemma 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}}. +Proof. exact: homoW_in. Qed. + +Lemma 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}}. +Proof. exact: homoW_in. Qed. + +Lemma 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}}. +Proof. exact: inj_homo_in. Qed. + +Lemma 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}}. +Proof. exact: inj_homo_in. Qed. + +Lemma incnr_inj_in : {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma decnr_inj_inj_in : {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma 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}}. +Proof. exact: anti_mono_in. Qed. + +Lemma 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}}. +Proof. exact: anti_mono_in. Qed. + +Lemma 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}}. +Proof. exact: total_homo_mono_in. Qed. + +Lemma 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}}. +Proof. exact: total_homo_mono_in. Qed. End NatToR. +Section RToNat. + +Variable D D' : pred R. +Variable (f : R -> nat). + +Lemma ltrnW_homo : {homo f : m n / m < n >-> (m < n)%N} -> + {homo f : m n / m <= n >-> (m <= n)%N}. +Proof. exact: homoW. Qed. + +Lemma ltrnW_nhomo : {homo f : m n / n < m >-> (m < n)%N} -> + {homo f : m n / n <= m >-> (m <= n)%N}. +Proof. exact: homoW. Qed. + +Lemma inj_homo_ltrn : injective f -> + {homo f : m n / m <= n >-> (m <= n)%N} -> + {homo f : m n / m < n >-> (m < n)%N}. +Proof. exact: inj_homo. Qed. + +Lemma inj_nhomo_ltrn : injective f -> + {homo f : m n / n <= m >-> (m <= n)%N} -> + {homo f : m n / n < m >-> (m < n)%N}. +Proof. exact: inj_homo. Qed. + +Lemma incrn_inj : {mono f : m n / m <= n >-> (m <= n)%N} -> injective f. +Proof. exact: mono_inj. Qed. + +Lemma decrn_inj : {mono f : m n / n <= m >-> (m <= n)%N} -> injective f. +Proof. exact: mono_inj. Qed. + +Lemma lernW_mono : {mono f : m n / m <= n >-> (m <= n)%N} -> + {mono f : m n / m < n >-> (m < n)%N}. +Proof. exact: anti_mono. Qed. + +Lemma lernW_nmono : {mono f : m n / n <= m >-> (m <= n)%N} -> + {mono f : m n / n < m >-> (m < n)%N}. +Proof. exact: anti_mono. Qed. + +Lemma 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}}. +Proof. exact: homoW_in. Qed. + +Lemma 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}}. +Proof. exact: homoW_in. Qed. + +Lemma 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}}. +Proof. exact: inj_homo_in. Qed. + +Lemma 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}}. +Proof. exact: inj_homo_in. Qed. + +Lemma incrn_inj_in : {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma decrn_inj_in : {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma 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}}. +Proof. exact: anti_mono_in. Qed. + +Lemma 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}}. +Proof. exact: anti_mono_in. Qed. + +End RToNat. + End NumIntegralDomainMonotonyTheory. Section NumDomainOperationTheory. @@ -1975,7 +2077,7 @@ Lemma ltr_pmuln2r n : (0 < n)%N -> {mono (@GRing.natmul R)^~ n : x y / x < y}. Proof. by move/ler_pmuln2r/lerW_mono. Qed. Lemma pmulrnI n : (0 < n)%N -> injective ((@GRing.natmul R)^~ n). -Proof. by move/ler_pmuln2r/mono_inj. Qed. +Proof. by move/ler_pmuln2r/incr_inj. Qed. Lemma eqr_pmuln2r n : (0 < n)%N -> {mono (@GRing.natmul R)^~ n : x y / x == y}. Proof. by move/pmulrnI/inj_eq. Qed. @@ -2054,7 +2156,7 @@ Qed. Lemma ltr_pmuln2l x : 0 < x -> {mono (@GRing.natmul R x) : m n / (m < n)%N >-> m < n}. -Proof. by move=> x_gt0; apply: leq_lerW_mono (ler_pmuln2l _). Qed. +Proof. by move=> x_gt0; apply: lenrW_mono (ler_pmuln2l _). Qed. Lemma ler_nmuln2l x : x < 0 -> {mono (@GRing.natmul R x) : m n / (n <= m)%N >-> m <= n}. @@ -2064,7 +2166,7 @@ Qed. Lemma ltr_nmuln2l x : x < 0 -> {mono (@GRing.natmul R x) : m n / (n < m)%N >-> m < n}. -Proof. by move=> x_lt0; apply: leq_lerW_nmono (ler_nmuln2l _). Qed. +Proof. by move=> x_lt0; apply: lenrW_nmono (ler_nmuln2l _). Qed. Lemma ler_nat m n : (m%:R <= n%:R :> R) = (m <= n)%N. Proof. by rewrite ler_pmuln2l. Qed. @@ -2470,28 +2572,28 @@ Qed. Lemma ler_iexpn2l x : 0 < x -> x < 1 -> {mono (GRing.exp x) : m n / (n <= m)%N >-> m <= n}. Proof. -move=> xgt0 xlt1; apply: (nhomo_leq_mono (nhomo_inj_ltn_lt _ _)); last first. +move=> xgt0 xlt1; apply: (lenr_nmono (inj_nhomo_ltnr _ _)); last first. by apply: ler_wiexpn2l; rewrite ltrW. by apply: ieexprIn; rewrite ?ltr_eqF ?ltr_cpable. Qed. Lemma ltr_iexpn2l x : 0 < x -> x < 1 -> {mono (GRing.exp x) : m n / (n < m)%N >-> m < n}. -Proof. by move=> xgt0 xlt1; apply: (leq_lerW_nmono (ler_iexpn2l _ _)). Qed. +Proof. by move=> xgt0 xlt1; apply: (lenrW_nmono (ler_iexpn2l _ _)). Qed. Definition lter_iexpn2l := (ler_iexpn2l, ltr_iexpn2l). Lemma ler_eexpn2l x : 1 < x -> {mono (GRing.exp x) : m n / (m <= n)%N >-> m <= n}. Proof. -move=> xgt1; apply: (homo_leq_mono (homo_inj_ltn_lt _ _)); last first. +move=> xgt1; apply: (lenr_mono (inj_homo_ltnr _ _)); last first. by apply: ler_weexpn2l; rewrite ltrW. by apply: ieexprIn; rewrite ?gtr_eqF ?gtr_cpable //; apply: ltr_trans xgt1. Qed. Lemma ltr_eexpn2l x : 1 < x -> {mono (GRing.exp x) : m n / (m < n)%N >-> m < n}. -Proof. by move=> xgt1; apply: (leq_lerW_mono (ler_eexpn2l _)). Qed. +Proof. by move=> xgt1; apply: (lenrW_mono (ler_eexpn2l _)). Qed. Definition lter_eexpn2l := (ler_eexpn2l, ltr_eexpn2l). @@ -2535,7 +2637,7 @@ Qed. Definition lter_pexpn2r := (ler_pexpn2r, ltr_pexpn2r). Lemma pexpIrn n : (0 < n)%N -> {in nneg &, injective ((@GRing.exp R)^~ n)}. -Proof. by move=> n_gt0; apply: mono_inj_in (ler_pexpn2r _). Qed. +Proof. by move=> n_gt0; apply: incr_inj_in (ler_pexpn2r _). Qed. (* expr and ler/ltr *) Lemma expr_le1 n x : (0 < n)%N -> 0 <= x -> (x ^+ n <= 1) = (x <= 1). @@ -2971,25 +3073,26 @@ Lemma 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)}. Proof. -by move=> mf x y Ax Ay; rewrite /lerif mf ?(inj_in_eq (mono_inj_in mf)). +by move=> mf x y Ax Ay; rewrite /lerif mf ?(inj_in_eq (incr_inj_in mf)). Qed. Lemma 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). -Proof. by move=> mf x y; rewrite /lerif mf (inj_eq (mono_inj _)). Qed. +Proof. by move=> mf x y; rewrite /lerif mf (inj_eq (incr_inj _)). Qed. Lemma 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)}. Proof. -by move=> mf x y Ax Ay; rewrite /lerif eq_sym mf ?(inj_in_eq (nmono_inj_in mf)). +move=> mf x y Ax Ay; rewrite /lerif eq_sym mf //. +by rewrite ?(inj_in_eq (decr_inj_in mf)). Qed. Lemma 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). -Proof. by move=> mf x y; rewrite /lerif eq_sym mf ?(inj_eq (nmono_inj mf)). Qed. +Proof. by move=> mf x y; rewrite /lerif eq_sym mf ?(inj_eq (decr_inj mf)). Qed. Lemma lerif_subLR x y z C : (x - y <= z ?= iff C) = (x <= z + y ?= iff C). Proof. by rewrite /lerif !eqr_le ler_subr_addr ler_subl_addr. Qed. @@ -3158,7 +3261,7 @@ Arguments nmono_lerif [R f C]. Section NumDomainMonotonyTheoryForReals. -Variables (R R' : numDomainType) (D : pred R) (f : R -> R'). +Variables (R R' : numDomainType) (D : pred R) (f : R -> R') (f' : R -> nat). Implicit Types (m n p : nat) (x y z : R) (u v w : R'). Lemma real_mono : @@ -3177,7 +3280,6 @@ move=> mf x y xR yR /=; have [lt_xy|le_yx] := real_ltrP xR yR. by rewrite ltrW_nhomo. Qed. -(* GG: Domain should precede condition. *) Lemma real_mono_in : {in D &, {homo f : x y / x < y}} -> {in [pred x in D | x \is real] &, {mono f : x y / x <= y}}. @@ -3196,6 +3298,38 @@ have [lt_xy|le_yx] := real_ltrP xR yR; last by rewrite (ltrW_nhomo_in Dmf). by rewrite ltr_geF ?Dmf. Qed. +Lemma realn_mono : {homo f' : x y / x < y >-> (x < y)%N} -> + {in real &, {mono f' : x y / x <= y >-> (x <= y)%N}}. +Proof. +move=> mf x y xR yR /=; have [lt_xy | le_yx] := real_lerP xR yR. + by rewrite ltrnW_homo. +by rewrite ltn_geF ?mf. +Qed. + +Lemma realn_nmono : {homo f' : x y / y < x >-> (x < y)%N} -> + {in real &, {mono f' : x y / y <= x >-> (x <= y)%N}}. +Proof. +move=> mf x y xR yR /=; have [lt_xy|le_yx] := real_ltrP xR yR. + by rewrite ltn_geF ?mf. +by rewrite ltrnW_nhomo. +Qed. + +Lemma realn_mono_in : {in D &, {homo f' : x y / x < y >-> (x < y)%N}} -> + {in [pred x in D | x \is real] &, {mono f' : x y / x <= y >-> (x <= y)%N}}. +Proof. +move=> Dmf x y /andP[hx xR] /andP[hy yR] /=. +have [lt_xy|le_yx] := real_lerP xR yR; first by rewrite (ltrnW_homo_in Dmf). +by rewrite ltn_geF ?Dmf. +Qed. + +Lemma realn_nmono_in : {in D &, {homo f' : x y / y < x >-> (x < y)%N}} -> + {in [pred x in D | x \is real] &, {mono f' : x y / y <= x >-> (x <= y)%N}}. +Proof. +move=> Dmf x y /andP[hx xR] /andP[hy yR] /=. +have [lt_xy|le_yx] := real_ltrP xR yR; last by rewrite (ltrnW_nhomo_in Dmf). +by rewrite ltn_geF ?Dmf. +Qed. + End NumDomainMonotonyTheoryForReals. Section FinGroup. @@ -3538,31 +3672,100 @@ Hint Resolve num_real : core. Section RealDomainMonotony. -Variables (R : realDomainType) (R' : numDomainType) (D : pred R) (f : R -> R'). +Variables (R : realDomainType) (R' : numDomainType) (D : pred R). +Variables (f : R -> R') (f' : R -> nat). Implicit Types (m n p : nat) (x y z : R) (u v w : R'). Hint Resolve (@num_real R) : core. -Lemma homo_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}. +Lemma ler_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}. Proof. by move=> mf x y; apply: real_mono. Qed. -Lemma nhomo_mono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y}. +Lemma ler_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y}. Proof. by move=> mf x y; apply: real_nmono. Qed. -Lemma homo_mono_in : +Lemma ler_mono_in : {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}}. Proof. by move=> mf x y Dx Dy; apply: (real_mono_in mf); rewrite ?inE ?Dx ?Dy /=. Qed. -Lemma nhomo_mono_in : +Lemma ler_nmono_in : {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}}. Proof. by move=> mf x y Dx Dy; apply: (real_nmono_in mf); rewrite ?inE ?Dx ?Dy /=. Qed. +Lemma lern_mono : {homo f' : m n / m < n >-> (m < n)%N} -> + {mono f' : m n / m <= n >-> (m <= n)%N}. +Proof. by move=> mf x y; apply: realn_mono. Qed. + +Lemma lern_nmono : {homo f' : m n / n < m >-> (m < n)%N} -> + {mono f' : m n / n <= m >-> (m <= n)%N}. +Proof. by move=> mf x y; apply: realn_nmono. Qed. + +Lemma 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}}. +Proof. +by move=> mf x y Dx Dy; apply: (realn_mono_in mf); rewrite ?inE ?Dx ?Dy /=. +Qed. + +Lemma 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}}. +Proof. +by move=> mf x y Dx Dy; apply: (realn_nmono_in mf); rewrite ?inE ?Dx ?Dy /=. +Qed. + End RealDomainMonotony. +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. + +Lemma arg_minrP: extremum_spec <=%R P F arg_minr. +Proof. by apply: extremumP => //; [apply: ler_trans|apply: ler_total]. Qed. + +Lemma arg_maxrP: extremum_spec >=%R P F arg_maxr. +Proof. +apply: extremumP => //; first exact: lerr. + by move=> ??? /(ler_trans _) le /le. +by move=> ??; apply: ler_total. +Qed. + +End RealDomainArgExtremum. + +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. + Section RealDomainOperations. (* sgr section *) @@ -4107,7 +4310,7 @@ Qed. Lemma ler_psqrt : {in @pos R &, {mono sqrt : a b / a <= b}}. Proof. -apply: homo_mono_in => x y x_gt0 y_gt0. +apply: ler_mono_in => x y x_gt0 y_gt0. rewrite !ltr_neqAle => /andP[neq_xy le_xy]. by rewrite ler_wsqrtr // eqr_sqrt ?ltrW // neq_xy. Qed. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 58ef844..13ba8ca 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -230,12 +230,27 @@ Proof. by move=> imp /eqP; apply: contraTF. Qed. Lemma contra_eqT b x y : (~~ b -> x != y) -> x = y -> b. Proof. by move=> imp /eqP; apply: contraLR. Qed. +Lemma contra_neqN b x y : (b -> x = y) -> x != y -> ~~ b. +Proof. by move=> imp; apply: contraNN => /imp->. Qed. + +Lemma contra_neqF b x y : (b -> x = y) -> x != y -> b = false. +Proof. by move=> imp; apply: contraNF => /imp->. Qed. + +Lemma contra_neqT b x y : (~~ b -> x = y) -> x != y -> b. +Proof. by move=> imp; apply: contraNT => /imp->. Qed. + Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2. Proof. by move=> imp /eqP; apply: contraTeq. Qed. Lemma contra_neq z1 z2 x1 x2 : (x1 = x2 -> z1 = z2) -> z1 != z2 -> x1 != x2. Proof. by move=> imp; apply: contraNneq => /imp->. Qed. +Lemma contra_neq_eq z1 z2 x1 x2 : (x1 != x2 -> z1 = z2) -> z1 != z2 -> x1 = x2. +Proof. by move=> imp; apply: contraNeq => /imp->. Qed. + +Lemma contra_eq_neq z1 z2 x1 x2 : (z1 = z2 -> x1 != x2) -> x1 = x2 -> z1 != z2. +Proof. by move=> imp; apply: contra_eqN => /eqP /imp. Qed. + Lemma memPn A x : reflect {in A, forall y, y != x} (x \notin A). Proof. apply: (iffP idP) => [notDx y | notDx]; first by apply: contraTneq => ->. @@ -882,3 +897,103 @@ End SumEqType. Arguments sum_eq {T1 T2} !u !v. Arguments sum_eqP {T1 T2 x y}. + +Section MonoHomoTheory. + +Variables (aT rT : eqType) (f : aT -> rT). +Variables (aR aR' : rel aT) (rR rR' : rel rT). + +Hypothesis aR_refl : reflexive aR. +Hypothesis rR_refl : reflexive rR. +Hypothesis aR'E : forall x y, aR' x y = (x != y) && (aR x y). +Hypothesis rR'E : forall x y, rR' x y = (x != y) && (rR x y). + +Let aRE x y : aR x y = (x == y) || (aR' x y). +Proof. by rewrite aR'E; case: (altP eqP) => //= ->; apply: aR_refl. Qed. +Let rRE x y : rR x y = (x == y) || (rR' x y). +Proof. by rewrite rR'E; case: (altP eqP) => //= ->; apply: rR_refl. Qed. + +Section InDom. +Variable D : pred aT. + +Section DifferentDom. +Variable D' : pred aT. + +Lemma homoW_in : {in D & D', {homo f : x y / aR' x y >-> rR' x y}} -> + {in D & D', {homo f : x y / aR x y >-> rR x y}}. +Proof. +move=> mf x y xD yD /=; rewrite aRE => /orP[/eqP->|/mf]; +by rewrite rRE ?eqxx // orbC => ->. +Qed. + +Lemma inj_homo_in : {in D & D', injective f} -> + {in D & D', {homo f : x y / aR x y >-> rR x y}} -> + {in D & D', {homo f : x y / aR' x y >-> rR' x y}}. +Proof. +move=> fI mf x y xD yD /=; rewrite aR'E rR'E => /andP[neq_xy xy]. +by rewrite mf ?andbT //; apply: contra_neq neq_xy => /fI; apply. +Qed. + +End DifferentDom. + +Hypothesis aR_anti : antisymmetric aR. +Hypothesis rR_anti : antisymmetric rR. + +Lemma mono_inj_in : {in D &, {mono f : x y / aR x y >-> rR x y}} -> + {in D &, injective f}. +Proof. by move=> mf x y ?? eqf; apply/aR_anti; rewrite -!mf// eqf rR_refl. Qed. + +Lemma anti_mono_in : {in D &, {mono f : x y / aR x y >-> rR x y}} -> + {in D &, {mono f : x y / aR' x y >-> rR' x y}}. +Proof. +move=> mf x y ??; rewrite rR'E aR'E mf// (@inj_in_eq _ _ D)//. +exact: mono_inj_in. +Qed. + +Lemma total_homo_mono_in : total aR -> + {in D &, {homo f : x y / aR' x y >-> rR' x y}} -> + {in D &, {mono f : x y / aR x y >-> rR x y}}. +Proof. +move=> aR_tot mf x y xD yD. +have [->|neq_xy] := altP (x =P y); first by rewrite ?eqxx ?aR_refl ?rR_refl. +have [xy|] := (boolP (aR x y)); first by rewrite rRE mf ?orbT// aR'E neq_xy. +have /orP [->//|] := aR_tot x y. +rewrite aRE eq_sym (negPf neq_xy) /= => /mf -/(_ yD xD). +rewrite rR'E => /andP[Nfxfy fyfx] _; apply: contra_neqF Nfxfy => fxfy. +by apply/rR_anti; rewrite fyfx fxfy. +Qed. + +End InDom. + +Let D := @predT aT. + +Lemma homoW : {homo f : x y / aR' x y >-> rR' x y} -> + {homo f : x y / aR x y >-> rR x y}. +Proof. by move=> mf ???; apply: (@homoW_in D D) => // ????; apply: mf. Qed. + +Lemma inj_homo : injective f -> + {homo f : x y / aR x y >-> rR x y} -> + {homo f : x y / aR' x y >-> rR' x y}. +Proof. +by move=> fI mf ???; apply: (@inj_homo_in D D) => //????; [apply: fI|apply: mf]. +Qed. + +Hypothesis aR_anti : antisymmetric aR. +Hypothesis rR_anti : antisymmetric rR. + +Lemma mono_inj : {mono f : x y / aR x y >-> rR x y} -> injective f. +Proof. by move=> mf x y eqf; apply/aR_anti; rewrite -!mf eqf rR_refl. Qed. + +Lemma anti_mono : {mono f : x y / aR x y >-> rR x y} -> + {mono f : x y / aR' x y >-> rR' x y}. +Proof. by move=> mf x y; rewrite rR'E aR'E mf inj_eq //; apply: mono_inj. Qed. + +Lemma total_homo_mono : total aR -> + {homo f : x y / aR' x y >-> rR' x y} -> + {mono f : x y / aR x y >-> rR x y}. +Proof. +move=> /(@total_homo_mono_in D rR_anti) hmf hf => x y. +by apply: hmf => // ?? _ _; apply: hf. +Qed. + +End MonoHomoTheory. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 06aca24..2544ab6 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2,7 +2,7 @@ (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice. +Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (******************************************************************************) (* The Finite interface describes Types with finitely many elements, *) @@ -133,15 +133,22 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice. (* [pick x | P & Q] := [pick x | P & Q]. *) (* [pick x in A | P & Q] := [pick x | P & Q]. *) (* and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. *) -(* [arg min_(i < i0 | P) M] == a value of i : T minimizing M : nat, subject *) +(* [arg min_(i < i0 | P) M] == a value i : T minimizing M : nat, subject *) (* to the condition P (i may appear in P and M), and *) (* provided P holds for i0. *) -(* [arg max_(i > i0 | P) M] == a value of i maximizing M subject to P and *) +(* [arg max_(i > i0 | P) M] == a value i maximizing M subject to P and *) (* provided P holds for i0. *) (* [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. *) (* [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. *) (* [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T. *) (* [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T. *) +(* These are special instances of *) +(* [arg[ord]_(i < i0 | P) F] == a value i : I, minimizing F wrt ord : rel T *) +(* such that for all j : T, ord (F i) (F j) *) +(* subject to the condition P, and provided P i0 *) +(* where I : finType, T : eqType and F : I -> T *) +(* [arg[ord]_(i < i0 in A) F] == an i \in A minimizing F wrt ord, if i0 \in A.*) +(* [arg[ord]_(i < i0) F] == an i : T minimizing F wrt ord, given i0 : T. *) (******************************************************************************) Set Implicit Arguments. @@ -942,47 +949,76 @@ Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view)) Section Extrema. -Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat). +Variant extremum_spec {T : eqType} (ord : rel T) {I : finType} + (P : pred I) (F : I -> T) : I -> Type := + ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) : + extremum_spec ord P F i. -Let arg_pred ord := [pred i | P i & [forall (j | P j), ord (F i) (F j)]]. +Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) := + [pred i | P i & [forall (j | P j), ord (F i) (F j)]]. -Definition arg_min := odflt i0 (pick (arg_pred leq)). +Section Extremum. -Definition arg_max := odflt i0 (pick (arg_pred geq)). +Context {T : eqType} {I : finType} (ord : rel T). +Context (i0 : I) (P : pred I) (F : I -> T). -Variant extremum_spec (ord : rel nat) : I -> Type := - ExtremumSpec i of P i & (forall j, P j -> ord (F i) (F j)) - : extremum_spec ord i. +Hypothesis ord_refl : reflexive ord. +Hypothesis ord_trans : transitive ord. +Hypothesis ord_total : total ord. -Hypothesis Pi0 : P i0. +Definition extremum := odflt i0 (pick (arg_pred ord P F)). -Let FP n := [exists (i | P i), F i == n]. -Let FP_F i : P i -> FP (F i). -Proof. by move=> Pi; apply/existsP; exists i; rewrite Pi /=. Qed. -Let exFP : exists n, FP n. Proof. by exists (F i0); apply: FP_F. Qed. +Hypothesis Pi0 : P i0. -Lemma arg_minP : extremum_spec leq arg_min. +Lemma extremumP : extremum_spec ord P F extremum. Proof. -rewrite /arg_min; case: pickP => [i /andP[Pi /forallP/= min_i] | no_i]. +rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i]. by split=> // j; apply/implyP. -case/ex_minnP: exFP => n ex_i min_i; case/pred0P: ex_i => i /=. -apply: contraFF (no_i i) => /andP[Pi /eqP def_n]; rewrite /= Pi. -by apply/forall_inP=> j Pj; rewrite def_n min_i ?FP_F. +have := sort_sorted ord_total [seq F i | i <- enum P]. +set s := sort _ _ => ss; have s_gt0 : size s > 0 + by rewrite size_sort size_map -cardE; apply/card_gt0P; exists i0. +pose t0 := nth (F i0) s 0; have: t0 \in s by rewrite mem_nth. +rewrite mem_sort => /mapP/sig2_eqW[it0]; rewrite mem_enum => it0P def_t0. +have /negP[/=] := no_i it0; rewrite [P _]it0P/=; apply/'forall_implyP=> j Pj. +have /(nthP (F i0))[k g_lt <-] : F j \in s by rewrite mem_sort map_f ?mem_enum. +by rewrite -def_t0 sorted_le_nth. Qed. -Lemma arg_maxP : extremum_spec geq arg_max. +End Extremum. + +Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" := + (extremum ord i0 (fun i => P%B) (fun i => F)) + (at level 0, ord, i, i0 at level 10, + format "[ 'arg[' ord ]_( i < i0 | P ) F ]") : form_scope. + +Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" := + [arg[ord]_(i < i0 | i \in A) F] + (at level 0, ord, i, i0 at level 10, + format "[ 'arg[' ord ]_( i < i0 'in' A ) F ]") : form_scope. + +Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg[ord]_(i < i0 | true) F] + (at level 0, ord, i, i0 at level 10, + format "[ 'arg[' ord ]_( i < i0 ) F ]") : form_scope. + +Section ArgMinMax. + +Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat) (Pi0 : P i0). + +Definition arg_min := extremum leq i0 P F. +Definition arg_max := extremum geq i0 P F. + +Lemma arg_minP : extremum_spec leq P F arg_min. +Proof. by apply: extremumP => //; [apply: leq_trans|apply: leq_total]. Qed. + +Lemma arg_maxP : extremum_spec geq P F arg_max. Proof. -rewrite /arg_max; case: pickP => [i /andP[Pi /forall_inP/= max_i] | no_i]. - by split=> // j; apply/implyP. -have (n): FP n -> n <= foldr maxn 0 (map F (enum P)). - case/existsP=> i; rewrite -[P i]mem_enum andbC /= => /andP[/eqP <-]. - elim: (enum P) => //= j e IHe; rewrite leq_max orbC !inE. - by case/predU1P=> [-> | /IHe-> //]; rewrite leqnn orbT. -case/ex_maxnP=> // n ex_i max_i; case/pred0P: ex_i => i /=. -apply: contraFF (no_i i) => /andP[Pi def_n]; rewrite /= Pi. -by apply/forall_inP=> j Pj; rewrite (eqP def_n) max_i ?FP_F. +apply: extremumP => //; first exact: leqnn. + by move=> n m p mn np; apply: leq_trans mn. +by move=> ??; apply: leq_total. Qed. +End ArgMinMax. + End Extrema. Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index dd67256..b6bc4ed 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -890,3 +890,46 @@ End CycleArc. Prenex Implicits arc. +Section Monotonicity. + +Variables (T : eqType) (r : rel T). + +Hypothesis r_trans : transitive r. + +Lemma sorted_lt_nth x0 (s : seq T) : sorted r s -> + {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> r i j}}. +Proof. +move=> s_sorted i j; rewrite -!topredE /=. +wlog ->: i j s s_sorted / i = 0 => [/(_ 0 (j - i) (drop i s)) hw|] ilt jlt ltij. + move: hw; rewrite !size_drop !nth_drop addn0 subnKC ?(ltnW ltij) //. + by rewrite (subseq_sorted _ (drop_subseq _ _)) ?subn_gt0 ?ltn_sub2r//; apply. +case: s ilt j jlt ltij => [|x s] //= _ [//|j] jlt _ in s_sorted *. +by have /allP -> //= := order_path_min r_trans s_sorted; rewrite mem_nth. +Qed. + +Lemma ltn_index (s : seq T) : sorted r s -> + {in s &, forall x y, index x s < index y s -> r x y}. +Proof. +case: s => [//|x0 s'] r_sorted x y xs ys. +move=> /(@sorted_lt_nth x0 (x0 :: s')). +by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. +Qed. + +Hypothesis r_refl : reflexive r. + +Lemma sorted_le_nth x0 (s : seq T) : sorted r s -> + {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> r i j}}. +Proof. +move=> s_sorted x y xs ys. +by rewrite leq_eqVlt=> /orP[/eqP->//|/sorted_lt_nth]; apply. +Qed. + +Lemma leq_index (s : seq T) : sorted r s -> + {in s &, forall x y, index x s <= index y s -> r x y}. +Proof. +case: s => [//|x0 s'] r_sorted x y xs ys. +move=> /(@sorted_le_nth x0 (x0 :: s')). +by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. +Qed. + +End Monotonicity.
\ No newline at end of file diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index a574710..a9cc2ac 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1842,6 +1842,12 @@ Proof. by rewrite -[s1 in subseq s1]cats0 cat_subseq ?sub0seq. Qed. Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2). Proof. exact: cat_subseq (sub0seq s1) _. Qed. +Lemma take_subseq s i : subseq (take i s) s. +Proof. by rewrite -[s in X in subseq _ X](cat_take_drop i) prefix_subseq. Qed. + +Lemma drop_subseq s i : subseq (drop i s) s. +Proof. by rewrite -[s in X in subseq _ X](cat_take_drop i) suffix_subseq. Qed. + Lemma mem_subseq s1 s2 : subseq s1 s2 -> {subset s1 <= s2}. Proof. by case/subseqP=> m _ -> x; apply: mem_mask. Qed. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 581a7ee..c2bd9f7 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -361,6 +361,12 @@ Proof. by rewrite eqn_leq (leqNgt n) => ->. Qed. Lemma ltn_eqF m n : m < n -> m == n = false. Proof. by move/gtn_eqF; rewrite eq_sym. Qed. +Lemma ltn_geF m n : m < n -> m >= n = false. +Proof. by rewrite (leqNgt n) => ->. Qed. + +Lemma leq_gtF m n : m <= n -> m > n = false. +Proof. by rewrite (ltnNge n) => ->. Qed. + Lemma leq_eqVlt m n : (m <= n) = (m == n) || (m < n). Proof. by elim: m n => [|m IHm] []. Qed. @@ -1375,6 +1381,138 @@ rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP. by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: ifP => ->. Qed. +Section Monotonicity. +Variable T : Type. + +Lemma homo_ltn_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) : + (forall y x z, r x y -> r y z -> r x z) -> + {in D &, forall i j k, i < k < j -> k \in D} -> + {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} -> + {in D &, {homo f : i j / i < j >-> r i j}}. +Proof. +move=> r_trans Dcx r_incr i j iD jD lt_ij; move: (lt_ij) (jD) => /subnKC<-. +elim: (_ - _) => [|k ihk]; first by rewrite addn0 => Dsi; apply: r_incr. +move=> DSiSk [: DSik]; apply: (r_trans _ _ _ (ihk _)); rewrite ?addnS. + by abstract: DSik; apply: (Dcx _ _ iD DSiSk); rewrite ltn_addr ?addnS /=. +by apply: r_incr; rewrite -?addnS. +Qed. + +Lemma homo_ltn (f : nat -> T) (r : T -> T -> Prop) : + (forall y x z, r x y -> r y z -> r x z) -> + (forall i, r (f i) (f i.+1)) -> {homo f : i j / i < j >-> r i j}. +Proof. by move=> /(@homo_ltn_in predT f) fr fS i j; apply: fr. Qed. + +Lemma homo_leq_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) : + (forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) -> + {in D &, forall i j k, i < k < j -> k \in D} -> + {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} -> + {in D &, {homo f : i j / i <= j >-> r i j}}. +Proof. +move=> r_refl r_trans Dcx /(homo_ltn_in r_trans Dcx) lt_r i j iD jD. +by rewrite leq_eqVlt => /predU1P[->//|/lt_r]; apply. +Qed. + +Lemma homo_leq (f : nat -> T) (r : T -> T -> Prop) : + (forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) -> + (forall i, r (f i) (f i.+1)) -> {homo f : i j / i <= j >-> r i j}. +Proof. by move=> rrefl /(@homo_leq_in predT f r) fr fS i j; apply: fr. Qed. + +Section NatToNat. +Variable (f : nat -> nat). + +(****************************************************************************) +(* This listing of "Let"s factor out the required premices for the *) +(* subsequent lemmas, putting them in the context so that "done" solves the *) +(* goals quickly *) +(****************************************************************************) + +Let ltn_neqAle := ltn_neqAle. +Let gtn_neqAge x y : (y < x) = (x != y) && (y <= x). +Proof. by rewrite ltn_neqAle eq_sym. Qed. +Let anti_leq := anti_leq. +Let anti_geq : antisymmetric geq. +Proof. by move=> m n /=; rewrite andbC => /anti_leq. Qed. +Let leq_total := leq_total. + +Lemma ltnW_homo : {homo f : m n / m < n} -> {homo f : m n / m <= n}. +Proof. exact: homoW. Qed. + +Lemma homo_inj_lt : injective f -> {homo f : m n / m <= n} -> + {homo f : m n / m < n}. +Proof. exact: inj_homo. Qed. + +Lemma ltnW_nhomo : {homo f : m n /~ m < n} -> {homo f : m n /~ m <= n}. +Proof. exact: homoW. Qed. + +Lemma nhomo_inj_lt : injective f -> {homo f : m n /~ m <= n} -> + {homo f : m n /~ m < n}. +Proof. exact: inj_homo. Qed. + +Lemma incrn_inj : {mono f : m n / m <= n} -> injective f. +Proof. exact: mono_inj. Qed. + +Lemma decrn_inj : {mono f : m n /~ m <= n} -> injective f. +Proof. exact: mono_inj. Qed. + +Lemma leqW_mono : {mono f : m n / m <= n} -> {mono f : m n / m < n}. +Proof. exact: anti_mono. Qed. + +Lemma leqW_nmono : {mono f : m n /~ m <= n} -> {mono f : m n /~ m < n}. +Proof. exact: anti_mono. Qed. + +Lemma leq_mono : {homo f : m n / m < n} -> {mono f : m n / m <= n}. +Proof. exact: total_homo_mono. Qed. + +Lemma leq_nmono : {homo f : m n /~ m < n} -> {mono f : m n /~ m <= n}. +Proof. exact: total_homo_mono. Qed. + +Variable (D D' : pred nat). + +Lemma ltnW_homo_in : {in D & D', {homo f : m n / m < n}} -> + {in D & D', {homo f : m n / m <= n}}. +Proof. exact: homoW_in. Qed. + +Lemma ltnW_nhomo_in : {in D & D', {homo f : m n /~ m < n}} -> + {in D & D', {homo f : m n /~ m <= n}}. +Proof. exact: homoW_in. Qed. + +Lemma homo_inj_lt_in : {in D & D', injective f} -> + {in D & D', {homo f : m n / m <= n}} -> + {in D & D', {homo f : m n / m < n}}. +Proof. exact: inj_homo_in. Qed. + +Lemma nhomo_inj_lt_in : {in D & D', injective f} -> + {in D & D', {homo f : m n /~ m <= n}} -> + {in D & D', {homo f : m n /~ m < n}}. +Proof. exact: inj_homo_in. Qed. + +Lemma incrn_inj_in : {in D &, {mono f : m n / m <= n}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma decrn_inj_in : {in D &, {mono f : m n /~ m <= n}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma leqW_mono_in : {in D &, {mono f : m n / m <= n}} -> + {in D &, {mono f : m n / m < n}}. +Proof. exact: anti_mono_in. Qed. + +Lemma leqW_nmono_in : {in D &, {mono f : m n /~ m <= n}} -> + {in D &, {mono f : m n /~ m < n}}. +Proof. exact: anti_mono_in. Qed. + +Lemma leq_mono_in : {in D &, {homo f : m n / m < n}} -> + {in D &, {mono f : m n / m <= n}}. +Proof. exact: total_homo_mono_in. Qed. + +Lemma leq_nmono_in : {in D &, {homo f : m n /~ m < n}} -> + {in D &, {mono f : m n /~ m <= n}}. +Proof. exact: total_homo_mono_in. Qed. + +End NatToNat. +End Monotonicity. + (* Support for larger integers. The normal definitions of +, - and even *) (* IO are unsuitable for Peano integers larger than 2000 or so because *) (* they are not tail-recursive. We provide a workaround module, along *) |