diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b..9d8675134 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/classical/classical_orders.v b/classical/classical_orders.v index bd82a8206..9d2eefccd 100644 --- a/classical/classical_orders.v +++ b/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|[]]// ?; 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. diff --git a/classical/set_interval.v b/classical/set_interval.v index ae5d6163c..99c290be5 100644 --- a/classical/set_interval.v +++ b/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 *) (* ``` *) (* *) (******************************************************************************) @@ -800,28 +806,22 @@ End disjoint_itv_numDomain. Section open_endpoints. Context {d} {T : porderType d}. +Implicit Types (i : interval T). 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)]. + (forall k, is_open_itv (F k)) /\ A `<=` \bigcup_k (F k)]. -Definition itv_is_ray (i : interval T) : Prop := +Definition itv_is_open_unbounded i : 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 : 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 : 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. @@ -839,20 +839,33 @@ Lemma itv_open_ends_linfty l b : itv_open_ends (Interval (BInfty T b) l) -> b = true. 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]. -Proof. -by case: i=> [] [[]l|[]] // [[]r|[]] // ?; exists (l,r). -Qed. +Lemma is_open_itv_itv_is_bd_openP 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}. +Implicit Types (i : interval T). + +Definition itv_is_closed_unbounded i : bool := + match i with + | `[_, +oo[ | `]-oo, _[ | `]-oo, +oo[ => true + | _ => false + end. + +Definition itv_is_cc i : bool := if i is `[_, _] then true else false. + +Definition itv_closed_ends i : bool := itv_is_closed_unbounded i || itv_is_cc i. + +End closed_endpoints. + +Arguments itv_open_ends {d T} !i /. 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|[]] []//= _; -by rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=; - try ((by left)||(by right)). +by move: i => [][[]a|[]] [[]b|[]]//=; move: j => [][[]x|[]] [[]y|[]]//=; + rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=. Qed. Lemma itv_setU {d} {T : orderType d} (i j : interval T) : diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v index 1898baccb..db2bca516 100644 --- a/theories/normedtype_theory/ereal_normedtype.v +++ b/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|[]] ]][]// _. + 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. diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index bdd696a64..27fedd92e 100644 --- a/theories/topology_theory/bool_topology.v +++ b/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. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 781873482..952362f47 100644 --- a/theories/topology_theory/nat_topology.v +++ b/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. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 98fea7cda..df7c804f2 100644 --- a/theories/topology_theory/num_topology.v +++ b/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|[]] []//= _. - 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. diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 8ebe9b922..0658f12ce 100644 --- a/theories/topology_theory/order_topology.v +++ b/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|[]]// ?. 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)//=. diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 963fefbf7..7d8ab3139 100644 --- a/theories/topology_theory/weak_topology.v +++ b/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|[]][]//= _ 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.