Require Import BinPos.
From mathcomp Require choice.
Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import finset interval.
# MathComp extra
This files contains lemmas and definitions missing from MathComp.
```
f \max g := fun x => Num.max (f x) (g x)
f \min g := fun x => Num.min (f x) (g x)
oflit f := Some \o f
pred_oapp T D := [pred x | oapp (mem D) false x]
f \* g := fun x => f x * g x
\- f := fun x => - f x
lteBSide, bnd_simp == multirule to simplify inequalities between
interval bounds
miditv i == middle point of interval i
proj i f == f i, where f : forall i, T i
dfwith f x == fun j => x if j = i, and f j otherwise
given x : T i
swap x := (x.2, x.1)
monotonous A f := {in A &, {mono f : x y / x <= y}} \/
{in A &, {mono f : x y /~ x <= y}}
```
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
MathComp 1.15 additions
Reserved Notation "f \* g" (
at level 40, left associativity).
Reserved Notation "f \- g" (
at level 50, left associativity).
Reserved Notation "\- f" (
at level 35, f at level 35).
Number Notation positive Pos.of_num_int Pos.to_num_uint : AC_scope.
Lemma
all_sig2_cond
{I : Type} {T : Type} (
D
: pred I)
(
P
Q
: I -> T -> Prop)
: T ->
(
forall
x
: I, D x -> {y : T | P x y & Q x y})
->
{f : forall
x
: I, T | forall
x
: I, D x -> P x (
f x)
& forall
x
: I, D x -> Q x (
f x)
}.
Proof.
by move=> /all_sig_cond/[apply]-[f Pf]; exists f => i Di; have [] := Pf i Di.
Qed.
Definition
olift
aT
rT
(
f
: aT -> rT)
:= Some \o f.
Lemma
oapp_comp
aT
rT
sT
(
f
: aT -> rT) (
g
: rT -> sT)
x
:
oapp (
g \o f)
x =1 (
@oapp _ _)
^~ x g \o omap f.
Proof.
by case. Qed.
Lemma
olift_comp
aT
rT
sT
(
f
: aT -> rT) (
g
: rT -> sT)
:
olift (
g \o f)
= olift g \o f.
Proof.
by []. Qed.
Lemma
compA
{A
B
C
D
: Type} (
f
: B -> A) (
g
: C -> B) (
h
: D -> C)
:
f \o (
g \o h)
= (
f \o g)
\o h.
Proof.
by []. Qed.
Lemma
can_in_pcan
[rT
aT
: Type] (
A
: {pred aT})
[f : aT -> rT] [g : rT -> aT] :
{in A, cancel f g} -> {in A, pcancel f (
fun
y
: rT => Some (
g y))
}.
Proof.
by move=> fK x Ax; rewrite fK. Qed.
Lemma
pcan_in_inj
[rT
aT
: Type] [A : {pred aT}] [f : aT -> rT] [g : rT -> option aT] :
{in A, pcancel f g} -> {in A &, injective f}.
Proof.
by move=> fK x y Ax Ay /(
congr1 g)
; rewrite !fK// => -[]. Qed.
Definition
pred_oapp
T
(
D
: {pred T})
: pred (
option T)
:=
[pred
x
| oapp (
mem D)
false x].
Lemma
ocan_in_comp
[A
B
C
: Type] (
D
: {pred B}) (
D'
: {pred C})
[f : B -> option A] [h : C -> option B]
[f' : A -> B] [h' : B -> C] :
{homo h :
x
/ x \in D' >-> x \in pred_oapp D} ->
{in D, ocancel f f'} -> {in D', ocancel h h'} ->
{in D', ocancel (
obind f \o h) (
h' \o f')
}.
Proof.
move=> hD fK hK c cD /=; rewrite -[RHS]hK/=; case hcE : (
h c)
=> [b|]//=.
have bD : b \in D by have := hD _ cD; rewrite hcE inE.
by rewrite -[b in RHS]fK; case: (
f b)
=> //=; have /hK := cD; rewrite hcE.
Qed.
Lemma
eqbRL
(
b1
b2
: bool)
: b1 = b2 -> b2 -> b1.
Proof.
by move->. Qed.
Definition
mul_fun
T
(
R
: ringType) (
f
g
: T -> R)
x
:= (
f x * g x)
%R.
Notation
"f \* g"
:= (
mul_fun f g)
: ring_scope.
Arguments mul_fun {T R} _ _ _ /.
Definition
opp_fun
T
(
R
: zmodType) (
f
: T -> R)
x
:= (
- f x)
%R.
Notation
"\- f"
:= (
opp_fun f)
: ring_scope.
Arguments opp_fun {T R} _ _ /.
Coercion
pair_of_interval
T
(
I
: interval T)
: itv_bound T * itv_bound T :=
let: Interval b1 b2 := I in (
b1, b2).
Import Order.TTheory GRing.Theory Num.Theory.
Section
itv_simp
.
Variables (
d
: unit) (
T
: porderType d).
Implicit Types (
x y : T) (
b : bool).
Lemma
ltBSide
x
y
b
b'
:
((
BSide b x < BSide b' y)
= (
x < y ?<= if b && ~~ b'))
%O.
Proof.
by []. Qed.
Lemma
leBSide
x
y
b
b'
:
((
BSide b x <= BSide b' y)
= (
x < y ?<= if b' ==> b))
%O.
Proof.
by []. Qed.
Definition
lteBSide
:= (
ltBSide, leBSide).
Let
BLeft_ltE
x
y
b
: (
BSide b x < BLeft y)
%O = (
x < y)
%O.
Proof.
by case: b. Qed.
Let
BRight_leE
x
y
b
: (
BSide b x <= BRight y)
%O = (
x <= y)
%O.
Proof.
by case: b. Qed.
Let
BRight_BLeft_leE
x
y
: (
BRight x <= BLeft y)
%O = (
x < y)
%O.
Proof.
by []. Qed.
Let
BLeft_BRight_ltE
x
y
: (
BLeft x < BRight y)
%O = (
x <= y)
%O.
Proof.
by []. Qed.
Let
BRight_BSide_ltE
x
y
b
: (
BRight x < BSide b y)
%O = (
x < y)
%O.
Proof.
by case: b. Qed.
Let
BLeft_BSide_leE
x
y
b
: (
BLeft x <= BSide b y)
%O = (
x <= y)
%O.
Proof.
by case: b. Qed.
Let
BSide_ltE
x
y
b
: (
BSide b x < BSide b y)
%O = (
x < y)
%O.
Proof.
by case: b. Qed.
Let
BSide_leE
x
y
b
: (
BSide b x <= BSide b y)
%O = (
x <= y)
%O.
Proof.
by case: b. Qed.
Let
BInfty_leE
a
: (
a <= BInfty T false)
%O
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_geE
a
: (
BInfty T true <= a)
%O
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_le_eqE
a
: (
BInfty T false <= a)
%O = (
a == BInfty T false).
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_ge_eqE
a
: (
a <= BInfty T true)
%O = (
a == BInfty T true).
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_ltE
a
: (
a < BInfty T false)
%O = (
a != BInfty T false).
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_gtE
a
: (
BInfty T true < a)
%O = (
a != BInfty T true).
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_ltF
a
: (
BInfty T false < a)
%O = false.
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_gtF
a
: (
a < BInfty T true)
%O = false.
Proof.
by case: a => [[] a|[]]. Qed.
Let
BInfty_BInfty_ltE
: (
BInfty T true < BInfty T false)
%O
Proof.
by []. Qed.
Lemma
ltBRight_leBLeft
(
a
: itv_bound T) (
r
: T)
:
(
a < BRight r)
%O = (
a <= BLeft r)
%O.
Proof.
by move: a => [[] a|[]]. Qed.
Lemma
leBRight_ltBLeft
(
a
: itv_bound T) (
r
: T)
:
(
BRight r <= a)
%O = (
BLeft r < a)
%O.
Proof.
by move: a => [[] a|[]]. Qed.
Definition
bnd_simp
:= (
BLeft_ltE, BRight_leE,
BRight_BLeft_leE, BLeft_BRight_ltE,
BRight_BSide_ltE, BLeft_BSide_leE, BSide_ltE, BSide_leE,
BInfty_leE, BInfty_geE, BInfty_BInfty_ltE,
BInfty_le_eqE, BInfty_ge_eqE, BInfty_ltE, BInfty_gtE, BInfty_ltF, BInfty_gtF,
@lexx _ T, @ltxx _ T, @eqxx T).
Lemma
itv_splitU1
(
a
: itv_bound T) (
x
: T)
: (
a <= BLeft x)
%O ->
Interval a (
BRight x)
=i [predU1 x & Interval a (
BLeft x)
].
Proof.
move=> ax z; rewrite !inE/= !subitvE ?bnd_simp//= lt_neqAle.
by case: (
eqVneq z x)
=> [->|]//=; rewrite lexx ax.
Qed.
Lemma
itv_split1U
(
a
: itv_bound T) (
x
: T)
: (
BRight x <= a)
%O ->
Interval (
BLeft x)
a =i [predU1 x & Interval (
BRight x)
a].
Proof.
move=> ax z; rewrite !inE/= !subitvE ?bnd_simp//= lt_neqAle.
by case: (
eqVneq z x)
=> [->|]//=; rewrite lexx ax.
Qed.
End itv_simp.
Definition
miditv
(
R
: numDomainType) (
i
: interval R)
: R :=
match i with
| Interval (
BSide _ a) (
BSide _ b)
=> (
a + b)
/ 2%:R
| Interval -oo%O (
BSide _ b)
=> b - 1
| Interval (
BSide _ a)
+oo%O => a + 1
| Interval -oo%O +oo%O => 0
| _ => 0
end.
Section
miditv_lemmas
.
Variable
R
: numFieldType.
Implicit Types i : interval R.
Lemma
mem_miditv
i
: (
i.
1 < i.
2)
%O -> miditv i \in i.
Proof.
Lemma
miditv_le_left
i
b
: (
i.
1 < i.
2)
%O -> (
BSide b (
miditv i)
<= i.
2)
%O.
Proof.
case: i => [x y] lti; have := mem_miditv lti; rewrite inE => /andP[_ ].
by apply: le_trans; rewrite !bnd_simp.
Qed.
Lemma
miditv_ge_right
i
b
: (
i.
1 < i.
2)
%O -> (
i.
1 <= BSide b (
miditv i))
%O.
Proof.
case: i => [x y] lti; have := mem_miditv lti; rewrite inE => /andP[+ _].
by move=> /le_trans; apply; rewrite !bnd_simp.
Qed.
End miditv_lemmas.
Section
itv_porderType
.
Variables (
d
: unit) (
T
: orderType d).
Implicit Types (
a : itv_bound T) (
x y : T) (
i j : interval T) (
b : bool).
Lemma
predC_itvl
a
: [predC Interval -oo%O a] =i Interval a +oo%O.
Proof.
Lemma
predC_itvr
a
: [predC Interval a +oo%O] =i Interval -oo%O a.
Proof.
by move=> y; rewrite inE/= -predC_itvl negbK. Qed.
Lemma
predC_itv
i
: [predC i] =i [predU Interval -oo%O i.
1 & Interval i.
2 +oo%O].
Proof.
End itv_porderType.
Lemma
sumr_le0
(
R
: numDomainType)
I
(
r
: seq I) (
P
: pred I) (
F
: I -> R)
:
(
forall
i,
P i -> F i <= 0)
%R -> (
\sum_(
i
<- r | P i)
F i <= 0)
%R.
Proof.
by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_naddl/F0. Qed.
Lemma
enum_ord0
: enum 'I_0 = [::].
Proof.
Lemma
enum_ordSr
n
: enum 'I_n.
+1 =
rcons (
map (
widen_ord (
leqnSn _)) (
enum 'I_n))
ord_max.
Proof.
Lemma
obindEapp
{aT
rT}
(
f
: aT -> option rT)
: obind f = oapp f None.
Proof.
by []. Qed.
Lemma
omapEbind
{aT
rT}
(
f
: aT -> rT)
: omap f = obind (
olift f).
Proof.
by []. Qed.
Lemma
omapEapp
{aT
rT}
(
f
: aT -> rT)
: omap f = oapp (
olift f)
None.
Proof.
by []. Qed.
Lemma
oappEmap
{aT
rT}
(
f
: aT -> rT) (
y0
: rT)
x
:
oapp f y0 x = odflt y0 (
omap f x).
Proof.
by case: x. Qed.
Lemma
omap_comp
aT
rT
sT
(
f
: aT -> rT) (
g
: rT -> sT)
:
omap (
g \o f)
=1 omap g \o omap f.
Proof.
by case. Qed.
Lemma
oapp_comp_f
{aT
rT
sT}
(
f
: aT -> rT) (
g
: rT -> sT) (
x
: rT)
:
oapp (
g \o f) (
g x)
=1 g \o oapp f x.
Proof.
by case. Qed.
Lemma
can_in_comp
[A
B
C
: Type] (
D
: {pred B}) (
D'
: {pred C})
[f : B -> A] [h : C -> B]
[f' : A -> B] [h' : B -> C] :
{homo h :
x
/ x \in D' >-> x \in D} ->
{in D, cancel f f'} -> {in D', cancel h h'} ->
{in D', cancel (
f \o h) (
h' \o f')
}.
Proof.
by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed.
Lemma
in_inj_comp
A
B
C
(
f
: B -> A) (
h
: C -> B) (
P
: pred B) (
Q
: pred C)
:
{in P &, injective f} -> {in Q &, injective h} -> {homo h :
x
/ Q x >-> P x} ->
{in Q &, injective (
f \o h)
}.
Proof.
by move=> Pf Qh QP x y xQ yQ xy; apply Qh => //; apply Pf => //; apply QP.
Qed.
Lemma
pcan_in_comp
[A
B
C
: Type] (
D
: {pred B}) (
D'
: {pred C})
[f : B -> A] [h : C -> B]
[f' : A -> option B] [h' : B -> option C] :
{homo h :
x
/ x \in D' >-> x \in D} ->
{in D, pcancel f f'} -> {in D', pcancel h h'} ->
{in D', pcancel (
f \o h) (
obind h' \o f')
}.
Proof.
by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed.
Lemma
ocan_comp
[A
B
C
: Type] [f : B -> option A] [h : C -> option B]
[f' : A -> B] [h' : B -> C] :
ocancel f f' -> ocancel h h' -> ocancel (
obind f \o h) (
h' \o f').
Proof.
move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (
h c)
=> [b|]//=.
by rewrite -[b in RHS]fK; case: (
f b)
=> //=; have := hK c; rewrite hcE.
Qed.
Lemma
eqbLR
(
b1
b2
: bool)
: b1 = b2 -> b1 -> b2.
Proof.
by move->. Qed.
Lemma
gtr_opp
(
R
: numDomainType) (
r
: R)
: (
0 < r)
%R -> (
- r < r)
%R.
Proof.
Lemma
le_le_trans
{disp : unit} {T : porderType disp} (
x
y
z
t
: T)
:
(
z <= x)
%O -> (
y <= t)
%O -> (
x <= y)
%O -> (
z <= t)
%O.
Proof.
Notation
eqLHS
:= (
X
in (
X == _))
%pattern.
Notation
eqRHS
:= (
X
in (
_ == X))
%pattern.
Notation
leLHS
:= (
X
in (
X <= _)
%O)
%pattern.
Notation
leRHS
:= (
X
in (
_ <= X)
%O)
%pattern.
Notation
ltLHS
:= (
X
in (
X < _)
%O)
%pattern.
Notation
ltRHS
:= (
X
in (
_ < X)
%O)
%pattern.
Inductive
boxed
T
:=
Box
of T.
Lemma
eq_bigl_supp
[R : eqType] [idx : R] [op : Monoid.law idx] [I : Type]
[r : seq I] [P1 : pred I] (
P2
: pred I) (
F
: I -> R)
:
{in [pred
x
| F x != idx], P1 =1 P2} ->
\big[op/idx]_(
i
<- r | P1 i)
F i = \big[op/idx]_(
i
<- r | P2 i)
F i.
Proof.
move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _.
by case: (
eqVneq (
F i)
idx)
=> [->|/P12->]; rewrite ?if_same.
Qed.
Lemma
perm_big_supp_cond
[R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType]
[r
s
: seq I] [P : pred I] (
F
: I -> R)
:
perm_eq [seq
i
<- r | P i && (
F i != idx)
] [seq
i
<- s | P i && (
F i != idx)
] ->
\big[op/idx]_(
i
<- r | P i)
F i = \big[op/idx]_(
i
<- s| P i)
F i.
Proof.
Lemma
perm_big_supp
[R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType]
[r
s
: seq I] [P : pred I] (
F
: I -> R)
:
perm_eq [seq
i
<- r | (
F i != idx)
] [seq
i
<- s | (
F i != idx)
] ->
\big[op/idx]_(
i
<- r | P i)
F i = \big[op/idx]_(
i
<- s| P i)
F i.
Proof.
Local Open Scope order_scope.
Local Open Scope ring_scope.
Import GRing.Theory Order.TTheory.
Lemma
mulr_ge0_gt0
(
R
: numDomainType) (
x
y
: R)
: 0 <= x -> 0 <= y ->
(
0 < x * y)
= (
0 < x)
&& (
0 < y).
Proof.
Section
lt_le_gt_ge
.
Variable (
R
: numFieldType).
Implicit Types x y z a b : R.
Lemma
splitr
x
: x = x / 2%:R + x / 2%:R.
Proof.
Lemma
ler_addgt0Pr
x
y
: reflect (
forall
e,
e > 0 -> x <= y + e) (
x <= y).
Proof.
Lemma
ler_addgt0Pl
x
y
: reflect (
forall
e,
e > 0 -> x <= e + y) (
x <= y).
Proof.
Lemma
in_segment_addgt0Pr
x
y
z
:
reflect (
forall
e,
e > 0 -> y \in `[x - e, z + e]) (
y \in `[x, z]).
Proof.
Lemma
in_segment_addgt0Pl
x
y
z
:
reflect (
forall
e,
e > 0 -> y \in `[(
- e + x)
, (
e + z)
]) (
y \in `[x, z]).
Proof.
Lemma
lt_le
a
b
: (
forall
x,
x < a -> x < b)
-> a <= b.
Proof.
move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -ler_subl_addr ltW//.
by rewrite ab // ltr_subl_addr -ltr_subl_addl subrr.
Qed.
Lemma
gt_ge
a
b
: (
forall
x,
b < x -> a < x)
-> a <= b.
Proof.
move=> ab; apply/ler_addgt0Pr => e e_gt0.
by rewrite ltW// ab// -ltr_subl_addl subrr.
Qed.
End lt_le_gt_ge.
Lemma
itvxx
d
(
T
: porderType d) (
x
: T)
: `[x, x] =i pred1 x.
Proof.
Lemma
itvxxP
d
(
T
: porderType d) (
x
y
: T)
: reflect (
y = x) (
y \in `[x, x]).
Proof.
by rewrite itvxx; apply/eqP. Qed.
Lemma
subset_itv_oo_cc
d
(
T
: porderType d) (
a
b
: T)
: {subset `]a, b[ <= `[a, b]}.
Proof.
End of MathComp 1.15 additions
Reserved Notation "`1- r" (format "`1- r", at level 2).
Reserved Notation "f \^-1" (at level 3, format "f \^-1", left associativity).
Lemma
natr1
(
R
: ringType) (
n
: nat)
: (
n%:R + 1 = n.
+1%:R :> R)
%R.
Proof.
Lemma
nat1r
(
R
: ringType) (
n
: nat)
: (
1 + n%:R = n.
+1%:R :> R)
%R.
Proof.
Lemma
fset_nat_maximum
(
X
: choiceType) (
A
: {fset X})
(
f
: X -> nat)
: A != fset0 ->
(
exists
i,
i \in A /\ forall
j,
j \in A -> f j <= f i)
%nat.
Proof.
move=> /fset0Pn[x Ax].
have [/= y _ /(
_ _ isT)
mf] := @arg_maxnP _ [` Ax]%fset xpredT (
f \o val)
isT.
exists (
val y)
; split; first exact: valP.
by move=> z Az; have := mf [` Az]%fset.
Qed.
Lemma
image_nat_maximum
n
(
f
: nat -> nat)
:
(
exists
i,
i <= n /\ forall
j,
j <= n -> f j <= f i)
%N.
Proof.
have [i _ /(
_ _ isT)
mf] := @arg_maxnP _ (
@ord0 n)
xpredT f isT.
by exists i; split; rewrite ?leq_ord// => j jn; have := mf (
@Ordinal n.
+1 j jn).
Qed.
Lemma
card_fset_sum1
(
T
: choiceType) (
A
: {fset T})
:
#|` A| = (
\sum_(
i
<- A)
1)
%N.
Proof.
Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.
MathComp 1.16.0 additions
Section
bigminr_maxr
.
Import Num.Def.
Lemma
bigminr_maxr
(
R
: realDomainType)
I
r
(
P
: pred I) (
F
: I -> R)
x
:
\big[minr/x]_(
i
<- r | P i)
F i = - \big[maxr/- x]_(
i
<- r | P i)
- F i.
Proof.
by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK.
Qed.
End bigminr_maxr.
Section
SemiGroupProperties
.
Variables (
R
: Type) (
op
: R -> R -> R).
Hypothesis
opA
: associative op.
Definition
AC_subdef
of associative op & commutative op :=
fun
x
=> oapp (
fun
y
=> Some (
oapp (
op^~ y)
y x))
x.
Definition
oAC
:= nosimpl AC_subdef.
Hypothesis
opC
: commutative op.
Let
opCA
: left_commutative op
Proof.
by move=> x *; rewrite !opA (
opC x). Qed.
Let
opAC
: right_commutative op.
Proof.
by move=> *; rewrite -!opA [X in op _ X]opC. Qed.
Hypothesis
opyy
: idempotent op.
Local Notation
oop
:= (
oAC opA opC).
Lemma
opACE
x
y
: oop (
Some x) (
Some y)
= some (
op x y)
Proof.
by []. Qed.
Lemma
oopA_subdef
: associative oop.
Proof.
by move=> [x|] [y|] [z|]//; rewrite /oAC/= opA. Qed.
Lemma
oopx1_subdef
: left_id None oop
Proof.
by case. Qed.
Lemma
oop1x_subdef
: right_id None oop
Proof.
by []. Qed.
Lemma
oopC_subdef
: commutative oop.
Proof.
by move=> [x|] [y|]//; rewrite /oAC/= opC. Qed.
Canonical
opAC_law
:= Monoid.Law oopA_subdef oopx1_subdef oop1x_subdef.
Canonical
opAC_com_law
:= Monoid.ComLaw oopC_subdef.
Context [x : R].
Lemma
some_big_AC
[I : Type]
r
P
(
F
: I -> R)
:
Some (
\big[op/x]_(
i
<- r | P i)
F i)
=
oop (
\big[oop/None]_(
i
<- r | P i)
Some (
F i)) (
Some x).
Proof.
by elim/big_rec2 : _ => //= i [y|] _ Pi [] -> //=; rewrite opA. Qed.
Lemma
big_ACE
[I : Type]
r
P
(
F
: I -> R)
:
\big[op/x]_(
i
<- r | P i)
F i =
odflt x (
oop (
\big[oop/None]_(
i
<- r | P i)
Some (
F i)) (
Some x)).
Proof.
Lemma
big_undup_AC
[I : eqType]
r
P
(
F
: I -> R) (
opK
: idempotent op)
:
\big[op/x]_(
i
<- undup r | P i)
F i = \big[op/x]_(
i
<- r | P i)
F i.
Proof.
by rewrite !big_ACE !big_undup//; case=> //= ?; rewrite /oAC/= opK. Qed.
Lemma
perm_big_AC
[I : eqType] [r]
s
[P : pred I] [F : I -> R] :
perm_eq r s -> \big[op/x]_(
i
<- r | P i)
F i = \big[op/x]_(
i
<- s | P i)
F i.
Proof.
by rewrite !big_ACE => /(@perm_big _ _)->. Qed.
Section
Id
.
Hypothesis
opxx
: op x x = x.
Lemma
big_const_idem
I
(
r
: seq I)
P
: \big[op/x]_(
i
<- r | P i)
x = x.
Proof.
by elim/big_ind : _ => // _ _ -> ->. Qed.
Lemma
big_id_idem
I
(
r
: seq I)
P
F
:
op (
\big[op/x]_(
i
<- r | P i)
F i)
x = \big[op/x]_(
i
<- r | P i)
F i.
Proof.
by elim/big_rec : _ => // ? ? ?; rewrite -opA => ->. Qed.
Lemma
big_mkcond_idem
I
r
(
P
: pred I)
F
:
\big[op/x]_(
i
<- r | P i)
F i = \big[op/x]_(
i
<- r) (
if P i then F i else x).
Proof.
Lemma
big_split_idem
I
r
(
P
: pred I)
F1
F2
:
\big[op/x]_(
i
<- r | P i)
op (
F1 i) (
F2 i)
=
op (
\big[op/x]_(
i
<- r | P i)
F1 i) (
\big[op/x]_(
i
<- r | P i)
F2 i).
Proof.
by elim/big_rec3 : _ => [//|i ? ? _ _ ->]; rewrite // opCA -!opA opCA. Qed.
Lemma
big_id_idem_AC
I
(
r
: seq I)
P
F
:
\big[op/x]_(
i
<- r | P i)
op (
F i)
x = \big[op/x]_(
i
<- r | P i)
F i.
Proof.
Lemma
bigID_idem
I
r
(
a
P
: pred I)
F
:
\big[op/x]_(
i
<- r | P i)
F i =
op (
\big[op/x]_(
i
<- r | P i && a i)
F i)
(
\big[op/x]_(
i
<- r | P i && ~~ a i)
F i).
Proof.
End Id.
Lemma
big_rem_AC
(
I
: eqType) (
r
: seq I)
z
(
P
: pred I)
F
: z \in r ->
\big[op/x]_(
y
<- r | P y)
F y =
if P z then op (
F z) (
\big[op/x]_(
y
<- rem z r | P y)
F y)
else \big[op/x]_(
y
<- rem z r | P y)
F y.
Proof.
by move=> /[!big_ACE] /(
big_rem _)
->//; case: ifP; case: (
bigop _ _ _)
=> /=.
Qed.
Lemma
bigD1_AC
(
I
: finType)
j
(
P
: pred I)
F
: P j ->
\big[op/x]_(
i
| P i)
F i = op (
F j) (
\big[op/x]_(
i
| P i && (
i != j))
F i).
Proof.
by move=> /[!big_ACE] /(
bigD1 _)
->; case: (
bigop _ _)
=> /=. Qed.
Variable
le
: rel R.
Hypothesis
le_refl
: reflexive le.
Hypothesis
op_incr
: forall
x
y,
le x (
op x y).
Lemma
sub_big
I
[s] (
P
P'
: {pred I}) (
F
: I -> R)
: (
forall
i,
P i -> P' i)
->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s | P' i)
F i).
Proof.
Lemma
sub_big_seq
(
I
: eqType)
s
s'
P
(
F
: I -> R)
:
(
forall
i,
count_mem i s <= count_mem i s')
%N ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s' | P i)
F i).
Proof.
Lemma
sub_big_seq_cond
(
I
: eqType)
s
s'
P
P'
(
F
: I -> R)
:
(
forall
i,
count_mem i (
filter P s)
<= count_mem i (
filter P' s'))
%N ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s' | P' i)
F i).
Proof.
Lemma
uniq_sub_big
(
I
: eqType)
s
s'
P
(
F
: I -> R)
: uniq s -> uniq s' ->
{subset s <= s'} ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s' | P i)
F i).
Proof.
move=> us us' ss'; rewrite sub_big_seq => // i; rewrite !count_uniq_mem//.
by have /implyP := ss' i; case: (
_ \in s) (
_ \in s')
=> [] [].
Qed.
Lemma
uniq_sub_big_cond
(
I
: eqType)
s
s'
P
P'
(
F
: I -> R)
:
uniq (
filter P s)
-> uniq (
filter P' s')
->
{subset [seq
i
<- s | P i] <= [seq
i
<- s' | P' i]} ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s' | P' i)
F i).
Proof.
Lemma
sub_big_idem
(
I
: eqType)
s
s'
P
(
F
: I -> R)
:
{subset s <= s'} ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s' | P i)
F i).
Proof.
Lemma
sub_big_idem_cond
(
I
: eqType)
s
s'
P
P'
(
F
: I -> R)
:
{subset [seq
i
<- s | P i] <= [seq
i
<- s' | P' i]} ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s' | P' i)
F i).
Proof.
Lemma
sub_in_big
[I : eqType] (
s
: seq I) (
P
P'
: {pred I}) (
F
: I -> R)
:
{in s, forall
i,
P i -> P' i} ->
le (
\big[op/x]_(
i
<- s | P i)
F i) (
\big[op/x]_(
i
<- s | P' i)
F i).
Proof.
Lemma
le_big_ord
n
m
[P : {pred nat}] [F : nat -> R] : (
n <= m)
%N ->
le (
\big[op/x]_(
i
< n | P i)
F i) (
\big[op/x]_(
i
< m | P i)
F i).
Proof.
Lemma
subset_big
[I : finType] [A
A'
P
: {pred I}] (
F
: I -> R)
:
A \subset A' ->
le (
\big[op/x]_(
i
in A | P i)
F i) (
\big[op/x]_(
i
in A' | P i)
F i).
Proof.
move=> AA'; apply: sub_big => y /andP[yA yP]; apply/andP; split => //.
exact: subsetP yA.
Qed.
Lemma
subset_big_cond
(
I
: finType) (
A
A'
P
P'
: {pred I}) (
F
: I -> R)
:
[set
i
in A | P i] \subset [set
i
in A' | P' i] ->
le (
\big[op/x]_(
i
in A | P i)
F i) (
\big[op/x]_(
i
in A' | P' i)
F i).
Proof.
by move=> /subsetP AP; apply: sub_big => i; have /[!inE] := AP i. Qed.
Lemma
le_big_nat_cond
n
m
n'
m'
(
P
P'
: {pred nat}) (
F
: nat -> R)
:
(
n' <= n)
%N -> (
m <= m')
%N -> (
forall
i,
(
n <= i < m)
%N -> P i -> P' i)
->
le (
\big[op/x]_(
n <=
i
< m | P i)
F i) (
\big[op/x]_(
n' <=
i
< m' | P' i)
F i).
Proof.
move=> len'n lemm' PP'i; rewrite uniq_sub_big_cond ?filter_uniq ?iota_uniq//.
move=> i; rewrite !mem_filter !mem_index_iota => /and3P[Pi ni im].
by rewrite PP'i ?ni//= (
leq_trans _ ni)
// (
leq_trans im).
Qed.
Lemma
le_big_nat
n
m
n'
m'
[P] [F : nat -> R] : (
n' <= n)
%N -> (
m <= m')
%N ->
le (
\big[op/x]_(
n <=
i
< m | P i)
F i) (
\big[op/x]_(
n' <=
i
< m' | P i)
F i).
Proof.
Lemma
le_big_ord_cond
n
m
(
P
P'
: {pred nat}) (
F
: nat -> R)
:
(
n <= m)
%N -> (
forall
i
: 'I_n, P i -> P' i)
->
le (
\big[op/x]_(
i
< n | P i)
F i) (
\big[op/x]_(
i
< m | P' i)
F i).
Proof.
End SemiGroupProperties.
Section
bigmaxmin
.
Local Notation
max
:= Order.max.
Local Notation
min
:= Order.min.
Local Open Scope order_scope.
Variables (
d
: _) (
T
: porderType d).
Variables (
I
: Type) (
r
: seq I) (
f
: I -> T) (
x0
x
: T) (
P
: pred I).
Lemma
bigmax_le
:
x0 <= x -> (
forall
i,
P i -> f i <= x)
-> \big[max/x0]_(
i
<- r | P i)
f i <= x.
Proof.
by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed.
Lemma
bigmax_lt
:
x0 < x -> (
forall
i,
P i -> f i < x)
-> \big[max/x0]_(
i
<- r | P i)
f i < x.
Proof.
by move=> ? ?; elim/big_ind: _ => // *; rewrite maxElt; case: ifPn. Qed.
Lemma
lt_bigmin
:
x < x0 -> (
forall
i,
P i -> x < f i)
-> x < \big[min/x0]_(
i
<- r | P i)
f i.
Proof.
by move=> ? ?; elim/big_ind: _ => // *; rewrite minElt; case: ifPn. Qed.
Lemma
le_bigmin
:
x <= x0 -> (
forall
i,
P i -> x <= f i)
-> x <= \big[min/x0]_(
i
<- r | P i)
f i.
Proof.
by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed.
End bigmaxmin.
Section
bigmax
.
Local Notation
max
:= Order.max.
Local Open Scope order_scope.
Variables (
d
: unit) (
T
: orderType d).
Section
bigmax_Type
.
Variables (
I
: Type) (
r
: seq I) (
x
: T).
Implicit Types (
P a : pred I) (
F : I -> T).
Lemma
bigmax_mkcond
P
F
: \big[max/x]_(
i
<- r | P i)
F i =
\big[max/x]_(
i
<- r) (
if P i then F i else x).
Proof.
Lemma
bigmax_split
P
F1
F2
:
\big[max/x]_(
i
<- r | P i) (
max (
F1 i) (
F2 i))
=
max (
\big[max/x]_(
i
<- r | P i)
F1 i) (
\big[max/x]_(
i
<- r | P i)
F2 i).
Proof.
Lemma
bigmax_idl
P
F
:
\big[max/x]_(
i
<- r | P i)
F i = max x (
\big[max/x]_(
i
<- r | P i)
F i).
Proof.
Lemma
bigmax_idr
P
F
:
\big[max/x]_(
i
<- r | P i)
F i = max (
\big[max/x]_(
i
<- r | P i)
F i)
x.
Proof.
by rewrite [LHS]bigmax_idl maxC. Qed.
Lemma
bigmaxID
a
P
F
: \big[max/x]_(
i
<- r | P i)
F i =
max (
\big[max/x]_(
i
<- r | P i && a i)
F i)
(
\big[max/x]_(
i
<- r | P i && ~~ a i)
F i).
Proof.
End bigmax_Type.
Let
le_maxr_id
(
x
y
: T)
: x <= max x y
Proof.
Lemma
sub_bigmax
[x0]
I
s
(
P
P'
: {pred I}) (
F
: I -> T)
:
(
forall
i,
P i -> P' i)
->
\big[max/x0]_(
i
<- s | P i)
F i <= \big[max/x0]_(
i
<- s | P' i)
F i.
Proof.
Lemma
sub_bigmax_seq
[x0] (
I
: eqType)
s
s'
P
(
F
: I -> T)
: {subset s <= s'} ->
\big[max/x0]_(
i
<- s | P i)
F i <= \big[max/x0]_(
i
<- s' | P i)
F i.
Proof.
Lemma
sub_bigmax_cond
[x0] (
I
: eqType)
s
s'
P
P'
(
F
: I -> T)
:
{subset [seq
i
<- s | P i] <= [seq
i
<- s' | P' i]} ->
\big[max/x0]_(
i
<- s | P i)
F i <= \big[max/x0]_(
i
<- s' | P' i)
F i.
Proof.
Lemma
sub_in_bigmax
[x0] [I : eqType] (
s
: seq I) (
P
P'
: {pred I}) (
F
: I -> T)
:
{in s, forall
i,
P i -> P' i} ->
\big[max/x0]_(
i
<- s | P i)
F i <= \big[max/x0]_(
i
<- s | P' i)
F i.
Proof.
Lemma
le_bigmax_nat
[x0]
n
m
n'
m'
P
(
F
: nat -> T)
: n' <= n -> m <= m' ->
\big[max/x0]_(
n <=
i
< m | P i)
F i <= \big[max/x0]_(
n' <=
i
< m' | P i)
F i.
Proof.
Lemma
le_bigmax_nat_cond
[x0]
n
m
n'
m'
(
P
P'
: {pred nat}) (
F
: nat -> T)
:
(
n' <= n)
%N -> (
m <= m')
%N -> (
forall
i,
n <= i < m -> P i -> P' i)
->
\big[max/x0]_(
n <=
i
< m | P i)
F i <= \big[max/x0]_(
n' <=
i
< m' | P' i)
F i.
Proof.
Lemma
le_bigmax_ord
[x0]
n
m
(
P
: {pred nat}) (
F
: nat -> T)
: (
n <= m)
%N ->
\big[max/x0]_(
i
< n | P i)
F i <= \big[max/x0]_(
i
< m | P i)
F i.
Proof.
Lemma
le_bigmax_ord_cond
[x0]
n
m
(
P
P'
: {pred nat}) (
F
: nat -> T)
:
(
n <= m)
%N -> (
forall
i
: 'I_n, P i -> P' i)
->
\big[max/x0]_(
i
< n | P i)
F i <= \big[max/x0]_(
i
< m | P' i)
F i.
Proof.
Lemma
subset_bigmax
[x0] [I : finType] (
A
A'
P
: {pred I}) (
F
: I -> T)
:
A \subset A' ->
\big[max/x0]_(
i
in A | P i)
F i <= \big[max/x0]_(
i
in A' | P i)
F i.
Proof.
Lemma
subset_bigmax_cond
[x0] (
I
: finType) (
A
A'
P
P'
: {pred I}) (
F
: I -> T)
:
[set
i
in A | P i] \subset [set
i
in A' | P' i] ->
\big[max/x0]_(
i
in A | P i)
F i <= \big[max/x0]_(
i
in A' | P' i)
F i.
Proof.
Section
bigmax_finType
.
Variables (
I
: finType) (
x
: T).
Implicit Types (
P : pred I) (
F : I -> T).
Lemma
bigmaxD1
j
P
F
: P j ->
\big[max/x]_(
i
| P i)
F i = max (
F j) (
\big[max/x]_(
i
| P i && (
i != j))
F i).
Proof.
Lemma
le_bigmax_cond
j
P
F
: P j -> F j <= \big[max/x]_(
i
| P i)
F i.
Proof.
Lemma
le_bigmax
F
j
: F j <= \big[max/x]_i F i.
Proof.
Lemma
bigmax_sup
j
P
m
F
: P j -> m <= F j -> m <= \big[max/x]_(
i
| P i)
F i.
Proof.
Lemma
bigmax_leP
m
P
F
: reflect (
x <= m /\ forall
i,
P i -> F i <= m)
(
\big[max/x]_(
i
| P i)
F i <= m).
Proof.
Lemma
bigmax_ltP
m
P
F
:
reflect (
x < m /\ forall
i,
P i -> F i < m) (
\big[max/x]_(
i
| P i)
F i < m).
Proof.
Lemma
bigmax_eq_arg
j
P
F
: P j -> (
forall
i,
P i -> x <= F i)
->
\big[max/x]_(
i
| P i)
F i = F [arg max_(
i
> j | P i)
F i].
Proof.
Lemma
eq_bigmax
j
P
F
: P j -> (
forall
i,
P i -> x <= F i)
->
{i0 | i0 \in P & \big[max/x]_(
i
| P i)
F i = F i0}.
Proof.
by move=> Pi0 Hx; rewrite (
bigmax_eq_arg Pi0)
//; eexists => //; case:arg_maxP.
Qed.
Lemma
le_bigmax2
P
F1
F2
: (
forall
i,
P i -> F1 i <= F2 i)
->
\big[max/x]_(
i
| P i)
F1 i <= \big[max/x]_(
i
| P i)
F2 i.
Proof.
move=> FG; elim/big_ind2 : _ => // a b e f ba fe.
rewrite le_maxr 2!le_maxl ba fe /= andbT; have [//|/= af] := leP f a.
by rewrite (
le_trans ba)
// (
le_trans _ fe)
// ltW.
Qed.
End bigmax_finType.
End bigmax.
Arguments bigmax_mkcond {d T I r}.
Arguments bigmaxID {d T I r}.
Arguments bigmaxD1 {d T I x} j.
Arguments bigmax_sup {d T I x} j.
Arguments bigmax_eq_arg {d T I} x j.
Arguments eq_bigmax {d T I x} j.
Section
bigmin
.
Local Notation
min
:= Order.min.
Local Open Scope order_scope.
Variables (
d
: _) (
T
: orderType d).
Section
bigmin_Type
.
Variable (
I
: Type) (
r
: seq I) (
x
: T).
Implicit Types (
P a : pred I) (
F : I -> T).
Lemma
bigmin_mkcond
P
F
: \big[min/x]_(
i
<- r | P i)
F i =
\big[min/x]_(
i
<- r) (
if P i then F i else x).
Proof.
Lemma
bigmin_split
P
F1
F2
:
\big[min/x]_(
i
<- r | P i) (
min (
F1 i) (
F2 i))
=
min (
\big[min/x]_(
i
<- r | P i)
F1 i) (
\big[min/x]_(
i
<- r | P i)
F2 i).
Proof.
Lemma
bigmin_idl
P
F
:
\big[min/x]_(
i
<- r | P i)
F i = min x (
\big[min/x]_(
i
<- r | P i)
F i).
Proof.
Lemma
bigmin_idr
P
F
:
\big[min/x]_(
i
<- r | P i)
F i = min (
\big[min/x]_(
i
<- r | P i)
F i)
x.
Proof.
by rewrite [LHS]bigmin_idl minC. Qed.
Lemma
bigminID
a
P
F
: \big[min/x]_(
i
<- r | P i)
F i =
min (
\big[min/x]_(
i
<- r | P i && a i)
F i)
(
\big[min/x]_(
i
<- r | P i && ~~ a i)
F i).
Proof.
End bigmin_Type.
Let
le_minr_id
(
x
y
: T)
: x >= min x y
Proof.
Lemma
sub_bigmin
[x0]
I
s
(
P
P'
: {pred I}) (
F
: I -> T)
:
(
forall
i,
P' i -> P i)
->
\big[min/x0]_(
i
<- s | P i)
F i <= \big[min/x0]_(
i
<- s | P' i)
F i.
Proof.
Lemma
sub_bigmin_cond
[x0] (
I
: eqType)
s
s'
P
P'
(
F
: I -> T)
:
{subset [seq
i
<- s | P i] <= [seq
i
<- s' | P' i]} ->
\big[min/x0]_(
i
<- s' | P' i)
F i <= \big[min/x0]_(
i
<- s | P i)
F i.
Proof.
Lemma
sub_bigmin_seq
[x0] (
I
: eqType)
s
s'
P
(
F
: I -> T)
: {subset s' <= s} ->
\big[min/x0]_(
i
<- s | P i)
F i <= \big[min/x0]_(
i
<- s' | P i)
F i.
Proof.
Lemma
sub_in_bigmin
[x0] [I : eqType] (
s
: seq I) (
P
P'
: {pred I}) (
F
: I -> T)
:
{in s, forall
i,
P' i -> P i} ->
\big[min/x0]_(
i
<- s | P i)
F i <= \big[min/x0]_(
i
<- s | P' i)
F i.
Proof.
Lemma
le_bigmin_nat
[x0]
n
m
n'
m'
P
(
F
: nat -> T)
:
(
n <= n')
%N -> (
m' <= m)
%N ->
\big[min/x0]_(
n <=
i
< m | P i)
F i <= \big[min/x0]_(
n' <=
i
< m' | P i)
F i.
Proof.
Lemma
le_bigmin_nat_cond
[x0]
n
m
n'
m'
(
P
P'
: pred nat) (
F
: nat -> T)
:
(
n <= n')
%N -> (
m' <= m)
%N -> (
forall
i,
n' <= i < m' -> P' i -> P i)
->
\big[min/x0]_(
n <=
i
< m | P i)
F i <= \big[min/x0]_(
n' <=
i
< m' | P' i)
F i.
Proof.
Lemma
le_bigmin_ord
[x0]
n
m
(
P
: pred nat) (
F
: nat -> T)
: (
m <= n)
%N ->
\big[min/x0]_(
i
< n | P i)
F i <= \big[min/x0]_(
i
< m | P i)
F i.
Proof.
Lemma
le_bigmin_ord_cond
[x0]
n
m
(
P
P'
: pred nat) (
F
: nat -> T)
:
(
m <= n)
%N -> (
forall
i
: 'I_m, P' i -> P i)
->
\big[min/x0]_(
i
< n | P i)
F i <= \big[min/x0]_(
i
< m | P' i)
F i.
Proof.
Lemma
subset_bigmin
[x0] [I : finType] [A
A'
P
: {pred I}] (
F
: I -> T)
:
A' \subset A ->
\big[min/x0]_(
i
in A | P i)
F i <= \big[min/x0]_(
i
in A' | P i)
F i.
Proof.
Lemma
subset_bigmin_cond
[x0] (
I
: finType) (
A
A'
P
P'
: {pred I}) (
F
: I -> T)
:
[set
i
in A' | P' i] \subset [set
i
in A | P i] ->
\big[min/x0]_(
i
in A | P i)
F i <= \big[min/x0]_(
i
in A' | P' i)
F i.
Proof.
Section
bigmin_finType
.
Variable (
I
: finType) (
x
: T).
Implicit Types (
P : pred I) (
F : I -> T).
Lemma
bigminD1
j
P
F
: P j ->
\big[min/x]_(
i
| P i)
F i = min (
F j) (
\big[min/x]_(
i
| P i && (
i != j))
F i).
Proof.
Lemma
bigmin_le_cond
j
P
F
: P j -> \big[min/x]_(
i
| P i)
F i <= F j.
Proof.
Lemma
bigmin_le
j
F
: \big[min/x]_i F i <= F j.
Proof.
Lemma
bigmin_inf
j
P
m
F
: P j -> F j <= m -> \big[min/x]_(
i
| P i)
F i <= m.
Proof.
Lemma
bigmin_geP
m
P
F
: reflect (
m <= x /\ forall
i,
P i -> m <= F i)
(
m <= \big[min/x]_(
i
| P i)
F i).
Proof.
Lemma
bigmin_gtP
m
P
F
:
reflect (
m < x /\ forall
i,
P i -> m < F i) (
m < \big[min/x]_(
i
| P i)
F i).
Proof.
Lemma
bigmin_eq_arg
j
P
F
: P j -> (
forall
i,
P i -> F i <= x)
->
\big[min/x]_(
i
| P i)
F i = F [arg min_(
i
< j | P i)
F i].
Proof.
move=> Pi0; case: arg_minP => //= i Pi PF PFx.
apply/eqP; rewrite eq_le bigmin_le_cond //=.
by apply/bigmin_geP; split => //; exact: PFx.
Qed.
Lemma
eq_bigmin
j
P
F
: P j -> (
forall
i,
P i -> F i <= x)
->
{i0 | i0 \in P & \big[min/x]_(
i
| P i)
F i = F i0}.
Proof.
by move=> Pi0 Hx; rewrite (
bigmin_eq_arg Pi0)
//; eexists => //; case:arg_minP.
Qed.
End bigmin_finType.
End bigmin.
Arguments bigmin_mkcond {d T I r}.
Arguments bigminID {d T I r}.
Arguments bigminD1 {d T I x} j.
Arguments bigmin_inf {d T I x} j.
Arguments bigmin_eq_arg {d T I} x j.
Arguments eq_bigmin {d T I x} j.
End of MathComp 1.16.0 additions
MathComp > 1.16 additions
Reserved Notation "f \max g" (
at level 50, left associativity).
Definition
max_fun
T
(
R
: numDomainType) (
f
g
: T -> R)
x
:= Num.max (
f x) (
g x).
Notation
"f \max g"
:= (
max_fun f g)
: ring_scope.
Arguments max_fun {T R} _ _ _ /.
End of mathComp > 1.16 additions
Reserved Notation "`1- x" (format "`1- x", at level 2).
Section
onem
.
Variable
R
: numDomainType.
Implicit Types r : R.
Definition
onem
r
:= 1 - r.
Local Notation
"`1- r"
:= (
onem r).
Lemma
onem0
: `1-0 = 1
Proof.
by rewrite /onem subr0. Qed.
Lemma
onem1
: `1-1 = 0
Proof.
by rewrite /onem subrr. Qed.
Lemma
onemK
r
: `1-(
`1-r)
= r.
Proof.
Lemma
add_onemK
r
: r + `1- r = 1.
Proof.
Lemma
onem_gt0
r
: r < 1 -> 0 < `1-r
Proof.
Lemma
onem_ge0
r
: r <= 1 -> 0 <= `1-r.
Proof.
by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed.
Lemma
onem_le1
r
: 0 <= r -> `1-r <= 1.
Proof.
Lemma
onem_lt1
r
: 0 < r -> `1-r < 1.
Proof.
Lemma
onemX_ge0
r
n
: 0 <= r -> r <= 1 -> 0 <= `1-(
r ^+ n).
Proof.
Lemma
onemX_lt1
r
n
: 0 < r -> `1-(
r ^+ n)
< 1.
Proof.
Lemma
onemD
r
s
: `1-(
r + s)
= `1-r - s.
Proof.
Lemma
onemMr
r
s
: s * `1-r = s - s * r.
Proof.
Lemma
onemM
r
s
: `1-(
r * s)
= `1-r + `1-s - `1-r * `1-s.
Proof.
End onem.
Notation
"`1- r"
:= (
onem r)
: ring_scope.
Lemma
onemV
(
F
: numFieldType) (
x
: F)
: x != 0 -> `1-(
x^-1)
= (
x - 1)
/ x.
Proof.
Lemma
lez_abs2
(
a
b
: int)
: 0 <= a -> a <= b -> (
`|a| <= `|b|)
%N.
Proof.
by case: a => //= n _; case: b. Qed.
Lemma
ler_gtP
(
R
: numFieldType) (
x
y
: R)
:
reflect (
forall
z,
z > y -> x <= z) (
x <= y).
Proof.
Lemma
ler_ltP
(
R
: numFieldType) (
x
y
: R)
:
reflect (
forall
z,
z < x -> z <= y) (
x <= y).
Proof.
Definition
inv_fun
T
(
R
: unitRingType) (
f
: T -> R)
x
:= (
f x)
^-1%R.
Notation
"f \^-1"
:= (
inv_fun f)
: ring_scope.
Arguments inv_fun {T R} _ _ /.
Definition
bound_side
d
(
T
: porderType d) (
c
: bool) (
x
: itv_bound T)
:=
if x is BSide c' _ then c == c' else false.
Lemma
real_ltr_distlC
[R : numDomainType] [x
y
: R] (
e
: R)
:
x - y \is Num.real -> (
`|x - y| < e)
= (
x - e < y < x + e).
Proof.
Definition
proj
{I} {T : I -> Type}
i
(
f
: forall
i,
T i)
:= f i.
Section
DFunWith
.
Variables (
I
: eqType) (
T
: I -> Type) (
f
: forall
i,
T i).
Definition
dfwith
i
(
x
: T i) (
j
: I)
: T j :=
if (
i =P j)
is ReflectT ij then ecast
j
(
T j)
ij x else f j.
Lemma
dfwithin
i
x
: dfwith x i = x.
Proof.
by rewrite /dfwith; case: eqP => // ii; rewrite eq_axiomK. Qed.
Lemma
dfwithout
i
(
x
: T i)
j
: i != j -> dfwith x j = f j.
Proof.
by rewrite /dfwith; case: eqP. Qed.
Variant
dfwith_spec
i
(
x
: T i)
: forall
j,
T j -> Type :=
|
DFunWithin
: dfwith_spec x x
|
DFunWithout
j
: i != j -> dfwith_spec x (
f j).
Lemma
dfwithP
i
(
x
: T i) (
j
: I)
: dfwith_spec x (
dfwith x j).
Proof.
Lemma
projK
i
(
x
: T i)
: cancel (
@dfwith i) (
proj i).
Proof.
by move=> z; rewrite /proj dfwithin. Qed.
End DFunWith.
Arguments dfwith {I T} f i x.
Definition
swap
(
T1
T2
: Type) (
x
: T1 * T2)
:= (
x.
2, x.
1).
Lemma
ler_sqrt
{R : rcfType} (
a
b
: R)
:
(
0 <= b -> (
Num.sqrt a <= Num.sqrt b)
= (
a <= b))
%R.
Proof.
Section
order_min
.
Variables (
d
: unit) (
T
: orderType d).
Import Order.
Local Open Scope order_scope.
Lemma
lt_min_lt
(
x
y
z
: T)
: (
min x z < min y z)
%O -> (
x < y)
%O.
Proof.
rewrite /Order.
min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
- by move=> /lt_le_trans; apply; rewrite leNgt.
- by rewrite ltNge (
ltW yz).
Qed.
End order_min.
MathComp 2.1 additions
From mathcomp Require Import poly.
Definition
coefE
:=
(
coef0, coef1, coefC, coefX, coefXn,
coefZ, coefMC, coefCM, coefXnM, coefMXn, coefXM, coefMX, coefMNn, coefMn,
coefN, coefB, coefD,
coef_cons, coef_Poly, coef_poly,
coef_deriv, coef_nderivn, coef_derivn, coef_map, coef_sum,
coef_comp_poly).
Module Export
Pdeg2
.
Module Export
Field
.
Section
Pdeg2Field
.
Variable
F
: fieldType.
Hypothesis
nz2
: 2%:R != 0 :> F.
Variable
p
: {poly F}.
Hypothesis
degp
: size p = 3%N.
Let
a
:= p`_2.
Let
b
:= p`_1.
Let
c
:= p`_0.
Let
pneq0
: p != 0
Proof.
by rewrite -size_poly_gt0 degp. Qed.
Let
aneq0
: a != 0.
Proof.
Let
a2neq0
: 2%:R * a != 0
Proof.
Let
sqa2neq0
: (
2%:R * a)
^+ 2 != 0
Proof.
Let
aa4
: 4%:R * a * a = (
2%:R * a)
^+2.
Proof.
Let
splitr
(
x
: F)
: x = x / 2%:R + x / 2%:R.
Proof.
Let
pE
: p = a *: 'X^2 + b *: 'X + c%:P.
Proof.
apply/polyP => + /[!coefE] => -[|[|[|i]]] /=; rewrite !Monoid.
simpm//.
by rewrite nth_default// degp.
Qed.
Let
delta
:= b ^+ 2 - 4%:R * a * c.
Lemma
deg2_poly_canonical
:
p = a *: ((
'X + (
b / (
2%:R * a))
%:P)
^+2 - (
delta / (
4%:R * a ^+ 2))
%:P).
Proof.
Variable
r
: F.
Hypothesis
r_sqrt_delta
: r ^+ 2 = delta.
Let
r1
:= (
- b - r)
/ (
2%:R * a).
Let
r2
:= (
- b + r)
/ (
2%:R * a).
Lemma
deg2_poly_factor
: p = a *: (
'X - r1%:P)
* (
'X - r2%:P).
Proof.
rewrite [p]deg2_poly_canonical//= -/a -/b -/c -/delta /r1 /r2.
rewrite ![(
- b + _)
* _]mulrDl 2!polyCD 2!opprD 2!addrA !mulNr !polyCN !opprK.
rewrite -scalerAl [in RHS]mulrC -subr_sqr -polyC_exp -[4%:R]/(
2 * 2)
%:R natrM.
by rewrite -expr2 -exprMn [in RHS]exprMn exprVn r_sqrt_delta.
Qed.
End Pdeg2Field.
End Field.
Module
Real
.
Section
Pdeg2Real
.
Variable
F
: realFieldType.
Section
Pdeg2RealConvex
.
Variable
p
: {poly F}.
Hypothesis
degp
: size p = 3%N.
Let
a
:= p`_2.
Let
b
:= p`_1.
Let
c
:= p`_0.
Hypothesis
age0
: 0 <= a.
Let
delta
:= b ^+ 2 - 4%:R * a * c.
Let
pneq0
: p != 0
Proof.
by rewrite -size_poly_gt0 degp. Qed.
Let
aneq0
: a != 0.
Proof.
Let
agt0
: 0 < a
Proof.
Let
a4gt0
: 0 < 4%:R * a
Proof.
Lemma
deg2_poly_min
x
: p.
[- b / (
2%:R * a)
] <= p.
[x].
Proof.
Lemma
deg2_poly_minE
: p.
[- b / (
2%:R * a)
] = - delta / (
4%:R * a).
Proof.
Lemma
deg2_poly_ge0
: reflect (
forall
x,
0 <= p.
[x]) (
delta <= 0).
Proof.
End Pdeg2RealConvex.
End Pdeg2Real.
Section
Pdeg2RealClosed
.
Variable
F
: rcfType.
Section
Pdeg2RealClosedConvex
.
Variable
p
: {poly F}.
Hypothesis
degp
: size p = 3%N.
Let
a
:= p`_2.
Let
b
:= p`_1.
Let
c
:= p`_0.
Let
nz2
: 2%:R != 0 :> F
Proof.
Let
delta
:= b ^+ 2 - 4%:R * a * c.
Let
r1
:= (
- b - Num.sqrt delta)
/ (
2%:R * a).
Let
r2
:= (
- b + Num.sqrt delta)
/ (
2%:R * a).
Lemma
deg2_poly_factor
: 0 <= delta -> p = a *: (
'X - r1%:P)
* (
'X - r2%:P).
Proof.
End Pdeg2RealClosedConvex.
End Pdeg2RealClosed.
End Real.
End Pdeg2.
Section
Degle2PolyRealConvex
.
Variable (
F
: realFieldType) (
p
: {poly F}).
Hypothesis
degp
: (
size p <= 3)
%N.
Let
a
:= p`_2.
Let
b
:= p`_1.
Let
c
:= p`_0.
Let
delta
:= b ^+ 2 - 4%:R * a * c.
Lemma
deg_le2_poly_delta_ge0
: 0 <= a -> (
forall
x,
0 <= p.
[x])
-> delta <= 0.
Proof.
End Degle2PolyRealConvex.
Section
Degle2PolyRealClosedConvex
.
Variable (
F
: rcfType) (
p
: {poly F}).
Hypothesis
degp
: (
size p <= 3)
%N.
Let
a
:= p`_2.
Let
b
:= p`_1.
Let
c
:= p`_0.
Let
delta
:= b ^+ 2 - 4%:R * a * c.
Lemma
deg_le2_poly_ge0
: (
forall
x,
0 <= p.
[x])
-> delta <= 0.
Proof.
End Degle2PolyRealClosedConvex.
Lemma
deg_le2_ge0
(
F
: rcfType) (
a
b
c
: F)
:
(
forall
x,
0 <= a * x ^+ 2 + b * x + c)
%R -> (
b ^+ 2 - 4%:R * a * c <= 0)
%R.
Proof.
Reserved Notation "f \min g" (
at level 50, left associativity).
Definition
min_fun
T
(
R
: numDomainType) (
f
g
: T -> R)
x
:= Num.min (
f x) (
g x).
Notation
"f \min g"
:= (
min_fun f g)
: ring_scope.
Arguments min_fun {T R} _ _ _ /.
Section
dependent_choice_Type
.
Context
X
(
R
: X -> X -> Prop).
Lemma
dependent_choice_Type
: (
forall
x,
{y | R x y})
->
forall
x0,
{f | f 0%N = x0 /\ forall
n,
R (
f n) (
f n.
+1)
}.
Proof.
move=> h x0.
set (
f := fix f
n
:= if n is n'.
+1 then proj1_sig (
h (
f n'))
else x0).
exists f; split => //.
intro n; induction n; simpl; apply: proj2_sig.
Qed.
End dependent_choice_Type.
Section
max_min
.
Variable
R
: realFieldType.
Import Num.Theory.
Let
nz2
: 2%:R != 0 :> R
Proof.
Lemma
maxr_absE
(
x
y
: R)
: Num.max x y = (
x + y + `|x - y|)
/ 2%:R.
Proof.
Lemma
minr_absE
(
x
y
: R)
: Num.min x y = (
x + y - `|x - y|)
/ 2%:R.
Proof.
End max_min.
Notation
trivial
:= (
ltac:(
done)).
Section
bigmax_seq
.
Context
d
{T : orderType d} {x : T} {I : eqType}.
Variables (
r
: seq I) (
i0
: I) (
P
: pred I).
Lemma
le_bigmax_seq
F
:
i0 \in r -> P i0 -> (
F i0 <= \big[Order.
max/x]_(
i
<- r | P i)
F i)
%O.
Proof.
Lemma
bigmax_sup_seq
(
m
: T) (
F
: I -> T)
:
i0 \in r -> P i0 -> (
m <= F i0)
%O ->
(
m <= \big[Order.
max/x]_(
i
<- r | P i)
F i)
%O.
Proof.
End bigmax_seq.
Arguments le_bigmax_seq {d T} x {I r} i0 P.
Lemma
gerBl
{R : numDomainType} (
x
y
: R)
: 0 <= y -> x - y <= x.
Proof.
Section
normr
.
Variable
R
: realDomainType.
Definition
Rnpos
: qualifier 0 R := [qualify
x
: R | x <= 0].
Lemma
nposrE
x
: (
x \is Rnpos)
= (
x <= 0)
Proof.
by []. Qed.
Lemma
ger0_le_norm
:
{in Num.nneg &, {mono (
@Num.
Def.normr _ R)
:
x
y
/ x <= y}}.
Proof.
by move=> x y; rewrite !nnegrE => x0 y0; rewrite !ger0_norm. Qed.
Lemma
gtr0_le_norm
:
{in Num.pos &, {mono (
@Num.
Def.normr _ R)
:
x
y
/ x <= y}}.
Proof.
by move=> x y; rewrite !posrE => /ltW x0 /ltW y0; exact: ger0_le_norm. Qed.
Lemma
ler0_ge_norm
:
{in Rnpos &, {mono (
@Num.
Def.normr _ R)
:
x
y
/ x <= y >-> x >= y}}.
Proof.
move=> x y; rewrite !nposrE => x0 y0.
by rewrite !ler0_norm// -subr_ge0 opprK addrC subr_ge0.
Qed.
Lemma
ltr0_ge_norm
:
{in Num.neg &, {mono (
@Num.
Def.normr _ R)
:
x
y
/ x <= y >-> x >= y}}.
Proof.
by move=> x y; rewrite !negrE => /ltW x0 /ltW y0; exact: ler0_ge_norm. Qed.
End normr.
Lemma
leq_ltn_expn
m
: exists
n,
(
2 ^ n <= m.
+1 < 2 ^ n.
+1)
%N.
Proof.
elim: m => [|m [n /andP[h1 h2]]]; first by exists O.
have [m2n|nm2] := ltnP m.
+2 (
2 ^ n.
+1)
%N.
by exists n; rewrite m2n andbT (
leq_trans h1).
exists n.
+1; rewrite nm2/= -addn1.
rewrite -[X in (
_ <= X)
%N]prednK ?expn_gt0// -[X in (
_ <= X)
%N]addn1 leq_add2r.
by rewrite (
leq_trans h2)
// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
Qed.
Definition
monotonous
d
(
T
: porderType d) (
pT
: predType T) (
A
: pT) (
f
: T -> T)
:=
{in A &, {mono f :
x
y
/ (
x <= y)
%O}} \/ {in A &, {mono f :
x
y
/~ (
x <= y)
%O}}.