diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 106 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 16 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 30 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 40 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 81 |
5 files changed, 213 insertions, 60 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 1cc585e..feb9edd 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -110,6 +110,9 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* A \in unitmx == A is invertible (R must be a comUnitRingType). *) (* invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. *) (* A \is a mxOver S == the matrix A has its coefficients in S. *) +(* comm_mx A B := A *m B = B *m A *) +(* comm_mxb A B := A *m B == B *m A *) +(* all_comm_mx As := allrel comm_mxb *) (* The following operations provide a correspondence between linear functions *) (* and matrices: *) (* lin1_mx f == the m x n matrix that emulates via right product *) @@ -2711,6 +2714,89 @@ Qed. End MapRingMatrix. +Section CommMx. +(***********************************************************************) +(************* Commutation property specialized to 'M[R]_n *************) +(***********************************************************************) +(* GRing.comm is bound to (non trivial) rings, and matrices form a *) +(* (non trivial) ring only when they are square and of manifestly *) +(* positive size. However during proofs in endomorphism reduction, we *) +(* take restrictions, which are matrices of size #|V| (with V a matrix *) +(* space) and it becomes cumbersome to state commutation between *) +(* restrictions, unless we relax the setting, and this relaxation *) +(* corresponds to comm_mx A B := A *m B = B *m A. *) +(* As witnessed by comm_mxE, when A and B have type 'M_n.+1, *) +(* comm_mx A B is convertible to GRing.comm A B. *) +(* The boolean version comm_mxb is designed to be used with seq.allrel *) +(***********************************************************************) + +Context {R : ringType} {n : nat}. +Implicit Types (f g p : 'M[R]_n) (fs : seq 'M[R]_n) (d : 'rV[R]_n) (I : Type). + +Definition comm_mx f g : Prop := f *m g = g *m f. +Definition comm_mxb f g : bool := f *m g == g *m f. + +Lemma comm_mx_sym f g : comm_mx f g -> comm_mx g f. +Proof. by rewrite /comm_mx. Qed. + +Lemma comm_mx_refl f : comm_mx f f. Proof. by []. Qed. + +Lemma comm_mx0 f : comm_mx f 0. Proof. by rewrite /comm_mx mulmx0 mul0mx. Qed. +Lemma comm0mx f : comm_mx 0 f. Proof. by rewrite /comm_mx mulmx0 mul0mx. Qed. + +Lemma comm_mx1 f : comm_mx f 1%:M. +Proof. by rewrite /comm_mx mulmx1 mul1mx. Qed. + +Lemma comm1mx f : comm_mx 1%:M f. +Proof. by rewrite /comm_mx mulmx1 mul1mx. Qed. + +Hint Resolve comm_mx0 comm0mx comm_mx1 comm1mx : core. + +Lemma comm_mxN f g : comm_mx f g -> comm_mx f (- g). +Proof. by rewrite /comm_mx mulmxN mulNmx => ->. Qed. + +Lemma comm_mxN1 f : comm_mx f (- 1%:M). Proof. exact/comm_mxN/comm_mx1. Qed. + +Lemma comm_mxD f g g' : comm_mx f g -> comm_mx f g' -> comm_mx f (g + g'). +Proof. by rewrite /comm_mx mulmxDl mulmxDr => -> ->. Qed. + +Lemma comm_mxB f g g' : comm_mx f g -> comm_mx f g' -> comm_mx f (g - g'). +Proof. by move=> fg fg'; apply/comm_mxD => //; apply/comm_mxN. Qed. + +Lemma comm_mxM f g g' : comm_mx f g -> comm_mx f g' -> comm_mx f (g *m g'). +Proof. by rewrite /comm_mx mulmxA => ->; rewrite -!mulmxA => ->. Qed. + +Lemma comm_mx_sum I (s : seq I) (P : pred I) (F : I -> 'M[R]_n) (f : 'M[R]_n) : + (forall i : I, P i -> comm_mx f (F i)) -> comm_mx f (\sum_(i <- s | P i) F i). +Proof. by move=> comm_mxfF; elim/big_ind: _ => // g h; apply: comm_mxD. Qed. + +Lemma comm_mxP f g : reflect (comm_mx f g) (comm_mxb f g). +Proof. exact: eqP. Qed. + +Notation all_comm_mx := (allrel comm_mxb). + +Lemma all_comm_mxP fs : + reflect {in fs &, forall f g, f *m g = g *m f} (all_comm_mx fs). +Proof. by apply: (iffP allrelP) => fsP ? ? ? ?; apply/eqP/fsP. Qed. + +Lemma all_comm_mx1 f : all_comm_mx [:: f]. +Proof. by rewrite /comm_mxb allrel1. Qed. + +Lemma all_comm_mx2P f g : reflect (f *m g = g *m f) (all_comm_mx [:: f; g]). +Proof. +by rewrite /comm_mxb; apply: (iffP and4P) => [[_/eqP//]|->]; rewrite ?eqxx. +Qed. + +Lemma all_comm_mx_cons f fs : + all_comm_mx (f :: fs) = all (comm_mxb f) fs && all_comm_mx fs. +Proof. by rewrite /comm_mxb [LHS]allrel_cons. Qed. + +End CommMx. +Notation all_comm_mx := (allrel comm_mxb). + +Lemma comm_mxE (R : ringType) (n : nat) : @comm_mx R n.+1 = @GRing.comm _. +Proof. by []. Qed. + Section ComMatrix. (* Lemmas for matrices with coefficients in a commutative ring *) Variable R : comRingType. @@ -2792,7 +2878,7 @@ Proof. by rewrite !mulmx_diag; congr (diag_mx _); apply/rowP=> i; rewrite !mxE mulrC. Qed. -Lemma diag_mx_comm n' (d e : 'rV[R]_n'.+1) : GRing.comm (diag_mx d) (diag_mx e). +Lemma diag_mx_comm n (d e : 'rV[R]_n) : comm_mx (diag_mx d) (diag_mx e). Proof. exact: diag_mxC. Qed. Lemma scalar_mxC m n a (A : 'M[R]_(m, n)) : A *m a%:M = a%:M *m A. @@ -2800,12 +2886,15 @@ Proof. by apply: trmx_inj; rewrite trmx_mul tr_scalar_mx !mul_scalar_mx linearZ. Qed. -Lemma scalar_mx_comm n' a (A : 'M[R]_n'.+1) : GRing.comm A a%:M. -Proof. exact: scalar_mxC. Qed. - Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A *m a%:M = a *: A. Proof. by rewrite scalar_mxC mul_scalar_mx. Qed. +Lemma comm_mxC n a (A : 'M[R]_n) : comm_mx A a%:M. +Proof. by rewrite /comm_mx mul_mx_scalar mul_scalar_mx. Qed. + +Lemma commCmx n a (A : 'M[R]_n) : comm_mx a%:M A. +Proof. exact/comm_mx_sym/comm_mxC. Qed. + Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B : \tr (A *m B) = \tr (B *m A). Proof. @@ -3051,10 +3140,19 @@ End ComMatrix. Arguments lin_mul_row {R m n} u. Arguments lin_mulmx {R m n p} A. +Arguments comm_mxC {R n}. +Arguments commCmx {R n}. +Arguments diag_mx_comm {R n}. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. +Hint Resolve comm_mxC commCmx : core. + +Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mxC) + (at level 10, only parsing) : fun_scope. +Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing). + (*****************************************************************************) (********************** Matrix unit ring and inverse matrices ****************) (*****************************************************************************) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 9cc7c94..9ffbe77 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -271,7 +271,7 @@ Local Notation n := n'.+1. Variable A : 'M[R]_n. Implicit Types p q : {poly R}. -Definition horner_mx := horner_morph (fun a => scalar_mx_comm a A). +Definition horner_mx := horner_morph (comm_mxC^~ A). Canonical horner_mx_additive := [additive of horner_mx]. Canonical horner_mx_rmorphism := [rmorphism of horner_mx]. @@ -948,6 +948,20 @@ Proof. by rewrite /eigenpoly -map_kermxpoly map_mx_eq0. Qed. End MapKermxPoly. +Section CommmxPoly. + +Lemma comm_mx_horner (R : comRingType) (n' : nat) (A B : 'M[R]_n'.+1) + (p : {poly R}) : comm_mx A B -> comm_mx A (horner_mx B p). +Proof. +by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx. +Qed. + +Lemma horner_mxC (R : comRingType) (n' : nat) (A : 'M_n'.+1) (p q : {poly R}) : + GRing.comm (horner_mx A p) (horner_mx A p). +Proof. exact/comm_mx_horner/comm_mx_sym/comm_mx_horner. Qed. + +End CommmxPoly. + Section IntegralOverRing. Definition integralOver (R K : ringType) (RtoK : R -> K) (z : K) := diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 97766c1..3100697 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -835,8 +835,11 @@ Qed. Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m. Proof. by rewrite -!mulrnA mulnC. Qed. -Lemma iter_addr_0 n (m : V) : iter n (+%R m) 0 = m *+ n. -Proof. by elim: n => //= n ->; rewrite mulrS. Qed. +Lemma iter_addr n x y : iter n (+%R x) y = x *+ n + y. +Proof. by elim: n => [|n ih]; rewrite ?add0r //= ih mulrS addrA. Qed. + +Lemma iter_addr_0 n x : iter n (+%R x) 0 = x *+ n. +Proof. by rewrite iter_addr addr0. Qed. Lemma sumrN I r P (F : I -> V) : (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)). @@ -855,11 +858,10 @@ Lemma sumrMnr x I r P (F : I -> nat) : \sum_(i <- r | P i) x *+ F i = x *+ (\sum_(i <- r | P i) F i). Proof. by rewrite (big_morph _ (mulrnDr x) (erefl _)). Qed. -Lemma sumr_const (I : finType) (A : pred I) (x : V) : - \sum_(i in A) x = x *+ #|A|. +Lemma sumr_const (I : finType) (A : pred I) x : \sum_(i in A) x = x *+ #|A|. Proof. by rewrite big_const -iteropE. Qed. -Lemma sumr_const_nat (m n : nat) (x : V) : \sum_(n <= i < m) x = x *+ (m - n). +Lemma sumr_const_nat m n x : \sum_(n <= i < m) x = x *+ (m - n). Proof. by rewrite big_const_nat iter_addr_0. Qed. Lemma telescope_sumr n m (f : nat -> V) : n <= m -> @@ -1248,10 +1250,18 @@ Qed. Lemma lreg_sign n : lreg ((-1) ^+ n : R). Proof. exact/lregX/lregN/lreg1. Qed. -Lemma prodr_const (I : finType) (A : pred I) (x : R) : - \prod_(i in A) x = x ^+ #|A|. +Lemma iter_mulr n x y : iter n ( *%R x) y = x ^+ n * y. +Proof. by elim: n => [|n ih]; rewrite ?expr0 ?mul1r //= ih exprS -mulrA. Qed. + +Lemma iter_mulr_1 n x : iter n ( *%R x) 1 = x ^+ n. +Proof. by rewrite iter_mulr mulr1. Qed. + +Lemma prodr_const (I : finType) (A : pred I) x : \prod_(i in A) x = x ^+ #|A|. Proof. by rewrite big_const -iteropE. Qed. +Lemma prodr_const_nat n m x : \prod_(n <= i < m) x = x ^+ (m - n). +Proof. by rewrite big_const_nat -iteropE. Qed. + Lemma prodrXr x I r P (F : I -> nat) : \prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i). Proof. by rewrite (big_morph _ (exprD _) (erefl _)). Qed. @@ -5604,6 +5614,7 @@ Definition sumrB := sumrB. Definition sumrMnl := sumrMnl. Definition sumrMnr := sumrMnr. Definition sumr_const := sumr_const. +Definition sumr_const_nat := sumr_const_nat. Definition telescope_sumr := telescope_sumr. Definition mulr0n := mulr0n. Definition mulr1n := mulr1n. @@ -5619,6 +5630,8 @@ Definition mulrnBl := mulrnBl. Definition mulrnBr := mulrnBr. Definition mulrnA := mulrnA. Definition mulrnAC := mulrnAC. +Definition iter_addr := iter_addr. +Definition iter_addr_0 := iter_addr_0. Definition mulrA := mulrA. Definition mul1r := mul1r. Definition mulr1 := mulr1. @@ -5733,7 +5746,10 @@ Definition addrr_char2 := addrr_char2. Definition oppr_char2 := oppr_char2. Definition addrK_char2 := addrK_char2. Definition addKr_char2 := addKr_char2. +Definition iter_mulr := iter_mulr. +Definition iter_mulr_1 := iter_mulr_1. Definition prodr_const := prodr_const. +Definition prodr_const_nat := prodr_const_nat. Definition mulrC := mulrC. Definition mulrCA := mulrCA. Definition mulrAC := mulrAC. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2eefe8e..0244891 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -464,9 +464,6 @@ Notation "< y :> T" := (< (y : T)) (only parsing) : ring_scope. Notation "> y" := (lt y) : ring_scope. Notation "> y :> T" := (> (y : T)) (only parsing) : ring_scope. -Notation ">=< y" := (comparable y) : ring_scope. -Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope. - Notation "x <= y" := (le x y) : ring_scope. Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : ring_scope. Notation "x >= y" := (y <= x) (only parsing) : ring_scope. @@ -490,12 +487,12 @@ Notation "x < y ?<= 'if' C" := (lterif x y C) : ring_scope. Notation "x < y ?<= 'if' C :> R" := ((x : R) < (y : R) ?<= if C) (only parsing) : ring_scope. -Notation ">=< x" := (comparable x) : ring_scope. -Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : ring_scope. +Notation ">=< y" := [pred x | comparable x y] : ring_scope. +Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope. Notation "x >=< y" := (comparable x y) : ring_scope. -Notation ">< x" := (fun y => ~~ (comparable x y)) : ring_scope. -Notation ">< x :> T" := (>< (x : T)) (only parsing) : ring_scope. +Notation ">< y" := [pred x | ~~ comparable x y] : ring_scope. +Notation ">< y :> T" := (>< (y : T)) (only parsing) : ring_scope. Notation "x >< y" := (~~ (comparable x y)) : ring_scope. Canonical Rpos_keyed. @@ -1479,6 +1476,19 @@ rewrite sqrf_eq1 => /orP[/eqP //|]; rewrite -ger0_def le0r oppr_eq0 oner_eq0. by move/(addr_gt0 ltr01); rewrite subrr ltxx. Qed. +Lemma big_real x0 op I (P : pred I) F (s : seq I) : + {in real &, forall x y, op x y \is real} -> x0 \is real -> + {in P, forall i, F i \is real} -> \big[op/x0]_(i <- s | P i) F i \is real. +Proof. exact: comparable_bigr. Qed. + +Lemma sum_real I (P : pred I) (F : I -> R) (s : seq I) : + {in P, forall i, F i \is real} -> \sum_(i <- s | P i) F i \is real. +Proof. by apply/big_real; [apply: rpredD | apply: rpred0]. Qed. + +Lemma prod_real I (P : pred I) (F : I -> R) (s : seq I) : + {in P, forall i, F i \is real} -> \prod_(i <- s | P i) F i \is real. +Proof. by apply/big_real; [apply: rpredM | apply: rpred1]. Qed. + Section NormedZmoduleTheory. Variable V : normedZmodType R. @@ -1779,6 +1789,22 @@ move=> hx; rewrite -[X in `|X|]subr0; case: (@real_ltgtP 0 x); by rewrite ?subr0 ?sub0r //; constructor. Qed. +Lemma max_real : {in real &, forall x y, max x y \is real}. +Proof. exact: comparable_maxr. Qed. + +Lemma min_real : {in real &, forall x y, min x y \is real}. +Proof. exact: comparable_minr. Qed. + +Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R): + x0 \is real -> {in P, forall i : I, f i \is real} -> + \big[max/x0]_(i <- r | P i) f i \is real. +Proof. exact/big_real/max_real. Qed. + +Lemma bigmin_real I x0 (r : seq I) (P : pred I) (f : I -> R): + x0 \is real -> {in P, forall i : I, f i \is real} -> + \big[min/x0]_(i <- r | P i) f i \is real. +Proof. exact/big_real/min_real. Qed. + Lemma real_neqr_lt : {in real &, forall x y, (x != y) = (x < y) || (y < x)}. Proof. by move=> * /=; case: real_ltgtP. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index b9ed011..da4d59d 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -419,7 +419,7 @@ Reserved Notation ">= y :> T" (at level 35, y at next level). Reserved Notation "< y :> T" (at level 35, y at next level). Reserved Notation "> y :> T" (at level 35, y at next level). Reserved Notation "x >=< y" (at level 70, no associativity). -Reserved Notation ">=< x" (at level 35). +Reserved Notation ">=< y" (at level 35). Reserved Notation ">=< y :> T" (at level 35, y at next level). Reserved Notation "x >< y" (at level 70, no associativity). Reserved Notation ">< x" (at level 35). @@ -454,7 +454,7 @@ Reserved Notation ">=^d y :> T" (at level 35, y at next level). Reserved Notation "<^d y :> T" (at level 35, y at next level). Reserved Notation ">^d y :> T" (at level 35, y at next level). Reserved Notation "x >=<^d y" (at level 70, no associativity). -Reserved Notation ">=<^d x" (at level 35). +Reserved Notation ">=<^d y" (at level 35). Reserved Notation ">=<^d y :> T" (at level 35, y at next level). Reserved Notation "x ><^d y" (at level 70, no associativity). Reserved Notation "><^d x" (at level 35). @@ -1146,9 +1146,6 @@ Notation "< y :> T" := (< (y : T)) (only parsing) : order_scope. Notation "> y" := (lt y) : order_scope. Notation "> y :> T" := (> (y : T)) (only parsing) : order_scope. -Notation ">=< y" := (comparable y) : order_scope. -Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope. - Notation "x <= y" := (le x y) : order_scope. Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : order_scope. Notation "x >= y" := (y <= x) (only parsing) : order_scope. @@ -1172,12 +1169,12 @@ Notation "x < y ?<= 'if' C" := (lteif x y C) : order_scope. Notation "x < y ?<= 'if' C :> T" := ((x : T) < (y : T) ?<= if C) (only parsing) : order_scope. -Notation ">=< x" := (comparable x) : order_scope. -Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope. +Notation ">=< y" := [pred x | comparable x y] : order_scope. +Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope. Notation "x >=< y" := (comparable x y) : order_scope. -Notation ">< x" := (fun y => ~~ (comparable x y)) : order_scope. -Notation ">< x :> T" := (>< (x : T)) (only parsing) : order_scope. +Notation ">< y" := [pred x | ~~ comparable x y] : order_scope. +Notation ">< y :> T" := (>< (y : T)) (only parsing) : order_scope. Notation "x >< y" := (~~ (comparable x y)) : order_scope. Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := @@ -2541,9 +2538,6 @@ Notation "<^d y :> T" := (<^d (y : T)) (only parsing) : order_scope. Notation ">^d y" := (<^d%O y) : order_scope. Notation ">^d y :> T" := (>^d (y : T)) (only parsing) : order_scope. -Notation ">=<^d y" := (>=<^d%O y) : order_scope. -Notation ">=<^d y :> T" := (>=<^d (y : T)) (only parsing) : order_scope. - Notation "x <=^d y" := (<=^d%O x y) : order_scope. Notation "x <=^d y :> T" := ((x : T) <=^d (y : T)) (only parsing) : order_scope. Notation "x >=^d y" := (y <=^d x) (only parsing) : order_scope. @@ -2568,11 +2562,11 @@ Notation "x <^d y ?<= 'if' C :> T" := ((x : T) <^d (y : T) ?<= if C) (only parsing) : order_scope. Notation ">=<^d x" := (>=<^d%O x) : order_scope. -Notation ">=<^d x :> T" := (>=<^d (x : T)) (only parsing) : order_scope. +Notation ">=<^d y :> T" := (>=<^d (y : T)) (only parsing) : order_scope. Notation "x >=<^d y" := (>=<^d%O x y) : order_scope. -Notation "><^d x" := (fun y => ~~ (>=<^d%O x y)) : order_scope. -Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope. +Notation "><^d y" := [pred x | ~~ dual_comparable x y] : order_scope. +Notation "><^d y :> T" := (><^d (y : T)) (only parsing) : order_scope. Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. Notation "x `&^d` y" := (dual_meet x y) : order_scope. @@ -2973,17 +2967,17 @@ 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. +Lemma comparable_minl z : {in >=< z &, forall x y, min x y >=< z}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. -Lemma comparable_minr x y z : z >=< x -> z >=< y -> z >=< min x y. -Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. +Lemma comparable_minr z : {in >=<%O z &, forall x y, z >=< min x y}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. -Lemma comparable_maxl x y z : x >=< z -> y >=< z -> max x y >=< z. -Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. +Lemma comparable_maxl z : {in >=< z &, forall x y, max x y >=< z}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. -Lemma comparable_maxr x y z : z >=< x -> z >=< y -> z >=< max x y. -Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. +Lemma comparable_maxr z : {in >=<%O z &, forall x y, z >=< max x y}. +Proof. by move=> x y cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. Section Comparable2. Variables (z x y : T) (cmp_xy : x >=< y). @@ -3165,7 +3159,7 @@ Lemma comparable_minACA x y z t : Proof. move=> xy xz xt yz yt zt; rewrite comparable_minA// ?comparable_minl//. rewrite [min _ z]comparable_minAC// -comparable_minA// ?comparable_minl//. -by rewrite comparable_sym. +by rewrite inE comparable_sym. Qed. Lemma comparable_maxACA x y z t : @@ -3174,7 +3168,7 @@ Lemma comparable_maxACA x y z t : Proof. move=> xy xz xt yz yt zt; rewrite comparable_maxA// ?comparable_maxl//. rewrite [max _ z]comparable_maxAC// -comparable_maxA// ?comparable_maxl//. -by rewrite comparable_sym. +by rewrite inE comparable_sym. Qed. Lemma comparable_max_minr x y z : x >=< y -> x >=< z -> y >=< z -> @@ -3226,12 +3220,23 @@ Lemma nmono_in_leif (A : {pred T}) (f : T -> T) C : {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}. Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed. -Lemma nmono_leif (f : T -> T) C : - {mono f : x y /~ x <= y} -> +Lemma nmono_leif (f : T -> T) 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 /leif !eq_le !mf. Qed. +Lemma comparable_bigl x x0 op I (P : pred I) F (s : seq I) : + {in >=< x &, forall y z, op y z >=< x} -> x0 >=< x -> + {in P, forall i, F i >=< x} -> \big[op/x0]_(i <- s | P i) F i >=< x. +Proof. by move=> *; elim/big_ind : _. Qed. + +Lemma comparable_bigr x x0 op I (P : pred I) F (s : seq I) : + {in >=<%O x &, forall y z, x >=< op y z} -> x >=< x0 -> + {in P, forall i, x >=< F i} -> x >=< \big[op/x0]_(i <- s | P i) F i. +Proof. by move=> *; elim/big_ind : _. Qed. + End POrderTheory. +Hint Resolve comparable_minr comparable_minl : core. +Hint Resolve comparable_maxr comparable_maxl : core. Section ContraTheory. Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : porderType disp2}. @@ -5785,9 +5790,6 @@ Notation "<^p y :> T" := (<^p (y : T)) (only parsing) : order_scope. Notation ">^p y" := (<^p%O y) : order_scope. Notation ">^p y :> T" := (>^p (y : T)) (only parsing) : order_scope. -Notation ">=<^p y" := (>=<^p%O y) : order_scope. -Notation ">=<^p y :> T" := (>=<^p (y : T)) (only parsing) : order_scope. - Notation "x <=^p y" := (<=^p%O x y) : order_scope. Notation "x <=^p y :> T" := ((x : T) <=^p (y : T)) (only parsing) : order_scope. Notation "x >=^p y" := (y <=^p x) (only parsing) : order_scope. @@ -5807,12 +5809,12 @@ Notation "x <=^p y ?= 'iff' C" := (<?=^p%O x y C) : order_scope. Notation "x <=^p y ?= 'iff' C :> T" := ((x : T) <=^p (y : T) ?= iff C) (only parsing) : order_scope. -Notation ">=<^p x" := (>=<^p%O x) : order_scope. -Notation ">=<^p x :> T" := (>=<^p (x : T)) (only parsing) : order_scope. +Notation ">=<^p y" := [pred x | >=<^p%O x y] : order_scope. +Notation ">=<^p y :> T" := (>=<^p (y : T)) (only parsing) : order_scope. Notation "x >=<^p y" := (>=<^p%O x y) : order_scope. -Notation "><^p x" := (fun y => ~~ (>=<^p%O x y)) : order_scope. -Notation "><^p x :> T" := (><^p (x : T)) (only parsing) : order_scope. +Notation "><^p y" := [pred x | ~~ (>=<^p%O x y)] : order_scope. +Notation "><^p y :> T" := (><^p (y : T)) (only parsing) : order_scope. Notation "x ><^p y" := (~~ (><^p%O x y)) : order_scope. Notation "x `&^p` y" := (@meet prod_display _ x y) : order_scope. @@ -5898,9 +5900,6 @@ Notation "<^l y :> T" := (<^l (y : T)) (only parsing) : order_scope. Notation ">^l y" := (<^l%O y) : order_scope. Notation ">^l y :> T" := (>^l (y : T)) (only parsing) : order_scope. -Notation ">=<^l y" := (>=<^l%O y) : order_scope. -Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope. - Notation "x <=^l y" := (<=^l%O x y) : order_scope. Notation "x <=^l y :> T" := ((x : T) <=^l (y : T)) (only parsing) : order_scope. Notation "x >=^l y" := (y <=^l x) (only parsing) : order_scope. @@ -5920,12 +5919,12 @@ Notation "x <=^l y ?= 'iff' C" := (<?=^l%O x y C) : order_scope. Notation "x <=^l y ?= 'iff' C :> T" := ((x : T) <=^l (y : T) ?= iff C) (only parsing) : order_scope. -Notation ">=<^l x" := (>=<^l%O x) : order_scope. -Notation ">=<^l x :> T" := (>=<^l (x : T)) (only parsing) : order_scope. +Notation ">=<^l y" := [pred x | >=<^l%O x y] : order_scope. +Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope. Notation "x >=<^l y" := (>=<^l%O x y) : order_scope. -Notation "><^l x" := (fun y => ~~ (>=<^l%O x y)) : order_scope. -Notation "><^l x :> T" := (><^l (x : T)) (only parsing) : order_scope. +Notation "><^l y" := [pred x | ~~ (>=<^l%O x y)] : order_scope. +Notation "><^l y :> T" := (><^l (y : T)) (only parsing) : order_scope. Notation "x ><^l y" := (~~ (><^l%O x y)) : order_scope. Notation meetlexi := (@meet lexi_display _). |