Library mathcomp.analysis.itv
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
From mathcomp Require Import interval mathcomp_extra.
From mathcomp.classical Require Import boolp.
Require Import signed.
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
From mathcomp Require Import interval mathcomp_extra.
From mathcomp.classical Require Import boolp.
Require Import signed.
This file develops tools to make the manipulation of numbers within
a known interval easier, thanks to canonical structures. This adds types
like {itv R & ` [a, b]}, a notation e%:itv that infers an enclosing
interval for expression e according to existing canonical instances and
%:inum to cast back from type {itv R & i} to R.
For instance, x : {i01 R}, we have (1 - x%:inum)%:itv : {i01 R}
automatically inferred.
types for values within known interval
{i01 R} == interface type for elements in R that live in ` [0, 1]; R must have a numDomainType structure. Allows to solve automatically goals of the form x >= 0 and x <= 1 if x is canonically a {i01 R}. {i01 R} is canonically stable by common operations. {itv R & i} == more generic type of values in interval i : interval int R must have a numDomainType structure. This type is shown to be a porderType.casts from/to values within known interval
x%:itv == explicitly casts x to the most precise known {itv R & i} according to existing canonical instances. x%:i01 == explicitly casts x to {i01 R} according to existing canonical instances. x%:inum == explicit cast from {itv R & i} to R.sign proofs
[itv of x] == proof that x is in interval inferred by x%:itv [lb of x] == proof that lb < x or lb <= x with lb the lower bound inferred by x%:itv [ub of x] == proof that x < ub or x <= ub with ub the upper bound inferred by x%:itv [lbe of x] == proof that lb <= x [ube of x] == proof that x <= ubconstructors
ItvNum xin == builds a {itv R & i} from a proof xin : x \in i where x : R --> A number of canonical instances are provided for common operations, if your favorite operator is missing, look below for examples on how to add the appropriate Canonical. > Canonical instances are also provided according to types, as a fallback when no known operator appears in the expression. Look to itv_top_typ below for an example on how to add your favorite type.Reserved Notation "{ 'itv' R & i }"
(at level 0, R at level 200, i at level 200, format "{ 'itv' R & i }").
Reserved Notation "{ 'i01' R }"
(at level 0, R at level 200, format "{ 'i01' R }").
Reserved Notation "x %:itv" (at level 2, format "x %:itv").
Reserved Notation "x %:i01" (at level 2, format "x %:i01").
Reserved Notation "x %:inum" (at level 2, format "x %:inum").
Reserved Notation "[ 'itv' 'of' x ]" (format "[ 'itv' 'of' x ]").
Reserved Notation "[ 'lb' 'of' x ]" (format "[ 'lb' 'of' x ]").
Reserved Notation "[ 'ub' 'of' x ]" (format "[ 'ub' 'of' x ]").
Reserved Notation "[ 'lbe' 'of' x ]" (format "[ 'lbe' 'of' x ]").
Reserved Notation "[ 'ube' 'of' x ]" (format "[ 'ube' 'of' x ]").
Set Implicit Arguments.
Import Order.TTheory Order.Syntax.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Local Open Scope order_scope.
Definition wider_itv (x y : interval int) := subitv y x.
Module Itv.
Section Itv.
Context (R : numDomainType).
Definition map_itv_bound S T (f : S → T) (b : itv_bound S) : itv_bound T :=
match b with
| BSide b x ⇒ BSide b (f x)
| BInfty b ⇒ BInfty _ b
end.
Definition map_itv S T (f : S → T) (i : interval S) : interval T :=
let 'Interval l u := i in Interval (map_itv_bound f l) (map_itv_bound f u).
Lemma le_map_itv_bound (x y : itv_bound int) :
x ≤ y →
map_itv_bound (fun x ⇒ x%:~R : R) x ≤ map_itv_bound (fun x ⇒ x%:~R : R) y.
Lemma subitv_map_itv (x y : interval int) :
x ≤ y →
map_itv (fun x ⇒ x%:~R : R) x ≤ map_itv (fun x ⇒ x%:~R : R) y.
Definition itv_cond (i : interval int) (x : R) :=
x \in map_itv (fun x ⇒ x%:~R : R) i.
Record def (i : interval int) := Def {
r :> R;
#[canonical=no]
P : itv_cond i r
}.
End Itv.
Notation spec i x := (itv_cond i%Z%R x).
Record typ := Typ {
sort : numDomainType;
#[canonical=no]
sort_itv : interval int;
#[canonical=no]
allP : ∀ x : sort, spec sort_itv x
}.
Definition mk {R} i r P : @def R i :=
@Def R i r P.
Definition from {R i}
{x : @def R i} (phx : phantom R x) := x.
Definition fromP {R i}
{x : @def R i} (phx : phantom R x) := P x.
Module Exports.
Notation "{ 'itv' R & i }" := (def R i%Z) : type_scope.
Notation "{ 'i01' R }" := (def R `[Posz 0, Posz 1]) : type_scope.
Notation "x %:itv" := (from (Phantom _ x)) : ring_scope.
Notation "[ 'itv' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope.
Notation inum := r.
Notation "x %:inum" := (r x) : ring_scope.
Arguments r {R i}.
End Exports.
End Itv.
Export Itv.Exports.
Section POrder.
Variables (R : numDomainType) (i : interval int).
Canonical itv_subType := [subType for @Itv.r R i].
Definition itv_eqMixin := [eqMixin of nR by <:].
Canonical itv_eqType := EqType nR itv_eqMixin.
Definition itv_choiceMixin := [choiceMixin of nR by <:].
Canonical itv_choiceType := ChoiceType nR itv_choiceMixin.
Definition itv_porderMixin := [porderMixin of nR by <:].
Canonical itv_porderType := POrderType ring_display nR itv_porderMixin.
End POrder.
TODO: numDomainType on sT ?
Lemma itv_top_typ_subproof (R : numDomainType) (x : R) :
Itv.spec `]-oo, +oo[ x.
Canonical itv_top_typ (R : numDomainType) := Itv.Typ (@itv_top_typ_subproof R).
Lemma typ_inum_subproof (xt : Itv.typ) (x : Itv.sort xt) :
Itv.spec (Itv.sort_itv xt) x.
This adds _ <- Itv.r ( typ_inum )
to canonical projections (c.f., Print Canonical Projections
Itv.r) meaning that if no other canonical instance (with a
registered head symbol) is found, a canonical instance of
Itv.typ, like the ones above, will be looked for.
Canonical typ_inum (xt : Itv.typ) (x : Itv.sort xt) :=
Itv.mk (typ_inum_subproof x).
Notation unify_itv ix iy := (unify wider_itv ix iy).
Section Theory.
Context {R : numDomainType} {i : interval int}.
Implicit Type x : sT.
Lemma itv_intro {x} : x%:inum = x%:inum :> R.
Definition empty_itv := `[Posz 1, Posz 0].
Lemma itv_bottom x : unify_itv empty_itv i → False.
Lemma itv_gt0 x : unify_itv `]Posz 0, +oo[ i → 0%R < x%:inum :> R.
Lemma itv_le0F x : unify_itv `]Posz 0, +oo[ i → x%:inum ≤ 0%R :> R = false.
Lemma itv_lt0 x : unify_itv `]-oo, Posz 0[ i → x%:inum < 0%R :> R.
Lemma itv_ge0F x : unify_itv `]-oo, Posz 0[ i → 0%R ≤ x%:inum :> R = false.
Lemma itv_ge0 x : unify_itv `[Posz 0, +oo[ i → 0%R ≤ x%:inum :> R.
Lemma itv_lt0F x : unify_itv `[Posz 0, +oo[ i → x%:inum < 0%R :> R = false.
Lemma itv_le0 x : unify_itv `]-oo, Posz 0] i → x%:inum ≤ 0%R :> R.
Lemma itv_gt0F x : unify_itv `]-oo, Posz 0] i → 0%R < x%:inum :> R = false.
Lemma lt1 x : unify_itv `]-oo, Posz 1[ i → x%:inum < 1%R :> R.
Lemma ge1F x : unify_itv `]-oo, Posz 1[ i → 1%R ≤ x%:inum :> R = false.
Lemma le1 x : unify_itv `]-oo, Posz 1] i → x%:inum ≤ 1%R :> R.
Lemma gt1F x : unify_itv `]-oo, Posz 1] i → 1%R < x%:inum :> R = false.
Lemma widen_itv_subproof x i' : unify_itv i' i → Itv.spec i' x%:inum.
Definition widen_itv x i' (uni : unify_itv i' i) :=
Itv.mk (widen_itv_subproof x uni).
Lemma widen_itvE x (uni : unify_itv i i) : @widen_itv x i uni = x.
End Theory.
Arguments itv_bottom {R i} _ {_}.
Arguments itv_gt0 {R i} _ {_}.
Arguments itv_le0F {R i} _ {_}.
Arguments itv_lt0 {R i} _ {_}.
Arguments itv_ge0F {R i} _ {_}.
Arguments itv_ge0 {R i} _ {_}.
Arguments itv_lt0F {R i} _ {_}.
Arguments itv_le0 {R i} _ {_}.
Arguments itv_gt0F {R i} _ {_}.
Arguments lt1 {R i} _ {_}.
Arguments ge1F {R i} _ {_}.
Arguments le1 {R i} _ {_}.
Arguments gt1F {R i} _ {_}.
Arguments widen_itv {R i} _ {_ _}.
Arguments widen_itvE {R i} _ {_}.
#[global] Hint Extern 0 (is_true (0%R < _)%O) ⇒ solve [apply: itv_gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%R)%O) ⇒ solve [apply: itv_lt0] : core.
#[global] Hint Extern 0 (is_true (0%R ≤ _)%O) ⇒ solve [apply: itv_ge0] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 0%R)%O) ⇒ solve [apply: itv_le0] : core.
#[global] Hint Extern 0 (is_true (_ < 1%R)%O) ⇒ solve [apply: lt1] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 1%R)%O) ⇒ solve [apply: le1] : core.
Notation "x %:i01" := (widen_itv x%:itv : {i01 _}) (only parsing) : ring_scope.
Notation "x %:i01" := (@widen_itv _ _
(@Itv.from _ _ _ (Phantom _ x)) `[Posz 0, Posz 1] _)
(only printing) : ring_scope.
Local Open Scope ring_scope.
Section NumDomainStability.
Context {R : numDomainType}.
Lemma zero_inum_subproof : Itv.spec `[0, 0] (0 : R).
Canonical zero_inum := Itv.mk zero_inum_subproof.
Lemma one_inum_subproof : Itv.spec `[1, 1] (1 : R).
Canonical one_inum := Itv.mk one_inum_subproof.
Definition opp_itv_bound_subdef (b : itv_bound int) : itv_bound int :=
match b with
| BSide b x ⇒ BSide (~~ b) (intZmod.oppz x)
| BInfty b ⇒ BInfty _ (~~ b)
end.
Arguments opp_itv_bound_subdef /.
Lemma opp_itv_ge0_subproof b :
(BLeft 0%R ≤ opp_itv_bound_subdef b)%O = (b ≤ BRight 0%R)%O.
Lemma opp_itv_gt0_subproof b :
(BLeft 0%R < opp_itv_bound_subdef b)%O = (b < BRight 0%R)%O.
Lemma opp_itv_boundr_subproof (x : R) b :
(BRight (- x)%R ≤ Itv.map_itv_bound intr (opp_itv_bound_subdef b))%O
= (Itv.map_itv_bound intr b ≤ BLeft x)%O.
Lemma opp_itv_le0_subproof b :
(opp_itv_bound_subdef b ≤ BRight 0%R)%O = (BLeft 0%R ≤ b)%O.
Lemma opp_itv_lt0_subproof b :
(opp_itv_bound_subdef b < BRight 0%R)%O = (BLeft 0%R < b)%O.
Lemma opp_itv_boundl_subproof (x : R) b :
(Itv.map_itv_bound intr (opp_itv_bound_subdef b) ≤ BLeft (- x)%R)%O
= (BRight x ≤ Itv.map_itv_bound intr b)%O.
Definition opp_itv_subdef (i : interval int) : interval int :=
let 'Interval l u := i in
Interval (opp_itv_bound_subdef u) (opp_itv_bound_subdef l).
Arguments opp_itv_subdef /.
Lemma opp_inum_subproof (i : interval int)
(x : {itv R & i}) (r := opp_itv_subdef i) :
Itv.spec r (- x%:inum).
Canonical opp_inum (i : interval int) (x : {itv R & i}) :=
Itv.mk (opp_inum_subproof x).
Definition add_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 && b2) (intZmod.addz x1 x2)
| _, _ ⇒ BInfty _ true
end.
Arguments add_itv_boundl_subdef /.
Definition add_itv_boundr_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 || b2) (intZmod.addz x1 x2)
| _, _ ⇒ BInfty _ false
end.
Arguments add_itv_boundr_subdef /.
Definition add_itv_subdef (i1 i2 : interval int) : interval int :=
let 'Interval l1 u1 := i1 in
let 'Interval l2 u2 := i2 in
Interval (add_itv_boundl_subdef l1 l2) (add_itv_boundr_subdef u1 u2).
Arguments add_itv_subdef /.
Lemma add_inum_subproof (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi})
(r := add_itv_subdef xi yi) :
Itv.spec r (x%:inum + y%:inum).
Canonical add_inum (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi}) :=
Itv.mk (add_inum_subproof x y).
End NumDomainStability.
Section RealDomainStability.
Context {R : realDomainType}.
Definition itv_bound_signl (b : itv_bound int) : KnownSign.sign :=
let b0 := BLeft 0%Z in
(if b == b0 then =0 else if (b ≤ b0)%O then <=0 else >=0)%snum_sign.
Definition itv_bound_signr (b : itv_bound int) : KnownSign.sign :=
let b0 := BRight 0%Z in
(if b == b0 then =0 else if (b ≤ b0)%O then <=0 else >=0)%snum_sign.
Definition interval_sign (i : interval int) : option KnownSign.real :=
let 'Interval l u := i in
(match itv_bound_signl l, itv_bound_signr u with
| =0, <=0
| >=0, =0
| >=0, <=0 ⇒ None
| =0, =0 ⇒ Some (KnownSign.Sign =0)
| <=0, =0
| <=0, <=0 ⇒ Some (KnownSign.Sign <=0)
| =0, >=0
| >=0, >=0 ⇒ Some (KnownSign.Sign >=0)
| <=0, >=0 ⇒ Some >=<0
end)%snum_sign.
Variant interval_sign_spec (l u : itv_bound int) : option KnownSign.real → Set :=
| ISignNone : (u ≤ l)%O → interval_sign_spec l u None
| ISignEqZero : l = BLeft 0 → u = BRight 0 →
interval_sign_spec l u (Some (KnownSign.Sign =0))
| ISignNeg : (l < BLeft 0%:Z)%O → (u ≤ BRight 0%:Z)%O →
interval_sign_spec l u (Some (KnownSign.Sign <=0))
| ISignPos : (BLeft 0%:Z ≤ l)%O → (BRight 0%:Z < u)%O →
interval_sign_spec l u (Some (KnownSign.Sign >=0))
| ISignBoth : (l < BLeft 0%:Z)%O → (BRight 0%:Z < u)%O →
interval_sign_spec l u (Some >=<0%snum_sign).
Lemma interval_signP l u :
interval_sign_spec l u (interval_sign (Interval l u)).
Definition mul_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide true 0%Z, BSide _ _
| BSide _ _, BSide true 0%Z ⇒ BSide true 0%Z
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 && b2) (intRing.mulz x1 x2)
| _, BInfty _
| BInfty _, _ ⇒ BInfty _ false
end.
Arguments mul_itv_boundl_subdef /.
Definition mul_itv_boundr_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide true 0%Z, _
| _, BSide true 0%Z ⇒ BSide true 0%Z
| BSide false 0%Z, _
| _, BSide false 0%Z ⇒ BSide false 0%Z
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 || b2) (intRing.mulz x1 x2)
| _, BInfty _
| BInfty _, _ ⇒ BInfty _ false
end.
Arguments mul_itv_boundr_subdef /.
Lemma mul_itv_boundl_subproof b1 b2 (x1 x2 : R) :
(BLeft 0%:Z ≤ b1 → BLeft 0%:Z ≤ b2 →
Itv.map_itv_bound intr b1 ≤ BLeft x1 →
Itv.map_itv_bound intr b2 ≤ BLeft x2 →
Itv.map_itv_bound intr (mul_itv_boundl_subdef b1 b2) ≤ BLeft (x1 × x2))%O.
Lemma mul_itv_boundrC_subproof b1 b2 :
mul_itv_boundr_subdef b1 b2 = mul_itv_boundr_subdef b2 b1.
Lemma mul_itv_boundr_subproof b1 b2 (x1 x2 : R) :
(BLeft 0%R ≤ BLeft x1 → BLeft 0%R ≤ BLeft x2 →
BRight x1 ≤ Itv.map_itv_bound intr b1 →
BRight x2 ≤ Itv.map_itv_bound intr b2 →
BRight (x1 × x2) ≤ Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O.
Lemma mul_itv_boundr'_subproof b1 b2 (x1 x2 : R) :
(BLeft 0%:R ≤ BLeft x1 → BRight 0%:Z ≤ b2 →
BRight x1 ≤ Itv.map_itv_bound intr b1 →
BRight x2 ≤ Itv.map_itv_bound intr b2 →
BRight (x1 × x2) ≤ Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O.
Definition mul_itv_subdef (i1 i2 : interval int) : interval int :=
let 'Interval l1 u1 := i1 in
let 'Interval l2 u2 := i2 in
let opp := opp_itv_bound_subdef in
let mull := mul_itv_boundl_subdef in
let mulr := mul_itv_boundr_subdef in
match interval_sign i1, interval_sign i2 with
| None, _ | _, None ⇒ `[1, 0]
| some s1, Some s2 ⇒
(match s1, s2 with
| =0, _ ⇒ `[0, 0]
| _, =0 ⇒ `[0, 0]
| >=0, >=0 ⇒ Interval (mull l1 l2) (mulr u1 u2)
| <=0, <=0 ⇒ Interval (mull (opp u1) (opp u2)) (mulr (opp l1) (opp l2))
| >=0, <=0 ⇒ Interval (opp (mulr u1 (opp l2))) (opp (mull l1 (opp u2)))
| <=0, >=0 ⇒ Interval (opp (mulr (opp l1) u2)) (opp (mull (opp u1) l2))
| >=0, >=<0 ⇒ Interval (opp (mulr u1 (opp l2))) (mulr u1 u2)
| <=0, >=<0 ⇒ Interval (opp (mulr (opp l1) u2)) (mulr (opp l1) (opp l2))
| >=<0, >=0 ⇒ Interval (opp (mulr (opp l1) u2)) (mulr u1 u2)
| >=<0, <=0 ⇒ Interval (opp (mulr u1 (opp l2))) (mulr (opp l1) (opp l2))
| >=<0, >=<0 ⇒ Interval
(Order.min (opp (mulr (opp l1) u2))
(opp (mulr u1 (opp l2))))
(Order.max (mulr (opp l1) (opp l2))
(mulr u1 u2))
end)%snum_sign
end.
Arguments mul_itv_subdef /.
Lemma map_itv_bound_min (x y : itv_bound int) :
Itv.map_itv_bound (fun x ⇒ x%:~R : R) (Order.min x y)
= Order.min (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y).
Lemma map_itv_bound_max (x y : itv_bound int) :
Itv.map_itv_bound (fun x ⇒ x%:~R : R) (Order.max x y)
= Order.max (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y).
Lemma mul_inum_subproof (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi})
(r := mul_itv_subdef xi yi) :
Itv.spec r (x%:inum × y%:inum).
Canonical mul_inum (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi}) :=
Itv.mk (mul_inum_subproof x y).
End RealDomainStability.
Section Morph.
Context {R : numDomainType} {i : interval int}.
Implicit Types x y : nR.
Lemma inum_eq : {mono inum : x y / x == y}.
Lemma inum_le : {mono inum : x y / (x ≤ y)%O}.
Lemma inum_lt : {mono inum : x y / (x < y)%O}.
End Morph.
Section Test1.
Variable R : numDomainType.
Variable x : {i01 R}.
Goal 0%:i01 = 1%:i01 :> {i01 R}.
Goal (- x%:inum)%:itv = (- x%:inum)%:itv :> {itv R & `[-1, 0]}.
Goal (1 - x%:inum)%:i01 = x.
End Test1.
Section Test2.
Variable R : realDomainType.
Variable x y : {i01 R}.
Goal (x%:inum × y%:inum)%:i01 = x%:inum%:i01.
End Test2.
Module Test3.
Section Test3.
Variable R : realDomainType.
Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
(1 - ((1 - p%:inum)%:i01%:inum × (1 - q%:inum)%:i01%:inum))%:i01.
Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
@Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
(`1- (`1-(p%:inum) × `1-(q%:inum)))%:i01.
End Test3.
End Test3.
Itv.mk (typ_inum_subproof x).
Notation unify_itv ix iy := (unify wider_itv ix iy).
Section Theory.
Context {R : numDomainType} {i : interval int}.
Implicit Type x : sT.
Lemma itv_intro {x} : x%:inum = x%:inum :> R.
Definition empty_itv := `[Posz 1, Posz 0].
Lemma itv_bottom x : unify_itv empty_itv i → False.
Lemma itv_gt0 x : unify_itv `]Posz 0, +oo[ i → 0%R < x%:inum :> R.
Lemma itv_le0F x : unify_itv `]Posz 0, +oo[ i → x%:inum ≤ 0%R :> R = false.
Lemma itv_lt0 x : unify_itv `]-oo, Posz 0[ i → x%:inum < 0%R :> R.
Lemma itv_ge0F x : unify_itv `]-oo, Posz 0[ i → 0%R ≤ x%:inum :> R = false.
Lemma itv_ge0 x : unify_itv `[Posz 0, +oo[ i → 0%R ≤ x%:inum :> R.
Lemma itv_lt0F x : unify_itv `[Posz 0, +oo[ i → x%:inum < 0%R :> R = false.
Lemma itv_le0 x : unify_itv `]-oo, Posz 0] i → x%:inum ≤ 0%R :> R.
Lemma itv_gt0F x : unify_itv `]-oo, Posz 0] i → 0%R < x%:inum :> R = false.
Lemma lt1 x : unify_itv `]-oo, Posz 1[ i → x%:inum < 1%R :> R.
Lemma ge1F x : unify_itv `]-oo, Posz 1[ i → 1%R ≤ x%:inum :> R = false.
Lemma le1 x : unify_itv `]-oo, Posz 1] i → x%:inum ≤ 1%R :> R.
Lemma gt1F x : unify_itv `]-oo, Posz 1] i → 1%R < x%:inum :> R = false.
Lemma widen_itv_subproof x i' : unify_itv i' i → Itv.spec i' x%:inum.
Definition widen_itv x i' (uni : unify_itv i' i) :=
Itv.mk (widen_itv_subproof x uni).
Lemma widen_itvE x (uni : unify_itv i i) : @widen_itv x i uni = x.
End Theory.
Arguments itv_bottom {R i} _ {_}.
Arguments itv_gt0 {R i} _ {_}.
Arguments itv_le0F {R i} _ {_}.
Arguments itv_lt0 {R i} _ {_}.
Arguments itv_ge0F {R i} _ {_}.
Arguments itv_ge0 {R i} _ {_}.
Arguments itv_lt0F {R i} _ {_}.
Arguments itv_le0 {R i} _ {_}.
Arguments itv_gt0F {R i} _ {_}.
Arguments lt1 {R i} _ {_}.
Arguments ge1F {R i} _ {_}.
Arguments le1 {R i} _ {_}.
Arguments gt1F {R i} _ {_}.
Arguments widen_itv {R i} _ {_ _}.
Arguments widen_itvE {R i} _ {_}.
#[global] Hint Extern 0 (is_true (0%R < _)%O) ⇒ solve [apply: itv_gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%R)%O) ⇒ solve [apply: itv_lt0] : core.
#[global] Hint Extern 0 (is_true (0%R ≤ _)%O) ⇒ solve [apply: itv_ge0] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 0%R)%O) ⇒ solve [apply: itv_le0] : core.
#[global] Hint Extern 0 (is_true (_ < 1%R)%O) ⇒ solve [apply: lt1] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 1%R)%O) ⇒ solve [apply: le1] : core.
Notation "x %:i01" := (widen_itv x%:itv : {i01 _}) (only parsing) : ring_scope.
Notation "x %:i01" := (@widen_itv _ _
(@Itv.from _ _ _ (Phantom _ x)) `[Posz 0, Posz 1] _)
(only printing) : ring_scope.
Local Open Scope ring_scope.
Section NumDomainStability.
Context {R : numDomainType}.
Lemma zero_inum_subproof : Itv.spec `[0, 0] (0 : R).
Canonical zero_inum := Itv.mk zero_inum_subproof.
Lemma one_inum_subproof : Itv.spec `[1, 1] (1 : R).
Canonical one_inum := Itv.mk one_inum_subproof.
Definition opp_itv_bound_subdef (b : itv_bound int) : itv_bound int :=
match b with
| BSide b x ⇒ BSide (~~ b) (intZmod.oppz x)
| BInfty b ⇒ BInfty _ (~~ b)
end.
Arguments opp_itv_bound_subdef /.
Lemma opp_itv_ge0_subproof b :
(BLeft 0%R ≤ opp_itv_bound_subdef b)%O = (b ≤ BRight 0%R)%O.
Lemma opp_itv_gt0_subproof b :
(BLeft 0%R < opp_itv_bound_subdef b)%O = (b < BRight 0%R)%O.
Lemma opp_itv_boundr_subproof (x : R) b :
(BRight (- x)%R ≤ Itv.map_itv_bound intr (opp_itv_bound_subdef b))%O
= (Itv.map_itv_bound intr b ≤ BLeft x)%O.
Lemma opp_itv_le0_subproof b :
(opp_itv_bound_subdef b ≤ BRight 0%R)%O = (BLeft 0%R ≤ b)%O.
Lemma opp_itv_lt0_subproof b :
(opp_itv_bound_subdef b < BRight 0%R)%O = (BLeft 0%R < b)%O.
Lemma opp_itv_boundl_subproof (x : R) b :
(Itv.map_itv_bound intr (opp_itv_bound_subdef b) ≤ BLeft (- x)%R)%O
= (BRight x ≤ Itv.map_itv_bound intr b)%O.
Definition opp_itv_subdef (i : interval int) : interval int :=
let 'Interval l u := i in
Interval (opp_itv_bound_subdef u) (opp_itv_bound_subdef l).
Arguments opp_itv_subdef /.
Lemma opp_inum_subproof (i : interval int)
(x : {itv R & i}) (r := opp_itv_subdef i) :
Itv.spec r (- x%:inum).
Canonical opp_inum (i : interval int) (x : {itv R & i}) :=
Itv.mk (opp_inum_subproof x).
Definition add_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 && b2) (intZmod.addz x1 x2)
| _, _ ⇒ BInfty _ true
end.
Arguments add_itv_boundl_subdef /.
Definition add_itv_boundr_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 || b2) (intZmod.addz x1 x2)
| _, _ ⇒ BInfty _ false
end.
Arguments add_itv_boundr_subdef /.
Definition add_itv_subdef (i1 i2 : interval int) : interval int :=
let 'Interval l1 u1 := i1 in
let 'Interval l2 u2 := i2 in
Interval (add_itv_boundl_subdef l1 l2) (add_itv_boundr_subdef u1 u2).
Arguments add_itv_subdef /.
Lemma add_inum_subproof (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi})
(r := add_itv_subdef xi yi) :
Itv.spec r (x%:inum + y%:inum).
Canonical add_inum (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi}) :=
Itv.mk (add_inum_subproof x y).
End NumDomainStability.
Section RealDomainStability.
Context {R : realDomainType}.
Definition itv_bound_signl (b : itv_bound int) : KnownSign.sign :=
let b0 := BLeft 0%Z in
(if b == b0 then =0 else if (b ≤ b0)%O then <=0 else >=0)%snum_sign.
Definition itv_bound_signr (b : itv_bound int) : KnownSign.sign :=
let b0 := BRight 0%Z in
(if b == b0 then =0 else if (b ≤ b0)%O then <=0 else >=0)%snum_sign.
Definition interval_sign (i : interval int) : option KnownSign.real :=
let 'Interval l u := i in
(match itv_bound_signl l, itv_bound_signr u with
| =0, <=0
| >=0, =0
| >=0, <=0 ⇒ None
| =0, =0 ⇒ Some (KnownSign.Sign =0)
| <=0, =0
| <=0, <=0 ⇒ Some (KnownSign.Sign <=0)
| =0, >=0
| >=0, >=0 ⇒ Some (KnownSign.Sign >=0)
| <=0, >=0 ⇒ Some >=<0
end)%snum_sign.
Variant interval_sign_spec (l u : itv_bound int) : option KnownSign.real → Set :=
| ISignNone : (u ≤ l)%O → interval_sign_spec l u None
| ISignEqZero : l = BLeft 0 → u = BRight 0 →
interval_sign_spec l u (Some (KnownSign.Sign =0))
| ISignNeg : (l < BLeft 0%:Z)%O → (u ≤ BRight 0%:Z)%O →
interval_sign_spec l u (Some (KnownSign.Sign <=0))
| ISignPos : (BLeft 0%:Z ≤ l)%O → (BRight 0%:Z < u)%O →
interval_sign_spec l u (Some (KnownSign.Sign >=0))
| ISignBoth : (l < BLeft 0%:Z)%O → (BRight 0%:Z < u)%O →
interval_sign_spec l u (Some >=<0%snum_sign).
Lemma interval_signP l u :
interval_sign_spec l u (interval_sign (Interval l u)).
Definition mul_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide true 0%Z, BSide _ _
| BSide _ _, BSide true 0%Z ⇒ BSide true 0%Z
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 && b2) (intRing.mulz x1 x2)
| _, BInfty _
| BInfty _, _ ⇒ BInfty _ false
end.
Arguments mul_itv_boundl_subdef /.
Definition mul_itv_boundr_subdef (b1 b2 : itv_bound int) : itv_bound int :=
match b1, b2 with
| BSide true 0%Z, _
| _, BSide true 0%Z ⇒ BSide true 0%Z
| BSide false 0%Z, _
| _, BSide false 0%Z ⇒ BSide false 0%Z
| BSide b1 x1, BSide b2 x2 ⇒ BSide (b1 || b2) (intRing.mulz x1 x2)
| _, BInfty _
| BInfty _, _ ⇒ BInfty _ false
end.
Arguments mul_itv_boundr_subdef /.
Lemma mul_itv_boundl_subproof b1 b2 (x1 x2 : R) :
(BLeft 0%:Z ≤ b1 → BLeft 0%:Z ≤ b2 →
Itv.map_itv_bound intr b1 ≤ BLeft x1 →
Itv.map_itv_bound intr b2 ≤ BLeft x2 →
Itv.map_itv_bound intr (mul_itv_boundl_subdef b1 b2) ≤ BLeft (x1 × x2))%O.
Lemma mul_itv_boundrC_subproof b1 b2 :
mul_itv_boundr_subdef b1 b2 = mul_itv_boundr_subdef b2 b1.
Lemma mul_itv_boundr_subproof b1 b2 (x1 x2 : R) :
(BLeft 0%R ≤ BLeft x1 → BLeft 0%R ≤ BLeft x2 →
BRight x1 ≤ Itv.map_itv_bound intr b1 →
BRight x2 ≤ Itv.map_itv_bound intr b2 →
BRight (x1 × x2) ≤ Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O.
Lemma mul_itv_boundr'_subproof b1 b2 (x1 x2 : R) :
(BLeft 0%:R ≤ BLeft x1 → BRight 0%:Z ≤ b2 →
BRight x1 ≤ Itv.map_itv_bound intr b1 →
BRight x2 ≤ Itv.map_itv_bound intr b2 →
BRight (x1 × x2) ≤ Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O.
Definition mul_itv_subdef (i1 i2 : interval int) : interval int :=
let 'Interval l1 u1 := i1 in
let 'Interval l2 u2 := i2 in
let opp := opp_itv_bound_subdef in
let mull := mul_itv_boundl_subdef in
let mulr := mul_itv_boundr_subdef in
match interval_sign i1, interval_sign i2 with
| None, _ | _, None ⇒ `[1, 0]
| some s1, Some s2 ⇒
(match s1, s2 with
| =0, _ ⇒ `[0, 0]
| _, =0 ⇒ `[0, 0]
| >=0, >=0 ⇒ Interval (mull l1 l2) (mulr u1 u2)
| <=0, <=0 ⇒ Interval (mull (opp u1) (opp u2)) (mulr (opp l1) (opp l2))
| >=0, <=0 ⇒ Interval (opp (mulr u1 (opp l2))) (opp (mull l1 (opp u2)))
| <=0, >=0 ⇒ Interval (opp (mulr (opp l1) u2)) (opp (mull (opp u1) l2))
| >=0, >=<0 ⇒ Interval (opp (mulr u1 (opp l2))) (mulr u1 u2)
| <=0, >=<0 ⇒ Interval (opp (mulr (opp l1) u2)) (mulr (opp l1) (opp l2))
| >=<0, >=0 ⇒ Interval (opp (mulr (opp l1) u2)) (mulr u1 u2)
| >=<0, <=0 ⇒ Interval (opp (mulr u1 (opp l2))) (mulr (opp l1) (opp l2))
| >=<0, >=<0 ⇒ Interval
(Order.min (opp (mulr (opp l1) u2))
(opp (mulr u1 (opp l2))))
(Order.max (mulr (opp l1) (opp l2))
(mulr u1 u2))
end)%snum_sign
end.
Arguments mul_itv_subdef /.
Lemma map_itv_bound_min (x y : itv_bound int) :
Itv.map_itv_bound (fun x ⇒ x%:~R : R) (Order.min x y)
= Order.min (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y).
Lemma map_itv_bound_max (x y : itv_bound int) :
Itv.map_itv_bound (fun x ⇒ x%:~R : R) (Order.max x y)
= Order.max (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y).
Lemma mul_inum_subproof (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi})
(r := mul_itv_subdef xi yi) :
Itv.spec r (x%:inum × y%:inum).
Canonical mul_inum (xi yi : interval int)
(x : {itv R & xi}) (y : {itv R & yi}) :=
Itv.mk (mul_inum_subproof x y).
End RealDomainStability.
Section Morph.
Context {R : numDomainType} {i : interval int}.
Implicit Types x y : nR.
Lemma inum_eq : {mono inum : x y / x == y}.
Lemma inum_le : {mono inum : x y / (x ≤ y)%O}.
Lemma inum_lt : {mono inum : x y / (x < y)%O}.
End Morph.
Section Test1.
Variable R : numDomainType.
Variable x : {i01 R}.
Goal 0%:i01 = 1%:i01 :> {i01 R}.
Goal (- x%:inum)%:itv = (- x%:inum)%:itv :> {itv R & `[-1, 0]}.
Goal (1 - x%:inum)%:i01 = x.
End Test1.
Section Test2.
Variable R : realDomainType.
Variable x y : {i01 R}.
Goal (x%:inum × y%:inum)%:i01 = x%:inum%:i01.
End Test2.
Module Test3.
Section Test3.
Variable R : realDomainType.
Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
(1 - ((1 - p%:inum)%:i01%:inum × (1 - q%:inum)%:i01%:inum))%:i01.
Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
@Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
(`1- (`1-(p%:inum) × `1-(q%:inum)))%:i01.
End Test3.
End Test3.