Library StandardResults
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
Theorems about Real numbers, distances, intervals.
*************************** Standard Imports
Require Import ComhCoq.Extras.LibTactics.
Require Export Reals.
Require Export Logic.ProofIrrelevance.
Require Import ComhCoq.GenTacs.
Require Export ComhCoq.RInequalities.
Open Scope R_scope.
Definition eqDec (X : Type) := forall x1 x2 : X,
{x1 = x2} + {x1 <> x2}.
Lemma notEq_symm : forall (X : Type) (x1 x2 : X), ~x1 = x2 -> ~x2 = x1.
Lemma two_nonneg : 0 <= 2.
Ltac Rplus3_swap_2_3 a b c := replace (a + b + c) with (a + c + b); [ | ring].
Ltac Rminus_plus_zero a b := replace (a - b) with (a + (0 - b));[ | ring].
Require Export Reals.
Require Export Logic.ProofIrrelevance.
Require Import ComhCoq.GenTacs.
Require Export ComhCoq.RInequalities.
Open Scope R_scope.
Definition eqDec (X : Type) := forall x1 x2 : X,
{x1 = x2} + {x1 <> x2}.
Lemma notEq_symm : forall (X : Type) (x1 x2 : X), ~x1 = x2 -> ~x2 = x1.
Lemma two_nonneg : 0 <= 2.
Ltac Rplus3_swap_2_3 a b c := replace (a + b + c) with (a + c + b); [ | ring].
Ltac Rminus_plus_zero a b := replace (a - b) with (a + (0 - b));[ | ring].
Performs a contradiction on the assumption that some non-negative real is
less than 0, i.e. negative.
Ltac nonneg_lt0_contra :=
match goal with
| [H : (nonneg ?x) < 0 |- _] =>
apply Rlt_not_le in H; false; apply H; unwrap_apply2 x
end.
match goal with
| [H : (nonneg ?x) < 0 |- _] =>
apply Rlt_not_le in H; false; apply H; unwrap_apply2 x
end.
The number one as a positive real number.
Definition onePos : posreal.
The minimum of two numbers. Note, r2 is returned if the numbers are equal,
but in that case r1 = r2, so this is the same as returning r1.
Definition minR (r1 r2 : R) : R :=
if (Rlt_le_dec r1 r2) then r1 else r2.
if (Rlt_le_dec r1 r2) then r1 else r2.
The maximum of two numbers. Note, r1 is returned if the numbers are equal,
but in that case r1 = r2, so this is the same as returning r2.
Definition maxR (r1 r2 : R) : R :=
if (Rlt_le_dec r1 r2) then r2 else r1.
Definition zeroNonneg : nonnegreal := mknonnegreal 0 (Rle_refl 0).
if (Rlt_le_dec r1 r2) then r2 else r1.
Definition zeroNonneg : nonnegreal := mknonnegreal 0 (Rle_refl 0).
Euclidean distance is always >= 0.
Lemma dist_euc_nonneg : forall (x1 y1 x2 y2 : R),
0 <= dist_euc x1 y1 x2 y2.
0 <= dist_euc x1 y1 x2 y2.
Adding a vector to both points leaves distance unchanged.
Lemma dist_eucAddPres : forall (x1 y1 x2 y2 x3 y3 : R),
dist_euc x1 y1 x2 y2 = dist_euc (x1 + x3) (y1 + y3) (x2 + x3) (y2 + y3).
dist_euc x1 y1 x2 y2 = dist_euc (x1 + x3) (y1 + y3) (x2 + x3) (y2 + y3).
Adding (x, y) to one of the coordinates of dist_euc yeilds and expression
that is within |(x, y)| of the original.
Lemma dist_eucAddLe : forall (x1 y1 x2 y2 x3 y3 : R),
dist_euc (x1 + x3) (y1 + y3) (x2) (y2) <=
dist_euc x1 y1 x2 y2 + dist_euc x3 y3 0 0.
Lemma nonnegRealEqR : forall (r1 r2 : nonnegreal),
nonneg r1 = nonneg r2 -> r1 = r2.
Lemma posRealEqR : forall (r1 r2 : posreal),
pos r1 = pos r2 -> r1 = r2.
Open Scope R_scope.
dist_euc (x1 + x3) (y1 + y3) (x2) (y2) <=
dist_euc x1 y1 x2 y2 + dist_euc x3 y3 0 0.
Lemma nonnegRealEqR : forall (r1 r2 : nonnegreal),
nonneg r1 = nonneg r2 -> r1 = r2.
Lemma posRealEqR : forall (r1 r2 : posreal),
pos r1 = pos r2 -> r1 = r2.
Open Scope R_scope.
Multiplication defined for nonneg reals.
Definition multNonneg (r1 r2 : nonnegreal) : nonnegreal :=
let prod := (r1 * r2) in
let h1 := cond_nonneg r1 in
let h2 := cond_nonneg r2 in
let h := Rmult_le_0_compat r1 r2 h1 h2 in
mknonnegreal prod h.
Notation "r1 *nn* r2" := (multNonneg r1 r2) (at level 40, left associativity).
let prod := (r1 * r2) in
let h1 := cond_nonneg r1 in
let h2 := cond_nonneg r2 in
let h := Rmult_le_0_compat r1 r2 h1 h2 in
mknonnegreal prod h.
Notation "r1 *nn* r2" := (multNonneg r1 r2) (at level 40, left associativity).
Subtraction on nonnegative reals as a total function.
Gives r1 - r2 if that result is nonnegative, else returns 0.
Definition subNonnegTot (r1 r2 : nonnegreal) : nonnegreal :=
match (Rle_dec r2 r1) with
| left p => mknonnegreal (r1 - r2) (RleMinusBothSides r1 r2 p)
| _ => zeroNonneg
end.
Notation "r1 -nn- r2" := (subNonnegTot r1 r2) (at level 50).
match (Rle_dec r2 r1) with
| left p => mknonnegreal (r1 - r2) (RleMinusBothSides r1 r2 p)
| _ => zeroNonneg
end.
Notation "r1 -nn- r2" := (subNonnegTot r1 r2) (at level 50).
Adds two nonnegreals together to get a resulting nonegreal.
Definition addNonneg (r1 r2 : nonnegreal) : nonnegreal :=
match r1 with
| {|nonneg := x1; cond_nonneg := cn1 |} => match r2 with
| {|nonneg := x2; cond_nonneg := cn2 |} => let r := x1 + x2 in
let Heqr := eq_refl r in
{| nonneg := r; cond_nonneg := eq_ind_r (fun r0 : R => 0 <= r0)
(Rplus_le_le_0_compat x1 x2 cn1 cn2) Heqr |} end end.
Notation "x +nn+ y" := (addNonneg x y) (at level 50).
match r1 with
| {|nonneg := x1; cond_nonneg := cn1 |} => match r2 with
| {|nonneg := x2; cond_nonneg := cn2 |} => let r := x1 + x2 in
let Heqr := eq_refl r in
{| nonneg := r; cond_nonneg := eq_ind_r (fun r0 : R => 0 <= r0)
(Rplus_le_le_0_compat x1 x2 cn1 cn2) Heqr |} end end.
Notation "x +nn+ y" := (addNonneg x y) (at level 50).
Adding two nonneg numbers and then removing the real part is the same
as removing the real part and then adding
Lemma addNonnegFact : forall (r1 r2 : nonnegreal),
nonneg (r1 +nn+ r2) = (nonneg r1) + (nonneg r2).
nonneg (r1 +nn+ r2) = (nonneg r1) + (nonneg r2).
zeroNonneg is the right zero for addNonneg
Lemma addNonnegZeroR : forall (r : nonnegreal),
r +nn+ zeroNonneg = r.
r +nn+ zeroNonneg = r.
zeroNonneg is the right zero for addNonneg
Lemma addNonnegZeroL : forall (r : nonnegreal),
zeroNonneg +nn+ r = r.
zeroNonneg +nn+ r = r.
Removes the proof from an equality of nonnegative reals, simplifying the
proof obligation to proving the equality on just the reals.
Lemma nonnegEqSimpl : forall (r1 r2 : nonnegreal),
nonneg r1 = nonneg r2 -> r1 = r2.
nonneg r1 = nonneg r2 -> r1 = r2.
Addition of nonnegative reals is associative
Lemma addNonnegAssoc : forall (r1 r2 r3 : nonnegreal),
r1 +nn+ (r2 +nn+ r3) = r1 +nn+ r2 +nn+ r3.
Lemma addNonnegComm : forall (r1 r2 : nonnegreal),
r1 +nn+ r2 = r2 +nn+ r1.
Lemma addNonnegCancel : forall (r1 r2 r3 : nonnegreal),
r1 +nn+ r2 = r1 +nn+ r3 -> r2 = r3.
Lemma eqDecReal : eqDec R.
Lemma eqDecNonnegReal : eqDec nonnegreal.
Lemma eqDecPosReal : eqDec posreal.
Definition sumSquares (r1 r2 : R) : R :=
Rsqr r1 + Rsqr r2.
r1 +nn+ (r2 +nn+ r3) = r1 +nn+ r2 +nn+ r3.
Lemma addNonnegComm : forall (r1 r2 : nonnegreal),
r1 +nn+ r2 = r2 +nn+ r1.
Lemma addNonnegCancel : forall (r1 r2 r3 : nonnegreal),
r1 +nn+ r2 = r1 +nn+ r3 -> r2 = r3.
Lemma eqDecReal : eqDec R.
Lemma eqDecNonnegReal : eqDec nonnegreal.
Lemma eqDecPosReal : eqDec posreal.
Definition sumSquares (r1 r2 : R) : R :=
Rsqr r1 + Rsqr r2.
Coerce a positive real to a nonnegative real.
Coercion posToNonneg (r : posreal) : nonnegreal :=
match r with mkposreal p c =>
mknonnegreal p (Rlt_le 0 p c) end.
match r with mkposreal p c =>
mknonnegreal p (Rlt_le 0 p c) end.
Every positive real is the sum of two positive reals. The simplest
existential witnesses for this are both half the original number i.e. every number is equal
to half itself plus half itself.
Theorem addPosRealExists : forall (r : posreal),
exists r1 r2, pos r = pos r1 + pos r2.
exists r1 r2, pos r = pos r1 + pos r2.
A position is a pair of reals.
Record Position := mkPosition {xCoord : R; yCoord : R}.
Addition on positions (vector addition).
Definition addPos (p1 p2 : Position) : Position :=
let x1 := xCoord p1 in let y1 := yCoord p1 in
let x2 := xCoord p2 in let y2 := yCoord p2 in
mkPosition (x1 + x2) (y1 + y2).
Notation "p1 +p+ p2" := (addPos p1 p2) (at level 50).
Hint Unfold addPos.
let x1 := xCoord p1 in let y1 := yCoord p1 in
let x2 := xCoord p2 in let y2 := yCoord p2 in
mkPosition (x1 + x2) (y1 + y2).
Notation "p1 +p+ p2" := (addPos p1 p2) (at level 50).
Hint Unfold addPos.
Subtraction (vector) on positions.
Definition minusPos (p1 p2 : Position) : Position :=
let x1 := xCoord p1 in let y1 := yCoord p1 in
let x2 := xCoord p2 in let y2 := yCoord p2 in
mkPosition (x1 - x2) (y1 - y2).
Notation "p1 -~p- p2" := (minusPos p1 p2) (at level 50).
Hint Unfold minusPos.
Definition oppPos (p : Position) : Position :=
let x := xCoord p in let y := yCoord p in
mkPosition (-x) (-y).
Notation "~- p" := (oppPos p) (at level 40).
Hint Unfold oppPos.
let x1 := xCoord p1 in let y1 := yCoord p1 in
let x2 := xCoord p2 in let y2 := yCoord p2 in
mkPosition (x1 - x2) (y1 - y2).
Notation "p1 -~p- p2" := (minusPos p1 p2) (at level 50).
Hint Unfold minusPos.
Definition oppPos (p : Position) : Position :=
let x := xCoord p in let y := yCoord p in
mkPosition (-x) (-y).
Notation "~- p" := (oppPos p) (at level 40).
Hint Unfold oppPos.
The Euclidean distance between a pair of positions.
Definition dist2d (p1 p2 : Position) : nonnegreal :=
mknonnegreal
(dist_euc (xCoord p1) (yCoord p1) (xCoord p2) (yCoord p2))
(dist_euc_nonneg (xCoord p1) (yCoord p1) (xCoord p2) (yCoord p2)).
mknonnegreal
(dist_euc (xCoord p1) (yCoord p1) (xCoord p2) (yCoord p2))
(dist_euc_nonneg (xCoord p1) (yCoord p1) (xCoord p2) (yCoord p2)).
The origin is the point (0, 0).
Definition origin := mkPosition 0 0.
The vector length of a position. Defined to be the distance between
that position and (0, 0).
Definition displacement (p : Position) : nonnegreal := dist2d p origin.
Ltac unfoldPosDefs := unfold addPos; unfold minusPos; unfold oppPos;
unfold dist; unfold origin; unfold displacement.
Ltac unfoldPosDefs := unfold addPos; unfold minusPos; unfold oppPos;
unfold dist; unfold origin; unfold displacement.
The negation of p1 - p2 is p2 - p1.
Theorem oppMinusPos : forall (p1 p2 : Position),
~-(p1 -~p- p2) = (p2 -~p- p1).
~-(p1 -~p- p2) = (p2 -~p- p1).
0 is the right unit of plus.
Theorem plusRightUnitPos : forall (p1 : Position),
p1 +p+ origin = p1.
p1 +p+ origin = p1.
0 is the left unit of plus.
Theorem plusLeftUnitPos : forall (p1 : Position),
origin +p+ p1 = p1.
Theorem minusCancellativePos : forall (p1 : Position),
p1 -~p- p1 = origin.
origin +p+ p1 = p1.
Theorem minusCancellativePos : forall (p1 : Position),
p1 -~p- p1 = origin.
Subtracting p2 is that same as adding -p2.
Theorem minusPlusOppPos : forall (p1 p2 : Position),
p1 -~p- p2 = p1 +p+ (~-p2).
p1 -~p- p2 = p1 +p+ (~-p2).
Add and then subtract p2 and you're left with the original position.
Lemma plusMinusCancelPos : forall (p1 p2 : Position),
p1 +p+ p2 -~p- p2 = p1.
p1 +p+ p2 -~p- p2 = p1.
Subtract and then add p2 and you're left with the original position.
Lemma minusPlusCancelPos : forall (p1 p2 : Position),
p1 -~p- p2 +p+ p2 = p1.
p1 -~p- p2 +p+ p2 = p1.
The distance function is symmetric.
Lemma distSymmetric : forall (p1 p2 : Position), dist2d p1 p2 = dist2d p2 p1.
Adding the difference between two vectors to the subtracted
vector gets you the other vector.
Theorem minusPlusInvPos : forall (p1 p2 : Position),
p1 = p2 +p+ (p1 -~p- p2).
p1 = p2 +p+ (p1 -~p- p2).
Adding the same vector to the arguments of dist2d preserves the result.
Theorem distAddPres : forall (p1 p2 p3 : Position),
dist2d p1 p2 = dist2d (p1 +p+ p3) (p2 +p+ p3).
dist2d p1 p2 = dist2d (p1 +p+ p3) (p2 +p+ p3).
Subtracting the same vector to the arguments of dist2d preserves the result.
Theorem distMinusPres : forall (p1 p2 p3 : Position),
dist2d p1 p2 = dist2d (p1 -~p- p3) (p2 -~p- p3).
dist2d p1 p2 = dist2d (p1 -~p- p3) (p2 -~p- p3).
The distance between p1 and p2 is the same as the length of p1 - p2.
Theorem minusLengthDistance : forall (p1 p2 : Position),
dist2d p1 p2 = displacement (p1 -~p- p2).
dist2d p1 p2 = displacement (p1 -~p- p2).
Adding p3 to p1 changes the distance between p1 and p2 by
at most |p3|.
Theorem distAddLe : forall (p1 p2 p3 : Position),
dist2d (p1 +p+ p3) (p2) <= dist2d p1 p2 + displacement p3.
dist2d (p1 +p+ p3) (p2) <= dist2d p1 p2 + displacement p3.
Adding p3 to p1 changes the distance between p1 and p2 by
at most r if |p3| <= r.
Theorem distAddLeLe : forall (p1 p2 p3 : Position) (r : R),
displacement p3 <= r -> dist2d (p1 +p+ p3) (p2) <= dist2d p1 p2 + r. Open Scope R_scope.
displacement p3 <= r -> dist2d (p1 +p+ p3) (p2) <= dist2d p1 p2 + r. Open Scope R_scope.
If the distance between p1 and p1' is bounded above by r, and the
same holds for p2 and p2', then the distance between p1 and p2 is
at most the difference between p1' and p2' + 2r.
Theorem posDiffBound : forall (p1 p2 p1' p2' : Position) (r : R),
dist2d p1 p1' <= r -> dist2d p2 p2' <= r ->
dist2d p1 p2 <= dist2d p1' p2' + 2*r.
Lemma eqDecPosition : eqDec Position.
Lemma dist_tri_ineq : forall (l1 l2 l3 : Position),
dist2d l1 l3 <= dist2d l1 l2 + dist2d l2 l3.
Lemma dist2D_refl : forall l : Position, dist2d l l = zeroNonneg.
dist2d p1 p1' <= r -> dist2d p2 p2' <= r ->
dist2d p1 p2 <= dist2d p1' p2' + 2*r.
Lemma eqDecPosition : eqDec Position.
Lemma dist_tri_ineq : forall (l1 l2 l3 : Position),
dist2d l1 l3 <= dist2d l1 l2 + dist2d l2 l3.
Lemma dist2D_refl : forall l : Position, dist2d l l = zeroNonneg.
An interval on the real line. We allow upper < lower, the interpretation
in this case being that the interval is empty. The two fields lowerClosed and
upperClosed allow for the four possibilities of interval, from fully closed
to fully open: ☐, ), (, ().
Record Interval := mkInterval{
lower : R;
upper : R;
lowerClosed : bool;
upperClosed : bool
}.
lower : R;
upper : R;
lowerClosed : bool;
upperClosed : bool
}.
inInterval r i means that the real number r is in the Interval i,
where i is interpreted as a closed interval.
Definition inInterval (r : R) (i : Interval) :=
match lowerClosed i, upperClosed i with
| true, true => lower i <= r <= upper i
| true, false => lower i <= r < upper i
| false, true => lower i < r <= upper i
| false, false => lower i < r < upper i
end.
Notation "r [:] i" := (inInterval r i) (at level 70).
match lowerClosed i, upperClosed i with
| true, true => lower i <= r <= upper i
| true, false => lower i <= r < upper i
| false, true => lower i < r <= upper i
| false, false => lower i < r < upper i
end.
Notation "r [:] i" := (inInterval r i) (at level 70).
v1 is a (non-strict) sub interval of v2
Definition subInterval (i1 i2 : Interval) : Prop :=
forall r : R, r [:] i1 -> r [:] i2.
Open Scope R_scope.
forall r : R, r [:] i1 -> r [:] i2.
Open Scope R_scope.
Add the lower bounds and the upper bounds just as in vector addition.
Closedness of a bound in the resulting interval is equivalent to closedness of
the respective bounds in both i1 and i2.
Definition addInterval (i1 i2 : Interval) : Interval :=
match i1 with (mkInterval l1 u1 lc1 uc1) =>
match i2 with (mkInterval l2 u2 lc2 uc2) =>
mkInterval (l1 + l2) (u1 + u2) (andb lc1 lc2) (andb uc1 uc2)
end end.
Notation "i [++] i'" := (addInterval i i') (at level 45).
match i1 with (mkInterval l1 u1 lc1 uc1) =>
match i2 with (mkInterval l2 u2 lc2 uc2) =>
mkInterval (l1 + l2) (u1 + u2) (andb lc1 lc2) (andb uc1 uc2)
end end.
Notation "i [++] i'" := (addInterval i i') (at level 45).
If x is in i then x is less than or equal to the upper bound of i.
Lemma inIntervalLeUpper : forall (i : Interval) (x : R),
x [:] i -> x <= upper i.
x [:] i -> x <= upper i.
If x is in i then the lower bound of i is less than or equal x.
Lemma inIntervalLeLower: forall (i : Interval) (x : R),
x [:] i -> lower i <= x.
Lemma inIntervalLtUpper : forall (i : Interval) (r : R),
r [:] i -> upperClosed i = false ->
r < upper i.
Lemma inIntervalLtLower : forall (i : Interval) (r : R),
r [:] i -> lowerClosed i = false ->
lower i < r.
Lemma inAddLtLower : forall (i1 i2 : Interval) (r1 r2 : R),
r1 [:] i1 -> r2 [:] i2 ->
lowerClosed i1 = false \/ lowerClosed i2 = false ->
lower i1 + lower i2 < r1 + r2.
Lemma inAddLtUpper : forall (i1 i2 : Interval) (r1 r2 : R),
r1 [:] i1 -> r2 [:] i2 ->
upperClosed i1 = false \/ upperClosed i2 = false ->
r1 + r2 < upper i1 + upper i2.
Lemma addIntervalLower : forall (i1 i2 : Interval),
lower (i1 [++] i2) = lower i1 + lower i2.
Lemma addIntervalUpper : forall (i1 i2 : Interval),
upper (i1 [++] i2) = upper i1 + upper i2.
Lemma addIntervalUpperOpen : forall (i1 i2 : Interval),
upperClosed (i1 [++] i2) = false ->
upperClosed i1 = false \/ upperClosed i2 = false.
Lemma addIntervalLowerOpen : forall (i1 i2 : Interval),
lowerClosed (i1 [++] i2) = false ->
lowerClosed i1 = false \/ lowerClosed i2 = false.
Theorem inAddInterval : forall (i1 i2 : Interval) (r1 r2 : R),
r1 [:] i1 -> r2 [:] i2 -> (r1 + r2) [:] (i1 [++] i2).
x [:] i -> lower i <= x.
Lemma inIntervalLtUpper : forall (i : Interval) (r : R),
r [:] i -> upperClosed i = false ->
r < upper i.
Lemma inIntervalLtLower : forall (i : Interval) (r : R),
r [:] i -> lowerClosed i = false ->
lower i < r.
Lemma inAddLtLower : forall (i1 i2 : Interval) (r1 r2 : R),
r1 [:] i1 -> r2 [:] i2 ->
lowerClosed i1 = false \/ lowerClosed i2 = false ->
lower i1 + lower i2 < r1 + r2.
Lemma inAddLtUpper : forall (i1 i2 : Interval) (r1 r2 : R),
r1 [:] i1 -> r2 [:] i2 ->
upperClosed i1 = false \/ upperClosed i2 = false ->
r1 + r2 < upper i1 + upper i2.
Lemma addIntervalLower : forall (i1 i2 : Interval),
lower (i1 [++] i2) = lower i1 + lower i2.
Lemma addIntervalUpper : forall (i1 i2 : Interval),
upper (i1 [++] i2) = upper i1 + upper i2.
Lemma addIntervalUpperOpen : forall (i1 i2 : Interval),
upperClosed (i1 [++] i2) = false ->
upperClosed i1 = false \/ upperClosed i2 = false.
Lemma addIntervalLowerOpen : forall (i1 i2 : Interval),
lowerClosed (i1 [++] i2) = false ->
lowerClosed i1 = false \/ lowerClosed i2 = false.
Theorem inAddInterval : forall (i1 i2 : Interval) (r1 r2 : R),
r1 [:] i1 -> r2 [:] i2 -> (r1 + r2) [:] (i1 [++] i2).
Shifts an interval right by some amount i.e. adds that amount to the upper and lower
bounds of the interval. Closedness does not change.
Definition plusInterval (i : Interval) (r : R) : Interval :=
match i with mkInterval l u cl cu=>
mkInterval (l + r) (u + r) cl cu end.
match i with mkInterval l u cl cu=>
mkInterval (l + r) (u + r) cl cu end.
Shifts an interval left by some amount i.e. adds that amount to the upper and lower
bounds of the interval.
Definition minusInterval (i : Interval) (r : R) : Interval :=
match i with mkInterval l u cl cu=>
mkInterval (l - r) (u - r) cl cu end.
Notation "i [+] r" := (plusInterval i r) (at level 45).
Notation "i [-] r" := (minusInterval i r) (at level 45).
Notation "[\ x , y \]" := (mkInterval x y true true).
Notation "[\ x , y \)" := (mkInterval x y true false).
Notation "(\ x , y \]" := (mkInterval x y false true).
Notation "(\ x , y \)" := (mkInterval x y false false).
Notation "i1 <[ i2" := (subInterval i1 i2) (at level 50).
match i with mkInterval l u cl cu=>
mkInterval (l - r) (u - r) cl cu end.
Notation "i [+] r" := (plusInterval i r) (at level 45).
Notation "i [-] r" := (minusInterval i r) (at level 45).
Notation "[\ x , y \]" := (mkInterval x y true true).
Notation "[\ x , y \)" := (mkInterval x y true false).
Notation "(\ x , y \]" := (mkInterval x y false true).
Notation "(\ x , y \)" := (mkInterval x y false false).
Notation "i1 <[ i2" := (subInterval i1 i2) (at level 50).
Every interval can be rewritten by subtracting and then adding the same r.
Theorem minusPlusInterval : forall (i : Interval) (r : R),
i = i [-] r [+] r.
i = i [-] r [+] r.
Every interval can be rewritten by adding and then subtracting the same r.
Theorem plusMinusInterval : forall (i : Interval) (r : R),
i = i [+] r [-] r.
i = i [+] r [-] r.
Adding a negative is the same as subtracting
Theorem minusOppInterval : forall (i : Interval) (r : R),
i [+] -r = i [-] r.
Theorem inIntervalPlusCancel : forall (i : Interval) (x r : R),
x + r [:] i [+] r -> x [:] i.
Theorem subIntervalPlusCancel : forall (i i' : Interval) (r : R),
i [+] r <[ i' [+] r -> i <[ i'.
Theorem inIntervalPlusCompat : forall (i : Interval) (x r : R),
x [:] i -> x + r [:] i [+] r.
i [+] -r = i [-] r.
Theorem inIntervalPlusCancel : forall (i : Interval) (x r : R),
x + r [:] i [+] r -> x [:] i.
Theorem subIntervalPlusCancel : forall (i i' : Interval) (r : R),
i [+] r <[ i' [+] r -> i <[ i'.
Theorem inIntervalPlusCompat : forall (i : Interval) (x r : R),
x [:] i -> x + r [:] i [+] r.
Every interval is a sub interval of itself.
Lemma subIntervalRefl : forall (i : Interval), i <[ i.
If a number is less than the lower bound of an interval then it is
not in that interval.
Lemma outIntervalLtLower : forall (r : R) (i : Interval),
r < lower i -> ~ r [:] i.
r < lower i -> ~ r [:] i.
If a number is greater than the upper bound of an interval then it is
not in that interval.
Lemma outIntervalLtUpper : forall (r : R) (i : Interval),
upper i < r-> ~ r [:] i.
upper i < r-> ~ r [:] i.
If a number is less than or equal the lower bound of an interval
that is lower closed then it is not in the interval.
Lemma outIntervalLeLower : forall (r : R) (i : Interval),
r <= lower i -> lowerClosed i = false -> ~ r [:] i.
r <= lower i -> lowerClosed i = false -> ~ r [:] i.
If a number is less than or equal the lower bound of an interval
that is lower closed then it is not in the interval.
Lemma outIntervalLeUpper : forall (r : R) (i : Interval),
upper i <= r -> upperClosed i = false -> ~ r [:] i.
upper i <= r -> upperClosed i = false -> ~ r [:] i.
Membership of an interval is decidable.
Lemma inIntervalDec : forall (r : R) (i : Interval),
r [:] i \/ ~ r [:] i.
Lemma inIntervalPoint : forall (x y : R),
x [:] [\y, y\] -> x = y.
Ltac Rminus_refl_simpl := match goal with |- context [?x - ?x] =>
replace (x - x) with 0; [ | ring] end.
Lemma Rminus_lt_subNonnegTot (a b : nonnegreal) c :
0 < c -> a - b < c -> a -nn- b < c.
Lemma Rminus_plus_lt_subNonnegTot (a b : nonnegreal) c z :
z < c -> a - b + z < c -> a -nn- b + z < c.
Lemma subNonnegTot_le_Rminus_eq (r1 r2 : nonnegreal) :
r2 <= r1 -> nonneg (r1 -nn- r2) = r1 - r2.
Lemma Rlt_double x : 0 < x -> x < x + x.
Lemma Rmult_lt_0 y z : 0 < y -> 0 < z -> 0 < y * z.
Lemma Rlt_le_zero_plus r1 r2 : 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
Lemma Rmax_lt_l x y a : a < x -> a < Rmax x y.
Lemma subNonnegTot_0_or_Rminus r1 r2 :
nonneg (r1 -nn- r2) = 0 \/
nonneg (r1 -nn- r2) = r1 - r2.
Lemma subNonnegTot_lt_0 (r1 r2 : nonnegreal) :
r1 < r2 -> nonneg (r1 -nn- r2) = 0.
Ltac Rplus3_swap_2_3_free := match goal with
| |- context[?r1 + ?r2 + ?r3] => Rplus3_swap_2_3 r1 r2 r3
| |- context[?r1 + (?r2 + ?r3)] => rewrite <- Rplus_assoc;
Rplus3_swap_2_3 r1 r2 r3
end.
Lemma Rle_subNonnegTot_r (r1 r2 r3 : nonnegreal) :
r1 <= r2 -> (r1 -nn- r3) <= (r2 -nn- r3).
Lemma addNonneg_subNonnegTot_le_assoc r1 r2 r3 :
(r1 +nn+ r2) -nn- r3 <= r1 +nn+ (r2 -nn- r3).
Lemma multNonneg_Rmult_eq r1 r2 :
nonneg (r1 *nn* r2) = r1 * r2.
Lemma subNonnegTot_le_Rminus (r1 r2 : nonnegreal) :
r1 - r2 <= (r1 -nn- r2).
Lemma subNonnegTot_plus_lt_Rminus (a b : nonnegreal) c z :
a -nn- b + z < c -> a - b + z < c.
r [:] i \/ ~ r [:] i.
Lemma inIntervalPoint : forall (x y : R),
x [:] [\y, y\] -> x = y.
Ltac Rminus_refl_simpl := match goal with |- context [?x - ?x] =>
replace (x - x) with 0; [ | ring] end.
Lemma Rminus_lt_subNonnegTot (a b : nonnegreal) c :
0 < c -> a - b < c -> a -nn- b < c.
Lemma Rminus_plus_lt_subNonnegTot (a b : nonnegreal) c z :
z < c -> a - b + z < c -> a -nn- b + z < c.
Lemma subNonnegTot_le_Rminus_eq (r1 r2 : nonnegreal) :
r2 <= r1 -> nonneg (r1 -nn- r2) = r1 - r2.
Lemma Rlt_double x : 0 < x -> x < x + x.
Lemma Rmult_lt_0 y z : 0 < y -> 0 < z -> 0 < y * z.
Lemma Rlt_le_zero_plus r1 r2 : 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
Lemma Rmax_lt_l x y a : a < x -> a < Rmax x y.
Lemma subNonnegTot_0_or_Rminus r1 r2 :
nonneg (r1 -nn- r2) = 0 \/
nonneg (r1 -nn- r2) = r1 - r2.
Lemma subNonnegTot_lt_0 (r1 r2 : nonnegreal) :
r1 < r2 -> nonneg (r1 -nn- r2) = 0.
Ltac Rplus3_swap_2_3_free := match goal with
| |- context[?r1 + ?r2 + ?r3] => Rplus3_swap_2_3 r1 r2 r3
| |- context[?r1 + (?r2 + ?r3)] => rewrite <- Rplus_assoc;
Rplus3_swap_2_3 r1 r2 r3
end.
Lemma Rle_subNonnegTot_r (r1 r2 r3 : nonnegreal) :
r1 <= r2 -> (r1 -nn- r3) <= (r2 -nn- r3).
Lemma addNonneg_subNonnegTot_le_assoc r1 r2 r3 :
(r1 +nn+ r2) -nn- r3 <= r1 +nn+ (r2 -nn- r3).
Lemma multNonneg_Rmult_eq r1 r2 :
nonneg (r1 *nn* r2) = r1 * r2.
Lemma subNonnegTot_le_Rminus (r1 r2 : nonnegreal) :
r1 - r2 <= (r1 -nn- r2).
Lemma subNonnegTot_plus_lt_Rminus (a b : nonnegreal) c z :
a -nn- b + z < c -> a - b + z < c.
This page has been generated by coqdoc