Library mathcomp.algebra.interval
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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.
Intervals in ordered types
This file provides 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 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 implies
lteBSide, bnd_simp == multirules to simplify inequalities between interval
bounds
miditv i == middle point of interval i
When using interval.v, the lemma `in_itv` is in practice very useful. For
example, the execution of the tactic `rewrite in_itv` w.r.t. an hypothesis
of the form x \in `]a, b[ into a < x < b.
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[
The substrings "oo", "oc", "co", "cc" in the names of lemmas respectively
stand for the intervals of the shape `]a, b[, `]a, b], `[a, b[, `[a, b].
The substrings "pinfty" and "ninfty" in the names of lemmas stand for
+oo and -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, these pathological issues do not arise when R is a
real domain: we could provide a specific theory for this important case.
References:
- Cyril Cohen, Assia Mahboubi, Formal proofs in real algebraic geometry:
- Cyril Cohen, Formalized algebraic numbers: construction and first-order
Set Implicit Arguments.
Local Open Scope order_scope.
Import Order.TTheory.
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.
Coercion pair_of_interval T (I : interval T) : itv_bound T × itv_bound T :=
let: Interval b1 b2 := I in (b1, b2).
We provide the 9 following notations to help writing formal intervals
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 (BRight a) (BRight b))
(at level 0, a, b at level 9 , format "`] a , b ]") : order_scope.
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 (BRight a) (BLeft b))
(at level 0, a, b at level 9 , format "`] a , b [") : order_scope.
Notation "`] '-oo' , b ]" := (Interval -oo (BRight b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : order_scope.
Notation "`] '-oo' , b [" := (Interval -oo (BLeft b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : order_scope.
Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo)
(at level 0, a at level 9 , format "`[ a , '+oo' [") : order_scope.
Notation "`] a , '+oo' [" := (Interval (BRight a) +oo)
(at level 0, a at level 9 , format "`] a , '+oo' [") : order_scope.
Notation "`] -oo , '+oo' [" := (Interval -oo +oo)
(at level 0, format "`] -oo , '+oo' [") : order_scope.
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 (BRight a) (BRight b))
(at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
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 (BRight a) (BLeft b))
(at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval -oo (BRight b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval -oo (BLeft b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo)
(at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BRight a) +oo)
(at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval -oo +oo)
(at level 0, format "`] -oo , '+oo' [") : ring_scope.
Fact itv_bound_display (disp : unit) : unit.
Fact interval_display (disp : unit) : unit.
Module IntervalCan.
Section IntervalCan.
Variable T : Type.
Lemma itv_bound_can :
cancel (fun b : itv_bound T ⇒
match b with BSide b x ⇒ (b, Some x) | BInfty b ⇒ (b, None) end)
(fun b ⇒
match b with (b, Some x) ⇒ BSide b x | (b, None) ⇒ BInfty _ b end).
Lemma interval_can :
@cancel _ (interval T)
(fun '(Interval b1 b2) ⇒ (b1, b2)) (fun '(b1, b2) ⇒ Interval b1 b2).
End IntervalCan.
#[export, hnf]
HB.instance Definition _ (T : eqType) := Equality.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : eqType) := Equality.copy (interval T)
(can_type (@interval_can T)).
#[export, hnf]
HB.instance Definition _ (T : choiceType) := Choice.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : choiceType) := Choice.copy (interval T)
(can_type (@interval_can T)).
#[export, hnf]
HB.instance Definition _ (T : countType) := Countable.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : countType) := Countable.copy (interval T)
(can_type (@interval_can T)).
#[export, hnf]
HB.instance Definition _ (T : finType) := Finite.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : finType) := Finite.copy (interval T)
(can_type (@interval_can T)).
Module Exports. End Exports.
End IntervalCan.
Export IntervalCan.Exports.
Section IntervalPOrder.
Variable (disp : unit) (T : porderType disp).
Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
Definition le_bound b1 b2 :=
match b1, b2 with
| -oo, _ | _, +oo ⇒ true
| BSide b1 x1, BSide b2 x2 ⇒ x1 < x2 ?<= if b2 ==> b1
| _, _ ⇒ false
end.
Definition lt_bound b1 b2 :=
match b1, b2 with
| -oo, +oo | -oo, BSide _ _ | BSide _ _, +oo ⇒ true
| BSide b1 x1, BSide b2 x2 ⇒ x1 < x2 ?<= if b1 && ~~ b2
| _, _ ⇒ false
end.
Lemma lt_bound_def b1 b2 : lt_bound b1 b2 = (b2 != b1) && le_bound b1 b2.
Lemma le_bound_refl : reflexive le_bound.
Lemma le_bound_anti : antisymmetric le_bound.
Lemma le_bound_trans : transitive le_bound.
Lemma bound_lexx c1 c2 x : (BSide c1 x ≤ BSide c2 x) = (c2 ==> c1).
Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2).
Lemma ge_pinfty b : (+oo ≤ b) = (b == +oo).
Lemma le_ninfty b : (b ≤ -oo) = (b == -oo).
Lemma gt_pinfty b : (+oo < b) = false.
Lemma lt_ninfty b : (b < -oo) = false.
Lemma ltBSide x y (b b' : bool) :
BSide b x < BSide b' y = (x < y ?<= if b && ~~ b').
Lemma leBSide x y (b b' : bool) :
BSide b x ≤ BSide b' y = (x < y ?<= if b' ==> b).
Definition lteBSide := (ltBSide, leBSide).
Lemma ltBRight_leBLeft b x : b < BRight x = (b ≤ BLeft x).
Lemma leBRight_ltBLeft b x : BRight x ≤ b = (BLeft x < b).
Let BLeft_ltE x y (b : bool) : BSide b x < BLeft y = (x < y).
Let BRight_leE x y (b : bool) : BSide b x ≤ BRight y = (x ≤ y).
Let BRight_BLeft_leE x y : BRight x ≤ BLeft y = (x < y).
Let BLeft_BRight_ltE x y : BLeft x < BRight y = (x ≤ y).
Let BRight_BSide_ltE x y (b : bool) : BRight x < BSide b y = (x < y).
Let BLeft_BSide_leE x y (b : bool) : BLeft x ≤ BSide b y = (x ≤ y).
Let BSide_ltE x y (b : bool) : BSide b x < BSide b y = (x < y).
Let BSide_leE x y (b : bool) : BSide b x ≤ BSide b y = (x ≤ y).
Let BInfty_leE a : a ≤ BInfty T false.
Let BInfty_geE a : BInfty T true ≤ a.
Let BInfty_le_eqE a : BInfty T false ≤ a = (a == BInfty T false).
Let BInfty_ge_eqE a : a ≤ BInfty T true = (a == BInfty T true).
Let BInfty_ltE a : a < BInfty T false = (a != BInfty T false).
Let BInfty_gtE a : BInfty T true < a = (a != BInfty T true).
Let BInfty_ltF a : BInfty T false < a = false.
Let BInfty_gtF a : a < BInfty T true = false.
Let BInfty_BInfty_ltE : BInfty T true < BInfty T false.
Definition bnd_simp := (BLeft_ltE, BRight_leE,
BRight_BLeft_leE, BLeft_BRight_ltE,
BRight_BSide_ltE, BLeft_BSide_leE, BSide_ltE, BSide_leE,
BInfty_leE, BInfty_geE, BInfty_BInfty_ltE,
BInfty_le_eqE, BInfty_ge_eqE, BInfty_ltE, BInfty_gtE, BInfty_ltF, BInfty_gtF,
@lexx _ T, @ltxx _ T, @eqxx T).
Definition subitv i1 i2 :=
let: Interval b1l b1r := i1 in
let: Interval b2l b2r := i2 in (b2l ≤ b1l) && (b1r ≤ b2r).
Lemma subitv_refl : reflexive subitv.
Lemma subitv_anti : antisymmetric subitv.
Lemma subitv_trans : transitive subitv.
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).
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.
Lemma itv_boundlr bl br x :
(x \in Interval bl br) = (bl ≤ BLeft x) && (BRight x ≤ br).
Lemma itv_splitI bl br x :
x \in Interval bl br = (x \in Interval bl +oo) && (x \in Interval -oo br).
Lemma subitvP i1 i2 : i1 ≤ i2 → {subset i1 ≤ i2}.
Lemma subset_itv (r s u v : bool) x y : r ≤ u → v ≤ s →
{subset Interval (BSide r x) (BSide s y) ≤ Interval (BSide u x) (BSide v y)}.
Lemma subset_itv_oo_cc x y : {subset `]x, y[ ≤ `[x, y]}.
Lemma subset_itv_oo_oc x y : {subset `]x, y[ ≤ `]x, y]}.
Lemma subset_itv_oo_co x y : {subset `]x, y[ ≤ `[x, y[}.
Lemma subset_itv_oc_cc x y : {subset `]x, y] ≤ `[x, y]}.
Lemma subset_itv_co_cc x y : {subset `[x, y[ ≤ `[x, y]}.
Lemma itvxx x : `[x, x] =i pred1 x.
Lemma itvxxP y x : reflect (y = x) (y \in `[x, x]).
Lemma subitvPl b1l b2l br :
b2l ≤ b1l → {subset Interval b1l br ≤ Interval b2l br}.
Lemma subitvPr bl b1r b2r :
b1r ≤ b2r → {subset Interval bl b1r ≤ Interval bl b2r}.
Lemma itv_xx x cl cr y :
y \in Interval (BSide cl x) (BSide cr x) = cl && ~~ cr && (y == x).
Lemma boundl_in_itv c x b : x \in Interval (BSide c x) b = c && (BRight x ≤ b).
Lemma boundr_in_itv c x b :
x \in Interval b (BSide c x) = ~~ c && (b ≤ BLeft x).
Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
Lemma lt_in_itv bl br x : x \in Interval bl br → bl < br.
Lemma lteif_in_itv cl cr yl yr x :
x \in Interval (BSide cl yl) (BSide cr yr) → yl < yr ?<= if cl && ~~ cr.
Lemma itv_ge b1 b2 : ~~ (b1 < b2) → Interval b1 b2 =i pred0.
Definition itv_decompose i x : Prop :=
let: Interval l u := i in
(match l return Prop with
| BSide b lb ⇒ lb < x ?<= if b
| BInfty b ⇒ b
end ×
match u return Prop with
| BSide b ub ⇒ x < ub ?<= if ~~ b
| BInfty b ⇒ ~~ b
end)%type.
Lemma itv_dec : ∀ x i, reflect (itv_decompose i x) (x \in i).
Arguments itv_dec {x i}.
(at level 0, a, b at level 9 , format "`[ a , b ]") : order_scope.
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 (BLeft a) (BLeft b))
(at level 0, a, b at level 9 , format "`[ a , b [") : order_scope.
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 -oo (BRight b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : order_scope.
Notation "`] '-oo' , b [" := (Interval -oo (BLeft b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : order_scope.
Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo)
(at level 0, a at level 9 , format "`[ a , '+oo' [") : order_scope.
Notation "`] a , '+oo' [" := (Interval (BRight a) +oo)
(at level 0, a at level 9 , format "`] a , '+oo' [") : order_scope.
Notation "`] -oo , '+oo' [" := (Interval -oo +oo)
(at level 0, format "`] -oo , '+oo' [") : order_scope.
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 (BRight a) (BRight b))
(at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
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 (BRight a) (BLeft b))
(at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval -oo (BRight b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval -oo (BLeft b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo)
(at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BRight a) +oo)
(at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval -oo +oo)
(at level 0, format "`] -oo , '+oo' [") : ring_scope.
Fact itv_bound_display (disp : unit) : unit.
Fact interval_display (disp : unit) : unit.
Module IntervalCan.
Section IntervalCan.
Variable T : Type.
Lemma itv_bound_can :
cancel (fun b : itv_bound T ⇒
match b with BSide b x ⇒ (b, Some x) | BInfty b ⇒ (b, None) end)
(fun b ⇒
match b with (b, Some x) ⇒ BSide b x | (b, None) ⇒ BInfty _ b end).
Lemma interval_can :
@cancel _ (interval T)
(fun '(Interval b1 b2) ⇒ (b1, b2)) (fun '(b1, b2) ⇒ Interval b1 b2).
End IntervalCan.
#[export, hnf]
HB.instance Definition _ (T : eqType) := Equality.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : eqType) := Equality.copy (interval T)
(can_type (@interval_can T)).
#[export, hnf]
HB.instance Definition _ (T : choiceType) := Choice.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : choiceType) := Choice.copy (interval T)
(can_type (@interval_can T)).
#[export, hnf]
HB.instance Definition _ (T : countType) := Countable.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : countType) := Countable.copy (interval T)
(can_type (@interval_can T)).
#[export, hnf]
HB.instance Definition _ (T : finType) := Finite.copy (itv_bound T)
(can_type (@itv_bound_can T)).
#[export, hnf]
HB.instance Definition _ (T : finType) := Finite.copy (interval T)
(can_type (@interval_can T)).
Module Exports. End Exports.
End IntervalCan.
Export IntervalCan.Exports.
Section IntervalPOrder.
Variable (disp : unit) (T : porderType disp).
Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
Definition le_bound b1 b2 :=
match b1, b2 with
| -oo, _ | _, +oo ⇒ true
| BSide b1 x1, BSide b2 x2 ⇒ x1 < x2 ?<= if b2 ==> b1
| _, _ ⇒ false
end.
Definition lt_bound b1 b2 :=
match b1, b2 with
| -oo, +oo | -oo, BSide _ _ | BSide _ _, +oo ⇒ true
| BSide b1 x1, BSide b2 x2 ⇒ x1 < x2 ?<= if b1 && ~~ b2
| _, _ ⇒ false
end.
Lemma lt_bound_def b1 b2 : lt_bound b1 b2 = (b2 != b1) && le_bound b1 b2.
Lemma le_bound_refl : reflexive le_bound.
Lemma le_bound_anti : antisymmetric le_bound.
Lemma le_bound_trans : transitive le_bound.
Lemma bound_lexx c1 c2 x : (BSide c1 x ≤ BSide c2 x) = (c2 ==> c1).
Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2).
Lemma ge_pinfty b : (+oo ≤ b) = (b == +oo).
Lemma le_ninfty b : (b ≤ -oo) = (b == -oo).
Lemma gt_pinfty b : (+oo < b) = false.
Lemma lt_ninfty b : (b < -oo) = false.
Lemma ltBSide x y (b b' : bool) :
BSide b x < BSide b' y = (x < y ?<= if b && ~~ b').
Lemma leBSide x y (b b' : bool) :
BSide b x ≤ BSide b' y = (x < y ?<= if b' ==> b).
Definition lteBSide := (ltBSide, leBSide).
Lemma ltBRight_leBLeft b x : b < BRight x = (b ≤ BLeft x).
Lemma leBRight_ltBLeft b x : BRight x ≤ b = (BLeft x < b).
Let BLeft_ltE x y (b : bool) : BSide b x < BLeft y = (x < y).
Let BRight_leE x y (b : bool) : BSide b x ≤ BRight y = (x ≤ y).
Let BRight_BLeft_leE x y : BRight x ≤ BLeft y = (x < y).
Let BLeft_BRight_ltE x y : BLeft x < BRight y = (x ≤ y).
Let BRight_BSide_ltE x y (b : bool) : BRight x < BSide b y = (x < y).
Let BLeft_BSide_leE x y (b : bool) : BLeft x ≤ BSide b y = (x ≤ y).
Let BSide_ltE x y (b : bool) : BSide b x < BSide b y = (x < y).
Let BSide_leE x y (b : bool) : BSide b x ≤ BSide b y = (x ≤ y).
Let BInfty_leE a : a ≤ BInfty T false.
Let BInfty_geE a : BInfty T true ≤ a.
Let BInfty_le_eqE a : BInfty T false ≤ a = (a == BInfty T false).
Let BInfty_ge_eqE a : a ≤ BInfty T true = (a == BInfty T true).
Let BInfty_ltE a : a < BInfty T false = (a != BInfty T false).
Let BInfty_gtE a : BInfty T true < a = (a != BInfty T true).
Let BInfty_ltF a : BInfty T false < a = false.
Let BInfty_gtF a : a < BInfty T true = false.
Let BInfty_BInfty_ltE : BInfty T true < BInfty T false.
Definition bnd_simp := (BLeft_ltE, BRight_leE,
BRight_BLeft_leE, BLeft_BRight_ltE,
BRight_BSide_ltE, BLeft_BSide_leE, BSide_ltE, BSide_leE,
BInfty_leE, BInfty_geE, BInfty_BInfty_ltE,
BInfty_le_eqE, BInfty_ge_eqE, BInfty_ltE, BInfty_gtE, BInfty_ltF, BInfty_gtF,
@lexx _ T, @ltxx _ T, @eqxx T).
Definition subitv i1 i2 :=
let: Interval b1l b1r := i1 in
let: Interval b2l b2r := i2 in (b2l ≤ b1l) && (b1r ≤ b2r).
Lemma subitv_refl : reflexive subitv.
Lemma subitv_anti : antisymmetric subitv.
Lemma subitv_trans : transitive subitv.
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).
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.
Lemma itv_boundlr bl br x :
(x \in Interval bl br) = (bl ≤ BLeft x) && (BRight x ≤ br).
Lemma itv_splitI bl br x :
x \in Interval bl br = (x \in Interval bl +oo) && (x \in Interval -oo br).
Lemma subitvP i1 i2 : i1 ≤ i2 → {subset i1 ≤ i2}.
Lemma subset_itv (r s u v : bool) x y : r ≤ u → v ≤ s →
{subset Interval (BSide r x) (BSide s y) ≤ Interval (BSide u x) (BSide v y)}.
Lemma subset_itv_oo_cc x y : {subset `]x, y[ ≤ `[x, y]}.
Lemma subset_itv_oo_oc x y : {subset `]x, y[ ≤ `]x, y]}.
Lemma subset_itv_oo_co x y : {subset `]x, y[ ≤ `[x, y[}.
Lemma subset_itv_oc_cc x y : {subset `]x, y] ≤ `[x, y]}.
Lemma subset_itv_co_cc x y : {subset `[x, y[ ≤ `[x, y]}.
Lemma itvxx x : `[x, x] =i pred1 x.
Lemma itvxxP y x : reflect (y = x) (y \in `[x, x]).
Lemma subitvPl b1l b2l br :
b2l ≤ b1l → {subset Interval b1l br ≤ Interval b2l br}.
Lemma subitvPr bl b1r b2r :
b1r ≤ b2r → {subset Interval bl b1r ≤ Interval bl b2r}.
Lemma itv_xx x cl cr y :
y \in Interval (BSide cl x) (BSide cr x) = cl && ~~ cr && (y == x).
Lemma boundl_in_itv c x b : x \in Interval (BSide c x) b = c && (BRight x ≤ b).
Lemma boundr_in_itv c x b :
x \in Interval b (BSide c x) = ~~ c && (b ≤ BLeft x).
Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
Lemma lt_in_itv bl br x : x \in Interval bl br → bl < br.
Lemma lteif_in_itv cl cr yl yr x :
x \in Interval (BSide cl yl) (BSide cr yr) → yl < yr ?<= if cl && ~~ cr.
Lemma itv_ge b1 b2 : ~~ (b1 < b2) → Interval b1 b2 =i pred0.
Definition itv_decompose i x : Prop :=
let: Interval l u := i in
(match l return Prop with
| BSide b lb ⇒ lb < x ?<= if b
| BInfty b ⇒ b
end ×
match u return Prop with
| BSide b ub ⇒ x < ub ?<= if ~~ b
| BInfty b ⇒ ~~ b
end)%type.
Lemma itv_dec : ∀ x i, reflect (itv_decompose i x) (x \in i).
Arguments itv_dec {x i}.
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 ⇒ ∀ x : T, x == x
| +oo ⇒ ∀ 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 ⇒ ∀ x : T, x == x
| -oo ⇒ ∀ b : bool, unkeyed b = false
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])
| _, _ ⇒ ∀ x : T, x == x
end)%type.
Lemma itvP x i : x \in i → itv_rewrite i x.
Arguments itvP [x i].
Lemma itv_splitU1 b x : b ≤ BLeft x →
Interval b (BRight x) =i [predU1 x & Interval b (BLeft x)].
Lemma itv_split1U b x : BRight x ≤ b →
Interval (BLeft x) b =i [predU1 x & Interval (BRight x) b].
End IntervalPOrder.
Section IntervalLattice.
Variable (disp : unit) (T : latticeType disp).
Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
Definition bound_meet bl br : itv_bound T :=
match bl, br with
| -oo, _ | _, -oo ⇒ -oo
| +oo, b | b, +oo ⇒ b
| 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
| BSide xb x, BSide yb y ⇒
BSide ((~~ (x ≤ y) || yb) && (~~ (y ≤ x) || xb)) (x `|` y)
end.
Lemma bound_meetC : commutative bound_meet.
Lemma bound_joinC : commutative bound_join.
Lemma bound_meetA : associative bound_meet.
Lemma bound_joinA : associative bound_join.
Lemma bound_meetKU b2 b1 : bound_join b1 (bound_meet b1 b2) = b1.
Lemma bound_joinKI b2 b1 : bound_meet b1 (bound_join b1 b2) = b1.
Lemma bound_leEmeet b1 b2 : (b1 ≤ b2) = (bound_meet b1 b2 == b1).
Lemma bound_le0x b : -oo ≤ b.
Lemma bound_lex1 b : b ≤ +oo.
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.
Lemma itv_joinC : commutative itv_join.
Lemma itv_meetA : associative itv_meet.
Lemma itv_joinA : associative itv_join.
Lemma itv_meetKU i2 i1 : itv_join i1 (itv_meet i1 i2) = i1.
Lemma itv_joinKI i2 i1 : itv_meet i1 (itv_join i1 i2) = i1.
Lemma itv_leEmeet i1 i2 : (i1 ≤ i2) = (itv_meet i1 i2 == i1).
Lemma itv_le0x i : Interval +oo -oo ≤ i.
Lemma itv_lex1 i : i ≤ `]-oo, +oo[.
Lemma in_itvI x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2).
End IntervalLattice.
Section IntervalTotal.
Variable (disp : unit) (T : orderType disp).
Implicit Types (a b c : itv_bound T) (x y z : T) (i : interval T).
Lemma itv_bound_total : total (<=%O : rel (itv_bound T)).
Lemma itv_meetUl : @left_distributive (interval T) _ Order.meet Order.join.
Lemma itv_splitU c a b : a ≤ c ≤ b →
∀ y, y \in Interval a b = (y \in Interval a c) || (y \in Interval c b).
Lemma itv_splitUeq x a b : x \in Interval a b →
∀ y, y \in Interval a b =
[|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b].
Lemma itv_total_meet3E i1 i2 i3 :
i1 `&` i2 `&` i3 \in [:: i1 `&` i2; i1 `&` i3; i2 `&` i3].
Lemma itv_total_join3E i1 i2 i3 :
i1 `|` i2 `|` i3 \in [:: i1 `|` i2; i1 `|` i3; i2 `|` i3].
Lemma predC_itvl a : [predC Interval -oo a] =i Interval a +oo.
Lemma predC_itvr a : [predC Interval a +oo] =i Interval -oo a.
Lemma predC_itv i : [predC i] =i [predU Interval -oo i.1 & Interval i.2 +oo].
End IntervalTotal.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.
Section IntervalNumDomain.
Variable R : numDomainType.
Implicit Types x : R.
Lemma mem0_itvcc_xNx x : (0 \in `[- x, x]) = (0 ≤ x).
Lemma mem0_itvoo_xNx x : 0 \in `](- x), x[ = (0 < x).
Lemma oppr_itv ba bb (xa xb x : R) :
(- x \in Interval (BSide ba xa) (BSide bb xb)) =
(x \in Interval (BSide (~~ bb) (- xb)) (BSide (~~ ba) (- xa))).
Lemma oppr_itvoo (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)]).
Lemma oppr_itvoc (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)]).
Definition miditv (R : numDomainType) (i : interval R) : R :=
match i with
| Interval (BSide _ a) (BSide _ b) ⇒ (a + b) / 2%:R
| Interval -oo%O (BSide _ b) ⇒ b - 1
| Interval (BSide _ a) +oo%O ⇒ a + 1
| Interval -oo%O +oo%O ⇒ 0
| _ ⇒ 0
end.
End IntervalNumDomain.
Section IntervalField.
Variable R : numFieldType.
Implicit Types (x y z : R) (i : interval R).
Local Notation mid x y := ((x + y) / 2).
Lemma mid_in_itv : ∀ ba bb (xa xb : R), xa < xb ?<= if ba && ~~ bb →
mid xa xb \in Interval (BSide ba xa) (BSide bb xb).
Lemma mid_in_itvoo : ∀ (xa xb : R), xa < xb → mid xa xb \in `]xa, xb[.
Lemma mid_in_itvcc : ∀ (xa xb : R), xa ≤ xb → mid xa xb \in `[xa, xb].
Lemma mem_miditv i : (i.1 < i.2)%O → miditv i \in i.
Lemma miditv_le_left i b : (i.1 < i.2)%O → (BSide b (miditv i) ≤ i.2)%O.
Lemma miditv_ge_right i b : (i.1 < i.2)%O → (i.1 ≤ BSide b (miditv i))%O.
Lemma in_segmentDgt0Pr x y z :
reflect (∀ e, e > 0 → y \in `[x - e, z + e]) (y \in `[x, z]).
Lemma in_segmentDgt0Pl x y z :
reflect (∀ e, e > 0 → y \in `[(- e + x), (e + z)]) (y \in `[x, z]).
End IntervalField.
#[deprecated(since="mathcomp 1.17.0", note="Use in_segmentDgt0Pr instead.")]
Notation in_segment_addgt0Pr := in_segmentDgt0Pr.
#[deprecated(since="mathcomp 1.17.0", note="Use in_segmentDgt0Pl instead.")]
Notation in_segment_addgt0Pl := in_segmentDgt0Pl.
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 ⇒ ∀ x : T, x == x
| +oo ⇒ ∀ 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 ⇒ ∀ x : T, x == x
| -oo ⇒ ∀ b : bool, unkeyed b = false
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])
| _, _ ⇒ ∀ x : T, x == x
end)%type.
Lemma itvP x i : x \in i → itv_rewrite i x.
Arguments itvP [x i].
Lemma itv_splitU1 b x : b ≤ BLeft x →
Interval b (BRight x) =i [predU1 x & Interval b (BLeft x)].
Lemma itv_split1U b x : BRight x ≤ b →
Interval (BLeft x) b =i [predU1 x & Interval (BRight x) b].
End IntervalPOrder.
Section IntervalLattice.
Variable (disp : unit) (T : latticeType disp).
Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
Definition bound_meet bl br : itv_bound T :=
match bl, br with
| -oo, _ | _, -oo ⇒ -oo
| +oo, b | b, +oo ⇒ b
| 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
| BSide xb x, BSide yb y ⇒
BSide ((~~ (x ≤ y) || yb) && (~~ (y ≤ x) || xb)) (x `|` y)
end.
Lemma bound_meetC : commutative bound_meet.
Lemma bound_joinC : commutative bound_join.
Lemma bound_meetA : associative bound_meet.
Lemma bound_joinA : associative bound_join.
Lemma bound_meetKU b2 b1 : bound_join b1 (bound_meet b1 b2) = b1.
Lemma bound_joinKI b2 b1 : bound_meet b1 (bound_join b1 b2) = b1.
Lemma bound_leEmeet b1 b2 : (b1 ≤ b2) = (bound_meet b1 b2 == b1).
Lemma bound_le0x b : -oo ≤ b.
Lemma bound_lex1 b : b ≤ +oo.
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.
Lemma itv_joinC : commutative itv_join.
Lemma itv_meetA : associative itv_meet.
Lemma itv_joinA : associative itv_join.
Lemma itv_meetKU i2 i1 : itv_join i1 (itv_meet i1 i2) = i1.
Lemma itv_joinKI i2 i1 : itv_meet i1 (itv_join i1 i2) = i1.
Lemma itv_leEmeet i1 i2 : (i1 ≤ i2) = (itv_meet i1 i2 == i1).
Lemma itv_le0x i : Interval +oo -oo ≤ i.
Lemma itv_lex1 i : i ≤ `]-oo, +oo[.
Lemma in_itvI x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2).
End IntervalLattice.
Section IntervalTotal.
Variable (disp : unit) (T : orderType disp).
Implicit Types (a b c : itv_bound T) (x y z : T) (i : interval T).
Lemma itv_bound_total : total (<=%O : rel (itv_bound T)).
Lemma itv_meetUl : @left_distributive (interval T) _ Order.meet Order.join.
Lemma itv_splitU c a b : a ≤ c ≤ b →
∀ y, y \in Interval a b = (y \in Interval a c) || (y \in Interval c b).
Lemma itv_splitUeq x a b : x \in Interval a b →
∀ y, y \in Interval a b =
[|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b].
Lemma itv_total_meet3E i1 i2 i3 :
i1 `&` i2 `&` i3 \in [:: i1 `&` i2; i1 `&` i3; i2 `&` i3].
Lemma itv_total_join3E i1 i2 i3 :
i1 `|` i2 `|` i3 \in [:: i1 `|` i2; i1 `|` i3; i2 `|` i3].
Lemma predC_itvl a : [predC Interval -oo a] =i Interval a +oo.
Lemma predC_itvr a : [predC Interval a +oo] =i Interval -oo a.
Lemma predC_itv i : [predC i] =i [predU Interval -oo i.1 & Interval i.2 +oo].
End IntervalTotal.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.
Section IntervalNumDomain.
Variable R : numDomainType.
Implicit Types x : R.
Lemma mem0_itvcc_xNx x : (0 \in `[- x, x]) = (0 ≤ x).
Lemma mem0_itvoo_xNx x : 0 \in `](- x), x[ = (0 < x).
Lemma oppr_itv ba bb (xa xb x : R) :
(- x \in Interval (BSide ba xa) (BSide bb xb)) =
(x \in Interval (BSide (~~ bb) (- xb)) (BSide (~~ ba) (- xa))).
Lemma oppr_itvoo (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)]).
Lemma oppr_itvoc (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)]).
Definition miditv (R : numDomainType) (i : interval R) : R :=
match i with
| Interval (BSide _ a) (BSide _ b) ⇒ (a + b) / 2%:R
| Interval -oo%O (BSide _ b) ⇒ b - 1
| Interval (BSide _ a) +oo%O ⇒ a + 1
| Interval -oo%O +oo%O ⇒ 0
| _ ⇒ 0
end.
End IntervalNumDomain.
Section IntervalField.
Variable R : numFieldType.
Implicit Types (x y z : R) (i : interval R).
Local Notation mid x y := ((x + y) / 2).
Lemma mid_in_itv : ∀ ba bb (xa xb : R), xa < xb ?<= if ba && ~~ bb →
mid xa xb \in Interval (BSide ba xa) (BSide bb xb).
Lemma mid_in_itvoo : ∀ (xa xb : R), xa < xb → mid xa xb \in `]xa, xb[.
Lemma mid_in_itvcc : ∀ (xa xb : R), xa ≤ xb → mid xa xb \in `[xa, xb].
Lemma mem_miditv i : (i.1 < i.2)%O → miditv i \in i.
Lemma miditv_le_left i b : (i.1 < i.2)%O → (BSide b (miditv i) ≤ i.2)%O.
Lemma miditv_ge_right i b : (i.1 < i.2)%O → (i.1 ≤ BSide b (miditv i))%O.
Lemma in_segmentDgt0Pr x y z :
reflect (∀ e, e > 0 → y \in `[x - e, z + e]) (y \in `[x, z]).
Lemma in_segmentDgt0Pl x y z :
reflect (∀ e, e > 0 → y \in `[(- e + x), (e + z)]) (y \in `[x, z]).
End IntervalField.
#[deprecated(since="mathcomp 1.17.0", note="Use in_segmentDgt0Pr instead.")]
Notation in_segment_addgt0Pr := in_segmentDgt0Pr.
#[deprecated(since="mathcomp 1.17.0", note="Use in_segmentDgt0Pl instead.")]
Notation in_segment_addgt0Pl := in_segmentDgt0Pl.