Commit 866daf89 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add functions I.lower_complement and I.upper_complement.

parent 96f51ca0
......@@ -170,6 +170,18 @@ Definition upper_extent xi :=
| _ => Inan
end.
Definition lower_complement xi :=
match xi with
| Ibnd xl _ => if F.real xl then Ibnd F.nan xl else empty
| Inan => empty
end.
Definition upper_complement xi :=
match xi with
| Ibnd _ xu => if F.real xu then Ibnd xu F.nan else empty
| Inan => empty
end.
Definition whole := Ibnd F.nan F.nan.
Definition lower xi :=
......@@ -673,6 +685,46 @@ rewrite F.nan_correct.
exact I.
Qed.
Theorem lower_complement_correct :
forall xi x y,
contains (convert xi) (Xreal x) ->
contains (convert (lower_complement xi)) (Xreal y) ->
(y <= x)%R.
Proof.
intros [|xl xu] x y.
intros _ H.
now apply empty_correct in H.
intros [H _].
simpl.
rewrite F.real_correct.
case_eq (F.toX xl).
intros _ H'.
now apply empty_correct in H'.
intros l Hl [_ H'].
rewrite Hl in H, H'.
now apply Rle_trans with l.
Qed.
Theorem upper_complement_correct :
forall xi x y,
contains (convert xi) (Xreal x) ->
contains (convert (upper_complement xi)) (Xreal y) ->
(x <= y)%R.
Proof.
intros [|xl xu] x y.
intros _ H.
now apply empty_correct in H.
intros [_ H].
simpl.
rewrite F.real_correct.
case_eq (F.toX xu).
intros _ H'.
now apply empty_correct in H'.
intros u Hu [H' _].
rewrite Hu in H, H'.
now apply Rle_trans with u.
Qed.
Theorem whole_correct :
forall x,
contains (convert whole) (Xreal x).
......
......@@ -406,6 +406,21 @@ Parameter whole_correct :
forall x,
contains (convert whole) (Xreal x).
Parameter lower_complement : type -> type.
Parameter upper_complement : type -> type.
Parameter lower_complement_correct :
forall xi x y,
contains (convert xi) (Xreal x) ->
contains (convert (lower_complement xi)) (Xreal y) ->
(y <= x)%R.
Parameter upper_complement_correct :
forall xi x y,
contains (convert xi) (Xreal x) ->
contains (convert (upper_complement xi)) (Xreal y) ->
(x <= y)%R.
Parameter lower : type -> bound_type.
Parameter upper : type -> bound_type.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment