@@ -12,22 +12,28 @@ From mathcomp Require Import functions.
1212(* This files contains lemmas about sets and intervals. *)
1313(* *)
1414(* ``` *)
15- (* neitv i == the interval i is non-empty *)
16- (* when the support type is a numFieldType, this *)
17- (* is equivalent to (i.1 < i.2)%O (lemma neitvE) *)
18- (* set_itv_infty_set0 == multirule to simplify empty intervals *)
19- (* line_path a b t := (1 - t) * a + t * b, convexity operator over a *)
20- (* numDomainType *)
21- (* ndline_path == line_path a b with the constraint that a < b *)
22- (* factor a b x := (x - a) / (b - a) *)
23- (* set_itvE == multirule to turn intervals into inequalities *)
24- (* disjoint_itv i j == intervals i and j are disjoint *)
25- (* itv_is_ray i == i is either `]x, +oo[ or `]-oo, x[ *)
26- (* itv_is_bd_open i == i is `]x, y[ *)
27- (* itv_open_ends i == i has open endpoints, i.e., it is one of the two *)
28- (* above *)
29- (* is_open_itv A == the set A can be written as an open interval *)
30- (* open_itv_cover A == the set A can be covered by open intervals *)
15+ (* neitv i == the interval i is non-empty *)
16+ (* when the support type is a numFieldType, this *)
17+ (* is equivalent to (i.1 < i.2)%O (lemma neitvE) *)
18+ (* set_itv_infty_set0 == multirule to simplify empty intervals *)
19+ (* line_path a b t := (1 - t) * a + t * b, convexity operator over *)
20+ (* a numDomainType *)
21+ (* ndline_path == line_path a b with the constraint that a < b *)
22+ (* factor a b x := (x - a) / (b - a) *)
23+ (* set_itvE == multirule to turn intervals into inequalities *)
24+ (* disjoint_itv i j == intervals i and j are disjoint *)
25+ (* itv_is_open_unbounded i == i is either `]x, +oo[, `]-oo, x[ or *)
26+ (* `]-oo, +oo[ *)
27+ (* itv_is_oo i == i is `]x, y[ *)
28+ (* itv_open_ends i == i has open endpoints, i.e., it is one of the *)
29+ (* two above *)
30+ (* itv_is_closed_unbounded i == i is either `[x, +oo[, `]-oo, x] or *)
31+ (* `]-oo, +oo[ *)
32+ (* itv_is_cc i == i is `[x, y] *)
33+ (* itv_closed_ends i == i has closed endpoints, i.e., it is one of *)
34+ (* the two above *)
35+ (* is_open_itv A == the set A can be written as an open interval *)
36+ (* open_itv_cover A == the set A can be covered by open intervals *)
3137(* ``` *)
3238(* *)
3339(***************************************************************************** *)
@@ -800,28 +806,22 @@ End disjoint_itv_numDomain.
800806
801807Section open_endpoints.
802808Context {d} {T : porderType d}.
809+ Implicit Types (i : interval T).
803810
804811Definition is_open_itv (A : set T) := exists ab, A = `]ab.1, ab.2[%classic.
805812
806813Definition open_itv_cover (A : set T) := [set F : nat -> set T |
807- (forall i , is_open_itv (F i )) /\ A `<=` \bigcup_k (F k)].
814+ (forall k , is_open_itv (F k )) /\ A `<=` \bigcup_k (F k)].
808815
809- Definition itv_is_ray ( i : interval T) : Prop :=
816+ Definition itv_is_open_unbounded i : bool :=
810817 match i with
811- | Interval -oo%O (BLeft _) => True
812- | Interval (BRight _) +oo%O => True
813- | Interval -oo%O +oo%O => True
814- | _ => False
818+ | `]-oo, _[ | `]_, +oo[ | `]-oo, +oo[ => true
819+ | _ => false
815820 end .
816821
817- Definition itv_is_bd_open (i : interval T) : Prop :=
818- match i with
819- | Interval (BRight _) (BLeft _) => True
820- | _ => False
821- end .
822+ Definition itv_is_oo i : bool := if i is `]_, _[ then true else false.
822823
823- Definition itv_open_ends (i : interval T) : Prop :=
824- itv_is_ray i \/ itv_is_bd_open i.
824+ Definition itv_open_ends i : bool := itv_is_open_unbounded i || itv_is_oo i.
825825
826826Lemma itv_open_ends_rside l b (t : T) :
827827 itv_open_ends (Interval l (BSide b t)) -> b = true.
@@ -839,20 +839,32 @@ Lemma itv_open_ends_linfty l b :
839839 itv_open_ends (Interval (BInfty T b) l) -> b = true.
840840Proof . by case: b => //; move: l => [[]?|[]] // []. Qed .
841841
842- Lemma is_open_itv_itv_is_bd_openP (i : interval T) :
843- itv_is_bd_open i -> is_open_itv [set` i].
844- Proof .
845- by case: i=> [] [[]l|[]] // [[]r|[]] // ?; exists (l,r).
846- Qed .
842+ Lemma is_open_itv_itv_is_bd_openP i : itv_is_oo i -> is_open_itv [set` i].
843+ Proof . by case: i=> [] [[]l|[]] // [[]r|[]] // ?; exists (l,r). Qed .
847844
848845End open_endpoints.
849846
847+ Section closed_endpoints.
848+ Context {d} {T : porderType d}.
849+ Implicit Types (i : interval T).
850+
851+ Definition itv_is_closed_unbounded i : bool :=
852+ match i with
853+ | `[_, +oo[ | `]-oo, _[ | `]-oo, +oo[ => true
854+ | _ => false
855+ end .
856+
857+ Definition itv_is_cc i : bool := if i is `[_, _] then true else false.
858+
859+ Definition itv_closed_ends i : bool := itv_is_closed_unbounded i || itv_is_cc i.
860+
861+ End closed_endpoints.
862+
850863Lemma itv_open_endsI {d} {T : orderType d} (i j : interval T) :
851864 itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O.
852865Proof .
853- move: i => [][[]a|[]] [[]b|[]] []//= _; move: j => [][[]x|[]] [[]y|[]] []//= _;
854- by rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=;
855- try ((by left)||(by right)).
866+ by move: i => [][[]a|[]] [[]b|[]]//=; move: j => [][[]x|[]] [[]y|[]]//=;
867+ rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=.
856868Qed .
857869
858870Lemma itv_setU {d} {T : orderType d} (i j : interval T) :
0 commit comments