Library mathcomp_extra
(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *)
Require Import BinPos.
From mathcomp Require choice.
Require Import BinPos.
From mathcomp Require choice.
Missing coercion (done before Import to avoid redeclaration error,
thanks to KS for the trick)
MathComp 1.15 addition
Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import finset interval.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import finset interval.
MathComp 1.15 additions
This files contains lemmas and definitions missing from MathComp.
f \max g := fun x => Num.max (f x) (g x)
oflit f := Some \o f
pred_oapp T D := [pred x | oapp (mem D) false x]
f \* g := fun x => f x * g x
\- f := fun x => - f x
lteBSide, bnd_simp == multirule to simplify inequalities between
interval bounds
miditv i == middle point of interval i
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)
Set Implicit Arguments.
Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "f \- g" (at level 50, left associativity).
Reserved Notation "\- f" (at level 35, f at level 35).
Reserved Notation "f \max g" (at level 50, left associativity).
Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I)
(P Q : I → T → Prop) : T →
(∀ x : I, D x → {y : T | P x y & Q x y}) →
{f : ∀ x : I, T | ∀ x : I, D x → P x (f x) & ∀ x : I, D x → Q x (f x)}.
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.
Lemma olift_comp aT rT sT (f : aT → rT) (g : rT → sT) :
olift (g \o f) = olift g \o f.
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.
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))}.
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}.
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')}.
Lemma eqbRL (b1 b2 : bool) : b1 = b2 → b2 → b1.
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.
Lemma leBSide x y b b' :
((BSide b x ≤ BSide b' y) = (x < y ?<= if b' ==> b))%O.
Definition lteBSide := (ltBSide, leBSide).
Let BLeft_ltE x y b : (BSide b x < BLeft y)%O = (x < y)%O.
Let BRight_leE x y b : (BSide b x ≤ BRight y)%O = (x ≤ y)%O.
Let BRight_BLeft_leE x y : (BRight x ≤ BLeft y)%O = (x < y)%O.
Let BLeft_BRight_ltE x y : (BLeft x < BRight y)%O = (x ≤ y)%O.
Let BRight_BSide_ltE x y b : (BRight x < BSide b y)%O = (x < y)%O.
Let BLeft_BSide_leE x y b : (BLeft x ≤ BSide b y)%O = (x ≤ y)%O.
Let BSide_ltE x y b : (BSide b x < BSide b y)%O = (x < y)%O.
Let BSide_leE x y b : (BSide b x ≤ BSide b y)%O = (x ≤ y)%O.
Let BInfty_leE a : (a ≤ BInfty T false)%O.
Let BInfty_geE a : (BInfty T true ≤ a)%O.
Let BInfty_le_eqE a : (BInfty T false ≤ a)%O = (a == BInfty T false).
Let BInfty_ge_eqE a : (a ≤ BInfty T true)%O = (a == BInfty T true).
Let BInfty_ltE a : (a < BInfty T false)%O = (a != BInfty T false).
Let BInfty_gtE a : (BInfty T true < a)%O = (a != BInfty T true).
Let BInfty_ltF a : (BInfty T false < a)%O = false.
Let BInfty_gtF a : (a < BInfty T true)%O = false.
Let BInfty_BInfty_ltE : (BInfty T true < BInfty T false)%O.
Lemma ltBRight_leBLeft (a : itv_bound T) (r : T) :
(a < BRight r)%O = (a ≤ BLeft r)%O.
Lemma leBRight_ltBLeft (a : itv_bound T) (r : T) :
(BRight r ≤ a)%O = (BLeft r < a)%O.
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)].
Lemma itv_split1U (a : itv_bound T) (x : T) : (BRight x ≤ a)%O →
Interval (BLeft x) a =i [predU1 x & Interval (BRight x) a].
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.
Lemma miditv_le_left i b : (i.1 < i.2)%O → (BSide b (miditv i) ≤ i.2)%O.
Lemma miditv_ge_right i b : (i.1 < i.2)%O → (i.1 ≤ BSide b (miditv i))%O.
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.
Lemma predC_itvr a : [predC Interval a +oo%O] =i Interval -oo%O a.
Lemma predC_itv i : [predC i] =i [predU Interval -oo%O i.1 & Interval i.2 +oo%O].
End itv_porderType.
Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I → R) :
(∀ i, P i → F i ≤ 0)%R → (\sum_(i <- r | P i) F i ≤ 0)%R.
Lemma enum_ord0 : enum 'I_0 = [::].
Lemma enum_ordSr n : enum 'I_n.+1 =
rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max.
Lemma obindEapp {aT rT} (f : aT → option rT) : obind f = oapp f None.
Lemma omapEbind {aT rT} (f : aT → rT) : omap f = obind (olift f).
Lemma omapEapp {aT rT} (f : aT → rT) : omap f = oapp (olift f) None.
Lemma oappEmap {aT rT} (f : aT → rT) (y0 : rT) x :
oapp f y0 x = odflt y0 (omap f x).
Lemma omap_comp aT rT sT (f : aT → rT) (g : rT → sT) :
omap (g \o f) =1 omap g \o omap f.
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.
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')}.
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)}.
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')}.
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').
Lemma eqbLR (b1 b2 : bool) : b1 = b2 → b1 → b2.
Definition max_fun T (R : numDomainType) (f g : T → R) x := Num.max (f x) (g x).
Notation "f \max g" := (max_fun f g) : ring_scope.
Arguments max_fun {T R} _ _ _ /.
Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R → (- r < r)%R.
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.
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.
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.
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.
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).
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.
Lemma ler_addgt0Pr x y : reflect (∀ e, e > 0 → x ≤ y + e) (x ≤ y).
Lemma ler_addgt0Pl x y : reflect (∀ e, e > 0 → x ≤ e + y) (x ≤ y).
Lemma in_segment_addgt0Pr x y z :
reflect (∀ e, e > 0 → y \in `[x - e, z + e]) (y \in `[x, z]).
Lemma in_segment_addgt0Pl x y z :
reflect (∀ e, e > 0 → y \in `[(- e + x), (e + z)]) (y \in `[x, z]).
Lemma lt_le a b : (∀ x, x < a → x < b) → a ≤ b.
Lemma gt_ge a b : (∀ x, b < x → a < x) → a ≤ b.
End lt_le_gt_ge.
Lemma itvxx d (T : porderType d) (x : T) : `[x, x] =i pred1 x.
Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).
Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ ≤ `[a, b]}.
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").
Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R.
Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R.
To be backported to finmap
Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
(f : X → nat) : A != fset0 →
(∃ i, i \in A ∧ ∀ j, j \in A → f j ≤ f i)%nat.
Lemma image_nat_maximum n (f : nat → nat) :
(∃ i, i ≤ n ∧ ∀ j, j ≤ n → f j ≤ f i)%N.
Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
#|` A| = (\sum_(i <- A) 1)%N.
Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.
MathComp > 1.15.0 additions
Section bigminr_maxr.
Import Num.Def.
Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i.
End bigminr_maxr.
Section SemiGroupProperties.
Variables (R : Type) (op : R → R → R).
Hypothesis opA : associative op.
Convert an AC op : R -> R -> R to a com_law on option R
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.
Let opAC : right_commutative op.
Hypothesis opyy : idempotent op.
Lemma opACE x y : oop (Some x) (Some y) = some (op x y).
Lemma oopA_subdef : associative oop.
Lemma oopx1_subdef : left_id None oop.
Lemma oop1x_subdef : right_id None oop.
Lemma oopC_subdef : commutative oop.
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).
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)).
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.
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.
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.
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.
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).
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).
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.
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).
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.
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).
Variable le : rel R.
Hypothesis le_refl : reflexive le.
Hypothesis op_incr : ∀ x y, le x (op x y).
Lemma sub_big I [s] (P P' : {pred I}) (F : I → R) : (∀ i, P i → P' i) →
le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
Lemma sub_big_seq (I : eqType) s s' P (F : I → R) :
(∀ 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).
Lemma sub_big_seq_cond (I : eqType) s s' P P' (F : I → R) :
(∀ 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).
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).
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).
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).
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).
Lemma sub_in_big [I : eqType] (s : seq I) (P P' : {pred I}) (F : I → R) :
{in s, ∀ i, P i → P' i} →
le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
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).
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).
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).
Lemma le_big_nat_cond n m n' m' (P P' : {pred nat}) (F : nat → R) :
(n' ≤ n)%N → (m ≤ m')%N → (∀ 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).
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).
Lemma le_big_ord_cond n m (P P' : {pred nat}) (F : nat → R) :
(n ≤ m)%N → (∀ 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).
End SemiGroupProperties.
Section bigmaxmin.
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 → (∀ i, P i → f i ≤ x) → \big[max/x0]_(i <- r | P i) f i ≤ x.
Lemma bigmax_lt :
x0 < x → (∀ i, P i → f i < x) → \big[max/x0]_(i <- r | P i) f i < x.
Lemma lt_bigmin :
x < x0 → (∀ i, P i → x < f i) → x < \big[min/x0]_(i <- r | P i) f i.
Lemma le_bigmin :
x ≤ x0 → (∀ i, P i → x ≤ f i) → x ≤ \big[min/x0]_(i <- r | P i) f i.
End bigmaxmin.
Section bigmax.
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).
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).
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).
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.
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).
End bigmax_Type.
Let le_maxr_id (x y : T) : x ≤ max x y.
Lemma sub_bigmax [x0] I s (P P' : {pred I}) (F : I → T) :
(∀ i, P i → P' i) →
\big[max/x0]_(i <- s | P i) F i ≤ \big[max/x0]_(i <- s | P' i) F i.
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.
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.
Lemma sub_in_bigmax [x0] [I : eqType] (s : seq I) (P P' : {pred I}) (F : I → T) :
{in s, ∀ i, P i → P' i} →
\big[max/x0]_(i <- s | P i) F i ≤ \big[max/x0]_(i <- s | P' i) F i.
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.
Lemma le_bigmax_nat_cond [x0] n m n' m' (P P' : {pred nat}) (F : nat → T) :
(n' ≤ n)%N → (m ≤ m')%N → (∀ 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.
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.
Lemma le_bigmax_ord_cond [x0] n m (P P' : {pred nat}) (F : nat → T) :
(n ≤ m)%N → (∀ 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.
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.
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.
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).
Lemma le_bigmax_cond j P F : P j → F j ≤ \big[max/x]_(i | P i) F i.
Lemma le_bigmax F j : F j ≤ \big[max/x]_i F i.
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.
Let opAC : right_commutative op.
Hypothesis opyy : idempotent op.
Lemma opACE x y : oop (Some x) (Some y) = some (op x y).
Lemma oopA_subdef : associative oop.
Lemma oopx1_subdef : left_id None oop.
Lemma oop1x_subdef : right_id None oop.
Lemma oopC_subdef : commutative oop.
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).
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)).
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.
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.
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.
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.
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).
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).
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.
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).
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.
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).
Variable le : rel R.
Hypothesis le_refl : reflexive le.
Hypothesis op_incr : ∀ x y, le x (op x y).
Lemma sub_big I [s] (P P' : {pred I}) (F : I → R) : (∀ i, P i → P' i) →
le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
Lemma sub_big_seq (I : eqType) s s' P (F : I → R) :
(∀ 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).
Lemma sub_big_seq_cond (I : eqType) s s' P P' (F : I → R) :
(∀ 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).
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).
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).
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).
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).
Lemma sub_in_big [I : eqType] (s : seq I) (P P' : {pred I}) (F : I → R) :
{in s, ∀ i, P i → P' i} →
le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
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).
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).
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).
Lemma le_big_nat_cond n m n' m' (P P' : {pred nat}) (F : nat → R) :
(n' ≤ n)%N → (m ≤ m')%N → (∀ 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).
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).
Lemma le_big_ord_cond n m (P P' : {pred nat}) (F : nat → R) :
(n ≤ m)%N → (∀ 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).
End SemiGroupProperties.
Section bigmaxmin.
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 → (∀ i, P i → f i ≤ x) → \big[max/x0]_(i <- r | P i) f i ≤ x.
Lemma bigmax_lt :
x0 < x → (∀ i, P i → f i < x) → \big[max/x0]_(i <- r | P i) f i < x.
Lemma lt_bigmin :
x < x0 → (∀ i, P i → x < f i) → x < \big[min/x0]_(i <- r | P i) f i.
Lemma le_bigmin :
x ≤ x0 → (∀ i, P i → x ≤ f i) → x ≤ \big[min/x0]_(i <- r | P i) f i.
End bigmaxmin.
Section bigmax.
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).
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).
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).
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.
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).
End bigmax_Type.
Let le_maxr_id (x y : T) : x ≤ max x y.
Lemma sub_bigmax [x0] I s (P P' : {pred I}) (F : I → T) :
(∀ i, P i → P' i) →
\big[max/x0]_(i <- s | P i) F i ≤ \big[max/x0]_(i <- s | P' i) F i.
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.
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.
Lemma sub_in_bigmax [x0] [I : eqType] (s : seq I) (P P' : {pred I}) (F : I → T) :
{in s, ∀ i, P i → P' i} →
\big[max/x0]_(i <- s | P i) F i ≤ \big[max/x0]_(i <- s | P' i) F i.
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.
Lemma le_bigmax_nat_cond [x0] n m n' m' (P P' : {pred nat}) (F : nat → T) :
(n' ≤ n)%N → (m ≤ m')%N → (∀ 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.
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.
Lemma le_bigmax_ord_cond [x0] n m (P P' : {pred nat}) (F : nat → T) :
(n ≤ m)%N → (∀ 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.
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.
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.
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).
Lemma le_bigmax_cond j P F : P j → F j ≤ \big[max/x]_(i | P i) F i.
Lemma le_bigmax F j : F j ≤ \big[max/x]_i F i.
NB: as of [2022-08-02], bigop.bigmax_sup already exists for nat
Lemma bigmax_sup j P m F : P j → m ≤ F j → m ≤ \big[max/x]_(i | P i) F i.
Lemma bigmax_leP m P F : reflect (x ≤ m ∧ ∀ i, P i → F i ≤ m)
(\big[max/x]_(i | P i) F i ≤ m).
Lemma bigmax_ltP m P F :
reflect (x < m ∧ ∀ i, P i → F i < m) (\big[max/x]_(i | P i) F i < m).
Lemma bigmax_eq_arg j P F : P j → (∀ i, P i → x ≤ F i) →
\big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i].
Lemma eq_bigmax j P F : P j → (∀ i, P i → x ≤ F i) →
{i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}.
Lemma le_bigmax2 P F1 F2 : (∀ i, P i → F1 i ≤ F2 i) →
\big[max/x]_(i | P i) F1 i ≤ \big[max/x]_(i | P i) F2 i.
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 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).
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).
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).
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.
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).
End bigmin_Type.
Let le_minr_id (x y : T) : x ≥ min x y.
Lemma sub_bigmin [x0] I s (P P' : {pred I}) (F : I → T) :
(∀ i, P' i → P i) →
\big[min/x0]_(i <- s | P i) F i ≤ \big[min/x0]_(i <- s | P' i) F i.
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.
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.
Lemma sub_in_bigmin [x0] [I : eqType] (s : seq I) (P P' : {pred I}) (F : I → T) :
{in s, ∀ i, P' i → P i} →
\big[min/x0]_(i <- s | P i) F i ≤ \big[min/x0]_(i <- s | P' i) F i.
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.
Lemma le_bigmin_nat_cond [x0] n m n' m' (P P' : pred nat) (F : nat → T) :
(n ≤ n')%N → (m' ≤ m)%N → (∀ 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.
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.
Lemma le_bigmin_ord_cond [x0] n m (P P' : pred nat) (F : nat → T) :
(m ≤ n)%N → (∀ 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.
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.
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.
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).
Lemma bigmin_le_cond j P F : P j → \big[min/x]_(i | P i) F i ≤ F j.
Lemma bigmin_le j F : \big[min/x]_i F i ≤ F j.
Lemma bigmin_inf j P m F : P j → F j ≤ m → \big[min/x]_(i | P i) F i ≤ m.
Lemma bigmin_geP m P F : reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
(m ≤ \big[min/x]_(i | P i) F i).
Lemma bigmin_gtP m P F :
reflect (m < x ∧ ∀ i, P i → m < F i) (m < \big[min/x]_(i | P i) F i).
Lemma bigmin_eq_arg j P F : P j → (∀ i, P i → F i ≤ x) →
\big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i].
Lemma eq_bigmin j P F : P j → (∀ i, P i → F i ≤ x) →
{i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}.
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.
Section onem.
Variable R : numDomainType.
Implicit Types r : R.
Definition onem r := 1 - r.
Lemma onem0 : `1-0 = 1.
Lemma onem1 : `1-1 = 0.
Lemma onemK r : `1-(`1-r) = r.
Lemma add_onemK r : r + `1- r = 1.
Lemma onem_gt0 r : r < 1 → 0 < `1-r.
Lemma onem_ge0 r : r ≤ 1 → 0 ≤ `1-r.
Lemma onem_le1 r : 0 ≤ r → `1-r ≤ 1.
Lemma onem_lt1 r : 0 < r → `1-r < 1.
Lemma onemX_ge0 r n : 0 ≤ r → r ≤ 1 → 0 ≤ `1-(r ^+ n).
Lemma onemX_lt1 r n : 0 < r → `1-(r ^+ n) < 1.
Lemma onemD r s : `1-(r + s) = `1-r - s.
Lemma onemMr r s : s × `1-r = s - s × r.
Lemma onemM r s : `1-(r × s) = `1-r + `1-s - `1-r × `1-s.
End onem.
Notation "`1- r" := (onem r) : ring_scope.
Lemma lez_abs2 (a b : int) : 0 ≤ a → a ≤ b → (`|a| ≤ `|b|)%N.
Lemma ler_gtP (R : numFieldType) (x y : R) :
reflect (∀ z, z > y → x ≤ z) (x ≤ y).
Lemma ler_ltP (R : numFieldType) (x y : R) :
reflect (∀ z, z < x → z ≤ y) (x ≤ y).
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).
Definition proj {I} {T : I → Type} i (f : ∀ i, T i) := f i.
Section DFunWith.
Variables (I : eqType) (T : I → Type) (f : ∀ 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.
Lemma dfwithout i (x : T i) j : i != j → dfwith x j = f j.
Variant dfwith_spec i (x : T i) : ∀ 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).
Lemma projK i (x : T i) : cancel (@dfwith i) (proj i).
End DFunWith.
Arguments dfwith {I T} f i x.
Definition swap (T1 T2 : Type) (x : T1 × T2) := (x.2, x.1).
Lemma bigmax_leP m P F : reflect (x ≤ m ∧ ∀ i, P i → F i ≤ m)
(\big[max/x]_(i | P i) F i ≤ m).
Lemma bigmax_ltP m P F :
reflect (x < m ∧ ∀ i, P i → F i < m) (\big[max/x]_(i | P i) F i < m).
Lemma bigmax_eq_arg j P F : P j → (∀ i, P i → x ≤ F i) →
\big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i].
Lemma eq_bigmax j P F : P j → (∀ i, P i → x ≤ F i) →
{i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}.
Lemma le_bigmax2 P F1 F2 : (∀ i, P i → F1 i ≤ F2 i) →
\big[max/x]_(i | P i) F1 i ≤ \big[max/x]_(i | P i) F2 i.
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 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).
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).
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).
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.
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).
End bigmin_Type.
Let le_minr_id (x y : T) : x ≥ min x y.
Lemma sub_bigmin [x0] I s (P P' : {pred I}) (F : I → T) :
(∀ i, P' i → P i) →
\big[min/x0]_(i <- s | P i) F i ≤ \big[min/x0]_(i <- s | P' i) F i.
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.
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.
Lemma sub_in_bigmin [x0] [I : eqType] (s : seq I) (P P' : {pred I}) (F : I → T) :
{in s, ∀ i, P' i → P i} →
\big[min/x0]_(i <- s | P i) F i ≤ \big[min/x0]_(i <- s | P' i) F i.
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.
Lemma le_bigmin_nat_cond [x0] n m n' m' (P P' : pred nat) (F : nat → T) :
(n ≤ n')%N → (m' ≤ m)%N → (∀ 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.
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.
Lemma le_bigmin_ord_cond [x0] n m (P P' : pred nat) (F : nat → T) :
(m ≤ n)%N → (∀ 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.
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.
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.
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).
Lemma bigmin_le_cond j P F : P j → \big[min/x]_(i | P i) F i ≤ F j.
Lemma bigmin_le j F : \big[min/x]_i F i ≤ F j.
Lemma bigmin_inf j P m F : P j → F j ≤ m → \big[min/x]_(i | P i) F i ≤ m.
Lemma bigmin_geP m P F : reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
(m ≤ \big[min/x]_(i | P i) F i).
Lemma bigmin_gtP m P F :
reflect (m < x ∧ ∀ i, P i → m < F i) (m < \big[min/x]_(i | P i) F i).
Lemma bigmin_eq_arg j P F : P j → (∀ i, P i → F i ≤ x) →
\big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i].
Lemma eq_bigmin j P F : P j → (∀ i, P i → F i ≤ x) →
{i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}.
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.
Section onem.
Variable R : numDomainType.
Implicit Types r : R.
Definition onem r := 1 - r.
Lemma onem0 : `1-0 = 1.
Lemma onem1 : `1-1 = 0.
Lemma onemK r : `1-(`1-r) = r.
Lemma add_onemK r : r + `1- r = 1.
Lemma onem_gt0 r : r < 1 → 0 < `1-r.
Lemma onem_ge0 r : r ≤ 1 → 0 ≤ `1-r.
Lemma onem_le1 r : 0 ≤ r → `1-r ≤ 1.
Lemma onem_lt1 r : 0 < r → `1-r < 1.
Lemma onemX_ge0 r n : 0 ≤ r → r ≤ 1 → 0 ≤ `1-(r ^+ n).
Lemma onemX_lt1 r n : 0 < r → `1-(r ^+ n) < 1.
Lemma onemD r s : `1-(r + s) = `1-r - s.
Lemma onemMr r s : s × `1-r = s - s × r.
Lemma onemM r s : `1-(r × s) = `1-r + `1-s - `1-r × `1-s.
End onem.
Notation "`1- r" := (onem r) : ring_scope.
Lemma lez_abs2 (a b : int) : 0 ≤ a → a ≤ b → (`|a| ≤ `|b|)%N.
Lemma ler_gtP (R : numFieldType) (x y : R) :
reflect (∀ z, z > y → x ≤ z) (x ≤ y).
Lemma ler_ltP (R : numFieldType) (x y : R) :
reflect (∀ z, z < x → z ≤ y) (x ≤ y).
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).
Definition proj {I} {T : I → Type} i (f : ∀ i, T i) := f i.
Section DFunWith.
Variables (I : eqType) (T : I → Type) (f : ∀ 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.
Lemma dfwithout i (x : T i) j : i != j → dfwith x j = f j.
Variant dfwith_spec i (x : T i) : ∀ 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).
Lemma projK i (x : T i) : cancel (@dfwith i) (proj i).
End DFunWith.
Arguments dfwith {I T} f i x.
Definition swap (T1 T2 : Type) (x : T1 × T2) := (x.2, x.1).