Library mathcomp.algebra.interval
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
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 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 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 imply.
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.
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.
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.
Section IntervalEq.
Variable T : eqType.
Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
match b1, b2 with
| BSide a x, BSide b y ⇒ (a == b) && (x == y)
| BInfty a, BInfty b ⇒ a == b
| _, _ ⇒ false
end.
Lemma eq_itv_boundP : Equality.axiom eq_itv_bound.
Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
Canonical itv_bound_eqType := EqType (itv_bound T) itv_bound_eqMixin.
Definition eqitv (x y : interval T) : bool :=
let: Interval x x' := x in
let: Interval y y' := y in (x == y) && (x' == y').
Lemma eqitvP : Equality.axiom eqitv.
Canonical interval_eqMixin := EqMixin eqitvP.
Canonical interval_eqType := EqType (interval T) interval_eqMixin.
End IntervalEq.
Module IntervalChoice.
Section IntervalChoice.
Variable T : choiceType.
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 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_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_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)).
End Exports.
End IntervalChoice.
Export IntervalChoice.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.
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 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).
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 interval_porderMixin :=
LePOrderMixin (fun _ _ ⇒ erefl) subitv_refl subitv_anti subitv_trans.
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 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 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).
(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.
Section IntervalEq.
Variable T : eqType.
Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
match b1, b2 with
| BSide a x, BSide b y ⇒ (a == b) && (x == y)
| BInfty a, BInfty b ⇒ a == b
| _, _ ⇒ false
end.
Lemma eq_itv_boundP : Equality.axiom eq_itv_bound.
Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
Canonical itv_bound_eqType := EqType (itv_bound T) itv_bound_eqMixin.
Definition eqitv (x y : interval T) : bool :=
let: Interval x x' := x in
let: Interval y y' := y in (x == y) && (x' == y').
Lemma eqitvP : Equality.axiom eqitv.
Canonical interval_eqMixin := EqMixin eqitvP.
Canonical interval_eqType := EqType (interval T) interval_eqMixin.
End IntervalEq.
Module IntervalChoice.
Section IntervalChoice.
Variable T : choiceType.
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 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_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_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)).
End Exports.
End IntervalChoice.
Export IntervalChoice.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.
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 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).
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 interval_porderMixin :=
LePOrderMixin (fun _ _ ⇒ erefl) subitv_refl subitv_anti subitv_trans.
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 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 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).
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.
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).
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.
Lemma bound_lex1 b : b ≤ +oo.
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).
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).
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.
Lemma itv_le0x i : Interval +oo -oo ≤ i.
Lemma itv_lex1 i : i ≤ `]-oo, +oo[.
Canonical interval_bLatticeType :=
BLatticeType (interval T) (BottomMixin itv_le0x).
Canonical interval_tbLatticeType :=
TBLatticeType (interval T) (TopMixin itv_lex1).
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 (x y z : T) (i : interval T).
Lemma itv_bound_totalMixin : totalLatticeMixin [latticeType of itv_bound T].
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.
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 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].
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)]).
End IntervalNumDomain.
Section IntervalField.
Variable R : numFieldType.
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].
End IntervalField.
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.
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).
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.
Lemma bound_lex1 b : b ≤ +oo.
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).
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).
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.
Lemma itv_le0x i : Interval +oo -oo ≤ i.
Lemma itv_lex1 i : i ≤ `]-oo, +oo[.
Canonical interval_bLatticeType :=
BLatticeType (interval T) (BottomMixin itv_le0x).
Canonical interval_tbLatticeType :=
TBLatticeType (interval T) (TopMixin itv_lex1).
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 (x y z : T) (i : interval T).
Lemma itv_bound_totalMixin : totalLatticeMixin [latticeType of itv_bound T].
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.
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 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].
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)]).
End IntervalNumDomain.
Section IntervalField.
Variable R : numFieldType.
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].
End IntervalField.
Compatibility layer
Module mc_1_11.
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).
Lemma subr_lersif0r b (x y : R) : (0 ≤ y - x ?< if b) = (x ≤ y ?< if b).
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 lersif01 b : (0 : R) ≤ 1 ?< if b.
Lemma lersif_anti b1 b2 x y :
(x ≤ y ?< if b1) && (y ≤ x ?< if b2) =
if b1 || b2 then false else x == y.
Lemma lersifxx x b : (x ≤ x ?< if b) = ~~ b.
Lemma lersifNF x y b : y ≤ x ?< if ~~ b → x ≤ y ?< if b = false.
Lemma lersifS x y b : x < y → x ≤ y ?< if b.
Lemma lersifT x y : x ≤ y ?< if true = (x < y).
Lemma lersifF x y : x ≤ y ?< if false = (x ≤ y).
Lemma lersif_oppl b x y : - x ≤ y ?< if b = (- y ≤ x ?< if b).
Lemma lersif_oppr b x y : x ≤ - y ?< if b = (y ≤ - x ?< if b).
Lemma lersif_0oppr b x : 0 ≤ - x ?< if b = (x ≤ 0 ?< if b).
Lemma lersif_oppr0 b x : - x ≤ 0 ?< if b = (0 ≤ x ?< if b).
Lemma lersif_opp2 b : {mono (-%R : R → R) : x y /~ x ≤ y ?< if b}.
Definition lersif_oppE := (lersif_0oppr, lersif_oppr0, lersif_opp2).
Lemma lersif_add2l b x : {mono +%R x : y z / y ≤ z ?< if b}.
Lemma lersif_add2r b x : {mono +%R^~ x : y z / y ≤ z ?< if b}.
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).
Lemma lersif_subr_addr b x y z : (x ≤ y - z ?< if b) = (x + z ≤ y ?< if b).
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).
Lemma lersif_subr_addl b x y z : (x ≤ y - z ?< if b) = (z + x ≤ y ?< if b).
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}.
Lemma lersif_orb x y :
{morph (fun b ⇒ lersif x y b) : p q / p && q >-> p || q}.
Lemma lersif_imply b1 b2 (r1 r2 : R) :
b2 ==> b1 → r1 ≤ r2 ?< if b1 → r1 ≤ r2 ?< if b2.
Lemma lersifW b x y : x ≤ y ?< if b → x ≤ y.
Lemma ltrW_lersif b x y : x < y → x ≤ y ?< if b.
Lemma lersif_pmul2l b x : 0 < x → {mono *%R x : y z / y ≤ z ?< if b}.
Lemma lersif_pmul2r b x : 0 < x → {mono *%R^~ x : y z / y ≤ z ?< if b}.
Lemma lersif_nmul2l b x : x < 0 → {mono *%R x : y z /~ y ≤ z ?< if b}.
Lemma lersif_nmul2r b x : x < 0 → {mono *%R^~ x : y z /~ y ≤ z ?< if b}.
Lemma real_lersifN x y b : x \is Num.real → y \is Num.real →
x ≤ y ?< if ~~b = ~~ (y ≤ x ?< if b).
Lemma real_lersif_norml b x y :
x \is Num.real →
(`|x| ≤ y ?< if b) = ((- y ≤ x ?< if b) && (x ≤ y ?< if b)).
Lemma real_lersif_normr b x y :
y \is Num.real →
(x ≤ `|y| ?< if b) = ((x ≤ y ?< if b) || (x ≤ - y ?< if b)).
Lemma lersif_nnormr b x y : y ≤ 0 ?< if ~~ b → (`|x| ≤ y ?< if b) = false.
End LersifPo.
Section LersifOrdered.
Variable (R : realDomainType) (b : bool) (x y z e : R).
Lemma lersifN : (x ≤ y ?< if ~~ b) = ~~ (y ≤ x ?< if b).
Lemma lersif_norml :
(`|x| ≤ y ?< if b) = (- y ≤ x ?< if b) && (x ≤ y ?< if b).
Lemma lersif_normr :
(x ≤ `|y| ?< if b) = (x ≤ y ?< if b) || (x ≤ - y ?< if b).
Lemma lersif_distl :
(`|x - y| ≤ e ?< if b) = (y - e ≤ x ?< if b) && (x ≤ y + e ?< if b).
Lemma lersif_minr :
(x ≤ Num.min y z ?< if b) = (x ≤ y ?< if b) && (x ≤ z ?< if b).
Lemma lersif_minl :
(Num.min y z ≤ x ?< if b) = (y ≤ x ?< if b) || (z ≤ x ?< if b).
Lemma lersif_maxr :
(x ≤ Num.max y z ?< if b) = (x ≤ y ?< if b) || (x ≤ z ?< if b).
Lemma lersif_maxl :
(Num.max y z ≤ x ?< if b) = (y ≤ x ?< if b) && (z ≤ x ?< if b).
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).
Lemma lersif_pdivr_mulr : 0 < z → y / z ≤ x ?< if b = (y ≤ x × z ?< if b).
Lemma lersif_pdivl_mull : 0 < z → x ≤ z^-1 × y ?< if b = (z × x ≤ y ?< if b).
Lemma lersif_pdivr_mull : 0 < z → z^-1 × y ≤ x ?< if b = (y ≤ z × x ?< if b).
Lemma lersif_ndivl_mulr : z < 0 → x ≤ y / z ?< if b = (y ≤ x × z ?< if b).
Lemma lersif_ndivr_mulr : z < 0 → y / z ≤ x ?< if b = (x × z ≤ y ?< if b).
Lemma lersif_ndivl_mull : z < 0 → x ≤ z^-1 × y ?< if b = (y ≤z × x ?< if b).
Lemma lersif_ndivr_mull : z < 0 → z^-1 × y ≤ x ?< if b = (z × x ≤ y ?< if b).
End LersifField.
Section IntervalPo.
Variable R : numDomainType.
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.
Lemma itv_gte ba xa bb xb :
xb ≤ xa ?< if ba && ~~ bb → Interval (BSide ba xa) (BSide bb xb) =i pred0.
Lemma ltr_in_itv ba bb xa xb x :
~~ ba || bb → x \in Interval (BSide ba xa) (BSide bb xb) → xa < xb.
Lemma ler_in_itv ba bb xa xb x :
x \in Interval (BSide ba xa) (BSide bb xb) → xa ≤ xb.
End IntervalPo.
Lemma itv_splitU2 (R : realDomainType) (x : R) 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].
End mc_1_11.
Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a
qualified name.)
Notation "@ 'lersif'" :=
((fun _ (R : numDomainType) x y b ⇒ @Order.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_lteifNE))
(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 lteifNE))
(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
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).
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`.
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 _ (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 _ (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).
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).
((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 _ (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 _ (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).
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).