Library mathcomp.analysis.mathcomp_extra

(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
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.

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)}.

Lemma enum_ord0 : enum 'I_0 = [::].

Lemma enum_ordS n : enum 'I_n.+1 =
  rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max.

Definition olift aT rT (f : aT → rT) := Some \o f.

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 aT rT sT (f : aT → rT) (g : rT → sT) x :
  oapp (g \o f) x =1 (@oapp _ _)^~ x 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 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}.

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').

Definition pred_omap 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_omap D} →
  {in D, ocancel f f'} → {in D', ocancel h h'} →
  {in D', ocancel (obind f \o h) (h' \o f')}.

Lemma eqbLR (b1 b2 : bool) : b1 = b2 → b1 → b2.

Lemma eqbRL (b1 b2 : bool) : b1 = b2 → b2 → b1.

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.

Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.

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} _ _ /.

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} _ _ _ /.

Import Order.TTheory GRing.Theory Num.Theory.

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_big_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.

Coercion pair_of_interval T (I : interval T) : itv_bound T × itv_bound T :=
  let: Interval b1 b2 := I in (b1, b2).

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.