rename and boolify some predicates for open intervals

Author: t6s

CHANGELOG_UNRELEASED.md

@@ -3,10 +3,17 @@
 ## [Unreleased]
 
 ### Added
+- in set_interval.v
+  + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
 ### Changed
+- in set_interval.v
+  + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
 ### Renamed
+- in set_interval.v
+  + `itv_is_ray` -> `itv_is_open_unbounded`,
+  + `itv_is_bd_open` -> `itv_is_oo`,
 
 ### Generalized
 

classical/classical_orders.v

@@ -329,7 +329,7 @@ Lemma big_lexi_order_interval_prefix (i : interval (big_lexi_order K))
   itv_open_ends i -> x \in i ->
   exists n, same_prefix n x `<=` [set` i].
 Proof.
-move: i; case=> [][[]l|[]] [[]r|[]] [][]; rewrite ?in_itv /= ?andbT.
+move: i; case=> [][[]l|[]] [[]r|[]] /orP []// ?; rewrite ?in_itv /= ?andbT.
 - move=> /andP[lx xr].
   case E1 : (first_diff l x) => [m|]; first last.
     by move: lx; move/first_diff_NoneP : E1 ->; rewrite bnd_simp.

classical/set_interval.v

@@ -12,22 +12,28 @@ From mathcomp Require Import functions.
 (* This files contains lemmas about sets and intervals.                       *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*              neitv i == the interval i is non-empty                        *)
-(*                         when the support type is a numFieldType, this      *)
-(*                         is equivalent to (i.1 < i.2)%O (lemma neitvE)      *)
-(*   set_itv_infty_set0 == multirule to simplify empty intervals              *)
-(*      line_path a b t := (1 - t) * a + t * b, convexity operator over a     *)
-(*                         numDomainType                                      *)
-(*          ndline_path == line_path a b with the constraint that a < b       *)
-(*         factor a b x := (x - a) / (b - a)                                  *)
-(*             set_itvE == multirule to turn intervals into inequalities      *)
-(*     disjoint_itv i j == intervals i and j are disjoint                     *)
-(*         itv_is_ray i == i is either `]x, +oo[ or `]-oo, x[                 *)
-(*     itv_is_bd_open i == i is `]x, y[                                       *)
-(*      itv_open_ends i == i has open endpoints, i.e., it is one of the two   *)
-(*                         above                                              *)
-(*        is_open_itv A == the set A can be written as an open interval       *)
-(*     open_itv_cover A == the set A can be covered by open intervals         *)
+(*                   neitv i == the interval i is non-empty                   *)
+(*                              when the support type is a numFieldType, this *)
+(*                              is equivalent to (i.1 < i.2)%O (lemma neitvE) *)
+(*        set_itv_infty_set0 == multirule to simplify empty intervals         *)
+(*           line_path a b t := (1 - t) * a + t * b, convexity operator over  *)
+(*                              a numDomainType                               *)
+(*               ndline_path == line_path a b with the constraint that a < b  *)
+(*              factor a b x := (x - a) / (b - a)                             *)
+(*                  set_itvE == multirule to turn intervals into inequalities *)
+(*          disjoint_itv i j == intervals i and j are disjoint                *)
+(*   itv_is_open_unbounded i == i is either `]x, +oo[, `]-oo, x[ or           *)
+(*                              `]-oo, +oo[                                   *)
+(*               itv_is_oo i == i is `]x, y[                                  *)
+(*           itv_open_ends i == i has open endpoints, i.e., it is one of the  *)
+(*                              two above                                     *)
+(* itv_is_closed_unbounded i == i is either `[x, +oo[, `]-oo, x] or           *)
+(*                              `]-oo, +oo[                                   *)
+(*               itv_is_cc i == i is `[x, y]                                  *)
+(*         itv_closed_ends i == i has closed endpoints, i.e., it is one of    *)
+(*                              the two above                                 *)
+(*             is_open_itv A == the set A can be written as an open interval  *)
+(*          open_itv_cover A == the set A can be covered by open intervals    *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -806,22 +812,17 @@ Definition is_open_itv (A : set T) := exists ab, A = `]ab.1, ab.2[%classic.
 Definition open_itv_cover (A : set T) := [set F : nat -> set T |
   (forall i, is_open_itv (F i)) /\ A `<=` \bigcup_k (F k)].
 
-Definition itv_is_ray (i : interval T) : Prop :=
+Definition itv_is_open_unbounded (i : interval T) : bool :=
   match i with
-  | Interval -oo%O (BLeft _) => True
-  | Interval (BRight _) +oo%O => True
-  | Interval -oo%O +oo%O => True
-  | _ => False
+  | `]-oo, _[ | `]_, +oo[ | `]-oo, +oo[ => true
+  | _ => false
   end.
 
-Definition itv_is_bd_open (i : interval T) : Prop :=
-  match i with
-  | Interval (BRight _) (BLeft _) => True
-  | _ => False
-  end.
+Definition itv_is_oo (i : interval T) : bool :=
+  if i is `]_, _[ then true else false.
 
-Definition itv_open_ends (i : interval T) : Prop :=
-  itv_is_ray i \/ itv_is_bd_open i.
+Definition itv_open_ends (i : interval T) : bool :=
+  (itv_is_open_unbounded i) || (itv_is_oo i).
 
 Lemma itv_open_ends_rside l b (t : T) :
   itv_open_ends (Interval l (BSide b t)) -> b = true.
@@ -840,17 +841,35 @@ Lemma itv_open_ends_linfty l b :
 Proof. by case: b => //; move: l => [[]?|[]] // []. Qed.
 
 Lemma is_open_itv_itv_is_bd_openP (i : interval T) :
-  itv_is_bd_open i -> is_open_itv [set` i].
+  itv_is_oo i -> is_open_itv [set` i].
 Proof.
 by case: i=> [] [[]l|[]] // [[]r|[]] // ?; exists (l,r).
 Qed.
 
 End open_endpoints.
 
+Section closed_endpoints.
+Context {d} {T : porderType d}.
+
+Definition itv_is_closed_unbounded (i : interval T) : bool :=
+  match i with
+  | `[_, +oo[ | `]-oo, _[ | `]-oo, +oo[ => true
+  | _ => false
+  end.
+
+Definition itv_is_cc (i : interval T) : bool :=
+  if i is `[_, _] then true else false.
+
+Definition itv_closed_ends (i : interval T) : bool :=
+  (itv_is_closed_unbounded i) || (itv_is_cc i).
+
+End closed_endpoints.
+
 Lemma itv_open_endsI {d} {T : orderType d} (i j : interval T) :
   itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O.
 Proof.
-move: i => [][[]a|[]] [[]b|[]] []//= _; move: j => [][[]x|[]] [[]y|[]] []//= _;
+move: i => [][[]a|[]] [[]b|[]] /orP []//= _;
+move: j => [][[]x|[]] [[]y|[]] /orP []//= _;
 by rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=;
   try ((by left)||(by right)).
 Qed.

theories/normedtype_theory/ereal_normedtype.v

@@ -496,7 +496,7 @@ apply/seteqP; split=> A.
   + case=> M [Mreal MA].
     exists `]-oo, M%:E[ => [|y/=]; rewrite in_itv/= ?ltNyr; last exact: MA.
     by split => //; left.
-- move=> [[ [[]/= r|[]] [[]/= s|[]] ]] [] []// _.
+- move=> [[ [[]/= r|[]] [[]/= s|[]] ]] [] /orP []// _.
   + move=> /[dup]/ltgte_fin_num/fineK <-; rewrite in_itv/=.
     move=> /andP[rx sx] rsA; apply: (nbhs_interval rx sx) => z rz zs.
     by apply: rsA =>/=; rewrite in_itv/= rz.

theories/topology_theory/bool_topology.v

@@ -30,9 +30,9 @@ Proof.
 rewrite nbhs_principalE eqEsubset; split=> U; first last.
   by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
 move/principal_filterP; case: b.
-  move=> Ut; exists `]false, +oo[; first split => //; first by left.
+  move=> Ut; exists `]false, +oo[; first split => //.
   by move=> r /=; rewrite in_itv /=; case: r.
-move=> Ut; exists `]-oo, true[; first split => //; first by left.
+move=> Ut; exists `]-oo, true[; first split => //.
 by move=> r /=; rewrite in_itv /=; case: r.
 Qed.
 

theories/topology_theory/nat_topology.v

@@ -27,9 +27,9 @@ Proof.
 rewrite nbhs_principalE eqEsubset; split=> U; first last.
   by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
 move/principal_filterP; case: n.
-  move=> U0; exists `]-oo, 1[; first split => //; first by left.
+  move=> U0; exists `]-oo, 1[; first split => //.
   by move=> r /=; rewrite in_itv /=; case: r.
-move=> n USn; exists `]n, n.+2[; first split => //; first by right.
+move=> n USn; exists `]n, n.+2[; first split => //.
   by rewrite in_itv; apply/andP;split => //=; rewrite /Order.lt //=.
 move=> r /=; rewrite in_itv /= => nr2; suff: r = n.+1 by move=> ->.
 exact/esym/le_anti.

theories/topology_theory/num_topology.v

@@ -86,11 +86,11 @@ Lemma real_order_nbhsE (R : realFieldType) (x : R^o) : nbhs x =
 Proof.
 rewrite eqEsubset; split => U.
   case => _ /posnumP[e] xeU.
-  exists (`]x - e%:num, x + e%:num[); first split; first by right.
+  exists (`]x - e%:num, x + e%:num[); first split => //.
     by rewrite in_itv/= -lter_distl subrr normr0.
   apply: subset_trans xeU => z /=.
   by rewrite in_itv /= -lter_distl distrC.
-case => [][[[]l|[]]] [[]r|[]] [[]]//= _.
+case => [][[[]l|[]]] [[]r|[]] [] /orP[]//= _.
 - move=> xlr lrU; exists (Order.min (x - l) (r - x)).
     by rewrite /= lt_min ?lterBDr ?add0r ?(itvP xlr).
   apply/(subset_trans _ lrU)/subset_ball_prop_in_itv.

theories/topology_theory/order_topology.v

@@ -95,7 +95,7 @@ Hint Resolve itv_open : core.
 
 Lemma itv_open_ends_open (i : interval T) : itv_open_ends i -> open [set` i].
 Proof.
-case: i; rewrite /itv_open_ends => [[[]t1|[]]] [[]t2|[]] []? => //.
+case: i; rewrite /itv_open_ends => [[[]t1|[]]] [[]t2|[]] /orP[]? => //.
 by rewrite set_itvE; exact: openT.
 Qed.
 
@@ -202,19 +202,19 @@ HB.instance Definition _ := isPointed.Build (interval T) (`]-oo,+oo[).
 
 HB.instance Definition _ := Order.Total.on oT.
 HB.instance Definition _ := @isSubBaseTopological.Build oT
-  (interval T) (itv_is_ray) (fun i => [set` i]).
+  (interval T) (itv_is_open_unbounded) (fun i => [set` i]).
 
 Lemma order_nbhs_itv (x : oT) : nbhs x = filter_from
     (fun i => itv_open_ends i /\ x \in i)
     (fun i => [set` i]).
 Proof.
 rewrite eqEsubset; split => U; first last.
-  case=> /= i [ro xi /filterS]; apply; move: ro => [rayi|].
+  case=> /= i [ro xi /filterS]; apply; move: ro => /orP [rayi|].
     exists [set` i]; split => //=.
     exists [set [set` i]]; last by rewrite bigcup_set1.
     move=> A ->; exists (fset1 i); last by rewrite set_fset1 bigcap_set1.
     by move=> ?; rewrite !inE => /eqP ->.
-  case: i xi => [][[]l|[]] [[]r|[]] xlr []//=; exists `]l, r[%classic.
+  case: i xi => [][[]l|[]] [[]r|[]] xlr//= ?; exists `]l, r[%classic.
   split => //; exists [set `]l, r[%classic]; last by rewrite bigcup_set1.
   move=> ? ->; exists [fset `]-oo, r[ ; `]l, +oo[]%fset.
     by move=> ?; rewrite !inE => /orP[] /eqP ->.
@@ -224,8 +224,8 @@ case=> ? [[ I Irp] <-] [?] /[dup] /(Irp _) [F rayF <-] IF Fix IU.
 pose j := \big[Order.meet/`]-oo, +oo[]_(i <- F) i.
 exists j; first split.
 - rewrite /j (@eq_fbig_cond _ _ _ _ _ F _ (mem F) _ id)//.
-  + apply: big_ind; [by left| exact: itv_open_endsI|].
-    by move=> i /rayF /set_mem ?; left.
+  + apply: (big_ind itv_open_ends) => //=; first exact: itv_open_endsI.
+    by rewrite /itv_open_ends;  move=> i /rayF /set_mem ->.
   + by move=> p /=; rewrite !inE/=; exact: andb_id2l.
 - pose f (i : interval T) : Prop := x \in i; suff : f j by [].
   rewrite /j (@eq_fbig_cond _ _ _ _ _ F _ (mem F) _ id)//=.

theories/topology_theory/weak_topology.v

@@ -203,7 +203,7 @@ Let WeakU : topologicalType := @weak_topology (sub_type Y) X val.
 Lemma open_order_weak (U : set Y) : @open OrdU U -> @open WeakU U.
 Proof.
 rewrite ?openE /= /interior => + x Ux => /(_ x Ux); rewrite itv_nbhsE /=.
-move=> [][][[]l|[]] [[]r|[]][][]//= _ xlr /filterS; apply.
+move=> [][][[]l|[]] [[]r|[]][]/orP[]//= _ xlr /filterS; apply.
 - exists `]l, r[%classic; split => //=; exists `]\val l, \val r[%classic.
     exact: itv_open.
   by rewrite eqEsubset; split => z; rewrite preimage_itv.