diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 46 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 11 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 494 |
6 files changed, 298 insertions, 265 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index f7b2e0f..3bae08e 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -84,8 +84,7 @@ From mathcomp Require Import ssralg poly. (* and ><) and lattice operations (meet and join) defined in order.v are *) (* redefined for the ring_display in the ring_scope (%R). 0-ary ordering *) (* symbols for the ring_display have the suffix "%R", e.g., <%R. All the *) -(* other ordering notations are the same as order.v. The meet and join *) -(* operators for the ring_display are Num.min and Num.max. *) +(* other ordering notations are the same as order.v. *) (* *) (* Over these structures, we have the following operations *) (* `|x| == norm of x. *) @@ -2877,6 +2876,24 @@ Proof. by move=> x_real; rewrite -[LHS]opprK real_oppr_min ?opprK ?real_maxrN ?realN. Qed. +Section RealDomainArgExtremum. + +Context {I : finType} (i0 : I). +Context (P : pred I) (F : I -> R) (Pi0 : P i0). +Hypothesis F_real : {in P, forall i, F i \is real}. + +Lemma real_arg_minP : extremum_spec <=%R P F [arg min_(i < i0 | P i) F i]. +Proof. +by apply: comparable_arg_minP => // i j iP jP; rewrite real_comparable ?F_real. +Qed. + +Lemma real_arg_maxP : extremum_spec >=%R P F [arg max_(i > i0 | P i) F i]. +Proof. +by apply: comparable_arg_maxP => // i j iP jP; rewrite real_comparable ?F_real. +Qed. + +End RealDomainArgExtremum. + (* norm *) Lemma real_ler_norm x : x \is real -> x <= `|x|. @@ -3981,7 +3998,7 @@ Section MinMax. Lemma oppr_max : {morph -%R : x y / max x y >-> min x y : R}. Proof. by move=> x y; apply: real_oppr_max. Qed. -Lemma oppr_min : {in real &, {morph -%R : x y / min x y >-> max x y : R}}. +Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}. Proof. by move=> x y; apply: real_oppr_min. Qed. Lemma addr_minl : @left_distributive R R +%R min. @@ -5239,7 +5256,15 @@ Module Num. (* revert them in order to compile and commit. This problem will be solved *) (* in Coq 8.10. See also: https://github.com/math-comp/math-comp/pull/270. *) Export ssrnum.Num. -Import ssrnum.Num.Def. + +Module Import Def. +Export ssrnum.Num.Def. +Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y. +Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x. +End Def. + +Notation min := minr. +Notation max := maxr. Module Import Syntax. Notation "`| x |" := @@ -5294,11 +5319,7 @@ Definition normr_lt0 x : `|x| < 0 = false := normr_lt0 x. Definition normr_gt0 x : (`|x| > 0) = (x != 0) := normr_gt0 x. Definition normrE := (normr_id, normr0, @normr1 R, @normrN1 R, normr_ge0, normr_eq0, normr_lt0, normr_le0, normr_gt0, normrN). -Definition minr x y := if x <= y then x else y. -Definition maxr x y := if x <= y then y else x. End NumIntegralDomainTheory. -Arguments minr {_}. -Arguments maxr {_}. Section NumIntegralDomainMonotonyTheory. Variables R R' : numDomainType. @@ -5611,14 +5632,11 @@ Variable R : realDomainType. Implicit Types x y z : R. Section MinMax. -Let mrE x y : ((minr x y = min x y) * (maxr x y = max x y))%type. +Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.max x y))%type. Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed. Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?]. Ltac mexact x := by mapply x. -Local Notation min := minr. -Local Notation max := maxr. - Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed. Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed. Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed. @@ -5672,8 +5690,8 @@ Definition lter_minl := (ler_minl, ltr_minl). Definition lter_maxr := (ler_maxr, ltr_maxr). Definition lter_maxl := (ler_maxl, ltr_maxl). -Lemma minrK x y : max (min x y) x = x. Proof. mexact @minxK. Qed. -Lemma minKr x y : min y (max x y) = y. Proof. mexact @maxKx. Qed. +Lemma minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed. +Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; mexact @maxKx. Qed. Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed. Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index f0d432f..492aed8 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -506,7 +506,7 @@ have [r r_dv_p irr_r]: {r | r %| p & irreducible_poly r}. pose rVp (v : 'rV_n) (r := rVpoly v) := (1 < size r) && (r %| p). have [v0 Dp]: {v0 | rVpoly v0 = p & rVp v0}. by exists (poly_rV p); rewrite /rVp poly_rV_K ?C'p /=. - case/(arg_minP (size \o rVpoly))=> /= v; set r := rVpoly v. + case/(arg_minnP (size \o rVpoly))=> /= v; set r := rVpoly v. case/andP=> C'r r_dv_p min_r; exists r => //; split=> // q C'q q_dv_r. have nz_r: r != 0 by rewrite -size_poly_gt0 ltnW. have le_q_r: size q <= size r by rewrite dvdp_leq. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 95bc562..3a5caeb 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -264,7 +264,7 @@ Qed. Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}. Proof. -move=> nilG; have [//=| /= x Gx max_x] := @arg_maxP _ 1 (mem G) order. +move=> nilG; have [//=| /= x Gx max_x] := @arg_maxnP _ 1 (mem G) order. exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT. apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p. rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr. @@ -726,12 +726,12 @@ Qed. Lemma grank_min B : 'm(<<B>>) <= #|B|. Proof. -by rewrite /gen_rank; case: arg_minP => [|_ _ -> //]; rewrite genGid. +by rewrite /gen_rank; case: arg_minnP => [|_ _ -> //]; rewrite genGid. Qed. Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}. Proof. -rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid. +rewrite /gen_rank; case: arg_minnP => [|B defG _]; first by rewrite genGid. by exists B; first apply/eqP. Qed. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index e35d2c8..de03369 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1888,7 +1888,7 @@ Arguments bigmax_sup [I] i0 [P m F]. Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F : P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i]. Proof. -move=> Pi0; case: arg_maxP => //= i Pi maxFi. +move=> Pi0; case: arg_maxnP => //= i Pi maxFi. by apply/eqP; rewrite eqn_leq leq_bigmax_cond // andbT; apply/bigmax_leqP. Qed. Arguments bigmax_eq_arg [I] i0 [P F]. @@ -1897,7 +1897,7 @@ Lemma eq_bigmax_cond (I : finType) (A : pred I) F : #|A| > 0 -> {i0 | i0 \in A & \max_(i in A) F i = F i0}. Proof. case: (pickP A) => [i0 Ai0 _ | ]; last by move/eq_card0->. -by exists [arg max_(i > i0 in A) F i]; [case: arg_maxP | apply: bigmax_eq_arg]. +by exists [arg max_(i > i0 in A) F i]; [case: arg_maxnP | apply: bigmax_eq_arg]. Qed. Lemma eq_bigmax (I : finType) F : #|I| > 0 -> {i0 : I | \max_i F i = F i0}. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index f69f336..abed211 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1636,10 +1636,10 @@ 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. +Lemma arg_minnP : 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. +Lemma arg_maxnP : extremum_spec geq P F arg_max. Proof. apply: extremumP => //; first exact: leqnn. by move=> n m p mn np; apply: leq_trans mn. @@ -1650,6 +1650,13 @@ End ArgMinMax. End Extrema. +Notation "@ 'arg_minP'" := + (deprecate arg_minP arg_minnP) (at level 10, only parsing) : fun_scope. +Notation arg_minP := (@arg_minP _ _ _) (only parsing). +Notation "@ 'arg_maxP'" := + (deprecate arg_maxP arg_maxnP) (at level 10, only parsing) : fun_scope. +Notation arg_maxP := (@arg_maxP _ _ _) (only parsing). + Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := (arg_min i0 (fun i => P%B) (fun i => F)) (at level 0, i, i0 at level 10, diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 59de10c..10a26f1 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -196,10 +196,10 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* above. *) (* *) (* For porderType we provide the following operations *) -(* [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to *) +(* [arg min_(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 *) +(* [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. *) @@ -718,6 +718,43 @@ Reserved Notation "\min_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \min_ ( i 'in' A ) '/ ' F ']'"). +Reserved Notation "\max_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \max_ i '/ ' F ']'"). +Reserved Notation "\max_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\max_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\max_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \max_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max_ ( i < n ) F ']'"). +Reserved Notation "\max_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max_ ( i 'in' A ) '/ ' F ']'"). + Reserved Notation "\meet^d_ i F" (at level 41, F at level 41, i at level 0, format "'[' \meet^d_ i '/ ' F ']'"). @@ -792,6 +829,80 @@ Reserved Notation "\join^d_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \join^d_ ( i 'in' A ) '/ ' F ']'"). +Reserved Notation "\min^d_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \min^d_ i '/ ' F ']'"). +Reserved Notation "\min^d_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \min^d_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \min^d_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \min^d_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \min^d_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \min^d_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\min^d_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\min^d_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \min^d_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \min^d_ ( i < n ) F ']'"). +Reserved Notation "\min^d_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \min^d_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \min^d_ ( i 'in' A ) '/ ' F ']'"). + +Reserved Notation "\max^d_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \max^d_ i '/ ' F ']'"). +Reserved Notation "\max^d_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max^d_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max^d_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max^d_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max^d_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \max^d_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max^d_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max^d_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max^d_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max^d_ ( i < n ) F ']'"). +Reserved Notation "\max^d_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max^d_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max^d_ ( i 'in' A ) '/ ' F ']'"). + Reserved Notation "\meet^p_ i F" (at level 41, F at level 41, i at level 0, format "'[' \meet^p_ i '/ ' F ']'"). @@ -866,80 +977,6 @@ Reserved Notation "\join^p_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \join^p_ ( i 'in' A ) '/ ' F ']'"). -Reserved Notation "\min^l_ i F" - (at level 41, F at level 41, i at level 0, - format "'[' \min^l_ i '/ ' F ']'"). -Reserved Notation "\min^l_ ( i <- r | P ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \min^l_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i <- r ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \min^l_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( m <= i < n | P ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \min^l_ ( m <= i < n | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( m <= i < n ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \min^l_ ( m <= i < n ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i | P ) F" - (at level 41, F at level 41, i at level 50, - format "'[' \min^l_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\min^l_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\min^l_ ( i < n | P ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \min^l_ ( i < n | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i < n ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \min^l_ ( i < n ) F ']'"). -Reserved Notation "\min^l_ ( i 'in' A | P ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \min^l_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i 'in' A ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \min^l_ ( i 'in' A ) '/ ' F ']'"). - -Reserved Notation "\max^l_ i F" - (at level 41, F at level 41, i at level 0, - format "'[' \max^l_ i '/ ' F ']'"). -Reserved Notation "\max^l_ ( i <- r | P ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \max^l_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i <- r ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \max^l_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( m <= i < n | P ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \max^l_ ( m <= i < n | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( m <= i < n ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \max^l_ ( m <= i < n ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i | P ) F" - (at level 41, F at level 41, i at level 50, - format "'[' \max^l_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\max^l_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\max^l_ ( i < n | P ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \max^l_ ( i < n | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i < n ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \max^l_ ( i < n ) F ']'"). -Reserved Notation "\max^l_ ( i 'in' A | P ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \max^l_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i 'in' A ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \max^l_ ( i 'in' A ) '/ ' F ']'"). - Module Order. (**************) @@ -1066,11 +1103,13 @@ Variant incompare (x y : T) : | InCompareGt of y < x : incompare x y y y x x false false true false true false true true | InCompare of x >< y : incompare x y - (min y x) (min x y) (max y x) (max x y) - false false false false false false false false + x y y x false false false false false false false false | InCompareEq of x = y : incompare x y x x x x true true true true false false true true. +Definition arg_min {I : finType} := @extremum T I le. +Definition arg_max {I : finType} := @extremum T I ge. + End POrderDef. Prenex Implicits lt le leif. @@ -1130,6 +1169,34 @@ Notation ">< x" := (fun y => ~~ (comparable x y)) : order_scope. Notation ">< x :> T" := (>< (x : T)) (only parsing) : order_scope. Notation "x >< y" := (~~ (comparable x y)) : order_scope. +Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := + (arg_min i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := + [arg min_(i < i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := + (arg_max i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := + [arg max_(i > i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope. + End POSyntax. Module POCoercions. @@ -1244,8 +1311,7 @@ Variant incomparel (x y : T) : | InComparelGt of y < x : incomparel x y y y x x y y x x false false true false true false true true | InComparel of x >< y : incomparel x y - (min y x) (min x y) (max y x) (max x y) - (meet y x) (meet x y) (join y x) (join x y) + x y y x (meet y x) (meet x y) (join y x) (join x y) false false false false false false false false | InComparelEq of x = y : incomparel x y x x x x x x x x true true true true false false true true. @@ -1946,96 +2012,6 @@ End Exports. End Total. Import Total.Exports. -Section TotalDef. -Context {disp : unit} {T : orderType disp} {I : finType}. -Definition arg_min := @extremum T I <=%O. -Definition arg_max := @extremum T I >=%O. -End TotalDef. - -Module Import TotalSyntax. - -Notation "\max_ ( i <- r | P ) F" := - (\big[max/0%O]_(i <- r | P%B) F%O) : order_scope. -Notation "\max_ ( i <- r ) F" := - (\big[max/0%O]_(i <- r) F%O) : order_scope. -Notation "\max_ ( i | P ) F" := - (\big[max/0%O]_(i | P%B) F%O) : order_scope. -Notation "\max_ i F" := - (\big[max/0%O]_i F%O) : order_scope. -Notation "\max_ ( i : I | P ) F" := - (\big[max/0%O]_(i : I | P%B) F%O) (only parsing) : - order_scope. -Notation "\max_ ( i : I ) F" := - (\big[max/0%O]_(i : I) F%O) (only parsing) : order_scope. -Notation "\max_ ( m <= i < n | P ) F" := - (\big[max/0%O]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\max_ ( m <= i < n ) F" := - (\big[max/0%O]_(m <= i < n) F%O) : order_scope. -Notation "\max_ ( i < n | P ) F" := - (\big[max/0%O]_(i < n | P%B) F%O) : order_scope. -Notation "\max_ ( i < n ) F" := - (\big[max/0%O]_(i < n) F%O) : order_scope. -Notation "\max_ ( i 'in' A | P ) F" := - (\big[max/0%O]_(i in A | P%B) F%O) : order_scope. -Notation "\max_ ( i 'in' A ) F" := - (\big[max/0%O]_(i in A) F%O) : order_scope. - -Notation "\min_ ( i <- r | P ) F" := - (\big[min/1%O]_(i <- r | P%B) F%O) : order_scope. -Notation "\min_ ( i <- r ) F" := - (\big[min/1%O]_(i <- r) F%O) : order_scope. -Notation "\min_ ( i | P ) F" := - (\big[min/1%O]_(i | P%B) F%O) : order_scope. -Notation "\min_ i F" := - (\big[min/1%O]_i F%O) : order_scope. -Notation "\min_ ( i : I | P ) F" := - (\big[min/1%O]_(i : I | P%B) F%O) (only parsing) : - order_scope. -Notation "\min_ ( i : I ) F" := - (\big[min/1%O]_(i : I) F%O) (only parsing) : order_scope. -Notation "\min_ ( m <= i < n | P ) F" := - (\big[min/1%O]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\min_ ( m <= i < n ) F" := - (\big[min/1%O]_(m <= i < n) F%O) : order_scope. -Notation "\min_ ( i < n | P ) F" := - (\big[min/1%O]_(i < n | P%B) F%O) : order_scope. -Notation "\min_ ( i < n ) F" := - (\big[min/1%O]_(i < n) F%O) : order_scope. -Notation "\min_ ( i 'in' A | P ) F" := - (\big[min/1%O]_(i in A | P%B) F%O) : order_scope. -Notation "\min_ ( i 'in' A ) F" := - (\big[min/1%O]_(i in A) F%O) : order_scope. - -Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := - (arg_min i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : order_scope. - -Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := - [arg min_(i < i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope. - -Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 ) F ]") : order_scope. - -Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := - (arg_max i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : order_scope. - -Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := - [arg max_(i > i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : order_scope. - -Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope. - -End TotalSyntax. - (**********) (* FINITE *) (**********) @@ -2586,13 +2562,15 @@ Notation "><^d x" := (fun y => ~~ (>=<^d%O x y)) : order_scope. Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope. Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. -Notation "x `&^d` y" := (@meet (dual_display _) _ x y) : order_scope. -Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope. - Notation dual_bottom := (@bottom (dual_display _)). Notation dual_top := (@top (dual_display _)). Notation dual_join := (@join (dual_display _) _). Notation dual_meet := (@meet (dual_display _) _). +Notation dual_max := (@max (dual_display _) _). +Notation dual_min := (@min (dual_display _) _). + +Notation "x `&^d` y" := (@meet (dual_display _) _ x y) : order_scope. +Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope. Notation "\join^d_ ( i <- r | P ) F" := (\big[join/0]_(i <- r | P%B) F%O) : order_scope. @@ -2824,8 +2802,8 @@ Lemma comparableP x y : incompare x y Proof. rewrite ![y >=< _]comparable_sym; have [c_xy|i_xy] := boolP (x >=< y). by case: (comparable_ltgtP c_xy) => ?; constructor. -by rewrite ?incomparable_eqF ?incomparable_leF ?incomparable_ltF // - 1?comparable_sym //; constructor. +by rewrite /min /max ?incomparable_eqF ?incomparable_leF; + rewrite ?incomparable_ltF// 1?comparable_sym //; constructor. Qed. Lemma le_comparable (x y : T) : x <= y -> x >=< y. @@ -2882,6 +2860,24 @@ Proof. by move=> /eq_leif<-/eqP. Qed. (* min and max *) +Lemma minElt x y : min x y = if x < y then x else y. Proof. by []. Qed. +Lemma maxElt x y : max x y = if x < y then y else x. Proof. by []. Qed. + +Lemma minEle x y : min x y = if x <= y then x else y. +Proof. by case: comparableP. Qed. + +Lemma maxEle x y : max x y = if x <= y then y else x. +Proof. by case: comparableP. Qed. + +Lemma comparable_minEgt x y : x >=< y -> min x y = if x > y then y else x. +Proof. by case: comparableP. Qed. +Lemma comparable_maxEgt x y : x >=< y -> max x y = if x > y then x else y. +Proof. by case: comparableP. Qed. +Lemma comparable_minEge x y : x >=< y -> min x y = if x >= y then y else x. +Proof. by case: comparableP. Qed. +Lemma comparable_maxEge x y : x >=< y -> max x y = if x >= y then x else y. +Proof. by case: comparableP. Qed. + Lemma min_l x y : x <= y -> min x y = x. Proof. by case: comparableP. Qed. Lemma min_r x y : y <= x -> min x y = y. Proof. by case: comparableP. Qed. Lemma max_l x y : y <= x -> max x y = x. Proof. by case: comparableP. Qed. @@ -2899,6 +2895,24 @@ Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed. Lemma eq_maxr x y : (max x y == y) = (x <= y). Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed. +Lemma min_idPl x y : reflect (min x y = x) (x <= y). +Proof. by apply: (iffP idP); rewrite (rwP eqP) eq_minl. Qed. + +Lemma max_idPr x y : reflect (max x y = y) (x <= y). +Proof. by apply: (iffP idP); rewrite (rwP eqP) eq_maxr. Qed. + +Lemma min_minKx x y : min (min x y) y = min x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma min_minxK x y : min x (min x y) = min x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma max_maxKx x y : max (max x y) y = max x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma max_maxxK x y : max x (max x y) = max x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + Lemma comparable_minl x y z : x >=< z -> y >=< z -> min x y >=< z. Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. @@ -2926,6 +2940,12 @@ Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed. Lemma comparable_eq_maxl : (max x y == x) = (y <= x). Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed. +Lemma comparable_min_idPr : reflect (min x y = y) (y <= x). +Proof. by apply: (iffP idP); rewrite (rwP eqP) comparable_eq_minr. Qed. + +Lemma comparable_max_idPl : reflect (max x y = x) (y <= x). +Proof. by apply: (iffP idP); rewrite (rwP eqP) comparable_eq_maxl. Qed. + Lemma comparable_le_minr : (z <= min x y) = (z <= x) && (z <= y). Proof. case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; last rewrite andbC; @@ -2974,16 +2994,16 @@ case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; first rewrite andbC; by case: (comparableP z) => // ylt /lt_trans->. Qed. -Lemma comparable_minxK : max (min x y) x = x. +Lemma comparable_minxK : max (min x y) y = y. Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. -Lemma comparable_minKx : max y (min x y) = y. +Lemma comparable_minKx : max x (min x y) = x. Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. -Lemma comparable_maxxK : min (max x y) x = x. +Lemma comparable_maxxK : min (max x y) y = y. Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. -Lemma comparable_maxKx : min y (max x y) = y. +Lemma comparable_maxKx : min x (max x y) = x. Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. End Comparable2. @@ -3092,6 +3112,24 @@ move=> xy xz yz; rewrite ![min x _]comparable_minC// ?comparable_maxr//. by rewrite comparable_min_maxl// 1?comparable_sym. Qed. +Section ArgExtremum. + +Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0). +Hypothesis F_comparable : {in P &, forall i j, F i >=< F j}. + +Lemma comparable_arg_minP: extremum_spec <=%O P F (arg_min i0 P F). +Proof. +by apply: extremum_inP => // [x _|y x z _ _ _]; [apply: lexx|apply: le_trans]. +Qed. + +Lemma comparable_arg_maxP: extremum_spec >=%O P F (arg_max i0 P F). +Proof. +apply: extremum_inP => // [x _|y x z _ _ _|]; [exact: lexx|exact: ge_trans|]. +by move=> x y xP yP; rewrite orbC [_ || _]F_comparable. +Qed. + +End ArgExtremum. + (* monotonicity *) Lemma mono_in_leif (A : {pred T}) (f : T -> T) C : @@ -3200,6 +3238,10 @@ Arguments mono_in_leif [disp T A f C]. Arguments nmono_in_leif [disp T A f C]. Arguments mono_leif [disp T f C]. Arguments nmono_leif [disp T f C]. +Arguments min_idPl {disp T x y}. +Arguments max_idPr {disp T x y}. +Arguments comparable_min_idPr {disp T x y _}. +Arguments comparable_max_idPl {disp T x y _}. Module Import DualPOrder. Section DualPOrder. @@ -3458,6 +3500,9 @@ Proof. by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed. End LatticeTheoryJoin. End LatticeTheoryJoin. +Arguments meet_idPl {disp L x y}. +Arguments join_idPl {disp L x y}. + Module Import DistrLatticeTheory. Section DistrLatticeTheory. Context {disp : unit}. @@ -3554,11 +3599,18 @@ Lemma eq_ltRL x y z t : (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y). Proof. by move=> *; symmetry; apply: eq_ltLR. Qed. -(* interaction with lattice operations *) +(* max and min is join and meet *) Lemma meetEtotal x y : x `&` y = min x y. Proof. by case: leP. Qed. Lemma joinEtotal x y : x `|` y = max x y. Proof. by case: leP. Qed. +(* max and min theory *) + +Lemma minEgt x y : min x y = if x > y then y else x. Proof. by case: ltP. Qed. +Lemma maxEgt x y : max x y = if x > y then x else y. Proof. by case: ltP. Qed. +Lemma minEge x y : min x y = if x >= y then y else x. Proof. by case: leP. Qed. +Lemma maxEge x y : max x y = if x >= y then x else y. Proof. by case: leP. Qed. + Lemma minC : commutative (min : T -> T -> T). Proof. by move=> x y; apply: comparable_minC. Qed. @@ -3595,6 +3647,12 @@ Proof. exact: comparable_eq_minr. Qed. Lemma eq_maxl x y : (max x y == x) = (y <= x). Proof. exact: comparable_eq_maxl. Qed. +Lemma min_idPr x y : reflect (min x y = y) (y <= x). +Proof. exact: comparable_min_idPr. Qed. + +Lemma max_idPl x y : reflect (max x y = x) (y <= x). +Proof. exact: comparable_max_idPl. Qed. + Lemma le_minr z x y : (z <= min x y) = (z <= x) && (z <= y). Proof. exact: comparable_le_minr. Qed. @@ -3619,10 +3677,10 @@ Proof. exact: comparable_lt_maxr. Qed. Lemma lt_maxl z x y : (max x y < z) = (x < z) && (y < z). Proof. exact: comparable_lt_maxl. Qed. -Lemma minxK x y : max (min x y) x = x. Proof. exact: comparable_minxK. Qed. -Lemma minKx x y : max y (min x y) = y. Proof. exact: comparable_minKx. Qed. -Lemma maxxK x y : min (max x y) x = x. Proof. exact: comparable_maxxK. Qed. -Lemma maxKx x y : min y (max x y) = y. Proof. exact: comparable_maxKx. Qed. +Lemma minxK x y : max (min x y) y = y. Proof. exact: comparable_minxK. Qed. +Lemma minKx x y : max x (min x y) = x. Proof. exact: comparable_minKx. Qed. +Lemma maxxK x y : min (max x y) y = y. Proof. exact: comparable_maxxK. Qed. +Lemma maxKx x y : min x (max x y) = x. Proof. exact: comparable_maxKx. Qed. Lemma max_minl : left_distributive (max : T -> T -> T) min. Proof. by move=> x y z; apply: comparable_max_minl. Qed. @@ -3663,9 +3721,6 @@ Section ArgExtremum. Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0). -Definition arg_minnP := arg_minP. -Definition arg_maxnP := arg_maxP. - Lemma arg_minP: extremum_spec <=%O P F (arg_min i0 P F). Proof. by apply: extremumP => //; apply: le_trans. Qed. @@ -3675,6 +3730,10 @@ Proof. by apply: extremumP => //; [apply: ge_refl | apply: ge_trans]. Qed. End ArgExtremum. End TotalTheory. + +Arguments min_idPr {disp T x y}. +Arguments max_idPl {disp T x y}. + Section TotalMonotonyTheory. Context {disp : unit} {disp' : unit}. @@ -5402,61 +5461,11 @@ Notation "><^l x" := (fun y => ~~ (>=<^l%O x y)) : order_scope. Notation "><^l x :> T" := (><^l (x : T)) (only parsing) : order_scope. Notation "x ><^l y" := (~~ (><^l%O x y)) : order_scope. -Notation minlexi := (@meet lexi_display _). -Notation maxlexi := (@join lexi_display _). - -Notation "x `&^l` y" := (minlexi x y) : order_scope. -Notation "x `|^l` y" := (maxlexi x y) : order_scope. - -Notation "\max^l_ ( i <- r | P ) F" := - (\big[maxlexi/0]_(i <- r | P%B) F%O) : order_scope. -Notation "\max^l_ ( i <- r ) F" := - (\big[maxlexi/0]_(i <- r) F%O) : order_scope. -Notation "\max^l_ ( i | P ) F" := - (\big[maxlexi/0]_(i | P%B) F%O) : order_scope. -Notation "\max^l_ i F" := - (\big[maxlexi/0]_i F%O) : order_scope. -Notation "\max^l_ ( i : I | P ) F" := - (\big[maxlexi/0]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\max^l_ ( i : I ) F" := - (\big[maxlexi/0]_(i : I) F%O) (only parsing) : order_scope. -Notation "\max^l_ ( m <= i < n | P ) F" := - (\big[maxlexi/0]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\max^l_ ( m <= i < n ) F" := - (\big[maxlexi/0]_(m <= i < n) F%O) : order_scope. -Notation "\max^l_ ( i < n | P ) F" := - (\big[maxlexi/0]_(i < n | P%B) F%O) : order_scope. -Notation "\max^l_ ( i < n ) F" := - (\big[maxlexi/0]_(i < n) F%O) : order_scope. -Notation "\max^l_ ( i 'in' A | P ) F" := - (\big[maxlexi/0]_(i in A | P%B) F%O) : order_scope. -Notation "\max^l_ ( i 'in' A ) F" := - (\big[maxlexi/0]_(i in A) F%O) : order_scope. - -Notation "\min^l_ ( i <- r | P ) F" := - (\big[minlexi/1]_(i <- r | P%B) F%O) : order_scope. -Notation "\min^l_ ( i <- r ) F" := - (\big[minlexi/1]_(i <- r) F%O) : order_scope. -Notation "\min^l_ ( i | P ) F" := - (\big[minlexi/1]_(i | P%B) F%O) : order_scope. -Notation "\min^l_ i F" := - (\big[minlexi/1]_i F%O) : order_scope. -Notation "\min^l_ ( i : I | P ) F" := - (\big[minlexi/1]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\min^l_ ( i : I ) F" := - (\big[minlexi/1]_(i : I) F%O) (only parsing) : order_scope. -Notation "\min^l_ ( m <= i < n | P ) F" := - (\big[minlexi/1]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\min^l_ ( m <= i < n ) F" := - (\big[minlexi/1]_(m <= i < n) F%O) : order_scope. -Notation "\min^l_ ( i < n | P ) F" := - (\big[minlexi/1]_(i < n | P%B) F%O) : order_scope. -Notation "\min^l_ ( i < n ) F" := - (\big[minlexi/1]_(i < n) F%O) : order_scope. -Notation "\min^l_ ( i 'in' A | P ) F" := - (\big[minlexi/1]_(i in A | P%B) F%O) : order_scope. -Notation "\min^l_ ( i 'in' A ) F" := - (\big[minlexi/1]_(i in A) F%O) : order_scope. +Notation meetlexi := (@meet lexi_display _). +Notation joinlexi := (@join lexi_display _). + +Notation "x `&^l` y" := (meetlexi x y) : order_scope. +Notation "x `|^l` y" := (joinlexi x y) : order_scope. End LexiSyntax. @@ -6997,7 +7006,6 @@ Export BLatticeSyntax. Export TBLatticeSyntax. Export CBDistrLatticeSyntax. Export CTBDistrLatticeSyntax. -Export TotalSyntax. Export DualSyntax. Export DvdSyntax. End Syntax. |