CoRN.ftc.MoreIntervals
Generalized Intervals
Definitions and Basic Results
Inductive interval : Type :=
| (-∞,+∞) : interval
| (⋅,+∞) : IR → interval
| (-∞,⋅) : IR → interval
| [⋅,+∞) : IR → interval
| (-∞,⋅] : IR → interval
| (⋅,⋅) : IR → IR → interval
| (⋅,⋅] : IR → IR → interval
| [⋅,⋅) : IR → IR → interval
| [⋅,⋅] : IR → IR → interval.
To each interval a predicate (set) is assigned by the following map:
Definition iprop (I : interval) (x : IR) : CProp :=
match I with
| (-∞,+∞) ⇒ True
| (-∞,⋅) b ⇒ x [<] b
| (⋅,+∞) a ⇒ a [<] x
| (-∞,⋅] b ⇒ x [<=] b
| [⋅,+∞) a ⇒ a [<=] x
| (⋅,⋅) a b ⇒ a [<] x and x [<] b
| (⋅,⋅] a b ⇒ a [<] x and x [<=] b
| [⋅,⋅) a b ⇒ a [<=] x and x [<] b
| [⋅,⋅] a b ⇒ a [<=] x and x [<=] b
end.
This map is made into a coercion, so that intervals
are really subsets of reals.
We now define what it means for an interval to be nonvoid, proper,
finite and compact in the obvious way.
Definition nonvoid (I : interval) : CProp :=
match I with
| (-∞,+∞) ⇒ True
| (-∞,⋅) b ⇒ True
| (⋅,+∞) a ⇒ True
| (-∞,⋅] b ⇒ True
| [⋅,+∞) a ⇒ True
| (⋅,⋅) a b ⇒ a [<] b
| (⋅,⋅] a b ⇒ a [<] b
| [⋅,⋅) a b ⇒ a [<] b
| [⋅,⋅] a b ⇒ a [<=] b
end.
Definition proper (I : interval) : CProp :=
match I with
| (-∞,+∞) ⇒ True
| (-∞,⋅) b ⇒ True
| (⋅,+∞) a ⇒ True
| (-∞,⋅] b ⇒ True
| [⋅,+∞) a ⇒ True
| (⋅,⋅) a b ⇒ a [<] b
| (⋅,⋅] a b ⇒ a [<] b
| [⋅,⋅) a b ⇒ a [<] b
| [⋅,⋅] a b ⇒ a [<] b
end.
Definition finite (I : interval) : CProp :=
match I with
| (-∞,+∞) ⇒ False
| (-∞,⋅) b ⇒ False
| (⋅,+∞) a ⇒ False
| (-∞,⋅] b ⇒ False
| [⋅,+∞) a ⇒ False
| (⋅,⋅) a b ⇒ True
| (⋅,⋅] a b ⇒ True
| [⋅,⋅) a b ⇒ True
| [⋅,⋅] a b ⇒ True
end.
Definition compact_ (I : interval) : CProp :=
match I with
| (-∞,+∞) ⇒ False
| (-∞,⋅) b ⇒ False
| (⋅,+∞) a ⇒ False
| (-∞,⋅] b ⇒ False
| [⋅,+∞) a ⇒ False
| (⋅,⋅) a b ⇒ False
| (⋅,⋅] a b ⇒ False
| [⋅,⋅) a b ⇒ False
| [⋅,⋅] a b ⇒ a [<=] b
end.
Finite intervals have a left end and a right end.
Definition left_end (I : interval) : finite I → IR.
Proof.
intro.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; rename X into H.
inversion H.
inversion H.
inversion H.
inversion H.
inversion H.
apply c.
apply c.
apply c.
apply c.
Defined.
Definition right_end (I : interval) : finite I → IR.
Proof.
intro.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; rename X into H.
inversion H.
inversion H.
inversion H.
inversion H.
inversion H.
apply c0.
apply c0.
apply c0.
apply c0.
Defined.
Some trivia: compact intervals are finite; proper intervals are nonvoid; an interval is nonvoid iff it contains some point.
Lemma compact_finite : ∀ I : interval, compact_ I → finite I.
intros; induction I as [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; auto.
Qed.
Lemma proper_nonvoid : ∀ I : interval, proper I → nonvoid I.
Proof.
intro.
elim I; simpl in |- *; intros; auto.
apply less_leEq; auto.
Qed.
Lemma nonvoid_point : ∀ I : interval, nonvoid I → {x : IR | I x}.
Proof.
intro.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try rename X into H.
∃ ZeroR; auto.
∃ (c[+][1]); apply less_plusOne.
∃ (c[-][1]); apply shift_minus_less; apply less_plusOne.
∃ c; apply leEq_reflexive.
∃ c; apply leEq_reflexive.
∃ (c[+] (c0[-]c) [/]TwoNZ); split.
astepl (c[+][0]); apply plus_resp_less_lft.
apply div_resp_pos.
apply pos_two.
apply shift_less_minus; astepl c; auto.
rstepr (c[+] (c0[-]c)).
apply plus_resp_less_lft.
apply pos_div_two'.
apply shift_less_minus; astepl c; auto.
∃ c0; split; auto; apply leEq_reflexive.
∃ c; split; auto; apply leEq_reflexive.
∃ c; split; [ apply leEq_reflexive | auto ].
Qed.
Lemma nonvoid_char : ∀ (I : interval) (x : IR), I x → nonvoid I.
Proof.
intro; induction I; simpl in |- *; intros x H; auto; inversion_clear H.
apply less_transitive_unfolded with x; auto.
apply less_leEq_trans with x; auto.
apply leEq_less_trans with x; auto.
apply leEq_transitive with x; auto.
Qed.
For practical reasons it helps to define left end and right end of compact intervals.
Definition Lend I (H : compact_ I) := left_end I (compact_finite I H).
Definition Rend I (H : compact_ I) := right_end I (compact_finite I H).
In a compact interval, the left end is always less than or equal
to the right end.
Lemma Lend_leEq_Rend : ∀ I cI, Lend I cI [<=] Rend I cI.
Proof.
intro; elim I; simpl in |- *; intros; try inversion cI; auto.
Qed.
Some nice characterizations of inclusion:
Lemma compact_included : ∀ a b Hab (I : interval),
I a → I b → included (compact a b Hab) I.
Proof.
induction I; red in |- *; simpl in |- *; intros X X0 x X1;
try inversion_clear X; try inversion_clear X0; try inversion_clear X1.
auto.
apply less_leEq_trans with a; auto.
apply leEq_less_trans with b; auto.
apply leEq_transitive with a; auto.
apply leEq_transitive with b; auto.
split; [ apply less_leEq_trans with a | apply leEq_less_trans with b ]; auto.
split; [ apply less_leEq_trans with a | apply leEq_transitive with b ]; auto.
split; [ apply leEq_transitive with a | apply leEq_less_trans with b ]; auto.
split; [ apply leEq_transitive with a | apply leEq_transitive with b ]; auto.
Qed.
Lemma included_interval' : ∀ (I : interval) x y z w, I x → I y → I z → I w →
∀ H, included (compact (Min x z) (Max y w) H) I.
Proof.
intros I x y z w; induction I; simpl in |- *; intros X X0 X1 X2 H; red in |- *; intros t Ht;
inversion_clear Ht; simpl in |- *; try inversion_clear X;
try inversion_clear X0; try inversion_clear X1; try inversion_clear X2; try split.
apply less_leEq_trans with (Min x z); try apply less_Min; auto.
apply leEq_less_trans with (Max y w); try apply Max_less; auto.
apply leEq_transitive with (Min x z); try apply leEq_Min; auto.
apply leEq_transitive with (Max y w); try apply Max_leEq; auto.
apply less_leEq_trans with (Min x z); try apply less_Min; auto.
apply leEq_less_trans with (Max y w); try apply Max_less; auto.
apply less_leEq_trans with (Min x z); try apply less_Min; auto.
apply leEq_transitive with (Max y w); try apply Max_leEq; auto.
apply leEq_transitive with (Min x z); try apply leEq_Min; auto.
apply leEq_less_trans with (Max y w); try apply Max_less; auto.
apply leEq_transitive with (Min x z); try apply leEq_Min; auto.
apply leEq_transitive with (Max y w); try apply Max_leEq; auto.
Qed.
Lemma included_interval : ∀ (I : interval) x y, I x → I y →
∀ H, included (compact (Min x y) (Max x y) H) I.
Proof.
intros; apply included_interval'; auto.
Qed.
A weirder inclusion result.
Lemma included3_interval : ∀ (I : interval) x y z Hxyz, I x → I y → I z →
included (compact (Min (Min x y) z) (Max (Max x y) z) Hxyz) I.
Proof.
intros I x y z Hxyz H H0 H1.
apply included_interval'; auto.
apply (included_interval I x y H H0 (Min_leEq_Max _ _)).
apply compact_inc_lft.
apply (included_interval I x y H H0 (Min_leEq_Max _ _)).
apply compact_inc_rht.
Qed.
Finally, all intervals are characterized by well defined predicates.
Lemma iprop_wd : ∀ I : interval, pred_wd _ I.
Proof.
induction I; unfold iprop in |- *; red in |- *; intros x y X X0;
try inversion_clear X; try inversion X0.
auto.
astepr x; auto.
astepl x; auto.
astepr x; auto.
astepl x; auto.
split.
astepr x; auto.
astepl x; auto.
split.
astepr x; auto.
astepl x; auto.
split.
astepr x; auto.
astepl x; auto.
split.
astepr x; auto.
astepl x; auto.
Qed.
End Intervals.
Implicit Arguments Lend [I].
Implicit Arguments Rend [I].
Section Compact_Constructions.
Section Single_Compact_Interval.
Constructions with Compact Intervals
Variable P : IR → CProp.
Hypothesis wdP : pred_wd IR P.
Variable x : IR.
Hypothesis Hx : P x.
Definition compact_single := Compact (leEq_reflexive _ x).
This interval contains x and only (elements equal to) x; furthermore, for every (well-defined) P, if x∈P then [x,x]⊆P.
Lemma compact_single_prop : compact_single x.
Proof.
split; apply leEq_reflexive.
Qed.
Lemma compact_single_pt : ∀ y : IR, compact_single y → x [=] y.
Proof.
intros y H.
inversion_clear H; apply leEq_imp_eq; auto.
Qed.
Lemma compact_single_inc : included compact_single P.
Proof.
red in |- *; intros.
apply wdP with x.
auto.
apply compact_single_pt; auto.
Qed.
End Single_Compact_Interval.
The special case of intervals is worth singling out, as one of the hypothesis becomes a theorem.
Now for more interesting and important results.
Let I be a proper interval and x be a point of I. Then there is
a proper compact interval [a,b] such that x∈[a,b]⊆I.
Section Proper_Compact_with_One_or_Two_Points.
Definition compact_in_interval I (pI : proper I) x (Hx : I x) : interval.
Proof.
intros; destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros.
apply ([⋅,⋅] x (x[+][1])).
apply ([⋅,⋅] x (x[+][1])).
apply ([⋅,⋅] (x[-][1]) x).
apply ([⋅,⋅] x (x[+][1])).
apply ([⋅,⋅] (x[-][1]) x).
apply ([⋅,⋅] (x[-] (x[-]c) [/]TwoNZ) (x[+] (c0[-]x) [/]TwoNZ)).
apply ([⋅,⋅] (x[-] (x[-]c) [/]TwoNZ) (x[+] (c0[-]x) [/]TwoNZ)).
apply ([⋅,⋅] (x[-] (x[-]c) [/]TwoNZ) (x[+] (c0[-]x) [/]TwoNZ)).
apply ([⋅,⋅] c c0).
Defined.
Lemma compact_compact_in_interval : ∀ I pI x Hx,
compact_ (compact_in_interval I pI x Hx).
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx; try apply ts; apply less_leEq.
apply less_plusOne.
apply less_plusOne.
apply shift_minus_less; apply less_plusOne.
apply less_plusOne.
apply shift_minus_less; apply less_plusOne.
eapply less_transitive_unfolded; [ apply cip1'' | apply cip1'''' ]; auto.
eapply less_leEq_trans; [ apply cip1'' | apply cip1''' ]; auto.
eapply leEq_less_trans; [ apply cip1' | apply cip1'''' ]; auto.
auto.
Qed.
Lemma proper_compact_in_interval : ∀ I pI x Hx,
proper (compact_in_interval I pI x Hx).
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx.
apply less_plusOne.
apply less_plusOne.
apply shift_minus_less; apply less_plusOne.
apply less_plusOne.
apply shift_minus_less; apply less_plusOne.
eapply less_transitive_unfolded; [ apply cip1'' | apply cip1'''' ]; auto.
eapply less_leEq_trans; [ apply cip1'' | apply cip1''' ]; auto.
eapply leEq_less_trans; [ apply cip1' | apply cip1'''' ]; auto.
auto.
Qed.
Lemma proper_compact_in_interval' : ∀ I pI x Hx
(H : compact_ (compact_in_interval I pI x Hx)), Lend H [<] Rend H.
Proof.
do 4 intro.
cut (proper (compact_in_interval I pI x Hx)).
2: apply proper_compact_in_interval.
elim (compact_in_interval I pI x Hx); intros; try inversion H.
simpl in |- *; simpl in H; auto.
Qed.
Lemma included_compact_in_interval : ∀ I pI x Hx,
included (compact_in_interval I pI x Hx) I.
Proof.
induction I; simpl in |- *; intros X x X0; try inversion_clear Hx; red in |- *;
simpl in |- *; intros x0 X1; try inversion_clear X; try inversion_clear X0;
try inversion_clear X1; auto.
apply less_leEq_trans with x; auto.
apply leEq_less_trans with x; auto.
apply leEq_transitive with x; auto.
apply leEq_transitive with x; auto.
split.
apply cip2' with x; auto.
apply cip3' with x; auto.
split.
apply cip2' with x; auto.
apply cip3 with x; auto.
split.
apply cip2 with x; auto.
apply cip3' with x; auto.
Qed.
Lemma iprop_compact_in_interval : ∀ I pI x Hx, compact_in_interval I pI x Hx x.
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx; split; auto; try apply leEq_reflexive.
apply less_leEq; apply less_plusOne.
apply less_leEq; apply less_plusOne.
apply less_leEq; apply shift_minus_less; apply less_plusOne.
apply less_leEq; apply less_plusOne.
apply less_leEq; apply shift_minus_less; apply less_plusOne.
apply less_leEq; apply cip1''; auto.
apply less_leEq; apply cip1''''; auto.
apply less_leEq; apply cip1''; auto.
apply less_leEq; apply cip1''''; auto.
Qed.
Lemma iprop_compact_in_interval' : ∀ I pI x Hx
(H : compact_ (compact_in_interval I pI x Hx)) H', compact (Lend H) (Rend H) H' x.
Proof.
do 4 intro.
cut (compact_in_interval I pI x Hx x).
2: apply iprop_compact_in_interval.
elim (compact_in_interval I pI x Hx); intros; try inversion H.
simpl in |- *; auto.
Qed.
Lemma iprop_compact_in_interval_inc1 : ∀ I pI x Hx
(H : compact_ (compact_in_interval I pI x Hx)) H',
included (compact (Lend H) (Rend H) H') (compact_in_interval I pI x Hx).
Proof.
do 4 intro.
elim (compact_in_interval I pI x Hx); intros; try inversion H.
unfold compact in |- *; simpl in |- *; Included.
Qed.
Lemma iprop_compact_in_interval_inc2 : ∀ I pI x Hx
(H : compact_ (compact_in_interval I pI x Hx)) H',
included (compact_in_interval I pI x Hx) (compact (Lend H) (Rend H) H').
Proof.
do 4 intro.
elim (compact_in_interval I pI x Hx); intros; try inversion H.
unfold compact in |- *; simpl in |- *; Included.
Qed.
If x [=] y then the construction yields the same interval whether we
use x or y in its definition. This property is required at some
stage, which is why we formalized this result as a functional
definition rather than as an existential formula.
Lemma compact_in_interval_wd1 : ∀ I pI x Hx y Hy
(H : compact_ (compact_in_interval I pI x Hx))
(H' : compact_ (compact_in_interval I pI y Hy)),
x [=] y → Lend H [=] Lend H'.
Proof.
intro I; elim I; simpl in |- *; intros; algebra.
Qed.
Lemma compact_in_interval_wd2 : ∀ I pI x Hx y Hy
(H : compact_ (compact_in_interval I pI x Hx))
(H' : compact_ (compact_in_interval I pI y Hy)),
x [=] y → Rend H [=] Rend H'.
Proof.
intro I; elim I; simpl in |- *; intros; algebra.
Qed.
We can make an analogous construction for two points.
Definition compact_in_interval2 I (pI : proper I) x y : I x → I y → interval.
Proof.
intros.
set (z1 := Min x y) in ×.
set (z2 := Max x y) in ×.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros.
apply ([⋅,⋅] z1 (z2[+][1])).
apply ([⋅,⋅] z1 (z2[+][1])).
apply ([⋅,⋅] (z1[-][1]) z2).
apply ([⋅,⋅] z1 (z2[+][1])).
apply ([⋅,⋅] (z1[-][1]) z2).
apply ([⋅,⋅] (z1[-] (z1[-]c) [/]TwoNZ) (z2[+] (c0[-]z2) [/]TwoNZ)).
apply ([⋅,⋅] (z1[-] (z1[-]c) [/]TwoNZ) (z2[+] (c0[-]z2) [/]TwoNZ)).
apply ([⋅,⋅] (z1[-] (z1[-]c) [/]TwoNZ) (z2[+] (c0[-]z2) [/]TwoNZ)).
apply ([⋅,⋅] c c0).
Defined.
Lemma compact_compact_in_interval2 : ∀ I pI x y Hx Hy,
compact_ (compact_in_interval2 I pI x y Hx Hy).
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx; try inversion_clear Hy;
try apply ts; apply less_leEq.
apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ].
apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ].
apply shift_minus_less; apply leEq_less_trans with (Max x y);
[ apply Min_leEq_Max | apply less_plusOne ].
apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ].
apply shift_minus_less; apply leEq_less_trans with (Max x y);
[ apply Min_leEq_Max | apply less_plusOne ].
eapply less_transitive_unfolded; [ apply cip1''
| eapply leEq_less_trans; [ apply Min_leEq_Max | apply cip1'''' ] ];
try apply less_Min; try apply Max_less; auto.
eapply less_leEq_trans; [ apply cip1''
| eapply leEq_transitive; [ apply Min_leEq_Max | apply cip1''' ] ];
try apply less_Min; try apply Max_leEq; auto.
eapply leEq_less_trans; [ apply cip1'
| eapply leEq_less_trans; [ apply Min_leEq_Max | apply cip1'''' ] ];
try apply leEq_Min; try apply Max_less; auto.
auto.
Qed.
Lemma proper_compact_in_interval2 : ∀ I pI x y Hx Hy,
proper (compact_in_interval2 I pI x y Hx Hy).
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx; try inversion_clear Hy.
apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ].
apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ].
apply shift_minus_less; apply leEq_less_trans with (Max x y);
[ apply Min_leEq_Max | apply less_plusOne ].
apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ].
apply shift_minus_less; apply leEq_less_trans with (Max x y);
[ apply Min_leEq_Max | apply less_plusOne ].
eapply less_transitive_unfolded; [ apply cip1''
| eapply leEq_less_trans; [ apply Min_leEq_Max | apply cip1'''' ] ];
try apply less_Min; try apply Max_less; auto.
eapply less_leEq_trans; [ apply cip1''
| eapply leEq_transitive; [ apply Min_leEq_Max | apply cip1''' ] ];
try apply less_Min; try apply Max_leEq; auto.
eapply leEq_less_trans; [ apply cip1'
| eapply leEq_less_trans; [ apply Min_leEq_Max | apply cip1'''' ] ];
try apply leEq_Min; try apply Max_less; auto.
auto.
Qed.
Lemma proper_compact_in_interval2' : ∀ I pI x y Hx Hy H,
Lend (I:=compact_in_interval2 I pI x y Hx Hy) H [<]
Rend (I:=compact_in_interval2 I pI x y Hx Hy) H.
Proof.
do 6 intro.
cut (proper (compact_in_interval2 I pI x y Hx Hy)).
2: apply proper_compact_in_interval2.
elim (compact_in_interval2 I pI x y Hx Hy); intros; try inversion H.
simpl in |- *; simpl in H; auto.
Qed.
Lemma included_compact_in_interval2 : ∀ I pI x y Hx Hy,
included (compact_in_interval2 I pI x y Hx Hy) I.
Proof.
induction I; simpl in |- *; intros; try inversion_clear Hx as (H,H0);
try inversion_clear Hy as (H1,H2); red in |- *; simpl in |- *;
intros x0 X; try inversion_clear X; auto.
apply less_leEq_trans with (Min x y); try apply less_Min; auto.
apply leEq_less_trans with (Max x y); try apply Max_less; auto.
apply leEq_transitive with (Min x y); try apply leEq_Min; auto.
apply leEq_transitive with (Max x y); try apply Max_leEq; auto.
split.
apply cip2' with (Min x y); try apply less_Min; auto.
apply cip3' with (Max x y); try apply Max_less; auto.
split.
apply cip2' with (Min x y); try apply less_Min; auto.
apply cip3 with (Max x y); try apply Max_leEq; auto.
split.
apply cip2 with (Min x y); try apply leEq_Min; auto.
apply cip3' with (Max x y); try apply Max_less; auto.
Qed.
Lemma iprop_compact_in_interval2x : ∀ I pI x y Hx Hy,
compact_in_interval2 I pI x y Hx Hy x.
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx; try inversion_clear Hy;
split; auto; try apply Min_leEq_lft; try apply lft_leEq_Max.
apply less_leEq; apply leEq_less_trans with (Max x y); [ apply lft_leEq_Max | apply less_plusOne ].
apply less_leEq; apply leEq_less_trans with (Max x y); [ apply lft_leEq_Max | apply less_plusOne ].
apply less_leEq; apply shift_minus_less; apply leEq_less_trans with x;
[ apply Min_leEq_lft | apply less_plusOne ].
apply less_leEq; apply leEq_less_trans with (Max x y); [ apply lft_leEq_Max | apply less_plusOne ].
apply less_leEq; apply shift_minus_less; apply leEq_less_trans with x;
[ apply Min_leEq_lft | apply less_plusOne ].
apply less_leEq; eapply less_leEq_trans; [ apply cip1'' | apply Min_leEq_lft ]; try apply less_Min;
auto.
apply less_leEq; apply leEq_less_trans with (Max x y);
[ apply lft_leEq_Max | apply cip1'''' ]; try apply Max_less; auto.
apply less_leEq; eapply less_leEq_trans; [ apply cip1'' | apply Min_leEq_lft ]; try apply less_Min;
auto.
apply leEq_transitive with (Max x y); [ apply lft_leEq_Max | apply cip1''' ];
try apply Max_leEq; auto.
eapply leEq_transitive; [ apply cip1' | apply Min_leEq_lft ]; try apply leEq_Min; auto.
apply less_leEq; apply leEq_less_trans with (Max x y);
[ apply lft_leEq_Max | apply cip1'''' ]; try apply Max_less; auto.
Qed.
Lemma iprop_compact_in_interval2y : ∀ I pI x y Hx Hy,
compact_in_interval2 I pI x y Hx Hy y.
Proof.
intro.
elim I; simpl in |- *; intros; try inversion_clear Hx; try inversion_clear Hy;
split; auto; try apply Min_leEq_rht; try apply rht_leEq_Max.
apply less_leEq; apply leEq_less_trans with (Max x y); [ apply rht_leEq_Max | apply less_plusOne ].
apply less_leEq; apply leEq_less_trans with (Max x y); [ apply rht_leEq_Max | apply less_plusOne ].
apply less_leEq; apply shift_minus_less; apply leEq_less_trans with y;
[ apply Min_leEq_rht | apply less_plusOne ].
apply less_leEq; apply leEq_less_trans with (Max x y); [ apply rht_leEq_Max | apply less_plusOne ].
apply less_leEq; apply shift_minus_less; apply leEq_less_trans with y;
[ apply Min_leEq_rht | apply less_plusOne ].
apply less_leEq; eapply less_leEq_trans; [ apply cip1'' | apply Min_leEq_rht ]; try apply less_Min;
auto.
apply less_leEq; apply leEq_less_trans with (Max x y);
[ apply rht_leEq_Max | apply cip1'''' ]; try apply Max_less; auto.
apply less_leEq; eapply less_leEq_trans; [ apply cip1'' | apply Min_leEq_rht ]; try apply less_Min;
auto.
apply leEq_transitive with (Max x y); [ apply rht_leEq_Max | apply cip1''' ];
try apply Max_leEq; auto.
eapply leEq_transitive; [ apply cip1' | apply Min_leEq_rht ]; try apply leEq_Min; auto.
apply less_leEq; apply leEq_less_trans with (Max x y);
[ apply rht_leEq_Max | apply cip1'''' ]; try apply Max_less; auto.
Qed.
Lemma iprop_compact_in_interval2x' : ∀ I pI x y Hx Hy
(H : compact_ (compact_in_interval2 I pI x y Hx Hy)) H',
compact (Lend H) (Rend H) H' x.
Proof.
do 6 intro.
cut (compact_in_interval2 I pI x y Hx Hy x).
2: apply iprop_compact_in_interval2x.
elim (compact_in_interval2 I pI x y Hx Hy); intros; try inversion H.
simpl in |- *; auto.
Qed.
Lemma iprop_compact_in_interval2y' : ∀ I pI x y Hx Hy
(H : compact_ (compact_in_interval2 I pI x y Hx Hy)) H',
compact (Lend H) (Rend H) H' y.
Proof.
do 6 intro.
cut (compact_in_interval2 I pI x y Hx Hy y).
2: apply iprop_compact_in_interval2y.
elim (compact_in_interval2 I pI x y Hx Hy); intros; try inversion H.
simpl in |- *; auto.
Qed.
Lemma iprop_compact_in_interval2_inc1 : ∀ I pI x y Hx Hy
(H : compact_ (compact_in_interval2 I pI x y Hx Hy)) H',
included (compact (Lend H) (Rend H) H') (compact_in_interval2 I pI x y Hx Hy).
Proof.
do 6 intro.
elim (compact_in_interval2 I pI x y Hx Hy); intros; try inversion H.
unfold compact in |- *; unfold iprop in |- *; simpl in |- *; Included.
Qed.
Lemma iprop_compact_in_interval2_inc2 : ∀ I pI x y Hx Hy
(H : compact_ (compact_in_interval2 I pI x y Hx Hy)) H',
included (compact_in_interval2 I pI x y Hx Hy) (compact (Lend H) (Rend H) H').
Proof.
do 6 intro.
elim (compact_in_interval2 I pI x y Hx Hy); intros; try inversion H.
unfold compact in |- *; unfold iprop in |- *; simpl in |- *; Included.
Qed.
Lemma compact_in_interval_x_lft : ∀ I pI x y Hx Hy H H',
Lend (I:=compact_in_interval2 I pI x y Hx Hy) H [<=]
Lend (I:=compact_in_interval I pI x Hx) H'.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try apply minus_resp_leEq;
try apply Min_leEq_lft; try apply leEq_reflexive;
(rstepl (c[+] (Min x y[-]c) [/]TwoNZ); rstepr (c[+] (x[-]c) [/]TwoNZ);
apply plus_resp_leEq_lft; apply div_resp_leEq;
[ apply pos_two | apply minus_resp_leEq; apply Min_leEq_lft ]).
Qed.
Lemma compact_in_interval_y_lft : ∀ I pI x y Hx Hy H H',
Lend (I:=compact_in_interval2 I pI x y Hx Hy) H [<=]
Lend (I:=compact_in_interval I pI y Hy) H'.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try apply minus_resp_leEq;
try apply Min_leEq_rht; try apply leEq_reflexive;
(rstepl (c[+] (Min x y[-]c) [/]TwoNZ); rstepr (c[+] (y[-]c) [/]TwoNZ);
apply plus_resp_leEq_lft; apply div_resp_leEq;
[ apply pos_two | apply minus_resp_leEq; apply Min_leEq_rht ]).
Qed.
Lemma compact_in_interval_x_rht : ∀ I pI x y Hx Hy H H',
Rend (I:=compact_in_interval I pI x Hx) H [<=]
Rend (I:=compact_in_interval2 I pI x y Hx Hy) H'.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try apply plus_resp_leEq;
try apply lft_leEq_Max; try apply leEq_reflexive;
(rstepl (c0[-] (c0[-]x) [/]TwoNZ); rstepr (c0[-] (c0[-]Max x y) [/]TwoNZ);
unfold cg_minus in |- *; apply plus_resp_leEq_lft; apply inv_resp_leEq; apply div_resp_leEq;
[ apply pos_two | apply plus_resp_leEq_lft; apply inv_resp_leEq; apply lft_leEq_Max ]).
Qed.
Lemma compact_in_interval_y_rht : ∀ I pI x y Hx Hy H H',
Rend (I:=compact_in_interval I pI y Hy) H [<=]
Rend (I:=compact_in_interval2 I pI x y Hx Hy) H'.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try apply plus_resp_leEq;
try apply rht_leEq_Max; try apply leEq_reflexive;
(rstepl (c0[-] (c0[-]y) [/]TwoNZ); rstepr (c0[-] (c0[-]Max x y) [/]TwoNZ);
unfold cg_minus in |- *; apply plus_resp_leEq_lft; apply inv_resp_leEq; apply div_resp_leEq;
[ apply pos_two | apply plus_resp_leEq_lft; apply inv_resp_leEq; apply rht_leEq_Max ]).
Qed.
End Proper_Compact_with_One_or_Two_Points.
Compact intervals are exactly compact intervals(!).
Lemma interval_compact_inc : ∀ I (cI : compact_ I) H,
included I (compact (Lend cI) (Rend cI) H).
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0];intros; try inversion cI.
generalize c c0 cI H; clear H cI c0 c.
simpl in |- *; intros a b Hab Hab'.
intros x H.
simpl in H.
inversion_clear H; split; auto.
Qed.
Lemma compact_interval_inc : ∀ I (cI : compact_ I) H,
included (compact (Lend cI) (Rend cI) H) I.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI H; clear H cI c0 c.
simpl in |- *; intros a b Hab.
intros H x H0.
inversion_clear H0; split; auto.
Qed.
A generalization of the previous results: if [a,b]⊆J
and J is proper, then we can find a proper interval [a',b'] such that
[a,b]⊆[a',b']⊆J.
Lemma compact_proper_in_interval : ∀ (J : interval) a b Hab,
included (compact a b Hab) J → proper J → {a' : IR | {b' : IR | {Hab' : _ |
included (compact a' b' (less_leEq _ _ _ Hab')) J |
included (Compact Hab) (Compact (less_leEq _ _ _ Hab'))}}}.
Proof.
intros J a b Hab H H0.
∃ (Lend (compact_compact_in_interval2 J H0 a b (H _ (compact_inc_lft _ _ Hab))
(H _ (compact_inc_rht _ _ Hab)))).
∃ (Rend (compact_compact_in_interval2 J H0 a b (H _ (compact_inc_lft _ _ Hab))
(H _ (compact_inc_rht _ _ Hab)))).
∃ (proper_compact_in_interval2' _ _ _ _ _ _
(compact_compact_in_interval2 J H0 a b (H _ (compact_inc_lft _ _ Hab))
(H _ (compact_inc_rht _ _ Hab)))).
eapply included_trans.
apply compact_interval_inc.
apply included_compact_in_interval2.
apply included_compact.
apply iprop_compact_in_interval2x'.
apply iprop_compact_in_interval2y'.
Qed.
End Compact_Constructions.
Section Functions.
Properties of Functions in Intervals
Variable n : nat.
Variable I : interval.
Definition Continuous F := included I (Dom F) and (∀ a b (Hab : a [<=] b),
included (Compact Hab) I → Continuous_I Hab F).
Definition Derivative (pI : proper I) F G := included I (Dom F) and included I (Dom G) and (∀ a b Hab,
included (Compact (less_leEq _ a b Hab)) I → Derivative_I Hab F G).
Definition Diffble (pI : proper I) F := included I (Dom F) and (∀ a b Hab,
included (Compact (less_leEq _ a b Hab)) I → Diffble_I Hab F).
Definition Derivative_n (pI : proper I) F G := included I (Dom F) and included I (Dom G) and
(∀ a b Hab, included (Compact (less_leEq _ a b Hab)) I → Derivative_I_n Hab n F G).
Definition Diffble_n (pI : proper I) F := included I (Dom F) and (∀ a b Hab,
included (Compact (less_leEq _ a b Hab)) I → Diffble_I_n Hab n F).
End Functions.
Section Reflexivity_Properties.
In the case of compact intervals, this definitions collapse to the old ones.
Lemma Continuous_Int :
∀ (I : interval) (cI : compact_ I) H (F : PartIR),
Continuous_I (a:=Lend cI) (b:=Rend cI) H F → Continuous I F.
Proof.
intros I cI H F H0.
cut (included I (compact (Lend cI) (Rend cI) H)).
2: apply interval_compact_inc; auto.
cut (included (compact (Lend cI) (Rend cI) H) I).
2: apply compact_interval_inc; auto.
generalize cI H H0; clear H0 H cI.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI H H0 X X0; clear X0 X H0 H cI c0 c.
simpl in |- *; intros a b Hab Hab' contF inc1 inc2.
split.
apply included_trans with (Compact Hab'); Included.
intros.
apply included_imp_contin with (Hab := Hab'); Included.
Qed.
Lemma Int_Continuous :
∀ (I : interval) (cI : compact_ I) H (F : PartIR),
Continuous I F → Continuous_I (a:=Lend cI) (b:=Rend cI) H F.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI H F X; clear X F H cI c0 c.
simpl in |- *; intros a b Hab Hab' F contF.
inversion_clear contF.
Contin.
Qed.
Lemma Derivative_Int :
∀ (I : interval) (cI : compact_ I) (pI : proper I) H (F F' : PartIR),
Derivative_I (a:=Lend cI) (b:=Rend cI) H F F' → Derivative I pI F F'.
Proof.
do 4 intro.
cut (included I (compact (Lend cI) (Rend cI) (less_leEq _ _ _ H))).
2: apply interval_compact_inc; auto.
cut (included (compact (Lend cI) (Rend cI) (less_leEq _ _ _ H)) I).
2: apply compact_interval_inc; auto.
generalize cI pI H; clear H cI pI.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI pI H X X0 F F' X1; clear X1 F' F X0 X H pI cI c0 c.
simpl in |- *; intros a b Hab Hnonv Hab' inc1 inc2 F F' derF.
split.
apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included.
split.
apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included.
intros c d Hcd' Hinc.
apply included_imp_deriv with (Hab := Hab'); Included.
Qed.
Lemma Int_Derivative :
∀ (I : interval) (cI : compact_ I) (pI : proper I) H (F F' : PartIR),
Derivative I pI F F' → Derivative_I (a:=Lend cI) (b:=Rend cI) H F F'.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI pI H F F' X; clear X F' F H pI cI c0 c.
simpl in |- *; intros a b Hab Hnonv Hab' F F' derF.
elim derF; intros H H0.
elim H0; intros H1 H2.
Included.
Qed.
Lemma Diffble_Int :
∀ (I : interval) (cI : compact_ I) (pI : proper I) H (F : PartIR),
Diffble_I (a:=Lend cI) (b:=Rend cI) H F → Diffble I pI F.
Proof.
do 4 intro.
cut (included I (compact (Lend cI) (Rend cI) (less_leEq _ _ _ H))).
2: apply interval_compact_inc; auto.
cut (included (compact (Lend cI) (Rend cI) (less_leEq _ _ _ H)) I).
2: apply compact_interval_inc; auto.
generalize cI pI H; clear H pI cI.
destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI pI H X X0 F X1; clear X1 F X0 X H pI cI c0 c.
simpl in |- *; intros a b Hab Hnonv Hab' inc1 inc2 F diffF.
red in |- *; simpl in |- ×.
split.
apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included.
intros c d Hcd' Hinc.
apply included_imp_diffble with (Hab := Hab'); auto.
Qed.
Lemma Int_Diffble :
∀ (I : interval) (cI : compact_ I) (pI : proper I) H (F : PartIR),
Diffble I pI F → Diffble_I (a:=Lend cI) (b:=Rend cI) H F.
Proof.
intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI.
generalize c c0 cI pI H F X; clear X F H pI cI c0 c.
simpl in |- *; intros a b Hab Hnonv Hab' F diffF.
inversion_clear diffF.
Included.
Qed.
End Reflexivity_Properties.
Section Lemmas.
Interestingly, inclusion and equality in an interval are also characterizable in a similar way:
Lemma included_imp_inc : ∀ (J : interval) P,
(∀ a b Hab, included (compact a b Hab) J → included (compact a b Hab) P) → included J P.
Proof.
intros J P H x H0.
apply (H _ _ (leEq_reflexive _ _) (compact_single_iprop J x H0)).
apply compact_inc_lft.
Qed.
Lemma included_Feq'' : ∀ I F G, proper I → (∀ a b Hab (Hab':=(less_leEq _ a b Hab)),
included (Compact Hab') I → Feq (Compact Hab') F G) → Feq I F G.
Proof.
intros I F G H H0.
apply eq_imp_Feq.
intros x H1.
elim (compact_proper_in_interval I x x (leEq_reflexive _ x)); Included.
2: exact (compact_single_iprop I x H1).
intros a Ha.
elim Ha; clear Ha.
intros b Hb.
elim Hb; clear Hb.
intros Hab H2 H3.
elim (H0 _ _ _ H2); intros.
apply a0; apply H3; apply compact_single_prop.
intros x H1.
elim (compact_proper_in_interval I x x (leEq_reflexive _ x)); Included.
2: exact (compact_single_iprop I x H1).
intros a Ha.
elim Ha; clear Ha.
intros b Hb.
elim Hb; clear Hb.
intros Hab H2 H3.
elim (H0 _ _ _ H2); intros.
inversion_clear b0.
apply X; apply H3; apply compact_single_prop.
intros x H1 Hx Hx'.
elim (compact_proper_in_interval I x x (leEq_reflexive _ x)); Included.
2: exact (compact_single_iprop I x H1).
intros a Ha.
elim Ha; clear Ha.
intros b Hb.
elim Hb; clear Hb.
intros Hab H2 H3.
elim (H0 _ _ _ H2); intros.
inversion_clear b0.
apply H4; apply H3; apply compact_single_prop.
Qed.
Lemma included_Feq' : ∀ (I : interval) F G,
(∀ a b Hab, included (compact a b Hab) I → Feq (Compact Hab) F G) → Feq I F G.
Proof.
intros I F G H.
apply eq_imp_Feq.
intros x H0.
elim (H x x (leEq_reflexive _ x) (compact_single_iprop I x H0)); intros.
apply a; apply compact_single_prop.
intros x H0.
elim (H x x (leEq_reflexive _ x) (compact_single_iprop I x H0)); intros.
inversion_clear b.
apply X; apply compact_single_prop.
intros x H0 Hx Hx'.
elim (H x x (leEq_reflexive _ x) (compact_single_iprop I x H0)); intros.
inversion_clear b.
apply H1; apply compact_single_prop.
Qed.
End Lemmas.
Hint Resolve included_interval included_interval' included3_interval
compact_single_inc compact_single_iprop included_compact_in_interval
iprop_compact_in_interval_inc1 iprop_compact_in_interval_inc2
included_compact_in_interval2 iprop_compact_in_interval2_inc1
iprop_compact_in_interval2_inc2 interval_compact_inc compact_interval_inc
iprop_wd: included.