From 3e292da9f901e1032311181990bbc1dd160105bb Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 7 Oct 2019 14:31:34 +0200 Subject: The new interval library - `x <= y ?< if c` (lersif) has been replaced with `x < y ?<= if c'` (lteif) where `c'` is negation of `c`. This change makes statements of several lemmas (e.g., `lteif_orb`) easily comprehensible. - The first constructor `BOpen_if` of `itv_bound` has been replaced with `BClose_if` where the first argument is inverted. Now `pred_of_itv` is defined by using `lteif` instead of `lersif`. - Intervals of `T : porderType` form a `porderType` where the ordering relation is the subset relation. If `T` is a `latticeType`, intervals also form a `latticeType` where the join and meet are intersection and convex hull respectively. They are distributive if `T` is an `orderType`. --- mathcomp/algebra/interval.v | 1783 +++++++++++++++++++++++++++++++++---------- 1 file changed, 1392 insertions(+), 391 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 950546b..03b5e4d 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -4,264 +4,164 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. From mathcomp Require Import div fintype bigop order ssralg finset fingroup. From mathcomp Require Import ssrnum. -(*****************************************************************************) -(* This file provide support for intervals in numerical and real domains. *) -(* The datatype (interval R) gives a formal characterization of an *) -(* interval, as the pair of its right and left bounds. *) -(* interval R == the type of formal intervals on R. *) -(* x \in i == when i is a formal interval on a numeric domain, *) -(* \in can be used to test membership. *) -(* itvP x_in_i == where x_in_i has type x \in i, if i is ground, *) -(* gives a set of rewrite rules that x_in_i imply. *) -(* x <= y ?< if c == x is smaller than y, and strictly if c is true *) -(* *) -(* We provide a set of notations to write intervals (see below) *) -(* `[a, b], `]a, b], ..., `]-oo, a], ..., `]-oo, +oo[ *) -(* We also provide the lemma subitvP which computes the inequalities one *) -(* needs to prove when trying to prove the inclusion of intervals. *) -(* *) -(* Remark that we cannot implement a boolean comparison test for intervals *) -(* on an arbitrary numeric domains, for this problem might be undecidable. *) -(* Note also that type (interval R) may contain several inhabitants coding *) -(* for the same interval. However, this pathological issues do nor arise *) -(* when R is a real domain: we could provide a specific theory for this *) -(* important case. *) -(* *) -(* See also ``Formal proofs in real algebraic geometry: from ordered fields *) -(* to quantifier elimination'', LMCS journal, 2012 *) -(* by Cyril Cohen and Assia Mahboubi *) -(* *) -(* And "Formalized algebraic numbers: construction and first-order theory" *) -(* Cyril Cohen, PhD, 2012, section 4.3. *) -(*****************************************************************************) +(******************************************************************************) +(* This file provide support for intervals in ordered types. The datatype *) +(* (interval T) gives a formal characterization of an interval, as the pair *) +(* of its right and left bounds. *) +(* interval R == the type of formal intervals on R. *) +(* x \in i == when i is a formal interval on an ordered type, *) +(* \in can be used to test membership. *) +(* itvP x_in_i == where x_in_i has type x \in i, if i is ground, *) +(* gives a set of rewrite rules that x_in_i imply. *) +(* x < y ?<= if c == x is smaller than y, and strictly if c is false *) +(* *) +(* Intervals of T form an partially ordered type (porderType) whose ordering *) +(* is the subset relation. If T is a lattice, intervals also form a lattice *) +(* (latticeType) whose meet and join are intersection and convex hull *) +(* respectively. They are distributive if T is an orderType. *) +(* *) +(* We provide a set of notations to write intervals (see below) *) +(* `[a, b], `]a, b], ..., `]-oo, a], ..., `]-oo, +oo[ *) +(* We also provide the lemma subitvP which computes the inequalities one *) +(* needs to prove when trying to prove the inclusion of intervals. *) +(* *) +(* Remark that we cannot implement a boolean comparison test for intervals on *) +(* an arbitrary ordered types, for this problem might be undecidable. Note *) +(* also that type (interval R) may contain several inhabitants coding for the *) +(* same interval. However, this pathological issues do nor arise when R is a *) +(* real domain: we could provide a specific theory for this important case. *) +(* *) +(* See also ``Formal proofs in real algebraic geometry: from ordered fields *) +(* to quantifier elimination'', LMCS journal, 2012 *) +(* by Cyril Cohen and Assia Mahboubi *) +(* *) +(* And "Formalized algebraic numbers: construction and first-order theory" *) +(* Cyril Cohen, PhD, 2012, section 4.3. *) +(******************************************************************************) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Local Open Scope ring_scope. -Import Order.TTheory GRing.Theory Num.Theory. - -Local Notation mid x y := ((x + y) / 2%:R). +Local Open Scope order_scope. +Import Order.TTheory. -Section LersifPo. +Section LteifPOrder. -Variable R : numDomainType. -Implicit Types (b : bool) (x y z : R). +Variable (disp : unit) (T : porderType disp). +Implicit Types (b : bool) (x y z : T). -Definition lersif (x y : R) b := if b then x < y else x <= y. +Definition lteif x y b := if b then x <= y else x < y. -Local Notation "x <= y ?< 'if' b" := (lersif x y b) +Local Notation "x < y ?<= 'if' b" := (lteif x y b) (at level 70, y at next level, - format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope. - -Lemma subr_lersifr0 b (x y : R) : (y - x <= 0 ?< if b) = (y <= x ?< if b). -Proof. by case: b => /=; rewrite subr_lte0. Qed. - -Lemma subr_lersif0r b (x y : R) : (0 <= y - x ?< if b) = (x <= y ?< if b). -Proof. by case: b => /=; rewrite subr_gte0. Qed. + format "x '[hv' < y '/' ?<= 'if' b ']'") : order_scope. -Definition subr_lersif0 := (subr_lersifr0, subr_lersif0r). - -Lemma lersif_trans x y z b1 b2 : - x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2. +Lemma lteif_trans x y z b1 b2 : + x < y ?<= if b1 -> y < z ?<= if b2 -> x < z ?<= if b1 && b2. Proof. -by case: b1 b2 => [] []; - [apply: lt_trans | apply: lt_le_trans | apply: le_lt_trans | apply: le_trans]. +case: b1 b2 => [][]; + [exact: le_trans | exact: le_lt_trans | exact: lt_le_trans | exact: lt_trans]. Qed. -Lemma lersif01 b : 0 <= 1 ?< if b. -Proof. by case: b; apply lter01. Qed. +Lemma lteif_anti b1 b2 x y : + (x < y ?<= if b1) && (y < x ?<= if b2) = b1 && b2 && (x == y). +Proof. by case: b1 b2 => [][]; rewrite lte_anti. Qed. -Lemma lersif_anti b1 b2 x y : - (x <= y ?< if b1) && (y <= x ?< if b2) = - if b1 || b2 then false else x == y. -Proof. by case: b1 b2 => [] []; rewrite lte_anti. Qed. - -Lemma lersifxx x b : (x <= x ?< if b) = ~~ b. +Lemma lteifxx x b : (x < x ?<= if b) = b. Proof. by case: b; rewrite /= ltexx. Qed. -Lemma lersifNF x y b : y <= x ?< if ~~ b -> x <= y ?< if b = false. -Proof. by case: b => /= [/le_gtF|/lt_geF]. Qed. +Lemma lteifNF x y b : y < x ?<= if ~~ b -> x < y ?<= if b = false. +Proof. by case: b => [/lt_geF|/le_gtF]. Qed. -Lemma lersifS x y b : x < y -> x <= y ?< if b. +Lemma lteifS x y b : x < y -> x < y ?<= if b. Proof. by case: b => //= /ltW. Qed. -Lemma lersifT x y : x <= y ?< if true = (x < y). Proof. by []. Qed. - -Lemma lersifF x y : x <= y ?< if false = (x <= y). Proof. by []. Qed. - -Lemma lersif_oppl b x y : - x <= y ?< if b = (- y <= x ?< if b). -Proof. by case: b; apply lter_oppl. Qed. - -Lemma lersif_oppr b x y : x <= - y ?< if b = (y <= - x ?< if b). -Proof. by case: b; apply lter_oppr. Qed. - -Lemma lersif_0oppr b x : 0 <= - x ?< if b = (x <= 0 ?< if b). -Proof. by case: b; apply (oppr_ge0, oppr_gt0). Qed. - -Lemma lersif_oppr0 b x : - x <= 0 ?< if b = (0 <= x ?< if b). -Proof. by case: b; apply (oppr_le0, oppr_lt0). Qed. - -Lemma lersif_opp2 b : {mono -%R : x y /~ x <= y ?< if b}. -Proof. by case: b; apply lter_opp2. Qed. - -Definition lersif_oppE := (lersif_0oppr, lersif_oppr0, lersif_opp2). - -Lemma lersif_add2l b x : {mono +%R x : y z / y <= z ?< if b}. -Proof. by case: b => ? ?; apply lter_add2. Qed. - -Lemma lersif_add2r b x : {mono +%R^~ x : y z / y <= z ?< if b}. -Proof. by case: b => ? ?; apply lter_add2. Qed. - -Definition lersif_add2 := (lersif_add2l, lersif_add2r). - -Lemma lersif_subl_addr b x y z : (x - y <= z ?< if b) = (x <= z + y ?< if b). -Proof. by case: b; apply lter_sub_addr. Qed. - -Lemma lersif_subr_addr b x y z : (x <= y - z ?< if b) = (x + z <= y ?< if b). -Proof. by case: b; apply lter_sub_addr. Qed. - -Definition lersif_sub_addr := (lersif_subl_addr, lersif_subr_addr). +Lemma lteifT x y : x < y ?<= if true = (x <= y). Proof. by []. Qed. -Lemma lersif_subl_addl b x y z : (x - y <= z ?< if b) = (x <= y + z ?< if b). -Proof. by case: b; apply lter_sub_addl. Qed. - -Lemma lersif_subr_addl b x y z : (x <= y - z ?< if b) = (z + x <= y ?< if b). -Proof. by case: b; apply lter_sub_addl. Qed. - -Definition lersif_sub_addl := (lersif_subl_addl, lersif_subr_addl). +Lemma lteifF x y : x < y ?<= if false = (x < y). Proof. by []. Qed. -Lemma lersif_andb x y : {morph lersif x y : p q / p || q >-> p && q}. -Proof. -by case=> [] [] /=; rewrite ?le_eqVlt; - case: (_ < _)%R; rewrite ?(orbT, orbF, andbF, andbb). -Qed. +Lemma lteif_orb x y : {morph lteif x y : p q / p || q}. +Proof. by case=> [][] /=; case: comparableP. Qed. -Lemma lersif_orb x y : {morph lersif x y : p q / p && q >-> p || q}. -Proof. -by case=> [] [] /=; rewrite ?le_eqVlt; - case: (_ < _)%R; rewrite ?(orbT, orbF, orbb). -Qed. +Lemma lteif_andb x y : {morph lteif x y : p q / p && q}. +Proof. by case=> [][] /=; case: comparableP. Qed. -Lemma lersif_imply b1 b2 r1 r2 : - b2 ==> b1 -> r1 <= r2 ?< if b1 -> r1 <= r2 ?< if b2. -Proof. by case: b1 b2 => [] [] //= _ /ltW. Qed. +Lemma lteif_imply b1 b2 x y : b1 ==> b2 -> x < y ?<= if b1 -> x < y ?<= if b2. +Proof. by case: b1 b2 => [][] //= _ /ltW. Qed. -Lemma lersifW b x y : x <= y ?< if b -> x <= y. +Lemma lteifW b x y : x < y ?<= if b -> x <= y. Proof. by case: b => // /ltW. Qed. -Lemma ltrW_lersif b x y : x < y -> x <= y ?< if b. +Lemma ltrW_lteif b x y : x < y -> x < y ?<= if b. Proof. by case: b => // /ltW. Qed. -Lemma lersif_pmul2l b x : 0 < x -> {mono *%R x : y z / y <= z ?< if b}. -Proof. by case: b; apply lter_pmul2l. Qed. - -Lemma lersif_pmul2r b x : 0 < x -> {mono *%R^~ x : y z / y <= z ?< if b}. -Proof. by case: b; apply lter_pmul2r. Qed. - -Lemma lersif_nmul2l b x : x < 0 -> {mono *%R x : y z /~ y <= z ?< if b}. -Proof. by case: b; apply lter_nmul2l. Qed. - -Lemma lersif_nmul2r b x : x < 0 -> {mono *%R^~ x : y z /~ y <= z ?< if b}. -Proof. by case: b; apply lter_nmul2r. Qed. - -Lemma real_lersifN x y b : x \is Num.real -> y \is Num.real -> - x <= y ?< if ~~b = ~~ (y <= x ?< if b). -Proof. by case: b => [] xR yR /=; case: real_ltgtP. Qed. - -Lemma real_lersif_norml b x y : - x \is Num.real -> - (`|x| <= y ?< if b) = ((- y <= x ?< if b) && (x <= y ?< if b)). -Proof. by case: b; apply real_lter_norml. Qed. - -Lemma real_lersif_normr b x y : - y \is Num.real -> - (x <= `|y| ?< if b) = ((x <= y ?< if b) || (x <= - y ?< if b)). -Proof. by case: b; apply real_lter_normr. Qed. - -Lemma lersif_nnormr b x y : y <= 0 ?< if ~~ b -> (`|x| <= y ?< if b) = false. -Proof. by case: b => /=; apply lter_nnormr. Qed. +Lemma comparable_lteifN x y b : + x >=< y -> x < y ?<= if ~~b = ~~ (y < x ?<= if b). +Proof. by case: b => /=; case: comparableP. Qed. -End LersifPo. +End LteifPOrder. -Notation "x <= y ?< 'if' b" := (lersif x y b) +Notation "x < y ?<= 'if' b" := (lteif x y b) (at level 70, y at next level, - format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope. - -Section LersifOrdered. - -Variable (R : realDomainType) (b : bool) (x y z e : R). - -Lemma lersifN : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b). -Proof. by rewrite real_lersifN ?num_real. Qed. + format "x '[hv' < y '/' ?<= 'if' b ']'") : order_scope. -Lemma lersif_norml : - (`|x| <= y ?< if b) = (- y <= x ?< if b) && (x <= y ?< if b). -Proof. by case: b; apply lter_norml. Qed. +Notation "x < y ?<= 'if' b" := (@lteif ring_display _ x y b) + (at level 70, y at next level, + format "x '[hv' < y '/' ?<= 'if' b ']'") : ring_scope. -Lemma lersif_normr : - (x <= `|y| ?< if b) = (x <= y ?< if b) || (x <= - y ?< if b). -Proof. by case: b; apply lter_normr. Qed. +Section LteifTotal. -Lemma lersif_distl : - (`|x - y| <= e ?< if b) = (y - e <= x ?< if b) && (x <= y + e ?< if b). -Proof. by case: b; apply lter_distl. Qed. +Variable (disp : unit) (T : orderType disp) (b : bool) (x y z e : T). -Lemma lersif_minr : - (x <= Num.min y z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b). +Lemma lteif_minr : + (x < Order.min y z ?<= if b) = (x < y ?<= if b) && (x < z ?<= if b). Proof. by case: b; rewrite /= (le_minr, lt_minr). Qed. -Lemma lersif_minl : - (Num.min y z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b). +Lemma lteif_minl : + (Order.min y z < x ?<= if b) = (y < x ?<= if b) || (z < x ?<= if b). Proof. by case: b; rewrite /= (le_minl, lt_minl). Qed. -Lemma lersif_maxr : - (x <= Num.max y z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b). +Lemma lteif_maxr : + (x < Order.max y z ?<= if b) = (x < y ?<= if b) || (x < z ?<= if b). Proof. by case: b; rewrite /= (le_maxr, lt_maxr). Qed. -Lemma lersif_maxl : - (Num.max y z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b). +Lemma lteif_maxl : + (Order.max y z < x ?<= if b) = (y < x ?<= if b) && (z < x ?<= if b). Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed. -End LersifOrdered. - -Section LersifField. - -Variable (F : numFieldType) (b : bool) (z x y : F). - -Lemma lersif_pdivl_mulr : 0 < z -> x <= y / z ?< if b = (x * z <= y ?< if b). -Proof. by case: b => ? /=; rewrite lter_pdivl_mulr. Qed. - -Lemma lersif_pdivr_mulr : 0 < z -> y / z <= x ?< if b = (y <= x * z ?< if b). -Proof. by case: b => ? /=; rewrite lter_pdivr_mulr. Qed. - -Lemma lersif_pdivl_mull : 0 < z -> x <= z^-1 * y ?< if b = (z * x <= y ?< if b). -Proof. by case: b => ? /=; rewrite lter_pdivl_mull. Qed. - -Lemma lersif_pdivr_mull : 0 < z -> z^-1 * y <= x ?< if b = (y <= z * x ?< if b). -Proof. by case: b => ? /=; rewrite lter_pdivr_mull. Qed. - -Lemma lersif_ndivl_mulr : z < 0 -> x <= y / z ?< if b = (y <= x * z ?< if b). -Proof. by case: b => ? /=; rewrite lter_ndivl_mulr. Qed. - -Lemma lersif_ndivr_mulr : z < 0 -> y / z <= x ?< if b = (x * z <= y ?< if b). -Proof. by case: b => ? /=; rewrite lter_ndivr_mulr. Qed. - -Lemma lersif_ndivl_mull : z < 0 -> x <= z^-1 * y ?< if b = (y <=z * x ?< if b). -Proof. by case: b => ? /=; rewrite lter_ndivl_mull. Qed. - -Lemma lersif_ndivr_mull : z < 0 -> z^-1 * y <= x ?< if b = (z * x <= y ?< if b). -Proof. by case: b => ? /=; rewrite lter_ndivr_mull. Qed. +Lemma lteifN : (x < y ?<= if ~~ b) = ~~ (y < x ?<= if b). +Proof. by rewrite comparable_lteifN ?comparableT. Qed. -End LersifField. +End LteifTotal. -Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty. -Notation BOpen := (BOpen_if true). -Notation BClose := (BOpen_if false). -Variant interval (T : Type) := Interval of itv_bound T & itv_bound T. +Variant itv_bound (T : Type) : Type := BClose_if of bool & T | BInfty. +Definition itv_boundl := itv_bound. +Definition itv_boundr := itv_bound. +Notation BOpen := (BClose_if false). +Notation BClose := (BClose_if true). +Variant interval (T : Type) := Interval of itv_boundl T & itv_boundr T. (* We provide the 9 following notations to help writing formal intervals *) +Notation "`[ a , b ]" := (Interval (BClose a) (BClose b)) + (at level 0, a, b at level 9 , format "`[ a , b ]") : order_scope. +Notation "`] a , b ]" := (Interval (BOpen a) (BClose b)) + (at level 0, a, b at level 9 , format "`] a , b ]") : order_scope. +Notation "`[ a , b [" := (Interval (BClose a) (BOpen b)) + (at level 0, a, b at level 9 , format "`[ a , b [") : order_scope. +Notation "`] a , b [" := (Interval (BOpen a) (BOpen b)) + (at level 0, a, b at level 9 , format "`] a , b [") : order_scope. +Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b)) + (at level 0, b at level 9 , format "`] '-oo' , b ]") : order_scope. +Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b)) + (at level 0, b at level 9 , format "`] '-oo' , b [") : order_scope. +Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _)) + (at level 0, a at level 9 , format "`[ a , '+oo' [") : order_scope. +Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _)) + (at level 0, a at level 9 , format "`] a , '+oo' [") : order_scope. +Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _)) + (at level 0, format "`] -oo , '+oo' [") : order_scope. + Notation "`[ a , b ]" := (Interval (BClose a) (BClose b)) (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope. Notation "`] a , b ]" := (Interval (BOpen a) (BClose b)) @@ -281,13 +181,17 @@ Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _)) Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _)) (at level 0, format "`] -oo , '+oo' [") : ring_scope. +Fact itv_boundl_display (disp : unit) : unit. Proof. exact. Qed. +Fact itv_boundr_display (disp : unit) : unit. Proof. exact. Qed. +Fact interval_display (disp : unit) : unit. Proof. exact. Qed. + Section IntervalEq. Variable T : eqType. Definition eq_itv_bound (b1 b2 : itv_bound T) : bool := match b1, b2 with - | BOpen_if a x, BOpen_if b y => (a == b) && (x == y) + | BClose_if a x, BClose_if b y => (a == b) && (x == y) | BInfty, BInfty => true | _, _ => false end. @@ -295,13 +199,14 @@ Definition eq_itv_bound (b1 b2 : itv_bound T) : bool := Lemma eq_itv_boundP : Equality.axiom eq_itv_bound. Proof. move=> b1 b2; apply: (iffP idP). -- by move: b1 b2 => [a x |] [b y |] => //= /andP [] /eqP -> /eqP ->. +- by move: b1 b2 => [a x|][b y|] => //= /andP [] /eqP -> /eqP ->. - by move=> <-; case: b1 => //= a x; rewrite !eqxx. Qed. Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP. -Canonical itv_bound_eqType := - Eval hnf in EqType (itv_bound T) itv_bound_eqMixin. +Canonical itv_bound_eqType := EqType (itv_bound T) itv_bound_eqMixin. +Canonical itv_boundl_eqType := [eqType of itv_boundl T]. +Canonical itv_boundr_eqType := [eqType of itv_boundr T]. Definition eqitv (x y : interval T) : bool := let: Interval x x' := x in @@ -310,327 +215,1423 @@ Definition eqitv (x y : interval T) : bool := Lemma eqitvP : Equality.axiom eqitv. Proof. move=> x y; apply: (iffP idP). -- by move: x y => [x x'] [y y'] => //= /andP [] /eqP -> /eqP ->. +- by move: x y => [x x'][y y'] => //= /andP [] /eqP -> /eqP ->. - by move=> <-; case: x => /= x x'; rewrite !eqxx. Qed. Canonical interval_eqMixin := EqMixin eqitvP. -Canonical interval_eqType := Eval hnf in EqType (interval T) interval_eqMixin. +Canonical interval_eqType := EqType (interval T) interval_eqMixin. End IntervalEq. -Section IntervalPo. +Module IntervalChoice. +Section IntervalChoice. -Variable R : numDomainType. +Variable T : choiceType. + +Lemma itv_bound_can : + cancel (fun b : itv_bound T => + match b with BInfty => None | BClose_if b x => Some (b, x) end) + (fun b => + match b with None => BInfty _ | Some (b, x) => BClose_if b x end). +Proof. by case. Qed. + +Lemma interval_can : + @cancel _ (interval T) + (fun '(Interval b1 b2) => (b1, b2)) (fun '(b1, b2) => Interval b1 b2). +Proof. by case. Qed. + +End IntervalChoice. + +Module Exports. + +Canonical itv_bound_choiceType (T : choiceType) := + ChoiceType (itv_bound T) (CanChoiceMixin (@itv_bound_can T)). +Canonical interval_choiceType (T : choiceType) := + ChoiceType (interval T) (CanChoiceMixin (@interval_can T)). +Canonical itv_boundl_choiceType (T : choiceType) := + [choiceType of itv_boundl T]. +Canonical itv_boundr_choiceType (T : choiceType) := + [choiceType of itv_boundr T]. + +Canonical itv_bound_countType (T : countType) := + CountType (itv_bound T) (CanCountMixin (@itv_bound_can T)). +Canonical interval_countType (T : countType) := + CountType (interval T) (CanCountMixin (@interval_can T)). +Canonical itv_boundl_countType (T : countType) := [countType of itv_boundl T]. +Canonical itv_boundr_countType (T : countType) := [countType of itv_boundr T]. + +Canonical itv_bound_finType (T : finType) := + FinType (itv_bound T) (CanFinMixin (@itv_bound_can T)). +Canonical interval_finType (T : finType) := + FinType (interval T) (CanFinMixin (@interval_can T)). +Canonical itv_boundl_finType (T : finType) := [finType of itv_boundl T]. +Canonical itv_boundr_finType (T : finType) := [finType of itv_boundr T]. -Definition pred_of_itv (i : interval R) : pred R := +End Exports. + +End IntervalChoice. +Export IntervalChoice.Exports. + +Section IntervalPOrder. + +Variable (disp : unit) (T : porderType disp). +Implicit Types (x y z : T) (i : interval T). + +Definition pred_of_itv i : pred T := [pred x | let: Interval l u := i in match l with - | BOpen_if b lb => lb <= x ?< if b + | BClose_if b lb => lb < x ?<= if b | BInfty => true end && match u with - | BOpen_if b ub => x <= ub ?< if b + | BClose_if b ub => x < ub ?<= if b | BInfty => true end]. + Canonical Structure itvPredType := PredType pred_of_itv. (* we compute a set of rewrite rules associated to an interval *) -Definition itv_rewrite (i : interval R) x : Type := +Definition itv_rewrite i x : Type := let: Interval l u := i in (match l with | BClose a => (a <= x) * (x < a = false) | BOpen a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false) - | BInfty => forall x : R, x == x + | BInfty => forall x : T, x == x end * - match u with + match u with | BClose b => (x <= b) * (b < x = false) | BOpen b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false) - | BInfty => forall x : R, x == x + | BInfty => forall x : T, x == x end * - match l, u with + match l, u with | BClose a, BClose b => (a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b]) | BClose a, BOpen b => (a <= b) * (a < b) * (b <= a = false) * (b < a = false) - * (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b]) + * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) | BOpen a, BClose b => (a <= b) * (a < b) * (b <= a = false) * (b < a = false) - * (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b]) + * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) | BOpen a, BOpen b => (a <= b) * (a < b) * (b <= a = false) * (b < a = false) - * (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b]) - | _, _ => forall x : R, x == x - end)%type. + * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) + | _, _ => forall x : T, x == x + end)%type. -Definition itv_decompose (i : interval R) x : Prop := +Definition itv_decompose i x : Prop := let: Interval l u := i in ((match l with - | BOpen_if b lb => (lb <= x ?< if b) : Prop + | BClose_if b lb => (lb < x ?<= if b) : Prop | BInfty => True end : Prop) * (match u with - | BOpen_if b ub => (x <= ub ?< if b) : Prop + | BClose_if b ub => (x < ub ?<= if b) : Prop | BInfty => True end : Prop))%type. -Lemma itv_dec : forall (x : R) (i : interval R), - reflect (itv_decompose i x) (x \in i). -Proof. by move=> ? [[? ?|] [? ?|]]; apply: (iffP andP); case. Qed. +Lemma itv_dec : forall x i, reflect (itv_decompose i x) (x \in i). +Proof. by move=> ? [[? ?|][? ?|]]; apply: (iffP andP); case. Qed. Arguments itv_dec {x i}. -Definition le_boundl (b1 b2 : itv_bound R) := +Definition le_boundl (b1 b2 : itv_boundl T) := match b1, b2 with - | BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if ~~ b2 && b1 - | BOpen_if _ _, BInfty => false + | BClose_if b1 x1, BClose_if b2 x2 => x1 < x2 ?<= if b2 ==> b1 + | BClose_if _ _, BInfty => false | _, _ => true end. -Definition le_boundr (b1 b2 : itv_bound R) := +Definition le_boundr (b1 b2 : itv_boundr T) := match b1, b2 with - | BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if ~~ b1 && b2 - | BInfty, BOpen_if _ _ => false + | BClose_if b1 x1, BClose_if b2 x2 => x1 < x2 ?<= if b1 ==> b2 + | BInfty, BClose_if _ _ => false | _, _ => true end. Lemma itv_boundlr bl br x : (x \in Interval bl br) = (le_boundl bl (BClose x)) && (le_boundr (BClose x) br). -Proof. by case: bl br => [? ? |] []. Qed. +Proof. by case: bl br => [? ?|][]. Qed. Lemma le_boundl_refl : reflexive le_boundl. Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed. -Hint Resolve le_boundl_refl : core. - Lemma le_boundr_refl : reflexive le_boundr. Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed. -Hint Resolve le_boundr_refl : core. +Hint Resolve le_boundl_refl le_boundr_refl : core. + +Lemma le_boundl_anti : antisymmetric le_boundl. +Proof. by case=> [[]?|][[]?|] //=; case: comparableP => // ->. Qed. + +Lemma le_boundl_converse_anti : antisymmetric (fun b => le_boundl ^~ b). +Proof. by move=> ? ? /le_boundl_anti. Qed. + +Lemma le_boundr_anti : antisymmetric le_boundr. +Proof. by case=> [[]?|][[]?|] //=; case: comparableP => // ->. Qed. Lemma le_boundl_trans : transitive le_boundl. Proof. -by move=> [[] x|] [[] y|] [[] z|] lexy leyz //; - apply: (lersif_imply _ (lersif_trans lexy leyz)). +by move=> [[] x|][[] y|][[] z|] lexy leyz //; + apply: (lteif_imply _ (lteif_trans lexy leyz)). Qed. +Lemma le_boundl_converse_trans : transitive (fun b => le_boundl ^~ b). +Proof. move=> ? ? ? ? /le_boundl_trans; exact. Qed. + Lemma le_boundr_trans : transitive le_boundr. Proof. -by move=> [[] x|] [[] y|] [[] z|] lexy leyz //; - apply: (lersif_imply _ (lersif_trans lexy leyz)). +by move=> [[] x|][[] y|][[] z|] lexy leyz //; + apply: (lteif_imply _ (lteif_trans lexy leyz)). Qed. Lemma le_boundl_bb x b1 b2 : - le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2). -Proof. by rewrite /le_boundl lersifxx andbC negb_and negbK implybE. Qed. + le_boundl (BClose_if b1 x) (BClose_if b2 x) = (b2 ==> b1). +Proof. by rewrite /le_boundl lteifxx. Qed. Lemma le_boundr_bb x b1 b2 : - le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1). -Proof. by rewrite /le_boundr lersifxx andbC negb_and negbK implybE. Qed. - -Lemma le_boundl_anti b1 b2 : (le_boundl b1 b2 && le_boundl b2 b1) = (b1 == b2). -Proof. by case: b1 b2 => [[] lr1 |] [[] lr2 |] //; rewrite lersif_anti. Qed. - -Lemma le_boundr_anti b1 b2 : (le_boundr b1 b2 && le_boundr b2 b1) = (b1 == b2). -Proof. by case: b1 b2 => [[] lr1 |] [[] lr2 |] //; rewrite lersif_anti. Qed. + le_boundr (BClose_if b1 x) (BClose_if b2 x) = (b1 ==> b2). +Proof. by rewrite /le_boundr lteifxx. Qed. Lemma itv_xx x bl br : - Interval (BOpen_if bl x) (BOpen_if br x) =i - if ~~ (bl || br) then pred1 x else pred0. -Proof. by move: bl br => [] [] y /=; rewrite !inE lersif_anti. Qed. + Interval (BClose_if bl x) (BClose_if br x) =i + if bl && br then pred1 x else pred0. +Proof. by move: bl br => [][] y /=; rewrite !inE lteif_anti /=. Qed. -Lemma itv_gte ba xa bb xb : xb <= xa ?< if ~~ (ba || bb) - -> Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0. +Lemma itv_gte ba xa bb xb : + xb < xa ?<= if ~~ (ba && bb) -> + Interval (BClose_if ba xa) (BClose_if bb xb) =i pred0. Proof. move=> ? y; rewrite itv_boundlr inE /=. -by apply/negP => /andP [] lexay /(lersif_trans lexay); rewrite lersifNF. +by apply/negP => /andP [] lexay /(lteif_trans lexay); rewrite lteifNF. Qed. Lemma boundl_in_itv : forall ba xa b, - xa \in Interval (BOpen_if ba xa) b = - if ba then false else le_boundr (BClose xa) b. -Proof. by move=> [] xa [b xb|]; rewrite inE lersifxx. Qed. + xa \in Interval (BClose_if ba xa) b = + if ba then le_boundr (BClose xa) b else false. +Proof. by move=> [] xa [b xb|]; rewrite inE lteifxx. Qed. Lemma boundr_in_itv : forall bb xb a, - xb \in Interval a (BOpen_if bb xb) = - if bb then false else le_boundl a (BClose xb). -Proof. by move=> [] xb [b xa|]; rewrite inE lersifxx /= ?andbT ?andbF. Qed. + xb \in Interval a (BClose_if bb xb) = + if bb then le_boundl a (BClose xb) else false. +Proof. by move=> [] xb [b xa|]; rewrite inE lteifxx /= ?andbT ?andbF. Qed. Definition bound_in_itv := (boundl_in_itv, boundr_in_itv). -Lemma itvP : forall (x : R) (i : interval R), x \in i -> itv_rewrite i x. +Lemma itvP : forall x i, x \in i -> itv_rewrite i x. Proof. -move=> x [[[] a|] [[] b|]] /itv_dec [ha hb]; do !split; +move=> x [[[] a|][[] b|]] /itv_dec [ha hb]; do !split; rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)]; - by [ | apply: ltW | move: (lersif_trans ha hb) => //=; exact: ltW ]. + by [| apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW]. Qed. Arguments itvP [x i]. -Definition itv_intersection (x y : interval R) : interval R := - let: Interval x x' := x in - let: Interval y y' := y in - Interval - (if le_boundl x y then y else x) - (if le_boundr x' y' then x' else y'). - -Definition itv_intersection1i : left_id `]-oo, +oo[ itv_intersection. -Proof. by case=> i []. Qed. - -Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection. -Proof. by case=> [[lb lr |] [ub ur |]]. Qed. +Definition itv_boundl_porderMixin := + @LePOrderMixin + (itv_boundl_eqType T) (fun b => le_boundl^~ b) _ (fun _ _ => erefl) + le_boundl_refl le_boundl_converse_anti le_boundl_converse_trans. +Canonical itv_boundl_porderType := + POrderType (itv_boundl_display disp) (itv_boundl T) itv_boundl_porderMixin. -Lemma itv_intersectionii : idempotent itv_intersection. -Proof. by case=> [[[] lr |] [[] ur |]] //=; rewrite !lexx. Qed. +Definition itv_boundr_porderMixin := + LePOrderMixin (fun _ _ => erefl) + le_boundr_refl le_boundr_anti le_boundr_trans. +Canonical itv_boundr_porderType := + POrderType (itv_boundr_display disp) (itv_boundr T) itv_boundr_porderMixin. -Definition subitv (i1 i2 : interval R) := +Definition subitv i1 i2 := match i1, i2 with - | Interval a1 b1, Interval a2 b2 => le_boundl a2 a1 && le_boundr b1 b2 + | Interval a1 b1, Interval a2 b2 => (a1 <= a2) && (b1 <= b2) end. -Lemma subitvP : forall (i2 i1 : interval R), subitv i1 i2 -> {subset i1 <= i2}. +Lemma subitv_refl : reflexive subitv. +Proof. by case=> /= ? ?; rewrite !lexx. Qed. + +Lemma subitv_anti : antisymmetric subitv. +Proof. +by case=> [? ?][? ?]; rewrite andbACA => /andP[] /le_anti -> /le_anti ->. +Qed. + +Lemma subitv_trans : transitive subitv. +Proof. +case=> [yl yr][xl xr][zl zr] /andP [Hl Hr] /andP [Hl' Hr'] /=. +by rewrite (le_trans Hl Hl') (le_trans Hr Hr'). +Qed. + +Definition interval_porderMixin := + LePOrderMixin (fun _ _ => erefl) subitv_refl subitv_anti subitv_trans. +Canonical interval_porderType := + POrderType (interval_display disp) (interval T) interval_porderMixin. + +Lemma subitvP i1 i2 : i1 <= i2 -> {subset i1 <= i2}. Proof. -by move=> [[b2 l2|] [b2' u2|]] [[b1 l1|] [b1' u1|]] +by case: i1 i2 => [[b2 l2|][b2' u2|]][[b1 l1|][b1' u1|]] /andP [] /= ha hb x /andP [ha' hb']; apply/andP; split => //; - (apply/lersif_imply: (lersif_trans ha ha'); case: b1 b2 ha ha' => [] []) || - (apply/lersif_imply: (lersif_trans hb' hb); case: b1' b2' hb hb' => [] []). + (apply/lteif_imply: (lteif_trans ha ha'); case: b1 b2 ha ha' => [][]) || + (apply/lteif_imply: (lteif_trans hb' hb); case: b1' b2' hb hb' => [][]). Qed. -Lemma subitvPr (a b1 b2 : itv_bound R) : +Lemma subitvPr (a : itv_boundl T) (b1 b2 : itv_boundr T) : le_boundr b1 b2 -> {subset (Interval a b1) <= (Interval a b2)}. -Proof. by move=> leb; apply: subitvP; rewrite /= leb andbT. Qed. +Proof. by move=> leb; apply: subitvP; rewrite /<=%O /= lexx. Qed. -Lemma subitvPl (a1 a2 b : itv_bound R) : +Lemma subitvPl (a1 a2 : itv_boundl T) (b : itv_boundr T) : le_boundl a2 a1 -> {subset (Interval a1 b) <= (Interval a2 b)}. -Proof. by move=> lea; apply: subitvP; rewrite /= lea /=. Qed. +Proof. by move=> lea; apply: subitvP; rewrite /<=%O /= lexx andbT. Qed. -Lemma lersif_in_itv ba bb xa xb x : - x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> - xa <= xb ?< if ba || bb. -Proof. by case: ba bb => [] [] /itvP /= ->. Qed. +Lemma inEsubitv x i : (x \in i) = (`[x, x] <= i). +Proof. by rewrite inE /=; case: i => [[[]?|][[]?|]]. Qed. + +Lemma lteif_in_itv ba bb xa xb x : + x \in Interval (BClose_if ba xa) (BClose_if bb xb) -> + xa < xb ?<= if ba && bb. +Proof. by case: ba bb => [][] /itvP /= ->. Qed. Lemma ltr_in_itv ba bb xa xb x : - ba || bb -> x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa < xb. -Proof. by move=> bab /lersif_in_itv; rewrite bab. Qed. + ~~ (ba && bb) -> x \in Interval (BClose_if ba xa) (BClose_if bb xb) -> + xa < xb. +Proof. by move=> /negbTE bab /lteif_in_itv; rewrite bab. Qed. Lemma ler_in_itv ba bb xa xb x : - x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa <= xb. -Proof. by move/lersif_in_itv/lersifW. Qed. - -Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x). -Proof. by rewrite !inE /= oppr_le0 andbb. Qed. - -Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x). -Proof. by rewrite !inE /= oppr_lt0 andbb. Qed. + x \in Interval (BClose_if ba xa) (BClose_if bb xb) -> xa <= xb. +Proof. by move/lteif_in_itv/lteifW. Qed. -Lemma itv_splitI : forall a b x, - x \in Interval a b = - (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b). -Proof. by move=> [? ?|] [? ?|] ?; rewrite !inE ?andbT. Qed. +End IntervalPOrder. -Lemma oppr_itv ba bb (xa xb x : R) : - (-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) = - (x \in Interval (BOpen_if bb (-xb)) (BOpen_if ba (-xa))). -Proof. by rewrite !inE lersif_oppr andbC lersif_oppl. Qed. +Section IntervalLattice. -Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[). -Proof. exact: oppr_itv. Qed. +Variable (disp : unit) (T : latticeType disp). +Implicit Types (x y z : T) (i : interval T). -Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]). -Proof. exact: oppr_itv. Qed. +Definition itv_boundl_meet (bl br : itv_boundl T) : itv_boundl T := + match bl, br with + | BInfty, _ => br | _, BInfty => bl + | BClose_if xb x, BClose_if yb y => + BClose_if ((~~ (x <= y) || yb) && (~~ (y <= x) || xb)) (x `|` y) + end. -Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[). -Proof. exact: oppr_itv. Qed. +Definition itv_boundr_meet (bl br : itv_boundr T) : itv_boundr T := + match bl, br with + | BInfty, _ => br | _, BInfty => bl + | BClose_if xb x, BClose_if yb y => + BClose_if ((~~ (x <= y) || xb) && (~~ (y <= x) || yb)) (x `&` y) + end. -Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]). -Proof. exact: oppr_itv. Qed. +Definition itv_boundl_join (bl br : itv_boundl T) : itv_bound T := + match bl, br with + | BInfty, _ | _, BInfty => BInfty _ + | BClose_if xb x, BClose_if yb y => + BClose_if ((x <= y) && xb || (y <= x) && yb) (x `&` y) + end. -End IntervalPo. +Definition itv_boundr_join (bl br : itv_boundr T) : itv_bound T := + match bl, br with + | BInfty, _ | _, BInfty => BInfty _ + | BClose_if xb x, BClose_if yb y => + BClose_if ((x <= y) && yb || (y <= x) && xb) (x `|` y) + end. -Section IntervalOrdered. +Lemma itv_boundl_meetC : commutative itv_boundl_meet. +Proof. +by case=> [? ?|][? ?|] //=; rewrite joinC; congr BClose_if; + case: lcomparableP; rewrite ?andbT // 1?andbC. +Qed. -Variable R : realDomainType. +Lemma itv_boundr_meetC : commutative itv_boundr_meet. +Proof. +by case=> [? ?|][? ?|] //=; rewrite meetC; congr BClose_if; + case: lcomparableP; rewrite ?andbT // 1?andbC. +Qed. -Lemma le_boundl_total : total (@le_boundl R). -Proof. by move=> [[] l |] [[] r |] //=; case: (ltrgtP l r). Qed. +Lemma itv_boundl_joinC : commutative itv_boundl_join. +Proof. +by case=> [? ?|][? ?|] //=; rewrite meetC; congr BClose_if; + case: lcomparableP; rewrite ?orbF // 1?orbC. +Qed. -Lemma le_boundr_total : total (@le_boundr R). -Proof. by move=> [[] l |] [[] r |] //=; case: (ltrgtP l r). Qed. +Lemma itv_boundr_joinC : commutative itv_boundr_join. +Proof. +by case=> [? ?|][? ?|] //=; rewrite joinC; congr BClose_if; + case: lcomparableP; rewrite ?orbF // 1?orbC. +Qed. -Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b -> - forall y, y \in Interval a b = - (y \in Interval a (BOpen_if (~~ bc) xc)) - || (y \in Interval (BOpen_if bc xc) b). +Lemma itv_boundl_meetA : associative itv_boundl_meet. Proof. -move=> xc_in y; move: xc_in. -rewrite !itv_boundlr [le_boundr (BClose _) (BOpen_if _ _)]/= - [le_boundr]lock /= lersifN -lock. -case/andP => leaxc lexcb; - case: (boolP (le_boundl a _)) => leay; case: (boolP (le_boundr _ b)) => leyb; - rewrite /= (andbT, andbF) ?orbF ?orNb //=; - [apply/esym/negbF | apply/esym/negbTE]. -- by case: b lexcb leyb => //= bb b; rewrite -lersifN => lexcb leyb; - apply/lersif_imply: (lersif_trans lexcb leyb); rewrite orbN implybT. -- by case: a leaxc leay => //= ab a leaxc; - apply/contra => /(lersif_trans leaxc); - apply/lersif_imply; rewrite implybE orbA orNb. +case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?leUx ?joinA //. +by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; + case: (lcomparableP x z) => [|||//<-] //=; + case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; + rewrite ?orbT ?andbT ?lexx ?andbA. Qed. -Lemma itv_splitU2 (x : R) a b : x \in Interval a b -> - forall y, y \in Interval a b = - [|| (y \in Interval a (BOpen x)), (y == x) - | (y \in Interval (BOpen x) b)]. +Lemma itv_boundr_meetA : associative itv_boundr_meet. Proof. -move=> xab y; rewrite (itv_splitU false xab y); congr (_ || _). -rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE. -by move: xab; rewrite boundl_in_itv itv_boundlr => /andP []. +case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?lexI ?meetA //. +by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; + case: (lcomparableP x z) => [|||//<-] //=; + case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; + rewrite ?orbT ?andbT ?lexx ?andbA. Qed. -Lemma itv_intersectionC : commutative (@itv_intersection R). +Lemma itv_boundl_joinA : associative itv_boundl_join. Proof. -move=> [x x'] [y y'] /=; congr Interval; do 2 case: ifP => //=. -- by move=> leyx lexy; apply/eqP; rewrite -le_boundl_anti leyx lexy. -- by case/orP: (le_boundl_total x y) => ->. -- by move=> leyx' lexy'; apply/eqP; rewrite -le_boundr_anti leyx' lexy'. -- by case/orP: (le_boundr_total x' y') => ->. +case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?lexI ?meetA //. +by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; + case: (lcomparableP x z) => [|||//<-] //=; + case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; + rewrite ?andbF ?orbF ?lexx ?orbA. Qed. -Lemma itv_intersectionA : associative (@itv_intersection R). +Lemma itv_boundr_joinA : associative itv_boundr_join. Proof. -move=> [x x'] [y y'] [z z'] /=; congr Interval; - do !case: ifP => //=; do 1?congruence. -- by move=> lexy leyz; rewrite (le_boundl_trans lexy leyz). -- move=> gtxy lexz gtyz _; apply/eqP; rewrite -le_boundl_anti lexz /=. - move: (le_boundl_total y z) (le_boundl_total x y). - by rewrite gtxy gtyz; apply: le_boundl_trans. -- by move=> lexy' gtxz' leyz'; rewrite (le_boundr_trans lexy' leyz') in gtxz'. -- move=> gtxy' gtyz' _ lexz'; apply/eqP; rewrite -le_boundr_anti lexz' /=. - move: (le_boundr_total y' z') (le_boundr_total x' y'). - by rewrite gtxy' gtyz'; apply: le_boundr_trans. +case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?leUx ?joinA //. +by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; + case: (lcomparableP x z) => [|||//<-] //=; + case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; + rewrite ?andbF ?orbF ?lexx ?orbA. Qed. -Canonical itv_intersection_monoid := - Monoid.Law itv_intersectionA (@itv_intersection1i R) (@itv_intersectioni1 R). +Lemma itv_boundl_meetKU b2 b1 : itv_boundl_join b1 (itv_boundl_meet b1 b2) = b1. +Proof. +case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; + rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?orbb //=. +by case: lcomparableP; rewrite ?orbb ?orbF ?andKb. +Qed. -Canonical itv_intersection_comoid := Monoid.ComLaw itv_intersectionC. +Lemma itv_boundr_meetKU b2 b1 : itv_boundr_join b1 (itv_boundr_meet b1 b2) = b1. +Proof. +case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; + rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?orbb //. +by case: lcomparableP; rewrite ?andbT /= ?orbb ?andbK. +Qed. -End IntervalOrdered. +Lemma itv_boundl_joinKI b2 b1 : itv_boundl_meet b1 (itv_boundl_join b1 b2) = b1. +Proof. +case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; + rewrite ?meetKU // leIl lexI lexx. +by case: lcomparableP; rewrite ?orbF ?andbb /= ?orbK. +Qed. -Section IntervalField. +Lemma itv_boundr_joinKI b2 b1 : itv_boundr_meet b1 (itv_boundr_join b1 b2) = b1. +Proof. +case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; + rewrite ?joinKI // leUl leUx lexx. +by case: lcomparableP; rewrite ?andbT ?andbb ?orKb. +Qed. -Variable R : realFieldType. +Lemma itv_boundl_leEmeet b1 b2 : + le_boundl b2 b1 = (itv_boundl_meet b1 b2 == b1). +Proof. +by case: b1 b2 => [[]?|][[]?|] //=; + rewrite /eq_op /= ?eqxx // eq_joinl; case: lcomparableP. +Qed. -Lemma mid_in_itv : forall ba bb (xa xb : R), xa <= xb ?< if ba || bb - -> mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb). +Lemma itv_boundr_leEmeet b1 b2 : + le_boundr b1 b2 = (itv_boundr_meet b1 b2 == b1). Proof. -by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW. +by case: b1 b2 => [[]?|][[]?|] //=; + rewrite /eq_op /= ?eqxx //= -leEmeet; case: lcomparableP. Qed. -Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[. -Proof. by move=> xa xb ?; apply: mid_in_itv. Qed. +Definition itv_boundl_latticeMixin := + LatticeMixin itv_boundl_meetC itv_boundl_joinC + itv_boundl_meetA itv_boundl_joinA + itv_boundl_joinKI itv_boundl_meetKU itv_boundl_leEmeet. +Canonical itv_boundl_latticeType := + LatticeType (itv_boundl T) itv_boundl_latticeMixin. -Lemma mid_in_itvcc : forall (xa xb : R), xa <= xb -> mid xa xb \in `[xa, xb]. -Proof. by move=> xa xb ?; apply: mid_in_itv. Qed. +Definition itv_boundr_latticeMixin := + LatticeMixin itv_boundr_meetC itv_boundr_joinC + itv_boundr_meetA itv_boundr_joinA + itv_boundr_joinKI itv_boundr_meetKU itv_boundr_leEmeet. +Canonical itv_boundr_latticeType := + LatticeType (itv_boundr T) itv_boundr_latticeMixin. -End IntervalField. +Definition itv_meet i1 i2 : interval T := + let: Interval b1l b1r := i1 in + let: Interval b2l b2r := i2 in Interval (b1l `&` b2l) (b1r `&` b2r). + +Definition itv_join i1 i2 : interval T := + let: Interval b1l b1r := i1 in + let: Interval b2l b2r := i2 in Interval (b1l `|` b2l) (b1r `|` b2r). + +Lemma itv_meetC : commutative itv_meet. +Proof. by case=> [? ?][? ?]; congr Interval; rewrite meetC. Qed. + +Lemma itv_joinC : commutative itv_join. +Proof. by case=> [? ?][? ?]; congr Interval; rewrite joinC. Qed. + +Lemma itv_meetA : associative itv_meet. +Proof. by case=> [? ?][? ?][? ?]; rewrite /= !meetA. Qed. + +Lemma itv_joinA : associative itv_join. +Proof. by case=> [? ?][? ?][? ?]; rewrite /= !joinA. Qed. + +Lemma itv_meetKU i2 i1 : itv_join i1 (itv_meet i1 i2) = i1. +Proof. by case: i1 i2 => [? ?][? ?]; rewrite /= !meetKU. Qed. + +Lemma itv_joinKI i2 i1 : itv_meet i1 (itv_join i1 i2) = i1. +Proof. by case: i1 i2 => [? ?][? ?]; rewrite /= !joinKI. Qed. + +Lemma itv_leEmeet i1 i2 : (i1 <= i2) = (itv_meet i1 i2 == i1). +Proof. by case: i1 i2 => [? ?][? ?]; rewrite /<=%O /eq_op /= !leEmeet. Qed. + +Definition interval_latticeMixin := + LatticeMixin itv_meetC itv_joinC itv_meetA itv_joinA + itv_joinKI itv_meetKU itv_leEmeet. +Canonical interval_latticeType := + LatticeType (interval T) interval_latticeMixin. + +Definition itv_meet1i : left_id `]-oo, +oo[ Order.meet. +Proof. by case=> i []. Qed. + +Definition itv_meeti1 : right_id `]-oo, +oo[ Order.meet. +Proof. by case=> [[? ?|][? ?|]]. Qed. + +Canonical itv_intersection_monoid := Monoid.Law itv_meetA itv_meet1i itv_meeti1. +Canonical itv_intersection_comoid := Monoid.ComLaw itv_meetC. + +Lemma in_itv_meet x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2). +Proof. by rewrite !inEsubitv lexI. Qed. + +End IntervalLattice. + +Section IntervalTotal. + +Variable (disp : unit) (T : orderType disp). +Implicit Types (x y z : T) (i : interval T). + +Lemma le_boundl_total : total (@le_boundl _ T). +Proof. by move=> [[]l|] [[]r|] //=; case: (ltgtP l r). Qed. + +Lemma le_boundr_total : total (@le_boundr _ T). +Proof. by move=> [[]l|] [[]r|] //=; case: (ltgtP l r). Qed. + +Definition itv_boundl_totalMixin : totalLatticeMixin _ := + fun b1 b2 => le_boundl_total b2 b1. + +Canonical itv_boundl_distrLatticeType := + DistrLatticeType (itv_boundl T) itv_boundl_totalMixin. +Canonical itv_boundl_orderType := + OrderType (itv_boundl T) itv_boundl_totalMixin. + +Canonical itv_boundr_distrLatticeType := + DistrLatticeType (itv_boundr T) (le_boundr_total : totalLatticeMixin _). +Canonical itv_boundr_orderType := OrderType (itv_boundr T) le_boundr_total. + +Lemma itv_meetUl : @left_distributive (interval T) _ Order.meet Order.join. +Proof. +by move=> [? ?][? ?][? ?]; rewrite /Order.meet /Order.join /= !meetUl. +Qed. + +Canonical interval_distrLatticeType := + DistrLatticeType (interval T) (DistrLatticeMixin itv_meetUl). + +Lemma itv_splitU (xc : T) bc a b : xc \in Interval a b -> + forall y, y \in Interval a b = + (y \in Interval a (BClose_if (~~ bc) xc)) + || (y \in Interval (BClose_if bc xc) b). +Proof. +move=> xc_in y; move: xc_in. +rewrite !itv_boundlr [le_boundr (BClose _) (BClose_if _ _)]/= + [le_boundr]lock /= lteifN -lock. +case/andP => leaxc lexcb; + case: (boolP (le_boundl a _)) => leay; case: (boolP (le_boundr _ b)) => leyb; + rewrite /= (andbT, andbF) ?orbF ?orNb //=; + [apply/esym/negbF | apply/esym/negbTE]. +- by case: b lexcb leyb => //= bb b; rewrite -lteifN => lexcb leyb; + apply/lteif_imply: (lteif_trans lexcb leyb); rewrite andbN. +- case: a leaxc leay => //= ab a leaxc; + apply/contra => /(lteif_trans leaxc); apply/lteif_imply. + by rewrite implybE negb_and orbC orbA orbN. +Qed. + +Lemma itv_splitU2 x a b : x \in Interval a b -> + forall y, y \in Interval a b = + [|| (y \in Interval a (BOpen x)), (y == x) + | (y \in Interval (BOpen x) b)]. +Proof. +move=> xab y; rewrite (itv_splitU true xab y); congr (_ || _). +rewrite (@itv_splitU x false _ _ _ y); first by rewrite itv_xx inE. +by move: xab; rewrite boundl_in_itv itv_boundlr => /andP []. +Qed. + +Lemma itv_total_meet3E i1 i2 i3 : + i1 `&` i2 `&` i3 \in [:: i1 `&` i2; i1 `&` i3; i2 `&` i3]. +Proof. +rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=. +case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l); + case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r); + rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l. +- by case: leP b31l (le_trans b32l b21l). +- by case: leP b31l (le_trans b32l b21l). +- by case: leP b31l (le_trans b32l b21l). +- by case: leP b13r (le_trans b12r b23r). +- by case: leP b13r (le_trans b12r b23r). +- by case: leP b13r (lt_trans b23r b12r). +- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b13r (lt_trans b23r b12r). +Qed. + +Lemma itv_total_join3E i1 i2 i3 : + i1 `|` i2 `|` i3 \in [:: i1 `|` i2; i1 `|` i3; i2 `|` i3]. +Proof. +rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=. +case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l); + case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r); + rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l. +- by case: leP b13r (le_trans b12r b23r). +- by case: leP b31l (le_trans b32l b21l). +- by case: leP b31l (le_trans b32l b21l). +- by case: leP b31l (le_trans b32l b21l). +- by case: leP b13r (le_trans b12r b23r). +- by case: leP b13r (lt_trans b23r b12r). +- by case: leP b13r (lt_trans b23r b12r). +- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b31l (lt_trans b21l b32l). +Qed. + +End IntervalTotal. + +Local Open Scope ring_scope. +Import GRing.Theory Num.Theory. + +Section LteifNumDomain. + +Variable R : numDomainType. +Implicit Types (b : bool) (x y z : R). + +Local Notation "x < y ?<= 'if' b" := (@lteif _ R x y b) + (at level 70, y at next level, + format "x '[hv' < y '/' ?<= 'if' b ']'") : ring_scope. + +Lemma subr_lteifr0 b (x y : R) : (y - x < 0 ?<= if b) = (y < x ?<= if b). +Proof. by case: b => /=; rewrite subr_lte0. Qed. + +Lemma subr_lteif0r b (x y : R) : (0 < y - x ?<= if b) = (x < y ?<= if b). +Proof. by case: b => /=; rewrite subr_gte0. Qed. + +Definition subr_lteif0 := (subr_lteifr0, subr_lteif0r). + +Lemma lteif01 b : 0 < 1 ?<= if b. +Proof. by case: b; rewrite /= lter01. Qed. + +Lemma lteif_oppl b x y : - x < y ?<= if b = (- y < x ?<= if b). +Proof. by case: b; rewrite /= lter_oppl. Qed. + +Lemma lteif_oppr b x y : x < - y ?<= if b = (y < - x ?<= if b). +Proof. by case: b; rewrite /= lter_oppr. Qed. + +Lemma lteif_0oppr b x : 0 < - x ?<= if b = (x < 0 ?<= if b). +Proof. by case: b; rewrite /= (oppr_ge0, oppr_gt0). Qed. + +Lemma lteif_oppr0 b x : - x < 0 ?<= if b = (0 < x ?<= if b). +Proof. by case: b; rewrite /= (oppr_le0, oppr_lt0). Qed. + +Lemma lteif_opp2 b : {mono -%R : x y /~ x < y ?<= if b}. +Proof. by case: b => ? ?; rewrite /= lter_opp2. Qed. + +Definition lteif_oppE := (lteif_0oppr, lteif_oppr0, lteif_opp2). + +Lemma lteif_add2l b x : {mono +%R x : y z / y < z ?<= if b}. +Proof. by case: b => ? ?; rewrite /= lter_add2. Qed. + +Lemma lteif_add2r b x : {mono +%R^~ x : y z / y < z ?<= if b}. +Proof. by case: b => ? ?; rewrite /= lter_add2. Qed. + +Definition lteif_add2 := (lteif_add2l, lteif_add2r). + +Lemma lteif_subl_addr b x y z : (x - y < z ?<= if b) = (x < z + y ?<= if b). +Proof. by case: b; rewrite /= lter_sub_addr. Qed. + +Lemma lteif_subr_addr b x y z : (x < y - z ?<= if b) = (x + z < y ?<= if b). +Proof. by case: b; rewrite /= lter_sub_addr. Qed. + +Definition lteif_sub_addr := (lteif_subl_addr, lteif_subr_addr). + +Lemma lteif_subl_addl b x y z : (x - y < z ?<= if b) = (x < y + z ?<= if b). +Proof. by case: b; rewrite /= lter_sub_addl. Qed. + +Lemma lteif_subr_addl b x y z : (x < y - z ?<= if b) = (z + x < y ?<= if b). +Proof. by case: b; rewrite /= lter_sub_addl. Qed. + +Definition lteif_sub_addl := (lteif_subl_addl, lteif_subr_addl). + +Lemma lteif_pmul2l b x : 0 < x -> {mono *%R x : y z / y < z ?<= if b}. +Proof. by case: b => ? ? ?; rewrite /= lter_pmul2l. Qed. + +Lemma lteif_pmul2r b x : 0 < x -> {mono *%R^~ x : y z / y < z ?<= if b}. +Proof. by case: b => ? ? ?; rewrite /= lter_pmul2r. Qed. + +Lemma lteif_nmul2l b x : x < 0 -> {mono *%R x : y z /~ y < z ?<= if b}. +Proof. by case: b => ? ? ?; rewrite /= lter_nmul2l. Qed. + +Lemma lteif_nmul2r b x : x < 0 -> {mono *%R^~ x : y z /~ y < z ?<= if b}. +Proof. by case: b => ? ? ?; rewrite /= lter_nmul2r. Qed. + +Lemma real_lteifN x y b : x \is Num.real -> y \is Num.real -> + x < y ?<= if ~~b = ~~ (y < x ?<= if b). +Proof. by move=> ? ?; rewrite comparable_lteifN ?real_comparable. Qed. + +Lemma real_lteif_norml b x y : + x \is Num.real -> + (`|x| < y ?<= if b) = ((- y < x ?<= if b) && (x < y ?<= if b)). +Proof. by case: b => ?; rewrite /= real_lter_norml. Qed. + +Lemma real_lteif_normr b x y : + y \is Num.real -> + (x < `|y| ?<= if b) = ((x < y ?<= if b) || (x < - y ?<= if b)). +Proof. by case: b => ?; rewrite /= real_lter_normr. Qed. + +Lemma lteif_nnormr b x y : y < 0 ?<= if ~~ b -> (`|x| < y ?<= if b) = false. +Proof. by case: b => ?; rewrite /= lter_nnormr. Qed. + +End LteifNumDomain. + +Section LteifRealDomain. + +Variable (R : realDomainType) (b : bool) (x y z e : R). + +Lemma lteif_norml : + (`|x| < y ?<= if b) = (- y < x ?<= if b) && (x < y ?<= if b). +Proof. by case: b; rewrite /= lter_norml. Qed. + +Lemma lteif_normr : + (x < `|y| ?<= if b) = (x < y ?<= if b) || (x < - y ?<= if b). +Proof. by case: b; rewrite /= lter_normr. Qed. + +Lemma lteif_distl : + (`|x - y| < e ?<= if b) = (y - e < x ?<= if b) && (x < y + e ?<= if b). +Proof. by case: b; rewrite /= lter_distl. Qed. + +End LteifRealDomain. + +Section LteifField. + +Variable (F : numFieldType) (b : bool) (z x y : F). + +Lemma lteif_pdivl_mulr : 0 < z -> x < y / z ?<= if b = (x * z < y ?<= if b). +Proof. by case: b => ? /=; rewrite lter_pdivl_mulr. Qed. + +Lemma lteif_pdivr_mulr : 0 < z -> y / z < x ?<= if b = (y < x * z ?<= if b). +Proof. by case: b => ? /=; rewrite lter_pdivr_mulr. Qed. + +Lemma lteif_pdivl_mull : 0 < z -> x < z^-1 * y ?<= if b = (z * x < y ?<= if b). +Proof. by case: b => ? /=; rewrite lter_pdivl_mull. Qed. + +Lemma lteif_pdivr_mull : 0 < z -> z^-1 * y < x ?<= if b = (y < z * x ?<= if b). +Proof. by case: b => ? /=; rewrite lter_pdivr_mull. Qed. + +Lemma lteif_ndivl_mulr : z < 0 -> x < y / z ?<= if b = (y < x * z ?<= if b). +Proof. by case: b => ? /=; rewrite lter_ndivl_mulr. Qed. + +Lemma lteif_ndivr_mulr : z < 0 -> y / z < x ?<= if b = (x * z < y ?<= if b). +Proof. by case: b => ? /=; rewrite lter_ndivr_mulr. Qed. + +Lemma lteif_ndivl_mull : z < 0 -> x < z^-1 * y ?<= if b = (y < z * x ?<= if b). +Proof. by case: b => ? /=; rewrite lter_ndivl_mull. Qed. + +Lemma lteif_ndivr_mull : z < 0 -> z^-1 * y < x ?<= if b = (z * x < y ?<= if b). +Proof. by case: b => ? /=; rewrite lter_ndivr_mull. Qed. + +End LteifField. + +Section IntervalNumDomain. + +Variable R : numFieldType. +Implicit Types x : R. + +Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x). +Proof. by rewrite !inE /= oppr_le0 andbb. Qed. + +Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x). +Proof. by rewrite !inE /= oppr_lt0 andbb. Qed. + +Lemma itv_splitI : forall a b x, + x \in Interval a b = + (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b). +Proof. by move=> [? ?|] [? ?|] ?; rewrite !inE ?andbT. Qed. + +Lemma oppr_itv ba bb (xa xb x : R) : + (-x \in Interval (BClose_if ba xa) (BClose_if bb xb)) = + (x \in Interval (BClose_if bb (-xb)) (BClose_if ba (-xa))). +Proof. by rewrite !inE lteif_oppr andbC lteif_oppl. Qed. + +Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[). +Proof. exact: oppr_itv. Qed. + +Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]). +Proof. exact: oppr_itv. Qed. + +Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[). +Proof. exact: oppr_itv. Qed. + +Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]). +Proof. exact: oppr_itv. Qed. + +End IntervalNumDomain. + +Section IntervalField. + +Variable R : realFieldType. + +Local Notation mid x y := ((x + y) / 2%:R). + +Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ba && bb + -> mid xa xb \in Interval (BClose_if ba xa) (BClose_if bb xb). +Proof. +by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW. +Qed. + +Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[. +Proof. by move=> xa xb ?; apply: mid_in_itv. Qed. + +Lemma mid_in_itvcc : forall (xa xb : R), xa <= xb -> mid xa xb \in `[xa, xb]. +Proof. by move=> xa xb ?; apply: mid_in_itv. Qed. + +End IntervalField. + +(******************************************************************************) +(* Compatibility layer *) +(******************************************************************************) + +Module mc_1_11. + +Local Notation lersif x y b := (lteif x y (~~ b)) (only parsing). + +Local Notation "x <= y ?< 'if' b" := (x < y ?<= if ~~ b) + (at level 70, y at next level, only parsing) : ring_scope. + +Section LersifPo. + +Variable R : numDomainType. +Implicit Types (b : bool) (x y z : R). + +Lemma subr_lersifr0 b (x y : R) : (y - x <= 0 ?< if b) = (y <= x ?< if b). +Proof. exact: subr_lteifr0. Qed. + +Lemma subr_lersif0r b (x y : R) : (0 <= y - x ?< if b) = (x <= y ?< if b). +Proof. exact: subr_lteif0r. Qed. + +Definition subr_lersif0 := (subr_lersifr0, subr_lersif0r). + +Lemma lersif_trans x y z b1 b2 : + x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2. +Proof. by rewrite negb_or; exact: lteif_trans. Qed. + +Lemma lersif01 b : (0 : R) <= 1 ?< if b. Proof. exact: lteif01. Qed. + +Lemma lersif_anti b1 b2 x y : + (x <= y ?< if b1) && (y <= x ?< if b2) = + if b1 || b2 then false else x == y. +Proof. by rewrite lteif_anti -negb_or; case: orb. Qed. + +Lemma lersifxx x b : (x <= x ?< if b) = ~~ b. Proof. exact: lteifxx. Qed. + +Lemma lersifNF x y b : y <= x ?< if ~~ b -> x <= y ?< if b = false. +Proof. exact: lteifNF. Qed. + +Lemma lersifS x y b : x < y -> x <= y ?< if b. +Proof. exact: lteifS. Qed. + +Lemma lersifT x y : x <= y ?< if true = (x < y). Proof. by []. Qed. + +Lemma lersifF x y : x <= y ?< if false = (x <= y). Proof. by []. Qed. + +Lemma lersif_oppl b x y : - x <= y ?< if b = (- y <= x ?< if b). +Proof. exact: lteif_oppl. Qed. + +Lemma lersif_oppr b x y : x <= - y ?< if b = (y <= - x ?< if b). +Proof. exact: lteif_oppr. Qed. + +Lemma lersif_0oppr b x : 0 <= - x ?< if b = (x <= 0 ?< if b). +Proof. exact: lteif_0oppr. Qed. + +Lemma lersif_oppr0 b x : - x <= 0 ?< if b = (0 <= x ?< if b). +Proof. exact: lteif_oppr0. Qed. + +Lemma lersif_opp2 b : {mono (-%R : R -> R) : x y /~ x <= y ?< if b}. +Proof. exact: lteif_opp2. Qed. + +Definition lersif_oppE := (lersif_0oppr, lersif_oppr0, lersif_opp2). + +Lemma lersif_add2l b x : {mono +%R x : y z / y <= z ?< if b}. +Proof. exact: lteif_add2l. Qed. + +Lemma lersif_add2r b x : {mono +%R^~ x : y z / y <= z ?< if b}. +Proof. exact: lteif_add2r. Qed. + +Definition lersif_add2 := (lersif_add2l, lersif_add2r). + +Lemma lersif_subl_addr b x y z : (x - y <= z ?< if b) = (x <= z + y ?< if b). +Proof. exact: lteif_subl_addr. Qed. + +Lemma lersif_subr_addr b x y z : (x <= y - z ?< if b) = (x + z <= y ?< if b). +Proof. exact: lteif_subr_addr. Qed. + +Definition lersif_sub_addr := (lersif_subl_addr, lersif_subr_addr). + +Lemma lersif_subl_addl b x y z : (x - y <= z ?< if b) = (x <= y + z ?< if b). +Proof. exact: lteif_subl_addl. Qed. + +Lemma lersif_subr_addl b x y z : (x <= y - z ?< if b) = (z + x <= y ?< if b). +Proof. exact: lteif_subr_addl. Qed. + +Definition lersif_sub_addl := (lersif_subl_addl, lersif_subr_addl). + +Lemma lersif_andb x y : + {morph (fun b => lersif x y b) : p q / p || q >-> p && q}. +Proof. by move=> ? ?; rewrite negb_or lteif_andb. Qed. + +Lemma lersif_orb x y : + {morph (fun b => lersif x y b) : p q / p && q >-> p || q}. +Proof. by move=> ? ?; rewrite negb_and lteif_orb. Qed. + +Lemma lersif_imply b1 b2 (r1 r2 : R) : + b2 ==> b1 -> r1 <= r2 ?< if b1 -> r1 <= r2 ?< if b2. +Proof. by move=> ?; apply: lteif_imply; rewrite implybNN. Qed. + +Lemma lersifW b x y : x <= y ?< if b -> x <= y. +Proof. exact: lteifW. Qed. + +Lemma ltrW_lersif b x y : x < y -> x <= y ?< if b. +Proof. exact: ltrW_lteif. Qed. + +Lemma lersif_pmul2l b x : 0 < x -> {mono *%R x : y z / y <= z ?< if b}. +Proof. exact: lteif_pmul2l. Qed. + +Lemma lersif_pmul2r b x : 0 < x -> {mono *%R^~ x : y z / y <= z ?< if b}. +Proof. exact: lteif_pmul2r. Qed. + +Lemma lersif_nmul2l b x : x < 0 -> {mono *%R x : y z /~ y <= z ?< if b}. +Proof. exact: lteif_nmul2l. Qed. + +Lemma lersif_nmul2r b x : x < 0 -> {mono *%R^~ x : y z /~ y <= z ?< if b}. +Proof. exact: lteif_nmul2r. Qed. + +Lemma real_lersifN x y b : x \is Num.real -> y \is Num.real -> + x <= y ?< if ~~b = ~~ (y <= x ?< if b). +Proof. exact: real_lteifN. Qed. + +Lemma real_lersif_norml b x y : + x \is Num.real -> + (`|x| <= y ?< if b) = ((- y <= x ?< if b) && (x <= y ?< if b)). +Proof. exact: real_lteif_norml. Qed. + +Lemma real_lersif_normr b x y : + y \is Num.real -> + (x <= `|y| ?< if b) = ((x <= y ?< if b) || (x <= - y ?< if b)). +Proof. exact: real_lteif_normr. Qed. + +Lemma lersif_nnormr b x y : y <= 0 ?< if ~~ b -> (`|x| <= y ?< if b) = false. +Proof. exact: lteif_nnormr. Qed. + +End LersifPo. + +Section LersifOrdered. + +Variable (R : realDomainType) (b : bool) (x y z e : R). + +Lemma lersifN : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b). +Proof. exact: lteifN. Qed. + +Lemma lersif_norml : + (`|x| <= y ?< if b) = (- y <= x ?< if b) && (x <= y ?< if b). +Proof. exact: lteif_norml. Qed. + +Lemma lersif_normr : + (x <= `|y| ?< if b) = (x <= y ?< if b) || (x <= - y ?< if b). +Proof. exact: lteif_normr. Qed. + +Lemma lersif_distl : + (`|x - y| <= e ?< if b) = (y - e <= x ?< if b) && (x <= y + e ?< if b). +Proof. exact: lteif_distl. Qed. + +Lemma lersif_minr : + (x <= Num.min y z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b). +Proof. exact: lteif_minr. Qed. + +Lemma lersif_minl : + (Num.min y z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b). +Proof. exact: lteif_minl. Qed. + +Lemma lersif_maxr : + (x <= Num.max y z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b). +Proof. exact: lteif_maxr. Qed. + +Lemma lersif_maxl : + (Num.max y z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b). +Proof. exact: lteif_maxl. Qed. + +End LersifOrdered. + +Section LersifField. + +Variable (F : numFieldType) (b : bool) (z x y : F). + +Lemma lersif_pdivl_mulr : 0 < z -> x <= y / z ?< if b = (x * z <= y ?< if b). +Proof. exact: lteif_pdivl_mulr. Qed. + +Lemma lersif_pdivr_mulr : 0 < z -> y / z <= x ?< if b = (y <= x * z ?< if b). +Proof. exact: lteif_pdivr_mulr. Qed. + +Lemma lersif_pdivl_mull : 0 < z -> x <= z^-1 * y ?< if b = (z * x <= y ?< if b). +Proof. exact: lteif_pdivl_mull. Qed. + +Lemma lersif_pdivr_mull : 0 < z -> z^-1 * y <= x ?< if b = (y <= z * x ?< if b). +Proof. exact: lteif_pdivr_mull. Qed. + +Lemma lersif_ndivl_mulr : z < 0 -> x <= y / z ?< if b = (y <= x * z ?< if b). +Proof. exact: lteif_ndivl_mulr. Qed. + +Lemma lersif_ndivr_mulr : z < 0 -> y / z <= x ?< if b = (x * z <= y ?< if b). +Proof. exact: lteif_ndivr_mulr. Qed. + +Lemma lersif_ndivl_mull : z < 0 -> x <= z^-1 * y ?< if b = (y <=z * x ?< if b). +Proof. exact: lteif_ndivl_mull. Qed. + +Lemma lersif_ndivr_mull : z < 0 -> z^-1 * y <= x ?< if b = (z * x <= y ?< if b). +Proof. exact: lteif_ndivr_mull. Qed. + +End LersifField. + +Section IntervalPo. + +Variable R : numDomainType. + +Local Notation BOpen_if b x := (BClose_if (~~ b) x) (only parsing). + +Lemma lersif_in_itv ba bb (xa xb x : R) : + x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> + xa <= xb ?< if ba || bb. +Proof. by move/lteif_in_itv; rewrite negb_or. Qed. + +End IntervalPo. + +End mc_1_11. + +Notation "@ 'lersif'" := + ((fun _ (R : numDomainType) x y b => @lteif _ R x y (~~ b)) + (deprecate lersif lteif)) + (at level 10, only parsing). + +Notation lersif := (@lersif _) (only parsing). + +Notation "x <= y ?< 'if' b" := + ((fun _ => x < y ?<= if ~~ b) (deprecate lersif lteif)) + (at level 70, y at next level, only parsing) : ring_scope. + +(* LersifPo *) + +Notation "@ 'subr_lersifr0'" := + ((fun _ => @mc_1_11.subr_lersifr0) (deprecate subr_lersifr0 subr_lteifr0)) + (at level 10, only parsing). + +Notation subr_lersifr0 := (@subr_lersifr0 _) (only parsing). + +Notation "@ 'subr_lersif0r'" := + ((fun _ => @mc_1_11.subr_lersif0r) (deprecate subr_lersif0r subr_lteif0r)) + (at level 10, only parsing). + +Notation subr_lersif0r := (@subr_lersif0r _) (only parsing). + +Notation subr_lersif0 := + ((fun _ => @mc_1_11.subr_lersif0) (deprecate subr_lersif0 subr_lteif0)) + (only parsing). + +Notation "@ 'lersif_trans'" := + ((fun _ => @mc_1_11.lersif_trans) (deprecate lersif_trans lteif_trans)) + (at level 10, only parsing). + +Notation lersif_trans := (@lersif_trans _ _ _ _ _ _) (only parsing). + +Notation lersif01 := + ((fun _ => @mc_1_11.lersif01) (deprecate lersif01 lteif01)) (only parsing). + +Notation "@ 'lersif_anti'" := + ((fun _ => @mc_1_11.lersif_anti) (deprecate lersif_anti lteif_anti)) + (at level 10, only parsing). + +Notation lersif_anti := (@lersif_anti _) (only parsing). + +Notation "@ 'lersifxx'" := + ((fun _ => @mc_1_11.lersifxx) (deprecate lersifxx lteifxx)) + (at level 10, only parsing). + +Notation lersifxx := (@lersifxx _) (only parsing). + +Notation "@ 'lersifNF'" := + ((fun _ => @mc_1_11.lersifNF) (deprecate lersifNF lteifNF)) + (at level 10, only parsing). + +Notation lersifNF := (@lersifNF _ _ _ _) (only parsing). + +Notation "@ 'lersifS'" := + ((fun _ => @mc_1_11.lersifS) (deprecate lersifS lteifS)) + (at level 10, only parsing). + +Notation lersifS := (@lersifS _ _ _) (only parsing). + +Notation "@ 'lersifT'" := + ((fun _ => @mc_1_11.lersifT) (deprecate lersifT lteifT)) + (at level 10, only parsing). + +Notation lersifT := (@lersifT _) (only parsing). + +Notation "@ 'lersifF'" := + ((fun _ => @mc_1_11.lersifF) (deprecate lersifF lteifF)) + (at level 10, only parsing). + +Notation lersifF := (@lersifF _) (only parsing). + +Notation "@ 'lersif_oppl'" := + ((fun _ => @mc_1_11.lersif_oppl) (deprecate lersif_oppl lteif_oppl)) + (at level 10, only parsing). + +Notation lersif_oppl := (@lersif_oppl _) (only parsing). + +Notation "@ 'lersif_oppr'" := + ((fun _ => @mc_1_11.lersif_oppr) (deprecate lersif_oppr lteif_oppr)) + (at level 10, only parsing). + +Notation lersif_oppr := (@lersif_oppr _) (only parsing). + +Notation "@ 'lersif_0oppr'" := + ((fun _ => @mc_1_11.lersif_0oppr) (deprecate lersif_0oppr lteif_0oppr)) + (at level 10, only parsing). + +Notation lersif_0oppr := (@lersif_0oppr _) (only parsing). + +Notation "@ 'lersif_oppr0'" := + ((fun _ => @mc_1_11.lersif_oppr0) (deprecate lersif_oppr0 lteif_oppr0)) + (at level 10, only parsing). + +Notation lersif_oppr0 := (@lersif_oppr0 _) (only parsing). + +Notation "@ 'lersif_opp2'" := + ((fun _ => @mc_1_11.lersif_opp2) (deprecate lersif_opp2 lteif_opp2)) + (at level 10, only parsing). + +Notation lersif_opp2 := (@lersif_opp2 _) (only parsing). + +Notation lersif_oppE := + ((fun _ => @mc_1_11.lersif_oppE) (deprecate lersif_oppE lteif_oppE)) + (only parsing). + +Notation "@ 'lersif_add2l'" := + ((fun _ => @mc_1_11.lersif_add2l) (deprecate lersif_add2l lteif_add2l)) + (at level 10, only parsing). + +Notation lersif_add2l := (@lersif_add2l _) (only parsing). + +Notation "@ 'lersif_add2r'" := + ((fun _ => @mc_1_11.lersif_add2r) (deprecate lersif_add2r lteif_add2r)) + (at level 10, only parsing). + +Notation lersif_add2r := (@lersif_add2r _) (only parsing). + +Notation lersif_add2 := + ((fun _ => @mc_1_11.lersif_add2) (deprecate lersif_add2 lteif_add2)) + (only parsing). + +Notation "@ 'lersif_subl_addr'" := + ((fun _ => @mc_1_11.lersif_subl_addr) + (deprecate lersif_subl_addr lteif_subl_addr)) + (at level 10, only parsing). + +Notation lersif_subl_addr := (@lersif_subl_addr _) (only parsing). + +Notation "@ 'lersif_subr_addr'" := + ((fun _ => @mc_1_11.lersif_subr_addr) + (deprecate lersif_subr_addr lteif_subr_addr)) + (at level 10, only parsing). + +Notation lersif_subr_addr := (@lersif_subr_addr _) (only parsing). + +Notation lersif_sub_addr := + ((fun _ => @mc_1_11.lersif_sub_addr) + (deprecate lersif_sub_addr lteif_sub_addr)) + (only parsing). + +Notation "@ 'lersif_subl_addl'" := + ((fun _ => @mc_1_11.lersif_subl_addl) + (deprecate lersif_subl_addl lteif_subl_addl)) + (at level 10, only parsing). + +Notation lersif_subl_addl := (@lersif_subl_addl _) (only parsing). + +Notation "@ 'lersif_subr_addl'" := + ((fun _ => @mc_1_11.lersif_subr_addl) + (deprecate lersif_subr_addl lteif_subr_addl)) + (at level 10, only parsing). + +Notation lersif_subr_addl := (@lersif_subr_addl _) (only parsing). + +Notation lersif_sub_addl := + ((fun _ => @mc_1_11.lersif_sub_addl) + (deprecate lersif_sub_addl lteif_sub_addl)) + (only parsing). + +Notation "@ 'lersif_andb'" := + ((fun _ => @mc_1_11.lersif_andb) (deprecate lersif_andb lteif_andb)) + (at level 10, only parsing). + +Notation lersif_andb := (@lersif_andb _) (only parsing). + +Notation "@ 'lersif_orb'" := + ((fun _ => @mc_1_11.lersif_orb) (deprecate lersif_orb lteif_orb)) + (at level 10, only parsing). + +Notation lersif_orb := (@lersif_orb _) (only parsing). + +Notation "@ 'lersif_imply'" := + ((fun _ => @mc_1_11.lersif_imply) (deprecate lersif_imply lteif_imply)) + (at level 10, only parsing). + +Notation lersif_imply := (@lersif_imply _ _ _ _ _) (only parsing). + +Notation "@ 'lersifW'" := + ((fun _ => @mc_1_11.lersifW) (deprecate lersifW lteifW)) + (at level 10, only parsing). + +Notation lersifW := (@lersifW _ _ _ _) (only parsing). + +Notation "@ 'ltrW_lersif'" := + ((fun _ => @mc_1_11.ltrW_lersif) (deprecate ltrW_lersif ltrW_lteif)) + (at level 10, only parsing). + +Notation ltrW_lersif := (@ltrW_lersif _) (only parsing). + +Notation "@ 'lersif_pmul2l'" := + ((fun _ => @mc_1_11.lersif_pmul2l) (deprecate lersif_pmul2l lteif_pmul2l)) + (at level 10, only parsing). + +Notation lersif_pmul2l := (fun b => @lersif_pmul2l _ b _) (only parsing). + +Notation "@ 'lersif_pmul2r'" := + ((fun _ => @mc_1_11.lersif_pmul2r) (deprecate lersif_pmul2r lteif_pmul2r)) + (at level 10, only parsing). + +Notation lersif_pmul2r := (fun b => @lersif_pmul2r _ b _) (only parsing). + +Notation "@ 'lersif_nmul2l'" := + ((fun _ => @mc_1_11.lersif_nmul2l) (deprecate lersif_nmul2l lteif_nmul2l)) + (at level 10, only parsing). + +Notation lersif_nmul2l := (fun b => @lersif_nmul2l _ b _) (only parsing). + +Notation "@ 'lersif_nmul2r'" := + ((fun _ => @mc_1_11.lersif_nmul2r) (deprecate lersif_nmul2r lteif_nmul2r)) + (at level 10, only parsing). + +Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing). + +Notation "@ 'real_lersifN'" := + ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifN)) + (at level 10, only parsing). + +Notation real_lersifN := (@real_lersifN _ _ _) (only parsing). + +Notation "@ 'real_lersif_norml'" := + ((fun _ => @mc_1_11.real_lersif_norml) + (deprecate real_lersif_norml real_lteif_norml)) + (at level 10, only parsing). + +Notation real_lersif_norml := + (fun b => @real_lersif_norml _ b _) (only parsing). + +Notation "@ 'real_lersif_normr'" := + ((fun _ => @mc_1_11.real_lersif_normr) + (deprecate real_lersif_normr real_lteif_normr)) + (at level 10, only parsing). + +Notation real_lersif_normr := + (fun b x => @real_lersif_normr _ b x _) (only parsing). + +Notation "@ 'lersif_nnormr'" := + ((fun _ => @mc_1_11.lersif_nnormr) (deprecate lersif_nnormr lteif_nnormr)) + (at level 10, only parsing). + +Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing). + +(* LersifOrdered *) + +Notation "@ 'lersifN'" := + ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifN)) + (at level 10, only parsing). + +Notation lersifN := (@lersifN _) (only parsing). + +Notation "@ 'lersif_norml'" := + ((fun _ => @mc_1_11.lersif_norml) (deprecate lersif_norml lteif_norml)) + (at level 10, only parsing). + +Notation lersif_norml := (@lersif_norml _) (only parsing). + +Notation "@ 'lersif_normr'" := + ((fun _ => @mc_1_11.lersif_normr) (deprecate lersif_normr lteif_normr)) + (at level 10, only parsing). + +Notation lersif_normr := (@lersif_normr _) (only parsing). + +Notation "@ 'lersif_distl'" := + ((fun _ => @mc_1_11.lersif_distl) (deprecate lersif_distl lteif_distl)) + (at level 10, only parsing). + +Notation lersif_distl := (@lersif_distl _) (only parsing). + +Notation "@ 'lersif_minr'" := + ((fun _ => @mc_1_11.lersif_minr) (deprecate lersif_minr lteif_minr)) + (at level 10, only parsing). + +Notation lersif_minr := (@lersif_minr _) (only parsing). + +Notation "@ 'lersif_minl'" := + ((fun _ => @mc_1_11.lersif_minl) (deprecate lersif_minl lteif_minl)) + (at level 10, only parsing). + +Notation lersif_minl := (@lersif_minl _) (only parsing). + +Notation "@ 'lersif_maxr'" := + ((fun _ => @mc_1_11.lersif_maxr) (deprecate lersif_maxr lteif_maxr)) + (at level 10, only parsing). + +Notation lersif_maxr := (@lersif_maxr _) (only parsing). + +Notation "@ 'lersif_maxl'" := + ((fun _ => @mc_1_11.lersif_maxl) (deprecate lersif_maxl lteif_maxl)) + (at level 10, only parsing). + +Notation lersif_maxl := (@lersif_maxl _) (only parsing). + +(* LersifField *) + +Notation "@ 'lersif_pdivl_mulr'" := + ((fun _ => @mc_1_11.lersif_pdivl_mulr) + (deprecate lersif_pdivl_mulr lteif_pdivl_mulr)) + (at level 10, only parsing). + +Notation lersif_pdivl_mulr := + (fun b => @lersif_pdivl_mulr _ b _) (only parsing). + +Notation "@ 'lersif_pdivr_mulr'" := + ((fun _ => @mc_1_11.lersif_pdivr_mulr) + (deprecate lersif_pdivr_mulr lteif_pdivr_mulr)) + (at level 10, only parsing). + +Notation lersif_pdivr_mulr := + (fun b => @lersif_pdivr_mulr _ b _) (only parsing). + +Notation "@ 'lersif_pdivl_mull'" := + ((fun _ => @mc_1_11.lersif_pdivl_mull) + (deprecate lersif_pdivl_mull lteif_pdivl_mull)) + (at level 10, only parsing). + +Notation lersif_pdivl_mull := + (fun b => @lersif_pdivl_mull _ b _) (only parsing). + +Notation "@ 'lersif_pdivr_mull'" := + ((fun _ => @mc_1_11.lersif_pdivr_mull) + (deprecate lersif_pdivr_mull lteif_pdivr_mull)) + (at level 10, only parsing). + +Notation lersif_pdivr_mull := + (fun b => @lersif_pdivr_mull _ b _) (only parsing). + +Notation "@ 'lersif_ndivl_mulr'" := + ((fun _ => @mc_1_11.lersif_ndivl_mulr) + (deprecate lersif_ndivl_mulr lteif_ndivl_mulr)) + (at level 10, only parsing). + +Notation lersif_ndivl_mulr := + (fun b => @lersif_ndivl_mulr _ b _) (only parsing). + +Notation "@ 'lersif_ndivr_mulr'" := + ((fun _ => @mc_1_11.lersif_ndivr_mulr) + (deprecate lersif_ndivr_mulr lteif_ndivr_mulr)) + (at level 10, only parsing). + +Notation lersif_ndivr_mulr := + (fun b => @lersif_ndivr_mulr _ b _) (only parsing). + +Notation "@ 'lersif_ndivl_mull'" := + ((fun _ => @mc_1_11.lersif_ndivl_mull) + (deprecate lersif_ndivl_mull lteif_ndivl_mull)) + (at level 10, only parsing). + +Notation lersif_ndivl_mull := + (fun b => @lersif_ndivl_mull _ b _) (only parsing). + +Notation "@ 'lersif_ndivr_mull'" := + ((fun _ => @mc_1_11.lersif_ndivr_mull) + (deprecate lersif_ndivr_mull lteif_ndivr_mull)) + (at level 10, only parsing). + +Notation lersif_ndivr_mull := + (fun b => @lersif_ndivr_mull _ b _) (only parsing). + +(* IntervalPo *) + +(* `BOpen_if` has been deprecated, but `deprecate` does not accept a *) +(* constructor that takes arguments. *) +Notation "@ 'BOpen_if'" := (fun T b x => @BClose_if T (~~ b) x) +(* ((fun _ T b x => @BClose_if T (~~ b) x) (deprecate BOpen_if BClose_if)) *) + (at level 10, only parsing). + +Notation BOpen_if := (@BOpen_if _). + +Notation "@ 'lersif_in_itv'" := + ((fun _ => @mc_1_11.lersif_in_itv) (deprecate lersif_in_itv lteif_in_itv)) + (at level 10, only parsing). + +Notation lersif_in_itv := (@lersif_in_itv _ _ _ _ _ _) (only parsing). + +(* `itv_intersection` accepts any `numDomainType` but `Order.meet` accepts *) +(* only `realDomainType`. Use `Order.meet` instead of `itv_meet`. *) +(* (`deprecate` does not accept a qualified name.) *) +Notation "@ 'itv_intersection'" := + ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R]) + (deprecate itv_intersection itv_meet)) + (at level 10, only parsing) : fun_scope. + +Notation itv_intersection := (@itv_intersection _) (only parsing). + +Notation "@ 'itv_intersection1i'" := + ((fun _ => @itv_meet1i _) (deprecate itv_intersection1i itv_meet1i)) + (at level 10, only parsing) : fun_scope. + +Notation itv_intersection1i := (@itv_intersection1i _) (only parsing). + +Notation "@ 'itv_intersectioni1'" := + ((fun _ => @itv_meeti1 _) (deprecate itv_intersectioni1 itv_meeti1)) + (at level 10, only parsing) : fun_scope. + +Notation itv_intersectioni1 := (@itv_intersectioni1 _) (only parsing). + +Notation "@ 'itv_intersectionii'" := + ((fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R]) + (deprecate itv_intersectionii meetxx)) + (at level 10, only parsing) : fun_scope. + +Notation itv_intersectionii := (@itv_intersectionii _) (only parsing). + +(* IntervalOrdered *) + +Notation "@ 'itv_intersectionC'" := + ((fun _ (R : realDomainType) => @meetC _ [latticeType of interval R]) + (deprecate itv_intersectionC meetC)) + (at level 10, only parsing) : fun_scope. + +Notation itv_intersectionC := (@itv_intersectionC _) (only parsing). + +Notation "@ 'itv_intersectionA'" := + ((fun _ (R : realDomainType) => @meetA _ [latticeType of interval R]) + (deprecate itv_intersectionA meetA)) + (at level 10, only parsing) : fun_scope. + +Notation itv_intersectionA := (@itv_intersectionA _) (only parsing). -- cgit v1.2.3 From 1f224d39ac3e3a68652d1a6b64387c22543b2663 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 12 Sep 2020 07:13:40 +0900 Subject: Redefine itv_bound with BRight_if and BRInfty_if --- mathcomp/algebra/interval.v | 703 +++++++++++++++++++------------------------- 1 file changed, 308 insertions(+), 395 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 03b5e4d..391998a 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -135,54 +135,54 @@ Proof. by rewrite comparable_lteifN ?comparableT. Qed. End LteifTotal. -Variant itv_bound (T : Type) : Type := BClose_if of bool & T | BInfty. -Definition itv_boundl := itv_bound. -Definition itv_boundr := itv_bound. -Notation BOpen := (BClose_if false). -Notation BClose := (BClose_if true). -Variant interval (T : Type) := Interval of itv_boundl T & itv_boundr T. +Variant itv_bound (T : Type) : Type := + BRight_if of bool & T | BRInfty_if of bool. +Notation BLeft := (BRight_if false). +Notation BRight := (BRight_if true). +Notation "'-oo'" := (BRInfty_if _ false) (at level 0) : order_scope. +Notation "'+oo'" := (BRInfty_if _ true) (at level 0) : order_scope. +Variant interval (T : Type) := Interval of itv_bound T & itv_bound T. (* We provide the 9 following notations to help writing formal intervals *) -Notation "`[ a , b ]" := (Interval (BClose a) (BClose b)) +Notation "`[ a , b ]" := (Interval (BLeft a) (BRight b)) (at level 0, a, b at level 9 , format "`[ a , b ]") : order_scope. -Notation "`] a , b ]" := (Interval (BOpen a) (BClose b)) +Notation "`] a , b ]" := (Interval (BRight a) (BRight b)) (at level 0, a, b at level 9 , format "`] a , b ]") : order_scope. -Notation "`[ a , b [" := (Interval (BClose a) (BOpen b)) +Notation "`[ a , b [" := (Interval (BLeft a) (BLeft b)) (at level 0, a, b at level 9 , format "`[ a , b [") : order_scope. -Notation "`] a , b [" := (Interval (BOpen a) (BOpen b)) +Notation "`] a , b [" := (Interval (BRight a) (BLeft b)) (at level 0, a, b at level 9 , format "`] a , b [") : order_scope. -Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b)) +Notation "`] '-oo' , b ]" := (Interval -oo (BRight b)) (at level 0, b at level 9 , format "`] '-oo' , b ]") : order_scope. -Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b)) +Notation "`] '-oo' , b [" := (Interval -oo (BLeft b)) (at level 0, b at level 9 , format "`] '-oo' , b [") : order_scope. -Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _)) +Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo) (at level 0, a at level 9 , format "`[ a , '+oo' [") : order_scope. -Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _)) +Notation "`] a , '+oo' [" := (Interval (BRight a) +oo) (at level 0, a at level 9 , format "`] a , '+oo' [") : order_scope. -Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _)) +Notation "`] -oo , '+oo' [" := (Interval -oo +oo) (at level 0, format "`] -oo , '+oo' [") : order_scope. -Notation "`[ a , b ]" := (Interval (BClose a) (BClose b)) +Notation "`[ a , b ]" := (Interval (BLeft a) (BRight b)) (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope. -Notation "`] a , b ]" := (Interval (BOpen a) (BClose b)) +Notation "`] a , b ]" := (Interval (BRight a) (BRight b)) (at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope. -Notation "`[ a , b [" := (Interval (BClose a) (BOpen b)) +Notation "`[ a , b [" := (Interval (BLeft a) (BLeft b)) (at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope. -Notation "`] a , b [" := (Interval (BOpen a) (BOpen b)) +Notation "`] a , b [" := (Interval (BRight a) (BLeft b)) (at level 0, a, b at level 9 , format "`] a , b [") : ring_scope. -Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b)) +Notation "`] '-oo' , b ]" := (Interval -oo (BRight b)) (at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope. -Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b)) +Notation "`] '-oo' , b [" := (Interval -oo (BLeft b)) (at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope. -Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _)) +Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo) (at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope. -Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _)) +Notation "`] a , '+oo' [" := (Interval (BRight a) +oo) (at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope. -Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _)) +Notation "`] -oo , '+oo' [" := (Interval -oo +oo) (at level 0, format "`] -oo , '+oo' [") : ring_scope. -Fact itv_boundl_display (disp : unit) : unit. Proof. exact. Qed. -Fact itv_boundr_display (disp : unit) : unit. Proof. exact. Qed. +Fact itv_bound_display (disp : unit) : unit. Proof. exact. Qed. Fact interval_display (disp : unit) : unit. Proof. exact. Qed. Section IntervalEq. @@ -191,22 +191,20 @@ Variable T : eqType. Definition eq_itv_bound (b1 b2 : itv_bound T) : bool := match b1, b2 with - | BClose_if a x, BClose_if b y => (a == b) && (x == y) - | BInfty, BInfty => true + | BRight_if a x, BRight_if b y => (a == b) && (x == y) + | BRInfty_if a, BRInfty_if b => a == b | _, _ => false end. Lemma eq_itv_boundP : Equality.axiom eq_itv_bound. Proof. move=> b1 b2; apply: (iffP idP). -- by move: b1 b2 => [a x|][b y|] => //= /andP [] /eqP -> /eqP ->. +- by move: b1 b2 => [a x|a][b y|b] => //= [/andP [/eqP -> /eqP ->]|/eqP ->]. - by move=> <-; case: b1 => //= a x; rewrite !eqxx. Qed. Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP. Canonical itv_bound_eqType := EqType (itv_bound T) itv_bound_eqMixin. -Canonical itv_boundl_eqType := [eqType of itv_boundl T]. -Canonical itv_boundr_eqType := [eqType of itv_boundr T]. Definition eqitv (x y : interval T) : bool := let: Interval x x' := x in @@ -231,9 +229,9 @@ Variable T : choiceType. Lemma itv_bound_can : cancel (fun b : itv_bound T => - match b with BInfty => None | BClose_if b x => Some (b, x) end) + match b with BRight_if b x => (b, Some x) | BRInfty_if b => (b, None) end) (fun b => - match b with None => BInfty _ | Some (b, x) => BClose_if b x end). + match b with (b, Some x) => BRight_if b x | (b, None) => BRInfty_if _ b end). Proof. by case. Qed. Lemma interval_can : @@ -249,24 +247,16 @@ Canonical itv_bound_choiceType (T : choiceType) := ChoiceType (itv_bound T) (CanChoiceMixin (@itv_bound_can T)). Canonical interval_choiceType (T : choiceType) := ChoiceType (interval T) (CanChoiceMixin (@interval_can T)). -Canonical itv_boundl_choiceType (T : choiceType) := - [choiceType of itv_boundl T]. -Canonical itv_boundr_choiceType (T : choiceType) := - [choiceType of itv_boundr T]. Canonical itv_bound_countType (T : countType) := CountType (itv_bound T) (CanCountMixin (@itv_bound_can T)). Canonical interval_countType (T : countType) := CountType (interval T) (CanCountMixin (@interval_can T)). -Canonical itv_boundl_countType (T : countType) := [countType of itv_boundl T]. -Canonical itv_boundr_countType (T : countType) := [countType of itv_boundr T]. Canonical itv_bound_finType (T : finType) := FinType (itv_bound T) (CanFinMixin (@itv_bound_can T)). Canonical interval_finType (T : finType) := FinType (interval T) (CanFinMixin (@interval_can T)). -Canonical itv_boundl_finType (T : finType) := [finType of itv_boundl T]. -Canonical itv_boundr_finType (T : finType) := [finType of itv_boundr T]. End Exports. @@ -278,172 +268,46 @@ Section IntervalPOrder. Variable (disp : unit) (T : porderType disp). Implicit Types (x y z : T) (i : interval T). -Definition pred_of_itv i : pred T := - [pred x | let: Interval l u := i in - match l with - | BClose_if b lb => lb < x ?<= if b - | BInfty => true - end && - match u with - | BClose_if b ub => x < ub ?<= if b - | BInfty => true - end]. - -Canonical Structure itvPredType := PredType pred_of_itv. - -(* we compute a set of rewrite rules associated to an interval *) -Definition itv_rewrite i x : Type := - let: Interval l u := i in - (match l with - | BClose a => (a <= x) * (x < a = false) - | BOpen a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false) - | BInfty => forall x : T, x == x - end * - match u with - | BClose b => (x <= b) * (b < x = false) - | BOpen b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false) - | BInfty => forall x : T, x == x - end * - match l, u with - | BClose a, BClose b => - (a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b]) - | BClose a, BOpen b => - (a <= b) * (a < b) * (b <= a = false) * (b < a = false) - * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) - | BOpen a, BClose b => - (a <= b) * (a < b) * (b <= a = false) * (b < a = false) - * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) - | BOpen a, BOpen b => - (a <= b) * (a < b) * (b <= a = false) * (b < a = false) - * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) - | _, _ => forall x : T, x == x - end)%type. - -Definition itv_decompose i x : Prop := - let: Interval l u := i in - ((match l with - | BClose_if b lb => (lb < x ?<= if b) : Prop - | BInfty => True - end : Prop) * - (match u with - | BClose_if b ub => (x < ub ?<= if b) : Prop - | BInfty => True - end : Prop))%type. - -Lemma itv_dec : forall x i, reflect (itv_decompose i x) (x \in i). -Proof. by move=> ? [[? ?|][? ?|]]; apply: (iffP andP); case. Qed. - -Arguments itv_dec {x i}. - -Definition le_boundl (b1 b2 : itv_boundl T) := +Definition le_bound (b1 b2 : itv_bound T) := match b1, b2 with - | BClose_if b1 x1, BClose_if b2 x2 => x1 < x2 ?<= if b2 ==> b1 - | BClose_if _ _, BInfty => false - | _, _ => true + | -oo, _ | _, +oo => true + | BRight_if b1 x1, BRight_if b2 x2 => x1 < x2 ?<= if b1 ==> b2 + | _, _ => false end. -Definition le_boundr (b1 b2 : itv_boundr T) := +Definition lt_bound (b1 b2 : itv_bound T) := match b1, b2 with - | BClose_if b1 x1, BClose_if b2 x2 => x1 < x2 ?<= if b1 ==> b2 - | BInfty, BClose_if _ _ => false - | _, _ => true + | -oo, +oo | -oo, BRight_if _ _ | BRight_if _ _, +oo => true + | BRight_if b1 x1, BRight_if b2 x2 => x1 < x2 ?<= if ~~ b1 && b2 + | _, _ => false end. -Lemma itv_boundlr bl br x : - (x \in Interval bl br) = - (le_boundl bl (BClose x)) && (le_boundr (BClose x) br). -Proof. by case: bl br => [? ?|][]. Qed. - -Lemma le_boundl_refl : reflexive le_boundl. -Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed. - -Lemma le_boundr_refl : reflexive le_boundr. -Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed. +Lemma lt_bound_def b1 b2 : lt_bound b1 b2 = (b2 != b1) && le_bound b1 b2. +Proof. by case: b1 b2 => [[]?|[]][[]?|[]] //=; rewrite lt_def. Qed. -Hint Resolve le_boundl_refl le_boundr_refl : core. +Lemma le_bound_refl : reflexive le_bound. +Proof. by move=> [[]?|[]] /=. Qed. -Lemma le_boundl_anti : antisymmetric le_boundl. -Proof. by case=> [[]?|][[]?|] //=; case: comparableP => // ->. Qed. +Lemma le_bound_anti : antisymmetric le_bound. +Proof. by case=> [[]?|[]] [[]?|[]] //=; case: comparableP => // ->. Qed. -Lemma le_boundl_converse_anti : antisymmetric (fun b => le_boundl ^~ b). -Proof. by move=> ? ? /le_boundl_anti. Qed. - -Lemma le_boundr_anti : antisymmetric le_boundr. -Proof. by case=> [[]?|][[]?|] //=; case: comparableP => // ->. Qed. - -Lemma le_boundl_trans : transitive le_boundl. +Lemma le_bound_trans : transitive le_bound. Proof. -by move=> [[] x|][[] y|][[] z|] lexy leyz //; +by case=> [[]?|[]] [[]?|[]] [[]?|[]] lexy leyz //; apply: (lteif_imply _ (lteif_trans lexy leyz)). Qed. -Lemma le_boundl_converse_trans : transitive (fun b => le_boundl ^~ b). -Proof. move=> ? ? ? ? /le_boundl_trans; exact. Qed. - -Lemma le_boundr_trans : transitive le_boundr. -Proof. -by move=> [[] x|][[] y|][[] z|] lexy leyz //; - apply: (lteif_imply _ (lteif_trans lexy leyz)). -Qed. +Definition itv_bound_porderMixin := + LePOrderMixin lt_bound_def le_bound_refl le_bound_anti le_bound_trans. +Canonical itv_bound_porderType := + POrderType (itv_bound_display disp) (itv_bound T) itv_bound_porderMixin. -Lemma le_boundl_bb x b1 b2 : - le_boundl (BClose_if b1 x) (BClose_if b2 x) = (b2 ==> b1). -Proof. by rewrite /le_boundl lteifxx. Qed. - -Lemma le_boundr_bb x b1 b2 : - le_boundr (BClose_if b1 x) (BClose_if b2 x) = (b1 ==> b2). -Proof. by rewrite /le_boundr lteifxx. Qed. - -Lemma itv_xx x bl br : - Interval (BClose_if bl x) (BClose_if br x) =i - if bl && br then pred1 x else pred0. -Proof. by move: bl br => [][] y /=; rewrite !inE lteif_anti /=. Qed. - -Lemma itv_gte ba xa bb xb : - xb < xa ?<= if ~~ (ba && bb) -> - Interval (BClose_if ba xa) (BClose_if bb xb) =i pred0. -Proof. -move=> ? y; rewrite itv_boundlr inE /=. -by apply/negP => /andP [] lexay /(lteif_trans lexay); rewrite lteifNF. -Qed. - -Lemma boundl_in_itv : forall ba xa b, - xa \in Interval (BClose_if ba xa) b = - if ba then le_boundr (BClose xa) b else false. -Proof. by move=> [] xa [b xb|]; rewrite inE lteifxx. Qed. - -Lemma boundr_in_itv : forall bb xb a, - xb \in Interval a (BClose_if bb xb) = - if bb then le_boundl a (BClose xb) else false. -Proof. by move=> [] xb [b xa|]; rewrite inE lteifxx /= ?andbT ?andbF. Qed. - -Definition bound_in_itv := (boundl_in_itv, boundr_in_itv). - -Lemma itvP : forall x i, x \in i -> itv_rewrite i x. -Proof. -move=> x [[[] a|][[] b|]] /itv_dec [ha hb]; do !split; - rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)]; - by [| apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW]. -Qed. - -Arguments itvP [x i]. - -Definition itv_boundl_porderMixin := - @LePOrderMixin - (itv_boundl_eqType T) (fun b => le_boundl^~ b) _ (fun _ _ => erefl) - le_boundl_refl le_boundl_converse_anti le_boundl_converse_trans. -Canonical itv_boundl_porderType := - POrderType (itv_boundl_display disp) (itv_boundl T) itv_boundl_porderMixin. - -Definition itv_boundr_porderMixin := - LePOrderMixin (fun _ _ => erefl) - le_boundr_refl le_boundr_anti le_boundr_trans. -Canonical itv_boundr_porderType := - POrderType (itv_boundr_display disp) (itv_boundr T) itv_boundr_porderMixin. +Lemma le_bound_bb x b1 b2 : (BRight_if b1 x <= BRight_if b2 x) = (b1 ==> b2). +Proof. by rewrite /<=%O /= lteifxx. Qed. Definition subitv i1 i2 := match i1, i2 with - | Interval a1 b1, Interval a2 b2 => (a1 <= a2) && (b1 <= b2) + | Interval a1 b1, Interval a2 b2 => (a2 <= a1) && (b1 <= b2) end. Lemma subitv_refl : reflexive subitv. @@ -457,7 +321,7 @@ Qed. Lemma subitv_trans : transitive subitv. Proof. case=> [yl yr][xl xr][zl zr] /andP [Hl Hr] /andP [Hl' Hr'] /=. -by rewrite (le_trans Hl Hl') (le_trans Hr Hr'). +by rewrite (le_trans Hl' Hl) (le_trans Hr Hr'). Qed. Definition interval_porderMixin := @@ -465,37 +329,135 @@ Definition interval_porderMixin := Canonical interval_porderType := POrderType (interval_display disp) (interval T) interval_porderMixin. +Definition pred_of_itv i : pred T := [pred x | `[x, x] <= i]. + +Canonical Structure itvPredType := PredType pred_of_itv. + +Lemma itv_boundlr bl br x : + (x \in Interval bl br) = (bl <= BLeft x) && (BRight x <= br). +Proof. by []. Qed. + Lemma subitvP i1 i2 : i1 <= i2 -> {subset i1 <= i2}. Proof. -by case: i1 i2 => [[b2 l2|][b2' u2|]][[b1 l1|][b1' u1|]] +by case: i1 i2 => [[b2 l2|[]][b2' u2|[]]][[b1 l1|[]][b1' u1|[]]] /andP [] /= ha hb x /andP [ha' hb']; apply/andP; split => //; (apply/lteif_imply: (lteif_trans ha ha'); case: b1 b2 ha ha' => [][]) || (apply/lteif_imply: (lteif_trans hb' hb); case: b1' b2' hb hb' => [][]). Qed. -Lemma subitvPr (a : itv_boundl T) (b1 b2 : itv_boundr T) : - le_boundr b1 b2 -> {subset (Interval a b1) <= (Interval a b2)}. -Proof. by move=> leb; apply: subitvP; rewrite /<=%O /= lexx. Qed. +Lemma subitvEl (a1 a2 b : itv_bound T) : + (Interval a1 b <= Interval a2 b) = (a2 <= a1). +Proof. by rewrite [LHS]/<=%O /= lexx andbT. Qed. -Lemma subitvPl (a1 a2 : itv_boundl T) (b : itv_boundr T) : - le_boundl a2 a1 -> {subset (Interval a1 b) <= (Interval a2 b)}. -Proof. by move=> lea; apply: subitvP; rewrite /<=%O /= lexx andbT. Qed. +Lemma subitvEr (a b1 b2 : itv_bound T) : + (Interval a b1 <= Interval a b2) = (b1 <= b2). +Proof. by rewrite [LHS]/<=%O /= lexx. Qed. -Lemma inEsubitv x i : (x \in i) = (`[x, x] <= i). -Proof. by rewrite inE /=; case: i => [[[]?|][[]?|]]. Qed. +Lemma subitvPl (a1 a2 b : itv_bound T) : + a2 <= a1 -> {subset Interval a1 b <= Interval a2 b}. +Proof. by move=> lea; apply: subitvP; rewrite subitvEl. Qed. + +Lemma subitvPr (a b1 b2 : itv_bound T) : + b1 <= b2 -> {subset Interval a b1 <= Interval a b2}. +Proof. by move=> leb; apply: subitvP; rewrite subitvEr. Qed. + +Definition itv_decompose i x : Prop := + let: Interval l u := i in + (match l return Prop with + | BRight_if b lb => lb < x ?<= if ~~ b + | BRInfty_if b => ~~ b + end * + match u return Prop with + | BRight_if b ub => x < ub ?<= if b + | BRInfty_if b => b + end)%type. + +Lemma itv_dec : forall x i, reflect (itv_decompose i x) (x \in i). +Proof. by move=> ? [[? ?|[]][? ?|[]]]; apply: (iffP andP); case. Qed. + +Arguments itv_dec {x i}. + +Lemma itv_xx x bl br : + Interval (BRight_if bl x) (BRight_if br x) =i + if ~~ bl && br then pred1 x else pred0. +Proof. +by move=> y; rewrite itv_boundlr lteif_anti implybF eq_sym; case: (~~ _ && _). +Qed. + +Lemma itv_gte ba xa bb xb : + xb < xa ?<= if ba || ~~ bb -> + Interval (BRight_if ba xa) (BRight_if bb xb) =i pred0. +Proof. +move=> ? y; apply/negP; rewrite inE /= itv_boundlr. +case/andP => lexay /(lteif_trans lexay). +by rewrite implybF lteifNF //= negb_and negbK. +Qed. + +Lemma boundl_in_itv : forall ba xa b, + xa \in Interval (BRight_if ba xa) b = + if ba then false else BRight xa <= b. +Proof. by case=> xa [b xb|[]]; rewrite itv_boundlr /<=%O /= ?(lexx, ltxx). Qed. + +Lemma boundr_in_itv : forall bb xb a, + xb \in Interval a (BRight_if bb xb) = + if bb then a <= BLeft xb else false. +Proof. +by case=> xb [b xa|[]]; rewrite itv_boundlr andbC /<=%O /= ?(lexx, ltxx). +Qed. + +Definition bound_in_itv := (boundl_in_itv, boundr_in_itv). + +(* we compute a set of rewrite rules associated to an interval *) +Definition itv_rewrite i x : Type := + let: Interval l u := i in + (match l with + | BLeft a => (a <= x) * (x < a = false) + | BRight a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false) + | -oo => forall x : T, x == x + | +oo => forall x : T, x == x (* ? *) + end * + match u with + | BRight b => (x <= b) * (b < x = false) + | BLeft b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false) + | +oo => forall x : T, x == x + | -oo => forall x : T, x == x (* ? *) + end * + match l, u with + | BLeft a, BRight b => + (a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b]) + | BLeft a, BLeft b => + (a <= b) * (a < b) * (b <= a = false) * (b < a = false) + * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) + | BRight a, BRight b => + (a <= b) * (a < b) * (b <= a = false) * (b < a = false) + * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) + | BRight a, BLeft b => + (a <= b) * (a < b) * (b <= a = false) * (b < a = false) + * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) + | _, _ => forall x : T, x == x + end)%type. + +Lemma itvP : forall x i, x \in i -> itv_rewrite i x. +Proof. +move=> x [[[]a|[]][[]b|[]]] /andP [] ha hb; do !split; + rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)]; + try by [| apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW]. +Qed. + +Arguments itvP [x i]. Lemma lteif_in_itv ba bb xa xb x : - x \in Interval (BClose_if ba xa) (BClose_if bb xb) -> - xa < xb ?<= if ba && bb. + x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> + xa < xb ?<= if ~~ ba && bb. Proof. by case: ba bb => [][] /itvP /= ->. Qed. Lemma ltr_in_itv ba bb xa xb x : - ~~ (ba && bb) -> x \in Interval (BClose_if ba xa) (BClose_if bb xb) -> + ba || ~~ bb -> x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> xa < xb. -Proof. by move=> /negbTE bab /lteif_in_itv; rewrite bab. Qed. +Proof. by case: ba bb => [][] // _ /itvP ->. Qed. Lemma ler_in_itv ba bb xa xb x : - x \in Interval (BClose_if ba xa) (BClose_if bb xb) -> xa <= xb. + x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> xa <= xb. Proof. by move/lteif_in_itv/lteifW. Qed. End IntervalPOrder. @@ -503,180 +465,118 @@ End IntervalPOrder. Section IntervalLattice. Variable (disp : unit) (T : latticeType disp). -Implicit Types (x y z : T) (i : interval T). +Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T). -Definition itv_boundl_meet (bl br : itv_boundl T) : itv_boundl T := +Definition bound_meet bl br : itv_bound T := match bl, br with - | BInfty, _ => br | _, BInfty => bl - | BClose_if xb x, BClose_if yb y => - BClose_if ((~~ (x <= y) || yb) && (~~ (y <= x) || xb)) (x `|` y) + | -oo, _ | _, -oo => -oo + | +oo, b | b, +oo => b + | BRight_if xb x, BRight_if yb y => + BRight_if ((~~ (x <= y) || xb) && (~~ (y <= x) || yb)) (x `&` y) end. -Definition itv_boundr_meet (bl br : itv_boundr T) : itv_boundr T := +Definition bound_join bl br : itv_bound T := match bl, br with - | BInfty, _ => br | _, BInfty => bl - | BClose_if xb x, BClose_if yb y => - BClose_if ((~~ (x <= y) || xb) && (~~ (y <= x) || yb)) (x `&` y) + | -oo, b | b, -oo => b + | +oo, _ | _, +oo => +oo + | BRight_if xb x, BRight_if yb y => + BRight_if ((x <= y) && yb || (y <= x) && xb) (x `|` y) end. -Definition itv_boundl_join (bl br : itv_boundl T) : itv_bound T := - match bl, br with - | BInfty, _ | _, BInfty => BInfty _ - | BClose_if xb x, BClose_if yb y => - BClose_if ((x <= y) && xb || (y <= x) && yb) (x `&` y) - end. - -Definition itv_boundr_join (bl br : itv_boundr T) : itv_bound T := - match bl, br with - | BInfty, _ | _, BInfty => BInfty _ - | BClose_if xb x, BClose_if yb y => - BClose_if ((x <= y) && yb || (y <= x) && xb) (x `|` y) - end. - -Lemma itv_boundl_meetC : commutative itv_boundl_meet. -Proof. -by case=> [? ?|][? ?|] //=; rewrite joinC; congr BClose_if; - case: lcomparableP; rewrite ?andbT // 1?andbC. -Qed. - -Lemma itv_boundr_meetC : commutative itv_boundr_meet. -Proof. -by case=> [? ?|][? ?|] //=; rewrite meetC; congr BClose_if; - case: lcomparableP; rewrite ?andbT // 1?andbC. -Qed. - -Lemma itv_boundl_joinC : commutative itv_boundl_join. -Proof. -by case=> [? ?|][? ?|] //=; rewrite meetC; congr BClose_if; - case: lcomparableP; rewrite ?orbF // 1?orbC. -Qed. - -Lemma itv_boundr_joinC : commutative itv_boundr_join. +Lemma bound_meetC : commutative bound_meet. Proof. -by case=> [? ?|][? ?|] //=; rewrite joinC; congr BClose_if; - case: lcomparableP; rewrite ?orbF // 1?orbC. +case=> [? ?|[]][? ?|[]] //=; rewrite meetC; congr BRight_if. +by case: lcomparableP; rewrite ?andbT // andbC. Qed. -Lemma itv_boundl_meetA : associative itv_boundl_meet. +Lemma bound_joinC : commutative bound_join. Proof. -case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?leUx ?joinA //. -by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; - case: (lcomparableP x z) => [|||//<-] //=; - case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; - rewrite ?orbT ?andbT ?lexx ?andbA. +case=> [? ?|[]][? ?|[]] //=; rewrite joinC; congr BRight_if. +by case: lcomparableP; rewrite ?orbF // orbC. Qed. -Lemma itv_boundr_meetA : associative itv_boundr_meet. +Lemma bound_meetA : associative bound_meet. Proof. -case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?lexI ?meetA //. +case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !lexI meetA; congr BRight_if. by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; case: (lcomparableP x z) => [|||//<-] //=; - case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; - rewrite ?orbT ?andbT ?lexx ?andbA. + case: (lcomparableP x y) => //=; case: (lcomparableP y z); + rewrite //= ?orbT ?andbT ?lexx ?andbA. Qed. -Lemma itv_boundl_joinA : associative itv_boundl_join. +Lemma bound_joinA : associative bound_join. Proof. -case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?lexI ?meetA //. +case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !leUx joinA //. by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; case: (lcomparableP x z) => [|||//<-] //=; - case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; - rewrite ?andbF ?orbF ?lexx ?orbA. -Qed. - -Lemma itv_boundr_joinA : associative itv_boundr_join. -Proof. -case=> [? x|][? y|][? z|]//; congr BClose_if; rewrite ?leUx ?joinA //. -by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; - case: (lcomparableP x z) => [|||//<-] //=; - case: (lcomparableP x y) => //=; case: (lcomparableP y z) => //=; - rewrite ?andbF ?orbF ?lexx ?orbA. -Qed. - -Lemma itv_boundl_meetKU b2 b1 : itv_boundl_join b1 (itv_boundl_meet b1 b2) = b1. -Proof. -case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; - rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?orbb //=. -by case: lcomparableP; rewrite ?orbb ?orbF ?andKb. + case: (lcomparableP x y) => //=; case: (lcomparableP y z); + rewrite //= ?andbF ?orbF ?lexx ?orbA. Qed. -Lemma itv_boundr_meetKU b2 b1 : itv_boundr_join b1 (itv_boundr_meet b1 b2) = b1. +Lemma bound_meetKU b2 b1 : bound_join b1 (bound_meet b1 b2) = b1. Proof. -case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; - rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?orbb //. +case: b1 b2 => [? ?|[]][? ?|[]] //=; congr BRight_if; + rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?orbb //=. by case: lcomparableP; rewrite ?andbT /= ?orbb ?andbK. Qed. -Lemma itv_boundl_joinKI b2 b1 : itv_boundl_meet b1 (itv_boundl_join b1 b2) = b1. +Lemma bound_joinKI b2 b1 : bound_meet b1 (bound_join b1 b2) = b1. Proof. -case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; - rewrite ?meetKU // leIl lexI lexx. -by case: lcomparableP; rewrite ?orbF ?andbb /= ?orbK. -Qed. - -Lemma itv_boundr_joinKI b2 b1 : itv_boundr_meet b1 (itv_boundr_join b1 b2) = b1. -Proof. -case: b1 b2 => [? ?|][? ?|] //=; congr BClose_if; - rewrite ?joinKI // leUl leUx lexx. +case: b1 b2 => [? ?|[]][? ?|[]] //=; congr BRight_if; + rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?andbb //=. by case: lcomparableP; rewrite ?andbT ?andbb ?orKb. Qed. -Lemma itv_boundl_leEmeet b1 b2 : - le_boundl b2 b1 = (itv_boundl_meet b1 b2 == b1). +Lemma bound_leEmeet b1 b2 : (b1 <= b2) = (bound_meet b1 b2 == b1). Proof. -by case: b1 b2 => [[]?|][[]?|] //=; - rewrite /eq_op /= ?eqxx // eq_joinl; case: lcomparableP. +by case: b1 b2 => [[]?|[]][[]?|[]] //=; + rewrite [LHS]/<=%O /eq_op /= ?eqxx //= -leEmeet; case: lcomparableP. Qed. -Lemma itv_boundr_leEmeet b1 b2 : - le_boundr b1 b2 = (itv_boundr_meet b1 b2 == b1). -Proof. -by case: b1 b2 => [[]?|][[]?|] //=; - rewrite /eq_op /= ?eqxx //= -leEmeet; case: lcomparableP. -Qed. +Definition itv_bound_latticeMixin := + LatticeMixin bound_meetC bound_joinC bound_meetA bound_joinA + bound_joinKI bound_meetKU bound_leEmeet. +Canonical itv_bound_latticeType := + LatticeType (itv_bound T) itv_bound_latticeMixin. + +Lemma bound_le0x b : -oo <= b. Proof. by []. Qed. -Definition itv_boundl_latticeMixin := - LatticeMixin itv_boundl_meetC itv_boundl_joinC - itv_boundl_meetA itv_boundl_joinA - itv_boundl_joinKI itv_boundl_meetKU itv_boundl_leEmeet. -Canonical itv_boundl_latticeType := - LatticeType (itv_boundl T) itv_boundl_latticeMixin. +Lemma bound_lex1 b : b <= +oo. Proof. by case: b => [|[]]. Qed. -Definition itv_boundr_latticeMixin := - LatticeMixin itv_boundr_meetC itv_boundr_joinC - itv_boundr_meetA itv_boundr_joinA - itv_boundr_joinKI itv_boundr_meetKU itv_boundr_leEmeet. -Canonical itv_boundr_latticeType := - LatticeType (itv_boundr T) itv_boundr_latticeMixin. +Canonical itv_bound_bLatticeType := + BLatticeType (itv_bound T) (BottomMixin bound_le0x). + +Canonical itv_bound_tbLatticeType := + TBLatticeType (itv_bound T) (TopMixin bound_lex1). Definition itv_meet i1 i2 : interval T := let: Interval b1l b1r := i1 in - let: Interval b2l b2r := i2 in Interval (b1l `&` b2l) (b1r `&` b2r). + let: Interval b2l b2r := i2 in Interval (b1l `|` b2l) (b1r `&` b2r). Definition itv_join i1 i2 : interval T := let: Interval b1l b1r := i1 in - let: Interval b2l b2r := i2 in Interval (b1l `|` b2l) (b1r `|` b2r). + let: Interval b2l b2r := i2 in Interval (b1l `&` b2l) (b1r `|` b2r). Lemma itv_meetC : commutative itv_meet. -Proof. by case=> [? ?][? ?]; congr Interval; rewrite meetC. Qed. +Proof. by case=> [? ?][? ?] /=; rewrite meetC joinC. Qed. Lemma itv_joinC : commutative itv_join. -Proof. by case=> [? ?][? ?]; congr Interval; rewrite joinC. Qed. +Proof. by case=> [? ?][? ?] /=; rewrite meetC joinC. Qed. Lemma itv_meetA : associative itv_meet. -Proof. by case=> [? ?][? ?][? ?]; rewrite /= !meetA. Qed. +Proof. by case=> [? ?][? ?][? ?] /=; rewrite meetA joinA. Qed. Lemma itv_joinA : associative itv_join. -Proof. by case=> [? ?][? ?][? ?]; rewrite /= !joinA. Qed. +Proof. by case=> [? ?][? ?][? ?] /=; rewrite meetA joinA. Qed. Lemma itv_meetKU i2 i1 : itv_join i1 (itv_meet i1 i2) = i1. -Proof. by case: i1 i2 => [? ?][? ?]; rewrite /= !meetKU. Qed. +Proof. by case: i1 i2 => [? ?][? ?] /=; rewrite meetKU joinKI. Qed. Lemma itv_joinKI i2 i1 : itv_meet i1 (itv_join i1 i2) = i1. -Proof. by case: i1 i2 => [? ?][? ?]; rewrite /= !joinKI. Qed. +Proof. by case: i1 i2 => [? ?][? ?] /=; rewrite meetKU joinKI. Qed. Lemma itv_leEmeet i1 i2 : (i1 <= i2) = (itv_meet i1 i2 == i1). -Proof. by case: i1 i2 => [? ?][? ?]; rewrite /<=%O /eq_op /= !leEmeet. Qed. +Proof. by case: i1 i2 => [? ?][? ?]; rewrite /eq_op /= eq_meetl eq_joinl. Qed. Definition interval_latticeMixin := LatticeMixin itv_meetC itv_joinC itv_meetA itv_joinA @@ -684,17 +584,18 @@ Definition interval_latticeMixin := Canonical interval_latticeType := LatticeType (interval T) interval_latticeMixin. -Definition itv_meet1i : left_id `]-oo, +oo[ Order.meet. -Proof. by case=> i []. Qed. +Lemma itv_le0x i : Interval +oo -oo <= i. Proof. by case: i => [[|[]]]. Qed. + +Lemma itv_lex1 i : i <= `]-oo, +oo[. Proof. by case: i => [?[|[]]]. Qed. -Definition itv_meeti1 : right_id `]-oo, +oo[ Order.meet. -Proof. by case=> [[? ?|][? ?|]]. Qed. +Canonical interval_bLatticeType := + BLatticeType (interval T) (BottomMixin itv_le0x). -Canonical itv_intersection_monoid := Monoid.Law itv_meetA itv_meet1i itv_meeti1. -Canonical itv_intersection_comoid := Monoid.ComLaw itv_meetC. +Canonical interval_tbLatticeType := + TBLatticeType (interval T) (TopMixin itv_lex1). Lemma in_itv_meet x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2). -Proof. by rewrite !inEsubitv lexI. Qed. +Proof. exact: lexI. Qed. End IntervalLattice. @@ -703,58 +604,45 @@ Section IntervalTotal. Variable (disp : unit) (T : orderType disp). Implicit Types (x y z : T) (i : interval T). -Lemma le_boundl_total : total (@le_boundl _ T). -Proof. by move=> [[]l|] [[]r|] //=; case: (ltgtP l r). Qed. - -Lemma le_boundr_total : total (@le_boundr _ T). -Proof. by move=> [[]l|] [[]r|] //=; case: (ltgtP l r). Qed. - -Definition itv_boundl_totalMixin : totalLatticeMixin _ := - fun b1 b2 => le_boundl_total b2 b1. - -Canonical itv_boundl_distrLatticeType := - DistrLatticeType (itv_boundl T) itv_boundl_totalMixin. -Canonical itv_boundl_orderType := - OrderType (itv_boundl T) itv_boundl_totalMixin. +Lemma itv_bound_totalMixin : totalLatticeMixin [latticeType of itv_bound T]. +Proof. by move=> [[]?|[]][[]?|[]]; rewrite /<=%O //=; case: ltgtP. Qed. -Canonical itv_boundr_distrLatticeType := - DistrLatticeType (itv_boundr T) (le_boundr_total : totalLatticeMixin _). -Canonical itv_boundr_orderType := OrderType (itv_boundr T) le_boundr_total. +Canonical itv_bound_distrLatticeType := + DistrLatticeType (itv_bound T) itv_bound_totalMixin. +Canonical itv_bound_bDistrLatticeType := [bDistrLatticeType of itv_bound T]. +Canonical itv_bound_tbDistrLatticeType := [tbDistrLatticeType of itv_bound T]. +Canonical itv_bound_orderType := OrderType (itv_bound T) itv_bound_totalMixin. Lemma itv_meetUl : @left_distributive (interval T) _ Order.meet Order.join. Proof. -by move=> [? ?][? ?][? ?]; rewrite /Order.meet /Order.join /= !meetUl. +by move=> [? ?][? ?][? ?]; rewrite /Order.meet /Order.join /= -meetUl -joinIl. Qed. Canonical interval_distrLatticeType := DistrLatticeType (interval T) (DistrLatticeMixin itv_meetUl). +Canonical interval_bDistrLatticeType := [bDistrLatticeType of interval T]. +Canonical interval_tbDistrLatticeType := [tbDistrLatticeType of interval T]. Lemma itv_splitU (xc : T) bc a b : xc \in Interval a b -> forall y, y \in Interval a b = - (y \in Interval a (BClose_if (~~ bc) xc)) - || (y \in Interval (BClose_if bc xc) b). + (y \in Interval a (BRight_if bc xc)) || + (y \in Interval (BRight_if bc xc) b). Proof. move=> xc_in y; move: xc_in. -rewrite !itv_boundlr [le_boundr (BClose _) (BClose_if _ _)]/= - [le_boundr]lock /= lteifN -lock. -case/andP => leaxc lexcb; - case: (boolP (le_boundl a _)) => leay; case: (boolP (le_boundr _ b)) => leyb; - rewrite /= (andbT, andbF) ?orbF ?orNb //=; - [apply/esym/negbF | apply/esym/negbTE]. -- by case: b lexcb leyb => //= bb b; rewrite -lteifN => lexcb leyb; - apply/lteif_imply: (lteif_trans lexcb leyb); rewrite andbN. -- case: a leaxc leay => //= ab a leaxc; - apply/contra => /(lteif_trans leaxc); apply/lteif_imply. - by rewrite implybE negb_and orbC orbA orbN. +rewrite !itv_boundlr ![BRight_if _ _ <= BRight_if _ _]/<=%O /= lteifN. +case/andP => leaxc lexcb; case: (leP a) => leay; case: (leP _ b) => leyb; + rewrite ?andbT ?andbF ?orbF ?orbN //=; [apply/esym/negbTE | apply/esym/negbF]. +- by rewrite -lteifN; apply/lteif_imply: (le_lt_trans lexcb leyb). +- by apply/lteif_imply: (lt_le_trans leay leaxc). Qed. Lemma itv_splitU2 x a b : x \in Interval a b -> forall y, y \in Interval a b = - [|| (y \in Interval a (BOpen x)), (y == x) - | (y \in Interval (BOpen x) b)]. + [|| (y \in Interval a (BLeft x)), (y == x) + | (y \in Interval (BRight x) b)]. Proof. -move=> xab y; rewrite (itv_splitU true xab y); congr (_ || _). -rewrite (@itv_splitU x false _ _ _ y); first by rewrite itv_xx inE. +move=> xab y; rewrite (itv_splitU false xab y); congr (_ || _). +rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE. by move: xab; rewrite boundl_in_itv itv_boundlr => /andP []. Qed. @@ -765,16 +653,16 @@ rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=. case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l); case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r); rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l. +- by case: leP b13r (lt_trans b23r b12r). - by case: leP b31l (le_trans b32l b21l). - by case: leP b31l (le_trans b32l b21l). - by case: leP b31l (le_trans b32l b21l). +- by case: leP b13r (lt_trans b23r b12r). - by case: leP b13r (le_trans b12r b23r). - by case: leP b13r (le_trans b12r b23r). -- by case: leP b13r (lt_trans b23r b12r). - by case: leP b31l (lt_trans b21l b32l). - by case: leP b31l (lt_trans b21l b32l). - by case: leP b31l (lt_trans b21l b32l). -- by case: leP b13r (lt_trans b23r b12r). Qed. Lemma itv_total_join3E i1 i2 i3 : @@ -784,16 +672,48 @@ rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=. case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l); case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r); rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l. -- by case: leP b13r (le_trans b12r b23r). - by case: leP b31l (le_trans b32l b21l). - by case: leP b31l (le_trans b32l b21l). - by case: leP b31l (le_trans b32l b21l). -- by case: leP b13r (le_trans b12r b23r). - by case: leP b13r (lt_trans b23r b12r). - by case: leP b13r (lt_trans b23r b12r). +- by case: leP b13r (le_trans b12r b23r). +- by case: leP b13r (le_trans b12r b23r). - by case: leP b31l (lt_trans b21l b32l). - by case: leP b31l (lt_trans b21l b32l). -- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b13r (le_trans b12r b23r). +Qed. + +Lemma itv_total_meetsE (S : Type) (s : seq S) (f : S -> interval T) : + \meet_(ix <- s) f ix \in + `]-oo, +oo[ :: [seq f ix `&` f ix' | ix <- s, ix' <- s]. +Proof. +case: s => [|x s]; rewrite ?big_nil // inE; apply/orP; right. +elim: s x => [|y s ih] x; rewrite !big_cons; + first by rewrite big_nil meetx1 inE meetxx. +move: (itv_total_meet3E (f x) (f y) (\meet_(ix <- s) f ix)). +rewrite meetA 3!inE => /or3P [] /eqP ->. +- by rewrite /= !inE eqxx orbT. +- move: (ih x); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. + by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. +- move: (ih y); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. + by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. +Qed. + +Lemma itv_total_joinsE (S : Type) (s : seq S) (f : S -> interval T) : + \join_(ix <- s) f ix \in + Interval +oo -oo :: [seq f ix `|` f ix' | ix <- s, ix' <- s]. +Proof. +case: s => [|x s]; rewrite ?big_nil // inE; apply/orP; right. +elim: s x => [|y s ih] x; rewrite !big_cons; + first by rewrite big_nil joinx0 inE joinxx. +move: (itv_total_join3E (f x) (f y) (\join_(ix <- s) f ix)). +rewrite joinA 3!inE => /or3P [] /eqP ->. +- by rewrite /= !inE eqxx orbT. +- move: (ih x); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. + by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. +- move: (ih y); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. + by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. Qed. End IntervalTotal. @@ -947,20 +867,21 @@ Variable R : numFieldType. Implicit Types x : R. Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x). -Proof. by rewrite !inE /= oppr_le0 andbb. Qed. +Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_le0 andbb. Qed. Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x). -Proof. by rewrite !inE /= oppr_lt0 andbb. Qed. +Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_lt0 andbb. Qed. -Lemma itv_splitI : forall a b x, - x \in Interval a b = - (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b). -Proof. by move=> [? ?|] [? ?|] ?; rewrite !inE ?andbT. Qed. +Lemma itv_splitI a b x : + x \in Interval a b = (x \in Interval a +oo) && (x \in Interval -oo b). +Proof. by rewrite !itv_boundlr ?andbT. Qed. Lemma oppr_itv ba bb (xa xb x : R) : - (-x \in Interval (BClose_if ba xa) (BClose_if bb xb)) = - (x \in Interval (BClose_if bb (-xb)) (BClose_if ba (-xa))). -Proof. by rewrite !inE lteif_oppr andbC lteif_oppl. Qed. + (-x \in Interval (BRight_if ba xa) (BRight_if bb xb)) = + (x \in Interval (BRight_if (~~ bb) (- xb)) (BRight_if (~~ ba) (-xa))). +Proof. +by rewrite !itv_boundlr /<=%O /= !implybF negbK andbC lteif_oppl lteif_oppr. +Qed. Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[). Proof. exact: oppr_itv. Qed. @@ -982,8 +903,8 @@ Variable R : realFieldType. Local Notation mid x y := ((x + y) / 2%:R). -Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ba && bb - -> mid xa xb \in Interval (BClose_if ba xa) (BClose_if bb xb). +Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ~~ ba && bb -> + mid xa xb \in Interval (BRight_if ba xa) (BRight_if bb xb). Proof. by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW. Qed. @@ -1204,12 +1125,10 @@ Section IntervalPo. Variable R : numDomainType. -Local Notation BOpen_if b x := (BClose_if (~~ b) x) (only parsing). - Lemma lersif_in_itv ba bb (xa xb x : R) : - x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> - xa <= xb ?< if ba || bb. -Proof. by move/lteif_in_itv; rewrite negb_or. Qed. + x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> + xa <= xb ?< if ba || ~~ bb. +Proof. by move/lteif_in_itv; rewrite negb_or negbK. Qed. End IntervalPo. @@ -1577,14 +1496,6 @@ Notation lersif_ndivr_mull := (* IntervalPo *) -(* `BOpen_if` has been deprecated, but `deprecate` does not accept a *) -(* constructor that takes arguments. *) -Notation "@ 'BOpen_if'" := (fun T b x => @BClose_if T (~~ b) x) -(* ((fun _ T b x => @BClose_if T (~~ b) x) (deprecate BOpen_if BClose_if)) *) - (at level 10, only parsing). - -Notation BOpen_if := (@BOpen_if _). - Notation "@ 'lersif_in_itv'" := ((fun _ => @mc_1_11.lersif_in_itv) (deprecate lersif_in_itv lteif_in_itv)) (at level 10, only parsing). @@ -1602,13 +1513,15 @@ Notation "@ 'itv_intersection'" := Notation itv_intersection := (@itv_intersection _) (only parsing). Notation "@ 'itv_intersection1i'" := - ((fun _ => @itv_meet1i _) (deprecate itv_intersection1i itv_meet1i)) + ((fun _ (R : realDomainType) => @meet1x _ [tbLatticeType of interval R]) + (deprecate itv_intersection1i meet1x)) (at level 10, only parsing) : fun_scope. Notation itv_intersection1i := (@itv_intersection1i _) (only parsing). Notation "@ 'itv_intersectioni1'" := - ((fun _ => @itv_meeti1 _) (deprecate itv_intersectioni1 itv_meeti1)) + ((fun _ (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R]) + (deprecate itv_intersectioni1 meetx1)) (at level 10, only parsing) : fun_scope. Notation itv_intersectioni1 := (@itv_intersectioni1 _) (only parsing). -- cgit v1.2.3 From 29d37a333d417c1bb27f4910704fd388b49f9a78 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 18 Sep 2020 06:28:33 +0900 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/algebra/interval.v | 649 ++++++++++++++------------------------------ mathcomp/algebra/ssrnum.v | 159 ++++++++++- mathcomp/ssreflect/order.v | 112 +++++++- 3 files changed, 468 insertions(+), 452 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 391998a..d6ea076 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -8,12 +8,11 @@ From mathcomp Require Import ssrnum. (* This file provide support for intervals in ordered types. The datatype *) (* (interval T) gives a formal characterization of an interval, as the pair *) (* of its right and left bounds. *) -(* interval R == the type of formal intervals on R. *) +(* interval T == the type of formal intervals on T. *) (* x \in i == when i is a formal interval on an ordered type, *) (* \in can be used to test membership. *) (* itvP x_in_i == where x_in_i has type x \in i, if i is ground, *) (* gives a set of rewrite rules that x_in_i imply. *) -(* x < y ?<= if c == x is smaller than y, and strictly if c is false *) (* *) (* Intervals of T form an partially ordered type (porderType) whose ordering *) (* is the subset relation. If T is a lattice, intervals also form a lattice *) @@ -46,101 +45,11 @@ Unset Printing Implicit Defensive. Local Open Scope order_scope. Import Order.TTheory. -Section LteifPOrder. - -Variable (disp : unit) (T : porderType disp). -Implicit Types (b : bool) (x y z : T). - -Definition lteif x y b := if b then x <= y else x < y. - -Local Notation "x < y ?<= 'if' b" := (lteif x y b) - (at level 70, y at next level, - format "x '[hv' < y '/' ?<= 'if' b ']'") : order_scope. - -Lemma lteif_trans x y z b1 b2 : - x < y ?<= if b1 -> y < z ?<= if b2 -> x < z ?<= if b1 && b2. -Proof. -case: b1 b2 => [][]; - [exact: le_trans | exact: le_lt_trans | exact: lt_le_trans | exact: lt_trans]. -Qed. - -Lemma lteif_anti b1 b2 x y : - (x < y ?<= if b1) && (y < x ?<= if b2) = b1 && b2 && (x == y). -Proof. by case: b1 b2 => [][]; rewrite lte_anti. Qed. - -Lemma lteifxx x b : (x < x ?<= if b) = b. -Proof. by case: b; rewrite /= ltexx. Qed. - -Lemma lteifNF x y b : y < x ?<= if ~~ b -> x < y ?<= if b = false. -Proof. by case: b => [/lt_geF|/le_gtF]. Qed. - -Lemma lteifS x y b : x < y -> x < y ?<= if b. -Proof. by case: b => //= /ltW. Qed. - -Lemma lteifT x y : x < y ?<= if true = (x <= y). Proof. by []. Qed. - -Lemma lteifF x y : x < y ?<= if false = (x < y). Proof. by []. Qed. - -Lemma lteif_orb x y : {morph lteif x y : p q / p || q}. -Proof. by case=> [][] /=; case: comparableP. Qed. - -Lemma lteif_andb x y : {morph lteif x y : p q / p && q}. -Proof. by case=> [][] /=; case: comparableP. Qed. - -Lemma lteif_imply b1 b2 x y : b1 ==> b2 -> x < y ?<= if b1 -> x < y ?<= if b2. -Proof. by case: b1 b2 => [][] //= _ /ltW. Qed. - -Lemma lteifW b x y : x < y ?<= if b -> x <= y. -Proof. by case: b => // /ltW. Qed. - -Lemma ltrW_lteif b x y : x < y -> x < y ?<= if b. -Proof. by case: b => // /ltW. Qed. - -Lemma comparable_lteifN x y b : - x >=< y -> x < y ?<= if ~~b = ~~ (y < x ?<= if b). -Proof. by case: b => /=; case: comparableP. Qed. - -End LteifPOrder. - -Notation "x < y ?<= 'if' b" := (lteif x y b) - (at level 70, y at next level, - format "x '[hv' < y '/' ?<= 'if' b ']'") : order_scope. - -Notation "x < y ?<= 'if' b" := (@lteif ring_display _ x y b) - (at level 70, y at next level, - format "x '[hv' < y '/' ?<= 'if' b ']'") : ring_scope. - -Section LteifTotal. - -Variable (disp : unit) (T : orderType disp) (b : bool) (x y z e : T). - -Lemma lteif_minr : - (x < Order.min y z ?<= if b) = (x < y ?<= if b) && (x < z ?<= if b). -Proof. by case: b; rewrite /= (le_minr, lt_minr). Qed. - -Lemma lteif_minl : - (Order.min y z < x ?<= if b) = (y < x ?<= if b) || (z < x ?<= if b). -Proof. by case: b; rewrite /= (le_minl, lt_minl). Qed. - -Lemma lteif_maxr : - (x < Order.max y z ?<= if b) = (x < y ?<= if b) || (x < z ?<= if b). -Proof. by case: b; rewrite /= (le_maxr, lt_maxr). Qed. - -Lemma lteif_maxl : - (Order.max y z < x ?<= if b) = (y < x ?<= if b) && (z < x ?<= if b). -Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed. - -Lemma lteifN : (x < y ?<= if ~~ b) = ~~ (y < x ?<= if b). -Proof. by rewrite comparable_lteifN ?comparableT. Qed. - -End LteifTotal. - -Variant itv_bound (T : Type) : Type := - BRight_if of bool & T | BRInfty_if of bool. -Notation BLeft := (BRight_if false). -Notation BRight := (BRight_if true). -Notation "'-oo'" := (BRInfty_if _ false) (at level 0) : order_scope. -Notation "'+oo'" := (BRInfty_if _ true) (at level 0) : order_scope. +Variant itv_bound (T : Type) : Type := BSide of bool & T | BInfty of bool. +Notation BLeft := (BSide true). +Notation BRight := (BSide false). +Notation "'-oo'" := (BInfty _ true) (at level 0) : order_scope. +Notation "'+oo'" := (BInfty _ false) (at level 0) : order_scope. Variant interval (T : Type) := Interval of itv_bound T & itv_bound T. (* We provide the 9 following notations to help writing formal intervals *) @@ -191,8 +100,8 @@ Variable T : eqType. Definition eq_itv_bound (b1 b2 : itv_bound T) : bool := match b1, b2 with - | BRight_if a x, BRight_if b y => (a == b) && (x == y) - | BRInfty_if a, BRInfty_if b => a == b + | BSide a x, BSide b y => (a == b) && (x == y) + | BInfty a, BInfty b => a == b | _, _ => false end. @@ -229,9 +138,9 @@ Variable T : choiceType. Lemma itv_bound_can : cancel (fun b : itv_bound T => - match b with BRight_if b x => (b, Some x) | BRInfty_if b => (b, None) end) + match b with BSide b x => (b, Some x) | BInfty b => (b, None) end) (fun b => - match b with (b, Some x) => BRight_if b x | (b, None) => BRInfty_if _ b end). + match b with (b, Some x) => BSide b x | (b, None) => BInfty _ b end). Proof. by case. Qed. Lemma interval_can : @@ -266,19 +175,19 @@ Export IntervalChoice.Exports. Section IntervalPOrder. Variable (disp : unit) (T : porderType disp). -Implicit Types (x y z : T) (i : interval T). +Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T). -Definition le_bound (b1 b2 : itv_bound T) := +Definition le_bound b1 b2 := match b1, b2 with | -oo, _ | _, +oo => true - | BRight_if b1 x1, BRight_if b2 x2 => x1 < x2 ?<= if b1 ==> b2 + | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b2 ==> b1 | _, _ => false end. -Definition lt_bound (b1 b2 : itv_bound T) := +Definition lt_bound b1 b2 := match b1, b2 with - | -oo, +oo | -oo, BRight_if _ _ | BRight_if _ _, +oo => true - | BRight_if b1 x1, BRight_if b2 x2 => x1 < x2 ?<= if ~~ b1 && b2 + | -oo, +oo | -oo, BSide _ _ | BSide _ _, +oo => true + | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b1 && ~~ b2 | _, _ => false end. @@ -302,13 +211,15 @@ Definition itv_bound_porderMixin := Canonical itv_bound_porderType := POrderType (itv_bound_display disp) (itv_bound T) itv_bound_porderMixin. -Lemma le_bound_bb x b1 b2 : (BRight_if b1 x <= BRight_if b2 x) = (b1 ==> b2). +Lemma bound_lexx c1 c2 x : (BSide c1 x <= BSide c2 x) = (c2 ==> c1). Proof. by rewrite /<=%O /= lteifxx. Qed. +Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2). +Proof. by rewrite /<%O /= lteifxx. Qed. + Definition subitv i1 i2 := - match i1, i2 with - | Interval a1 b1, Interval a2 b2 => (a2 <= a1) && (b1 <= b2) - end. + let: Interval b1l b1r := i1 in + let: Interval b2l b2r := i2 in (b2l <= b1l) && (b1r <= b2r). Lemma subitv_refl : reflexive subitv. Proof. by case=> /= ? ?; rewrite !lexx. Qed. @@ -333,43 +244,74 @@ Definition pred_of_itv i : pred T := [pred x | `[x, x] <= i]. Canonical Structure itvPredType := PredType pred_of_itv. +Lemma subitvE b1l b1r b2l b2r : + (Interval b1l b1r <= Interval b2l b2r) = (b2l <= b1l) && (b1r <= b2r). +Proof. by []. Qed. + +Lemma in_itv x i : + x \in i = + let: Interval l u := i in + match l with + | BSide b lb => lb < x ?<= if b + | BInfty b => b + end && + match u with + | BSide b ub => x < ub ?<= if ~~ b + | BInfty b => ~~ b + end. +Proof. by case: i => [[? ?|[]][|[]]]. Qed. + Lemma itv_boundlr bl br x : (x \in Interval bl br) = (bl <= BLeft x) && (BRight x <= br). Proof. by []. Qed. +Lemma itv_splitI bl br x : + x \in Interval bl br = (x \in Interval bl +oo) && (x \in Interval -oo br). +Proof. by rewrite !itv_boundlr andbT. Qed. + Lemma subitvP i1 i2 : i1 <= i2 -> {subset i1 <= i2}. -Proof. -by case: i1 i2 => [[b2 l2|[]][b2' u2|[]]][[b1 l1|[]][b1' u1|[]]] - /andP [] /= ha hb x /andP [ha' hb']; apply/andP; split => //; - (apply/lteif_imply: (lteif_trans ha ha'); case: b1 b2 ha ha' => [][]) || - (apply/lteif_imply: (lteif_trans hb' hb); case: b1' b2' hb hb' => [][]). -Qed. +Proof. by move=> ? ? /le_trans; exact. Qed. + +Lemma subitvPl b1l b2l br : + b2l <= b1l -> {subset Interval b1l br <= Interval b2l br}. +Proof. by move=> ?; apply: subitvP; rewrite subitvE lexx andbT. Qed. -Lemma subitvEl (a1 a2 b : itv_bound T) : - (Interval a1 b <= Interval a2 b) = (a2 <= a1). -Proof. by rewrite [LHS]/<=%O /= lexx andbT. Qed. +Lemma subitvPr bl b1r b2r : + b1r <= b2r -> {subset Interval bl b1r <= Interval bl b2r}. +Proof. by move=> ?; apply: subitvP; rewrite subitvE lexx. Qed. -Lemma subitvEr (a b1 b2 : itv_bound T) : - (Interval a b1 <= Interval a b2) = (b1 <= b2). -Proof. by rewrite [LHS]/<=%O /= lexx. Qed. +Lemma itv_xx x cl cr y : + y \in Interval (BSide cl x) (BSide cr x) = cl && ~~ cr && (y == x). +Proof. by case: cl cr => [] []; rewrite [LHS]lteif_anti // eq_sym. Qed. -Lemma subitvPl (a1 a2 b : itv_bound T) : - a2 <= a1 -> {subset Interval a1 b <= Interval a2 b}. -Proof. by move=> lea; apply: subitvP; rewrite subitvEl. Qed. +Lemma boundl_in_itv c x b : x \in Interval (BSide c x) b = c && (BRight x <= b). +Proof. by rewrite itv_boundlr bound_lexx. Qed. + +Lemma boundr_in_itv c x b : + x \in Interval b (BSide c x) = ~~ c && (b <= BLeft x). +Proof. by rewrite itv_boundlr bound_lexx implybF andbC. Qed. + +Definition bound_in_itv := (boundl_in_itv, boundr_in_itv). -Lemma subitvPr (a b1 b2 : itv_bound T) : - b1 <= b2 -> {subset Interval a b1 <= Interval a b2}. -Proof. by move=> leb; apply: subitvP; rewrite subitvEr. Qed. +Lemma lt_in_itv bl br x : x \in Interval bl br -> bl < br. +Proof. by case/andP; apply/le_lt_trans. Qed. + +Lemma lteif_in_itv cl cr yl yr x : + x \in Interval (BSide cl yl) (BSide cr yr) -> yl < yr ?<= if cl && ~~ cr. +Proof. exact: lt_in_itv. Qed. + +Lemma itv_ge b1 b2 : ~~ (b1 < b2) -> Interval b1 b2 =i pred0. +Proof. by move=> ltb12 y; apply/contraNF: ltb12; apply/lt_in_itv. Qed. Definition itv_decompose i x : Prop := let: Interval l u := i in (match l return Prop with - | BRight_if b lb => lb < x ?<= if ~~ b - | BRInfty_if b => ~~ b + | BSide b lb => lb < x ?<= if b + | BInfty b => b end * match u return Prop with - | BRight_if b ub => x < ub ?<= if b - | BRInfty_if b => b + | BSide b ub => x < ub ?<= if ~~ b + | BInfty b => ~~ b end)%type. Lemma itv_dec : forall x i, reflect (itv_decompose i x) (x \in i). @@ -377,36 +319,6 @@ Proof. by move=> ? [[? ?|[]][? ?|[]]]; apply: (iffP andP); case. Qed. Arguments itv_dec {x i}. -Lemma itv_xx x bl br : - Interval (BRight_if bl x) (BRight_if br x) =i - if ~~ bl && br then pred1 x else pred0. -Proof. -by move=> y; rewrite itv_boundlr lteif_anti implybF eq_sym; case: (~~ _ && _). -Qed. - -Lemma itv_gte ba xa bb xb : - xb < xa ?<= if ba || ~~ bb -> - Interval (BRight_if ba xa) (BRight_if bb xb) =i pred0. -Proof. -move=> ? y; apply/negP; rewrite inE /= itv_boundlr. -case/andP => lexay /(lteif_trans lexay). -by rewrite implybF lteifNF //= negb_and negbK. -Qed. - -Lemma boundl_in_itv : forall ba xa b, - xa \in Interval (BRight_if ba xa) b = - if ba then false else BRight xa <= b. -Proof. by case=> xa [b xb|[]]; rewrite itv_boundlr /<=%O /= ?(lexx, ltxx). Qed. - -Lemma boundr_in_itv : forall bb xb a, - xb \in Interval a (BRight_if bb xb) = - if bb then a <= BLeft xb else false. -Proof. -by case=> xb [b xa|[]]; rewrite itv_boundlr andbC /<=%O /= ?(lexx, ltxx). -Qed. - -Definition bound_in_itv := (boundl_in_itv, boundr_in_itv). - (* we compute a set of rewrite rules associated to an interval *) Definition itv_rewrite i x : Type := let: Interval l u := i in @@ -414,13 +326,13 @@ Definition itv_rewrite i x : Type := | BLeft a => (a <= x) * (x < a = false) | BRight a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false) | -oo => forall x : T, x == x - | +oo => forall x : T, x == x (* ? *) + | +oo => forall b : bool, unkeyed b = false end * match u with | BRight b => (x <= b) * (b < x = false) | BLeft b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false) | +oo => forall x : T, x == x - | -oo => forall x : T, x == x (* ? *) + | -oo => forall b : bool, unkeyed b = false end * match l, u with | BLeft a, BRight b => @@ -437,29 +349,15 @@ Definition itv_rewrite i x : Type := | _, _ => forall x : T, x == x end)%type. -Lemma itvP : forall x i, x \in i -> itv_rewrite i x. +Lemma itvP x i : x \in i -> itv_rewrite i x. Proof. -move=> x [[[]a|[]][[]b|[]]] /andP [] ha hb; do !split; - rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)]; - try by [| apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW]. +case: i => [[[]a|[]][[]b|[]]] /andP [] ha hb; rewrite /= ?bound_in_itv; + do ![split | apply/negbTE; rewrite (le_gtF, lt_geF)]; + by [|apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW]. Qed. Arguments itvP [x i]. -Lemma lteif_in_itv ba bb xa xb x : - x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> - xa < xb ?<= if ~~ ba && bb. -Proof. by case: ba bb => [][] /itvP /= ->. Qed. - -Lemma ltr_in_itv ba bb xa xb x : - ba || ~~ bb -> x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> - xa < xb. -Proof. by case: ba bb => [][] // _ /itvP ->. Qed. - -Lemma ler_in_itv ba bb xa xb x : - x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> xa <= xb. -Proof. by move/lteif_in_itv/lteifW. Qed. - End IntervalPOrder. Section IntervalLattice. @@ -471,60 +369,58 @@ Definition bound_meet bl br : itv_bound T := match bl, br with | -oo, _ | _, -oo => -oo | +oo, b | b, +oo => b - | BRight_if xb x, BRight_if yb y => - BRight_if ((~~ (x <= y) || xb) && (~~ (y <= x) || yb)) (x `&` y) + | BSide xb x, BSide yb y => + BSide (((x <= y) && xb) || ((y <= x) && yb)) (x `&` y) end. Definition bound_join bl br : itv_bound T := match bl, br with | -oo, b | b, -oo => b | +oo, _ | _, +oo => +oo - | BRight_if xb x, BRight_if yb y => - BRight_if ((x <= y) && yb || (y <= x) && xb) (x `|` y) + | BSide xb x, BSide yb y => + BSide ((~~ (x <= y) || yb) && (~~ (y <= x) || xb)) (x `|` y) end. Lemma bound_meetC : commutative bound_meet. Proof. -case=> [? ?|[]][? ?|[]] //=; rewrite meetC; congr BRight_if. -by case: lcomparableP; rewrite ?andbT // andbC. +case=> [? ?|[]][? ?|[]] //=; rewrite meetC; congr BSide. +by case: lcomparableP; rewrite ?orbF // orbC. Qed. Lemma bound_joinC : commutative bound_join. Proof. -case=> [? ?|[]][? ?|[]] //=; rewrite joinC; congr BRight_if. -by case: lcomparableP; rewrite ?orbF // orbC. +case=> [? ?|[]][? ?|[]] //=; rewrite joinC; congr BSide. +by case: lcomparableP; rewrite ?andbT // andbC. Qed. Lemma bound_meetA : associative bound_meet. Proof. -case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !lexI meetA; congr BRight_if. +case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !lexI meetA; congr BSide. by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; - case: (lcomparableP x z) => [|||//<-] //=; - case: (lcomparableP x y) => //=; case: (lcomparableP y z); - rewrite //= ?orbT ?andbT ?lexx ?andbA. + case: (lcomparableP x z) => [|||//<-]; case: (lcomparableP x y); + rewrite //= ?andbF ?orbF ?lexx ?orbA //; case: (lcomparableP y z). Qed. Lemma bound_joinA : associative bound_join. Proof. -case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !leUx joinA //. +case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !leUx joinA; congr BSide. by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; - case: (lcomparableP x z) => [|||//<-] //=; - case: (lcomparableP x y) => //=; case: (lcomparableP y z); - rewrite //= ?andbF ?orbF ?lexx ?orbA. + case: (lcomparableP x z) => [|||//<-]; case: (lcomparableP x y); + rewrite //= ?orbT ?andbT ?lexx ?andbA //; case: (lcomparableP y z). Qed. Lemma bound_meetKU b2 b1 : bound_join b1 (bound_meet b1 b2) = b1. Proof. -case: b1 b2 => [? ?|[]][? ?|[]] //=; congr BRight_if; - rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?orbb //=. -by case: lcomparableP; rewrite ?andbT /= ?orbb ?andbK. +case: b1 b2 => [? ?|[]][? ?|[]] //=; + rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?andbb //=; congr BSide. +by case: lcomparableP; rewrite ?orbF /= ?andbb ?orbK. Qed. Lemma bound_joinKI b2 b1 : bound_meet b1 (bound_join b1 b2) = b1. Proof. -case: b1 b2 => [? ?|[]][? ?|[]] //=; congr BRight_if; - rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?andbb //=. -by case: lcomparableP; rewrite ?andbT ?andbb ?orKb. +case: b1 b2 => [? ?|[]][? ?|[]] //=; + rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?orbb //=; congr BSide. +by case: lcomparableP; rewrite ?orbF ?orbb ?andKb. Qed. Lemma bound_leEmeet b1 b2 : (b1 <= b2) = (bound_meet b1 b2 == b1). @@ -594,7 +490,7 @@ Canonical interval_bLatticeType := Canonical interval_tbLatticeType := TBLatticeType (interval T) (TopMixin itv_lex1). -Lemma in_itv_meet x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2). +Lemma in_itvI x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2). Proof. exact: lexI. Qed. End IntervalLattice. @@ -623,97 +519,60 @@ Canonical interval_distrLatticeType := Canonical interval_bDistrLatticeType := [bDistrLatticeType of interval T]. Canonical interval_tbDistrLatticeType := [tbDistrLatticeType of interval T]. -Lemma itv_splitU (xc : T) bc a b : xc \in Interval a b -> - forall y, y \in Interval a b = - (y \in Interval a (BRight_if bc xc)) || - (y \in Interval (BRight_if bc xc) b). +Lemma itv_splitU c a b : a <= c <= b -> + forall y, y \in Interval a b = (y \in Interval a c) || (y \in Interval c b). Proof. -move=> xc_in y; move: xc_in. -rewrite !itv_boundlr ![BRight_if _ _ <= BRight_if _ _]/<=%O /= lteifN. -case/andP => leaxc lexcb; case: (leP a) => leay; case: (leP _ b) => leyb; - rewrite ?andbT ?andbF ?orbF ?orbN //=; [apply/esym/negbTE | apply/esym/negbF]. -- by rewrite -lteifN; apply/lteif_imply: (le_lt_trans lexcb leyb). -- by apply/lteif_imply: (lt_le_trans leay leaxc). +case/andP => leac lecb y. +rewrite !itv_boundlr !(ltNge (BLeft y) _ : (BRight y <= _) = _). +case: (leP a) (leP b) (leP c) => leay [] leby [] lecy //=. +- by case: leP lecy (le_trans lecb leby). +- by case: leP leay (le_trans leac lecy). Qed. -Lemma itv_splitU2 x a b : x \in Interval a b -> +Lemma itv_splitUeq x a b : x \in Interval a b -> forall y, y \in Interval a b = - [|| (y \in Interval a (BLeft x)), (y == x) - | (y \in Interval (BRight x) b)]. + [|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b]. Proof. -move=> xab y; rewrite (itv_splitU false xab y); congr (_ || _). -rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE. -by move: xab; rewrite boundl_in_itv itv_boundlr => /andP []. +case/andP => ax xb y; rewrite (@itv_splitU (BLeft x)) ?ax ?ltW //. +by congr orb; rewrite (@itv_splitU (BRight x)) ?bound_lexx // itv_xx. Qed. Lemma itv_total_meet3E i1 i2 i3 : i1 `&` i2 `&` i3 \in [:: i1 `&` i2; i1 `&` i3; i2 `&` i3]. Proof. -rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=. -case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l); - case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r); - rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l. -- by case: leP b13r (lt_trans b23r b12r). -- by case: leP b31l (le_trans b32l b21l). -- by case: leP b31l (le_trans b32l b21l). -- by case: leP b31l (le_trans b32l b21l). -- by case: leP b13r (lt_trans b23r b12r). +case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r]; rewrite !inE /eq_op /=. +case: (leP b1l b2l); case: (leP b1l b3l); case: (leP b2l b3l); + case: (leP b1r b2r); case: (leP b1r b3r); case: (leP b2r b3r); + rewrite ?eqxx ?orbT //= => b23r b13r b12r b23l b13l b12l. +- by case: leP b13r (le_trans b12r b23r). +- by case: leP b13l (le_trans b12l b23l). +- by case: leP b13l (le_trans b12l b23l). - by case: leP b13r (le_trans b12r b23r). - by case: leP b13r (le_trans b12r b23r). -- by case: leP b31l (lt_trans b21l b32l). -- by case: leP b31l (lt_trans b21l b32l). -- by case: leP b31l (lt_trans b21l b32l). +- by case: leP b13l (lt_trans b23l b12l). +- by case: leP b13r (lt_trans b23r b12r). +- by case: leP b13l (lt_trans b23l b12l). +- by case: leP b13r (lt_trans b23r b12r). +- by case: leP b13r (lt_trans b23r b12r). Qed. Lemma itv_total_join3E i1 i2 i3 : i1 `|` i2 `|` i3 \in [:: i1 `|` i2; i1 `|` i3; i2 `|` i3]. Proof. -rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=. -case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l); - case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r); - rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l. -- by case: leP b31l (le_trans b32l b21l). -- by case: leP b31l (le_trans b32l b21l). -- by case: leP b31l (le_trans b32l b21l). -- by case: leP b13r (lt_trans b23r b12r). -- by case: leP b13r (lt_trans b23r b12r). -- by case: leP b13r (le_trans b12r b23r). +case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r]; rewrite !inE /eq_op /=. +case: (leP b1l b2l); case: (leP b1l b3l); case: (leP b2l b3l); + case: (leP b1r b2r); case: (leP b1r b3r); case: (leP b2r b3r); + rewrite ?eqxx ?orbT //= => b23r b13r b12r b23l b13l b12l. - by case: leP b13r (le_trans b12r b23r). -- by case: leP b31l (lt_trans b21l b32l). -- by case: leP b31l (lt_trans b21l b32l). - by case: leP b13r (le_trans b12r b23r). -Qed. - -Lemma itv_total_meetsE (S : Type) (s : seq S) (f : S -> interval T) : - \meet_(ix <- s) f ix \in - `]-oo, +oo[ :: [seq f ix `&` f ix' | ix <- s, ix' <- s]. -Proof. -case: s => [|x s]; rewrite ?big_nil // inE; apply/orP; right. -elim: s x => [|y s ih] x; rewrite !big_cons; - first by rewrite big_nil meetx1 inE meetxx. -move: (itv_total_meet3E (f x) (f y) (\meet_(ix <- s) f ix)). -rewrite meetA 3!inE => /or3P [] /eqP ->. -- by rewrite /= !inE eqxx orbT. -- move: (ih x); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. - by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. -- move: (ih y); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. - by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. -Qed. - -Lemma itv_total_joinsE (S : Type) (s : seq S) (f : S -> interval T) : - \join_(ix <- s) f ix \in - Interval +oo -oo :: [seq f ix `|` f ix' | ix <- s, ix' <- s]. -Proof. -case: s => [|x s]; rewrite ?big_nil // inE; apply/orP; right. -elim: s x => [|y s ih] x; rewrite !big_cons; - first by rewrite big_nil joinx0 inE joinxx. -move: (itv_total_join3E (f x) (f y) (\join_(ix <- s) f ix)). -rewrite joinA 3!inE => /or3P [] /eqP ->. -- by rewrite /= !inE eqxx orbT. -- move: (ih x); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. - by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. -- move: (ih y); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=. - by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT. +- by case: leP b13l (le_trans b12l b23l). +- by case: leP b13l (le_trans b12l b23l). +- by case: leP b13l (le_trans b12l b23l). +- by case: leP b13r (lt_trans b23r b12r). +- by case: leP b13l (lt_trans b23l b12l). +- by case: leP b13l (lt_trans b23l b12l). +- by case: leP b13l (lt_trans b23l b12l). +- by case: leP b13r (lt_trans b23r b12r). Qed. End IntervalTotal. @@ -721,178 +580,34 @@ End IntervalTotal. Local Open Scope ring_scope. Import GRing.Theory Num.Theory. -Section LteifNumDomain. - -Variable R : numDomainType. -Implicit Types (b : bool) (x y z : R). - -Local Notation "x < y ?<= 'if' b" := (@lteif _ R x y b) - (at level 70, y at next level, - format "x '[hv' < y '/' ?<= 'if' b ']'") : ring_scope. - -Lemma subr_lteifr0 b (x y : R) : (y - x < 0 ?<= if b) = (y < x ?<= if b). -Proof. by case: b => /=; rewrite subr_lte0. Qed. - -Lemma subr_lteif0r b (x y : R) : (0 < y - x ?<= if b) = (x < y ?<= if b). -Proof. by case: b => /=; rewrite subr_gte0. Qed. - -Definition subr_lteif0 := (subr_lteifr0, subr_lteif0r). - -Lemma lteif01 b : 0 < 1 ?<= if b. -Proof. by case: b; rewrite /= lter01. Qed. - -Lemma lteif_oppl b x y : - x < y ?<= if b = (- y < x ?<= if b). -Proof. by case: b; rewrite /= lter_oppl. Qed. - -Lemma lteif_oppr b x y : x < - y ?<= if b = (y < - x ?<= if b). -Proof. by case: b; rewrite /= lter_oppr. Qed. - -Lemma lteif_0oppr b x : 0 < - x ?<= if b = (x < 0 ?<= if b). -Proof. by case: b; rewrite /= (oppr_ge0, oppr_gt0). Qed. - -Lemma lteif_oppr0 b x : - x < 0 ?<= if b = (0 < x ?<= if b). -Proof. by case: b; rewrite /= (oppr_le0, oppr_lt0). Qed. - -Lemma lteif_opp2 b : {mono -%R : x y /~ x < y ?<= if b}. -Proof. by case: b => ? ?; rewrite /= lter_opp2. Qed. - -Definition lteif_oppE := (lteif_0oppr, lteif_oppr0, lteif_opp2). - -Lemma lteif_add2l b x : {mono +%R x : y z / y < z ?<= if b}. -Proof. by case: b => ? ?; rewrite /= lter_add2. Qed. - -Lemma lteif_add2r b x : {mono +%R^~ x : y z / y < z ?<= if b}. -Proof. by case: b => ? ?; rewrite /= lter_add2. Qed. - -Definition lteif_add2 := (lteif_add2l, lteif_add2r). - -Lemma lteif_subl_addr b x y z : (x - y < z ?<= if b) = (x < z + y ?<= if b). -Proof. by case: b; rewrite /= lter_sub_addr. Qed. - -Lemma lteif_subr_addr b x y z : (x < y - z ?<= if b) = (x + z < y ?<= if b). -Proof. by case: b; rewrite /= lter_sub_addr. Qed. - -Definition lteif_sub_addr := (lteif_subl_addr, lteif_subr_addr). - -Lemma lteif_subl_addl b x y z : (x - y < z ?<= if b) = (x < y + z ?<= if b). -Proof. by case: b; rewrite /= lter_sub_addl. Qed. - -Lemma lteif_subr_addl b x y z : (x < y - z ?<= if b) = (z + x < y ?<= if b). -Proof. by case: b; rewrite /= lter_sub_addl. Qed. - -Definition lteif_sub_addl := (lteif_subl_addl, lteif_subr_addl). - -Lemma lteif_pmul2l b x : 0 < x -> {mono *%R x : y z / y < z ?<= if b}. -Proof. by case: b => ? ? ?; rewrite /= lter_pmul2l. Qed. - -Lemma lteif_pmul2r b x : 0 < x -> {mono *%R^~ x : y z / y < z ?<= if b}. -Proof. by case: b => ? ? ?; rewrite /= lter_pmul2r. Qed. - -Lemma lteif_nmul2l b x : x < 0 -> {mono *%R x : y z /~ y < z ?<= if b}. -Proof. by case: b => ? ? ?; rewrite /= lter_nmul2l. Qed. - -Lemma lteif_nmul2r b x : x < 0 -> {mono *%R^~ x : y z /~ y < z ?<= if b}. -Proof. by case: b => ? ? ?; rewrite /= lter_nmul2r. Qed. - -Lemma real_lteifN x y b : x \is Num.real -> y \is Num.real -> - x < y ?<= if ~~b = ~~ (y < x ?<= if b). -Proof. by move=> ? ?; rewrite comparable_lteifN ?real_comparable. Qed. - -Lemma real_lteif_norml b x y : - x \is Num.real -> - (`|x| < y ?<= if b) = ((- y < x ?<= if b) && (x < y ?<= if b)). -Proof. by case: b => ?; rewrite /= real_lter_norml. Qed. - -Lemma real_lteif_normr b x y : - y \is Num.real -> - (x < `|y| ?<= if b) = ((x < y ?<= if b) || (x < - y ?<= if b)). -Proof. by case: b => ?; rewrite /= real_lter_normr. Qed. - -Lemma lteif_nnormr b x y : y < 0 ?<= if ~~ b -> (`|x| < y ?<= if b) = false. -Proof. by case: b => ?; rewrite /= lter_nnormr. Qed. - -End LteifNumDomain. - -Section LteifRealDomain. - -Variable (R : realDomainType) (b : bool) (x y z e : R). - -Lemma lteif_norml : - (`|x| < y ?<= if b) = (- y < x ?<= if b) && (x < y ?<= if b). -Proof. by case: b; rewrite /= lter_norml. Qed. - -Lemma lteif_normr : - (x < `|y| ?<= if b) = (x < y ?<= if b) || (x < - y ?<= if b). -Proof. by case: b; rewrite /= lter_normr. Qed. - -Lemma lteif_distl : - (`|x - y| < e ?<= if b) = (y - e < x ?<= if b) && (x < y + e ?<= if b). -Proof. by case: b; rewrite /= lter_distl. Qed. - -End LteifRealDomain. - -Section LteifField. - -Variable (F : numFieldType) (b : bool) (z x y : F). - -Lemma lteif_pdivl_mulr : 0 < z -> x < y / z ?<= if b = (x * z < y ?<= if b). -Proof. by case: b => ? /=; rewrite lter_pdivl_mulr. Qed. - -Lemma lteif_pdivr_mulr : 0 < z -> y / z < x ?<= if b = (y < x * z ?<= if b). -Proof. by case: b => ? /=; rewrite lter_pdivr_mulr. Qed. - -Lemma lteif_pdivl_mull : 0 < z -> x < z^-1 * y ?<= if b = (z * x < y ?<= if b). -Proof. by case: b => ? /=; rewrite lter_pdivl_mull. Qed. - -Lemma lteif_pdivr_mull : 0 < z -> z^-1 * y < x ?<= if b = (y < z * x ?<= if b). -Proof. by case: b => ? /=; rewrite lter_pdivr_mull. Qed. - -Lemma lteif_ndivl_mulr : z < 0 -> x < y / z ?<= if b = (y < x * z ?<= if b). -Proof. by case: b => ? /=; rewrite lter_ndivl_mulr. Qed. - -Lemma lteif_ndivr_mulr : z < 0 -> y / z < x ?<= if b = (x * z < y ?<= if b). -Proof. by case: b => ? /=; rewrite lter_ndivr_mulr. Qed. - -Lemma lteif_ndivl_mull : z < 0 -> x < z^-1 * y ?<= if b = (y < z * x ?<= if b). -Proof. by case: b => ? /=; rewrite lter_ndivl_mull. Qed. - -Lemma lteif_ndivr_mull : z < 0 -> z^-1 * y < x ?<= if b = (z * x < y ?<= if b). -Proof. by case: b => ? /=; rewrite lter_ndivr_mull. Qed. - -End LteifField. - Section IntervalNumDomain. Variable R : numFieldType. Implicit Types x : R. -Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x). +Lemma mem0_itvcc_xNx x : (0 \in `[- x, x]) = (0 <= x). Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_le0 andbb. Qed. -Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x). +Lemma mem0_itvoo_xNx x : 0 \in `](- x), x[ = (0 < x). Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_lt0 andbb. Qed. -Lemma itv_splitI a b x : - x \in Interval a b = (x \in Interval a +oo) && (x \in Interval -oo b). -Proof. by rewrite !itv_boundlr ?andbT. Qed. - Lemma oppr_itv ba bb (xa xb x : R) : - (-x \in Interval (BRight_if ba xa) (BRight_if bb xb)) = - (x \in Interval (BRight_if (~~ bb) (- xb)) (BRight_if (~~ ba) (-xa))). + (- x \in Interval (BSide ba xa) (BSide bb xb)) = + (x \in Interval (BSide (~~ bb) (- xb)) (BSide (~~ ba) (- xa))). Proof. by rewrite !itv_boundlr /<=%O /= !implybF negbK andbC lteif_oppl lteif_oppr. Qed. -Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[). +Lemma oppr_itvoo (a b x : R) : (- x \in `]a, b[) = (x \in `](- b), (- a)[). Proof. exact: oppr_itv. Qed. -Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]). +Lemma oppr_itvco (a b x : R) : (- x \in `[a, b[) = (x \in `](- b), (- a)]). Proof. exact: oppr_itv. Qed. -Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[). +Lemma oppr_itvoc (a b x : R) : (- x \in `]a, b]) = (x \in `[(- b), (- a)[). Proof. exact: oppr_itv. Qed. -Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]). +Lemma oppr_itvcc (a b x : R) : (- x \in `[a, b]) = (x \in `[(- b), (- a)]). Proof. exact: oppr_itv. Qed. End IntervalNumDomain. @@ -903,10 +618,10 @@ Variable R : realFieldType. Local Notation mid x y := ((x + y) / 2%:R). -Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ~~ ba && bb -> - mid xa xb \in Interval (BRight_if ba xa) (BRight_if bb xb). +Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ba && ~~ bb -> + mid xa xb \in Interval (BSide ba xa) (BSide bb xb). Proof. -by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW. +by move=> [] [] xa xb /= ?; apply/itv_dec; rewrite /= ?midf_lte // ?ltW. Qed. Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[. @@ -923,7 +638,7 @@ End IntervalField. Module mc_1_11. -Local Notation lersif x y b := (lteif x y (~~ b)) (only parsing). +Local Notation lersif x y b := (Order.lteif x y (~~ b)) (only parsing). Local Notation "x <= y ?< 'if' b" := (x < y ?<= if ~~ b) (at level 70, y at next level, only parsing) : ring_scope. @@ -1037,7 +752,7 @@ Proof. exact: lteif_nmul2r. Qed. Lemma real_lersifN x y b : x \is Num.real -> y \is Num.real -> x <= y ?< if ~~b = ~~ (y <= x ?< if b). -Proof. exact: real_lteifN. Qed. +Proof. exact: real_lteifNE. Qed. Lemma real_lersif_norml b x y : x \is Num.real -> @@ -1059,7 +774,7 @@ Section LersifOrdered. Variable (R : realDomainType) (b : bool) (x y z e : R). Lemma lersifN : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b). -Proof. exact: lteifN. Qed. +Proof. exact: lteifNE. Qed. Lemma lersif_norml : (`|x| <= y ?< if b) = (- y <= x ?< if b) && (x <= y ?< if b). @@ -1125,17 +840,40 @@ Section IntervalPo. Variable R : numDomainType. -Lemma lersif_in_itv ba bb (xa xb x : R) : - x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> - xa <= xb ?< if ba || ~~ bb. -Proof. by move/lteif_in_itv; rewrite negb_or negbK. Qed. +Implicit Types (x xa xb : R). + +Lemma lersif_in_itv ba bb xa xb x : + x \in Interval (BSide ba xa) (BSide bb xb) -> xa <= xb ?< if ~~ ba || bb. +Proof. by move/lt_in_itv; rewrite negb_or negbK. Qed. + +Lemma itv_gte ba xa bb xb : + xb <= xa ?< if ba && ~~ bb -> Interval (BSide ba xa) (BSide bb xb) =i pred0. +Proof. by move=> ?; apply: itv_ge; rewrite /<%O /= lteifNF. Qed. + +Lemma ltr_in_itv ba bb xa xb x : + ~~ ba || bb -> x \in Interval (BSide ba xa) (BSide bb xb) -> xa < xb. +Proof. by move=> bab /lersif_in_itv; rewrite bab. Qed. + +Lemma ler_in_itv ba bb xa xb x : + x \in Interval (BSide ba xa) (BSide bb xb) -> xa <= xb. +Proof. by move/lt_in_itv/lteifW. Qed. End IntervalPo. +Lemma itv_splitU2 (R : realDomainType) (x : R) a b : + x \in Interval a b -> + forall y, y \in Interval a b = + [|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b]. +Proof. exact: itv_splitUeq. Qed. + End mc_1_11. +(* Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a *) +(* qualified name.) *) +Local Notation lteif := Order.lteif (only parsing). + Notation "@ 'lersif'" := - ((fun _ (R : numDomainType) x y b => @lteif _ R x y (~~ b)) + ((fun _ (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b)) (deprecate lersif lteif)) (at level 10, only parsing). @@ -1351,7 +1089,7 @@ Notation "@ 'lersif_nmul2r'" := Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing). Notation "@ 'real_lersifN'" := - ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifN)) + ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifNE)) (at level 10, only parsing). Notation real_lersifN := (@real_lersifN _ _ _) (only parsing). @@ -1381,7 +1119,7 @@ Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing). (* LersifOrdered *) Notation "@ 'lersifN'" := - ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifN)) + ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifNE)) (at level 10, only parsing). Notation lersifN := (@lersifN _) (only parsing). @@ -1502,9 +1240,32 @@ Notation "@ 'lersif_in_itv'" := Notation lersif_in_itv := (@lersif_in_itv _ _ _ _ _ _) (only parsing). +Notation "@ 'itv_gte'" := + ((fun _ => @mc_1_11.itv_gte) (deprecate itv_gte itv_ge)) + (at level 10, only parsing). + +Notation itv_gte := (@itv_gte _ _ _ _ _) (only parsing). + +Notation "@ 'ltr_in_itv'" := + ((fun _ => @mc_1_11.ltr_in_itv) (deprecate ltr_in_itv lt_in_itv)) + (at level 10, only parsing). + +Notation ltr_in_itv := (@ltr_in_itv _ _ _ _ _ _) (only parsing). + +Notation "@ 'ler_in_itv'" := + ((fun _ => @mc_1_11.ler_in_itv) (deprecate ler_in_itv lt_in_itv)) + (at level 10, only parsing). + +Notation ler_in_itv := (@ler_in_itv _ _ _ _ _ _) (only parsing). + +Notation "@ 'itv_splitU2'" := + ((fun _ => @mc_1_11.itv_splitU2) (deprecate itv_splitU2 itv_splitUeq)) + (at level 10, only parsing). + +Notation itv_splitU2 := (@itv_splitU2 _ _ _ _) (only parsing). + (* `itv_intersection` accepts any `numDomainType` but `Order.meet` accepts *) (* only `realDomainType`. Use `Order.meet` instead of `itv_meet`. *) -(* (`deprecate` does not accept a qualified name.) *) Notation "@ 'itv_intersection'" := ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R]) (deprecate itv_intersection itv_meet)) diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index e09ba9b..2ebbdcc 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -80,11 +80,11 @@ From mathcomp Require Import ssralg poly. (* [rcfType of T for S] *) (* == T-clone of the realClosedFieldType structure S. *) (* *) -(* The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _, >=<, *) -(* and ><) and lattice operations (meet and join) defined in order.v are *) -(* redefined for the ring_display in the ring_scope (%R). 0-ary ordering *) -(* symbols for the ring_display have the suffix "%R", e.g., <%R. All the *) -(* other ordering notations are the same as order.v. *) +(* The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _, *) +(* _ < _ ?<= if _, >=<, and ><) and lattice operations (meet and join) *) +(* defined in order.v are redefined for the ring_display in the ring_scope *) +(* (%R). 0-ary ordering symbols for the ring_display have the suffix "%R", *) +(* e.g., <%R. All the other ordering notations are the same as order.v. *) (* *) (* Over these structures, we have the following operations *) (* `|x| == norm of x. *) @@ -387,6 +387,9 @@ Notation "@ 'gtr' R" := (@Order.gt ring_display R) Notation lerif := (@Order.leif ring_display _) (only parsing). Notation "@ 'lerif' R" := (@Order.leif ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. +Notation lterif := (@Order.lteif ring_display _) (only parsing). +Notation "@ 'lteif' R" := (@Order.lteif ring_display R) + (at level 10, R at level 8, only parsing) : fun_scope. Notation comparabler := (@Order.comparable ring_display _) (only parsing). Notation "@ 'comparabler' R" := (@Order.comparable ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. @@ -416,6 +419,7 @@ Notation lt := ltr (only parsing). Notation ge := ger (only parsing). Notation gt := gtr (only parsing). Notation leif := lerif (only parsing). +Notation lteif := lterif (only parsing). Notation comparable := comparabler (only parsing). Notation sg := sgr. Notation max := maxr. @@ -448,6 +452,7 @@ Notation ">=%R" := ge : fun_scope. Notation "<%R" := lt : fun_scope. Notation ">%R" := gt : fun_scope. Notation "=<%R" := comparable : fun_scope. Notation "><%R" := (fun x y => ~~ (comparable x y)) : fun_scope. @@ -483,6 +488,10 @@ Notation "x <= y ?= 'iff' C" := (lerif x y C) : ring_scope. Notation "x <= y ?= 'iff' C :> R" := ((x : R) <= (y : R) ?= iff C) (only parsing) : ring_scope. +Notation "x < y ?<= 'if' C" := (lterif x y C) : ring_scope. +Notation "x < y ?<= 'if' C :> R" := ((x : R) < (y : R) ?<= if C) + (only parsing) : ring_scope. + Notation ">=< x" := (comparable x) : ring_scope. Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : ring_scope. Notation "x >=< y" := (comparable x y) : ring_scope. @@ -3313,6 +3322,94 @@ congr (leif _ _ _): (leif_pmul Ei_ge0 m1ge0 (leE12 i Pi) le_m12). by rewrite mulf_eq0 -!orbA; congr (_ || _); rewrite !orb_andr orbA orbb. Qed. +(* lteif *) + +Lemma subr_lteifr0 C x y : (y - x < 0 ?<= if C) = (y < x ?<= if C). +Proof. by case: C => /=; rewrite subr_lte0. Qed. + +Lemma subr_lteif0r C x y : (0 < y - x ?<= if C) = (x < y ?<= if C). +Proof. by case: C => /=; rewrite subr_gte0. Qed. + +Definition subr_lteif0 := (subr_lteifr0, subr_lteif0r). + +Lemma lteif01 C : 0 < 1 ?<= if C :> R. +Proof. by case: C; rewrite /= lter01. Qed. + +Lemma lteif_oppl C x y : - x < y ?<= if C = (- y < x ?<= if C). +Proof. by case: C; rewrite /= lter_oppl. Qed. + +Lemma lteif_oppr C x y : x < - y ?<= if C = (y < - x ?<= if C). +Proof. by case: C; rewrite /= lter_oppr. Qed. + +Lemma lteif_0oppr C x : 0 < - x ?<= if C = (x < 0 ?<= if C). +Proof. by case: C; rewrite /= (oppr_ge0, oppr_gt0). Qed. + +Lemma lteif_oppr0 C x : - x < 0 ?<= if C = (0 < x ?<= if C). +Proof. by case: C; rewrite /= (oppr_le0, oppr_lt0). Qed. + +Lemma lteif_opp2 C : {mono -%R : x y /~ x < y ?<= if C :> R}. +Proof. by case: C => ? ?; rewrite /= lter_opp2. Qed. + +Definition lteif_oppE := (lteif_0oppr, lteif_oppr0, lteif_opp2). + +Lemma lteif_add2l C x : {mono +%R x : y z / y < z ?<= if C}. +Proof. by case: C => ? ?; rewrite /= lter_add2. Qed. + +Lemma lteif_add2r C x : {mono +%R^~ x : y z / y < z ?<= if C}. +Proof. by case: C => ? ?; rewrite /= lter_add2. Qed. + +Definition lteif_add2 := (lteif_add2l, lteif_add2r). + +Lemma lteif_subl_addr C x y z : (x - y < z ?<= if C) = (x < z + y ?<= if C). +Proof. by case: C; rewrite /= lter_sub_addr. Qed. + +Lemma lteif_subr_addr C x y z : (x < y - z ?<= if C) = (x + z < y ?<= if C). +Proof. by case: C; rewrite /= lter_sub_addr. Qed. + +Definition lteif_sub_addr := (lteif_subl_addr, lteif_subr_addr). + +Lemma lteif_subl_addl C x y z : (x - y < z ?<= if C) = (x < y + z ?<= if C). +Proof. by case: C; rewrite /= lter_sub_addl. Qed. + +Lemma lteif_subr_addl C x y z : (x < y - z ?<= if C) = (z + x < y ?<= if C). +Proof. by case: C; rewrite /= lter_sub_addl. Qed. + +Definition lteif_sub_addl := (lteif_subl_addl, lteif_subr_addl). + +Lemma lteif_pmul2l C x : 0 < x -> {mono *%R x : y z / y < z ?<= if C}. +Proof. by case: C => ? ? ?; rewrite /= lter_pmul2l. Qed. + +Lemma lteif_pmul2r C x : 0 < x -> {mono *%R^~ x : y z / y < z ?<= if C}. +Proof. by case: C => ? ? ?; rewrite /= lter_pmul2r. Qed. + +Lemma lteif_nmul2l C x : x < 0 -> {mono *%R x : y z /~ y < z ?<= if C}. +Proof. by case: C => ? ? ?; rewrite /= lter_nmul2l. Qed. + +Lemma lteif_nmul2r C x : x < 0 -> {mono *%R^~ x : y z /~ y < z ?<= if C}. +Proof. by case: C => ? ? ?; rewrite /= lter_nmul2r. Qed. + +Lemma lteif_nnormr C x y : y < 0 ?<= if ~~ C -> (`|x| < y ?<= if C) = false. +Proof. by case: C => ?; rewrite /= lter_nnormr. Qed. + +Lemma real_lteifNE x y C : x \is Num.real -> y \is Num.real -> + x < y ?<= if ~~ C = ~~ (y < x ?<= if C). +Proof. by move=> ? ?; rewrite comparable_lteifNE ?real_comparable. Qed. + +Lemma real_lteif_norml C x y : + x \is Num.real -> + (`|x| < y ?<= if C) = ((- y < x ?<= if C) && (x < y ?<= if C)). +Proof. by case: C => ?; rewrite /= real_lter_norml. Qed. + +Lemma real_lteif_normr C x y : + y \is Num.real -> + (x < `|y| ?<= if C) = ((x < y ?<= if C) || (x < - y ?<= if C)). +Proof. by case: C => ?; rewrite /= real_lter_normr. Qed. + +Lemma real_lteif_distl C x y e : + x - y \is real -> + (`|x - y| < e ?<= if C) = (y - e < x ?<= if C) && (x < y + e ?<= if C). +Proof. by case: C => /= ?; rewrite real_lter_distl. Qed. + (* Mean inequalities. *) Lemma real_leif_mean_square_scaled x y : @@ -3621,17 +3718,51 @@ Proof. by rewrite !(fun_if GRing.inv) !(invr0, invrN, invr1). Qed. Lemma sgrV x : sgr x^-1 = sgr x. Proof. by rewrite /sgr invr_eq0 invr_lt0. Qed. +(* lteif *) + +Lemma lteif_pdivl_mulr C z x y : + 0 < z -> x < y / z ?<= if C = (x * z < y ?<= if C). +Proof. by case: C => ? /=; rewrite lter_pdivl_mulr. Qed. + +Lemma lteif_pdivr_mulr C z x y : + 0 < z -> y / z < x ?<= if C = (y < x * z ?<= if C). +Proof. by case: C => ? /=; rewrite lter_pdivr_mulr. Qed. + +Lemma lteif_pdivl_mull C z x y : + 0 < z -> x < z^-1 * y ?<= if C = (z * x < y ?<= if C). +Proof. by case: C => ? /=; rewrite lter_pdivl_mull. Qed. + +Lemma lteif_pdivr_mull C z x y : + 0 < z -> z^-1 * y < x ?<= if C = (y < z * x ?<= if C). +Proof. by case: C => ? /=; rewrite lter_pdivr_mull. Qed. + +Lemma lteif_ndivl_mulr C z x y : + z < 0 -> x < y / z ?<= if C = (y < x * z ?<= if C). +Proof. by case: C => ? /=; rewrite lter_ndivl_mulr. Qed. + +Lemma lteif_ndivr_mulr C z x y : + z < 0 -> y / z < x ?<= if C = (x * z < y ?<= if C). +Proof. by case: C => ? /=; rewrite lter_ndivr_mulr. Qed. + +Lemma lteif_ndivl_mull C z x y : + z < 0 -> x < z^-1 * y ?<= if C = (y < z * x ?<= if C). +Proof. by case: C => ? /=; rewrite lter_ndivl_mull. Qed. + +Lemma lteif_ndivr_mull C z x y : + z < 0 -> z^-1 * y < x ?<= if C = (z * x < y ?<= if C). +Proof. by case: C => ? /=; rewrite lter_ndivr_mull. Qed. + (* Interval midpoint. *) Local Notation mid x y := ((x + y) / 2%:R). -Lemma midf_le x y : x <= y -> (x <= mid x y) * (mid x y <= y). +Lemma midf_le x y : x <= y -> (x <= mid x y) * (mid x y <= y). Proof. move=> lexy; rewrite ler_pdivl_mulr ?ler_pdivr_mulr ?ltr0Sn //. by rewrite !mulrDr !mulr1 ler_add2r ler_add2l. Qed. -Lemma midf_lt x y : x < y -> (x < mid x y) * (mid x y < y). +Lemma midf_lt x y : x < y -> (x < mid x y) * (mid x y < y). Proof. move=> ltxy; rewrite ltr_pdivl_mulr ?ltr_pdivr_mulr ?ltr0Sn //. by rewrite !mulrDr !mulr1 ltr_add2r ltr_add2l. @@ -3969,6 +4100,20 @@ Proof. by move=> even_n; rewrite real_exprn_odd_le0 ?num_real. Qed. Lemma exprn_odd_lt0 n x : odd n -> (x ^+ n < 0) = (x < 0). Proof. by move=> even_n; rewrite real_exprn_odd_lt0 ?num_real. Qed. +(* lteif *) + +Lemma lteif_norml C x y : + (`|x| < y ?<= if C) = (- y < x ?<= if C) && (x < y ?<= if C). +Proof. by case: C; rewrite /= lter_norml. Qed. + +Lemma lteif_normr C x y : + (x < `|y| ?<= if C) = (x < y ?<= if C) || (x < - y ?<= if C). +Proof. by case: C; rewrite /= lter_normr. Qed. + +Lemma lteif_distl C x y e : + (`|x - y| < e ?<= if C) = (y - e < x ?<= if C) && (x < y + e ?<= if C). +Proof. by case: C; rewrite /= lter_distl. Qed. + (* Special lemmas for squares. *) Lemma sqr_ge0 x : 0 <= x ^+ 2. Proof. by rewrite exprn_even_ge0. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index da0e4d7..e4b956d 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -55,6 +55,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* @Order.ge disp T == >=%O (in fun_scope) *) (* @Order.gt disp T == >%O (in fun_scope) *) (* @Order.leif disp T == = y <-> x is greater than or equal to y (:= y <= x). *) (* x > y <-> x is greater than y (:= y < x). *) (* x <= y ?= iff C <-> x is less than y, or equal iff C is true. *) +(* x < y ?<= if C <-> x is smaller than y, and strictly if C is false. *) (* x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)). *) (* x >< y <-> x and y are incomparable (:= ~~ x >=< y). *) (* For x, y of type T, where T is canonically a latticeType d: *) @@ -423,6 +425,11 @@ Reserved Notation "x >< y" (at level 70, no associativity). Reserved Notation ">< x" (at level 35). Reserved Notation ">< y :> T" (at level 35, y at next level). +Reserved Notation "x < y ?<= 'if' c" (at level 70, y, c at next level, + format "x '[hv' < y '/' ?<= 'if' c ']'"). +Reserved Notation "x < y ?<= 'if' c :> T" (at level 70, y, c at next level, + format "x '[hv' < y '/' ?<= 'if' c :> T ']'"). + (* Reserved notation for lattice operations. *) Reserved Notation "A `&` B" (at level 48, left associativity). Reserved Notation "A `|` B" (at level 52, left associativity). @@ -461,6 +468,10 @@ Reserved Notation "x <=^d y ?= 'iff' c" (at level 70, y, c at next level, format "x '[hv' <=^d y '/' ?= 'iff' c ']'"). Reserved Notation "x <=^d y ?= 'iff' c :> T" (at level 70, y, c at next level, format "x '[hv' <=^d y '/' ?= 'iff' c :> T ']'"). +Reserved Notation "x <^d y ?<= 'if' c" (at level 70, y, c at next level, + format "x '[hv' <^d y '/' ?<= 'if' c ']'"). +Reserved Notation "x <^d y ?<= 'if' c :> T" (at level 70, y, c at next level, + format "x '[hv' <^d y '/' ?<= 'if' c :> T ']'"). (* Reserved notation for dual lattice operations. *) Reserved Notation "A `&^d` B" (at level 48, left associativity). @@ -1065,6 +1076,8 @@ Definition leif (x y : T) C : Prop := ((x <= y) * ((x == y) = C))%type. Definition le_of_leif x y C (le_xy : @leif x y C) := le_xy.1 : le x y. +Definition lteif x y C := if C then x <= y else x < y. + Variant le_xor_gt (x y : T) : T -> T -> T -> T -> bool -> bool -> Set := | LeNotGt of x <= y : le_xor_gt x y x x y y true false @@ -1105,7 +1118,7 @@ Definition arg_max {I : finType} := @extremum T I ge. End POrderDef. -Prenex Implicits lt le leif. +Prenex Implicits lt le leif lteif. Arguments ge {_ _}. Arguments gt {_ _}. Arguments min {_ _}. @@ -1119,6 +1132,7 @@ Notation ">=%O" := ge : fun_scope. Notation "<%O" := lt : fun_scope. Notation ">%O" := gt : fun_scope. Notation "=<%O" := comparable : fun_scope. Notation "><%O" := (fun x y => ~~ (comparable x y)) : fun_scope. @@ -1154,6 +1168,10 @@ Notation "x <= y ?= 'iff' C" := (leif x y C) : order_scope. Notation "x <= y ?= 'iff' C :> T" := ((x : T) <= (y : T) ?= iff C) (only parsing) : order_scope. +Notation "x < y ?<= 'if' C" := (lteif x y C) : order_scope. +Notation "x < y ?<= 'if' C :> T" := ((x : T) < (y : T) ?<= if C) + (only parsing) : order_scope. + Notation ">=< x" := (comparable x) : order_scope. Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope. Notation "x >=< y" := (comparable x y) : order_scope. @@ -2493,6 +2511,7 @@ Notation dual_comparable := (@comparable (dual_display _) _). Notation dual_ge := (@ge (dual_display _) _). Notation dual_gt := (@gt (dual_display _) _). Notation dual_leif := (@leif (dual_display _) _). +Notation dual_lteif := (@lteif (dual_display _) _). Notation dual_max := (@max (dual_display _) _). Notation dual_min := (@min (dual_display _) _). Notation dual_meet := (@meet (dual_display _) _). @@ -2508,6 +2527,7 @@ Notation ">=^d%O" := dual_ge : fun_scope. Notation "<^d%O" := dual_lt : fun_scope. Notation ">^d%O" := dual_gt : fun_scope. Notation "=<^d%O" := dual_comparable : fun_scope. Notation "><^d%O" := (fun x y => ~~ dual_comparable x y) : fun_scope. @@ -2543,6 +2563,10 @@ Notation "x <=^d y ?= 'iff' C" := ( T" := ((x : T) <=^d (y : T) ?= iff C) (only parsing) : order_scope. +Notation "x <^d y ?<= 'if' C" := ( T" := ((x : T) <^d (y : T) ?<= if C) + (only parsing) : order_scope. + Notation ">=<^d x" := (>=<^d%O x) : order_scope. Notation ">=<^d x :> T" := (>=<^d (x : T)) (only parsing) : order_scope. Notation "x >=<^d y" := (>=<^d%O x y) : order_scope. @@ -2808,6 +2832,8 @@ Proof. by case: comparableP. Qed. Lemma gt_comparable (x y : T) : y < x -> x >=< y. Proof. by case: comparableP. Qed. +(* leif *) + Lemma leifP x y C : reflect (x <= y ?= iff C) (if C then x == y else x < y). Proof. rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]]. @@ -2848,6 +2874,50 @@ Proof. by move=> /leifP; case: C comparableP => [] []. Qed. Lemma eqTleif x y C : x <= y ?= iff C -> C -> x = y. Proof. by move=> /eq_leif<-/eqP. Qed. +(* lteif *) + +Lemma lteif_trans x y z C1 C2 : + x < y ?<= if C1 -> y < z ?<= if C2 -> x < z ?<= if C1 && C2. +Proof. +case: C1 C2 => [][]; + [exact: le_trans | exact: le_lt_trans | exact: lt_le_trans | exact: lt_trans]. +Qed. + +Lemma lteif_anti C1 C2 x y : + (x < y ?<= if C1) && (y < x ?<= if C2) = C1 && C2 && (x == y). +Proof. by case: C1 C2 => [][]; rewrite lte_anti. Qed. + +Lemma lteifxx x C : (x < x ?<= if C) = C. +Proof. by case: C; rewrite /= ltexx. Qed. + +Lemma lteifNF x y C : y < x ?<= if ~~ C -> x < y ?<= if C = false. +Proof. by case: C => [/lt_geF|/le_gtF]. Qed. + +Lemma lteifS x y C : x < y -> x < y ?<= if C. +Proof. by case: C => //= /ltW. Qed. + +Lemma lteifT x y : x < y ?<= if true = (x <= y). Proof. by []. Qed. + +Lemma lteifF x y : x < y ?<= if false = (x < y). Proof. by []. Qed. + +Lemma lteif_orb x y : {morph lteif x y : p q / p || q}. +Proof. by case=> [][] /=; case: comparableP. Qed. + +Lemma lteif_andb x y : {morph lteif x y : p q / p && q}. +Proof. by case=> [][] /=; case: comparableP. Qed. + +Lemma lteif_imply C1 C2 x y : C1 ==> C2 -> x < y ?<= if C1 -> x < y ?<= if C2. +Proof. by case: C1 C2 => [][] //= _ /ltW. Qed. + +Lemma lteifW C x y : x < y ?<= if C -> x <= y. +Proof. by case: C => // /ltW. Qed. + +Lemma ltrW_lteif C x y : x < y -> x < y ?<= if C. +Proof. by case: C => // /ltW. Qed. + +Lemma lteifN C x y : x < y ?<= if ~~ C -> ~~ (y < x ?<= if C). +Proof. by case: C => /=; case: comparableP. Qed. + (* min and max *) Lemma minElt x y : min x y = if x < y then x else y. Proof. by []. Qed. @@ -2996,6 +3066,25 @@ Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. Lemma comparable_maxKx : min x (max x y) = x. Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. +Lemma comparable_lteifNE C : x >=< y -> x < y ?<= if ~~ C = ~~ (y < x ?<= if C). +Proof. by case: C => /=; case: comparableP. Qed. + +Lemma comparable_lteif_minr C : + (z < Order.min x y ?<= if C) = (z < x ?<= if C) && (z < y ?<= if C). +Proof. by case: C; rewrite /= (comparable_le_minr, comparable_lt_minr). Qed. + +Lemma comparable_lteif_minl C : + (Order.min x y < z ?<= if C) = (x < z ?<= if C) || (y < z ?<= if C). +Proof. by case: C; rewrite /= (comparable_le_minl, comparable_lt_minl). Qed. + +Lemma comparable_lteif_maxr C : + (z < Order.max x y ?<= if C) = (z < x ?<= if C) || (z < y ?<= if C). +Proof. by case: C; rewrite /= (comparable_le_maxr, comparable_lt_maxr). Qed. + +Lemma comparable_lteif_maxl C : + (Order.max x y < z ?<= if C) = (x < z ?<= if C) && (y < z ?<= if C). +Proof. by case: C; rewrite /= (comparable_le_maxl, comparable_lt_maxl). Qed. + End Comparable2. Section Comparable3. @@ -3799,6 +3888,27 @@ Definition lteIx := (leIx, ltIx). Definition ltexU := (lexU, ltxU). Definition lteUx := (@leUx _ T, ltUx). +(* lteif *) + +Lemma lteifNE x y C : x < y ?<= if ~~ C = ~~ (y < x ?<= if C). +Proof. by case: C => /=; case: leP. Qed. + +Lemma lteif_minr z x y C : + (z < Order.min x y ?<= if C) = (z < x ?<= if C) && (z < y ?<= if C). +Proof. by case: C; rewrite /= (le_minr, lt_minr). Qed. + +Lemma lteif_minl z x y C : + (Order.min x y < z ?<= if C) = (x < z ?<= if C) || (y < z ?<= if C). +Proof. by case: C; rewrite /= (le_minl, lt_minl). Qed. + +Lemma lteif_maxr z x y C : + (z < Order.max x y ?<= if C) = (z < x ?<= if C) || (z < y ?<= if C). +Proof. by case: C; rewrite /= (le_maxr, lt_maxr). Qed. + +Lemma lteif_maxl z x y C : + (Order.max x y < z ?<= if C) = (x < z ?<= if C) && (y < z ?<= if C). +Proof. by case: C; rewrite /= (le_maxl, lt_maxl). Qed. + Section ArgExtremum. Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0). -- cgit v1.2.3