Move part of set_interval to classical

Everything not dealing with reals or ereal is moved to classicel,
the remaining is left in analysis.

CHANGELOG_UNRELEASED.md

@@ -27,6 +27,28 @@
     `ge0_mule_fsumr`, `ge0_mule_fsuml` (from `fsbigop.v`)
   + lemmas `finite_supportNe`, `dual_fsumeE`, `dfsume_ge0`, `dfsume_le0`,
     `dfsume_gt0`, `dfsume_lt0`, `pdfsume_eq0`, `le0_mule_dfsumr`, `le0_mule_dfsuml`
+- file `classical/set_interval.v`
+- in file `classical/set_interval.v`:
+  + definitions `neitv`, `set_itv_infty_set0`, `set_itvE`, `disjoint_itv`
+    (from `set_interval.v`)
+  + lemmas `neitv_lt_bnd`, `set_itvP`, `subset_itvP`, `set_itvoo`, `set_itv_cc`,
+    `set_itvco`, `set_itvoc`, `set_itv1`, `set_itvoo0`, `set_itvoc0`, `set_itvco0`,
+    `set_itv_infty_infty`, `set_itv_o_infty`, `set_itv_c_infty`, `set_itv_infty_o`,
+    `set_itv_infty_c`, `set_itv_pinfty_bnd`, `set_itv_bnd_ninfty`, `setUitv1`,
+    `setU1itv`, `set_itvI`, `neitvE`, `neitvP`, `setitv0`, `has_lbound_itv`,
+    `has_ubound_itv`, `hasNlbound`, `hasNubound`, `opp_itv_bnd_infty`, `opp_itvoo`,
+    `setCitvl`, `setCitvr`, `set_itv_splitI`, `setCitv`, `set_itv_splitD`,
+    `set_itv_ge`, `trivIset_set_itv_nth`, `disjoint_itvxx`, `lt_disjoint`,
+    `disjoint_neitv`, `neitv_bnd1`, `neitv_bnd2` (from `set_interval.v`)
+  + lemmas `setNK`, `lb_ubN`, `ub_lbN`, `mem_NE`, `nonemptyN`, `opp_set_eq0`,
+    `has_lb_ubN`, `has_ubPn`, `has_lbPn` (from `reals.v`)
+- in file `classical/mathcomp_extra.v`:
+  + coercion `pair_of_interval` (from `mathcomp_extra.v`)
+  + definition `miditv` (from `mathcomp_extra.v`)
+  + lemmas `ltBside`, `leBside`, `ltBRight`, `leBRight`, `bnd_simp`,
+    `itv_splitU1`, `itv_split1U`, `mem_miditv`, `miditv_le_left`,
+    `miditv_ge_right`, `predC_itvl`, `predC_itvr`, `predC_itv`
+    (from `mathcomp_extra.v`)
 
 ### Changed
 
@@ -57,6 +79,28 @@
     `fsume_gt0`, `fsume_lt0`, `pfsume_eq0` (moved to `ereal.v`)
   + lemma `pair_fsum` (subsumed by `pair_fsbig`)
   + lemma `exchange_fsum` (subsumed by `exchange_fsbig`)
+- in file `mathcomp_extra.v`:
+  + coercion `pair_of_interval` (moved to `classical/mathcomp_extra.v`)
+  + definition `miditv` (moved to `classical/mathcomp_extra.v`)
+  + lemmas `ltBside`, `leBside`, `ltBRight`, `leBRight`, `bnd_simp`,
+    `itv_splitU1`, `itv_split1U`, `mem_miditv`, `miditv_le_left`,
+    `miditv_ge_right`, `predC_itvl`, `predC_itvr`, `predC_itv`
+    (moved to `classical/mathcomp_extra.v`)
+- in file `reals.v`:
+  + lemmas `setNK`, `lb_ubN`, `ub_lbN`, `mem_NE`, `nonemptyN`, `opp_set_eq0`,
+    `has_lb_ubN`, `has_ubPn`, `has_lbPn` (moved to `classical/set_interval.v`)
+- in file `set_interval.v`:
+  + definitions `neitv`, `set_itv_infty_set0`, `set_itvE`, `disjoint_itv`
+    (moved to `classical/set_interval.v`)
+  + lemmas `neitv_lt_bnd`, `set_itvP`, `subset_itvP`, `set_itvoo`, `set_itv_cc`,
+    `set_itvco`, `set_itvoc`, `set_itv1`, `set_itvoo0`, `set_itvoc0`, `set_itvco0`,
+    `set_itv_infty_infty`, `set_itv_o_infty`, `set_itv_c_infty`, `set_itv_infty_o`,
+    `set_itv_infty_c`, `set_itv_pinfty_bnd`, `set_itv_bnd_ninfty`, `setUitv1`,
+    `setU1itv`, `set_itvI`, `neitvE`, `neitvP`, `setitv0`, `has_lbound_itv`,
+    `has_ubound_itv`, `hasNlbound`, `hasNubound`, `opp_itv_bnd_infty`, `opp_itvoo`,
+    `setCitvl`, `setCitvr`, `set_itv_splitI`, `setCitv`, `set_itv_splitD`,
+    `set_itv_ge`, `trivIset_set_itv_nth`, `disjoint_itvxx`, `lt_disjoint`,
+    `disjoint_neitv`, `neitv_bnd1`, `neitv_bnd2` (moved to `classical/set_interval.v`)
 
 ### Infrastructure
 

_CoqProject

@@ -14,6 +14,7 @@ classical/mathcomp_extra.v
 classical/functions.v
 classical/cardinality.v
 classical/fsbigop.v
+classical/set_interval.v
 theories/mathcomp_extra.v
 theories/ereal.v
 theories/reals.v

classical/Make

@@ -13,3 +13,4 @@ mathcomp_extra.v
 functions.v
 cardinality.v
 fsbigop.v
+set_interval.v

classical/all_classical.v

@@ -4,3 +4,4 @@ Require Export mathcomp_extra.
 Require Export functions.
 Require Export cardinality.
 Require Export fsbigop.
+Require Export set_interval.

classical/mathcomp_extra.v

@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import ssreflect ssrbool ssrfun seq bigop ssralg ssrnum.
+From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
 Require Import boolp classical_sets.
 
 (******************************************************************************)
@@ -9,6 +9,8 @@ Require Import boolp classical_sets.
 (*          pred_omap 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                                  *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -90,6 +92,142 @@ 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.
+move: i => [[ba a|[]] [bb b|[]]] //= ab; first exact: mid_in_itv.
+  by rewrite !in_itv -lteif_subl_addl subrr lteif01.
+by rewrite !in_itv lteif_subl_addr -lteif_subl_addl subrr lteif01.
+Qed.
+
+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.
+case: a => [b x|[]//] y.
+by rewrite !inE !subitvE/= bnd_simp andbT !lteBSide/= lteifNE negbK.
+Qed.
+
+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.
+case: i => [a a']; move=> x; rewrite inE/= itv_splitI negb_and.
+by symmetry; rewrite inE/= -predC_itvl -predC_itvr.
+Qed.
+
+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.