Commit 830c8c7d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add I.real to check the validity of an interval.

parent c39aa028
......@@ -1413,8 +1413,7 @@ Definition taylor_integral :=
(* now we take the intersection of a naive and intelligent way of computing the integral *)
Definition taylor_integral_naive_intersection :=
let temp := I.mul prec (I.sub prec ib ia) (iF (I.join ia ib)) in
if I.subset I.nai temp then I.nai
else I.meet temp taylor_integral.
if I.real temp then I.meet temp taylor_integral else temp.
Lemma taylor_integral_correct :
contains
......@@ -1436,8 +1435,9 @@ Lemma taylor_integral_naive_intersection_correct :
Proof.
rewrite /taylor_integral_naive_intersection.
set tmp := I.mul prec (I.sub prec ib ia) (iF (I.join ia ib)).
case I.subset.
by rewrite I.nai_correct.
generalize (I.real_correct tmp).
case I.real ; intros Hr.
2: now destruct (I.convert tmp).
apply I.meet_correct.
apply J.contains_RInt => //.
intros x Hx.
......
......@@ -49,16 +49,21 @@ Definition bound_type := F.type.
Definition precision := F.precision.
Definition convert_bound := F.toX.
Definition convert xi :=
Definition convert (xi : type) :=
match xi with
| Inan => Interval.Inan
| Ibnd l u => Interval.Ibnd (F.toX l) (F.toX u)
end.
Definition nai := @Inan F.type.
Definition bnd := @Ibnd F.type.
Definition zero := Ibnd F.zero F.zero.
Definition empty := Ibnd (F.fromZ 1) F.zero.
Definition nai : type := @Inan F.type.
Definition bnd l u : type := Ibnd l u.
Definition zero : type := Ibnd F.zero F.zero.
Definition empty : type := Ibnd (F.fromZ 1) F.zero.
Definition real (xi : type) :=
match xi with
| Inan => false
| Ibnd _ _ => true
end.
Lemma bnd_correct :
forall l u,
......@@ -90,6 +95,12 @@ rewrite F.fromZ_correct, F.zero_correct.
lra.
Qed.
Lemma real_correct :
forall xi, real xi = match convert xi with Interval.Inan => false | _ => true end.
Proof.
now intros [|xl xu].
Qed.
Definition bounded xi :=
match xi with
| Ibnd xl xu => F.real xl && F.real xu
......
......@@ -77,6 +77,12 @@ intros xi.
now case xi ; split.
Qed.
Lemma contains_Inan :
forall xi x, xi = Inan -> contains xi x.
Proof.
now intros xi x ->.
Qed.
Definition le_upper x y :=
match y with
| Xnan => True
......@@ -287,6 +293,7 @@ Parameter zero : type.
Parameter nai : type.
Parameter empty : type.
Parameter bnd : bound_type -> bound_type -> type.
Parameter real : type -> bool.
Parameter bnd_correct :
forall l u,
......@@ -301,6 +308,9 @@ Parameter nai_correct :
Parameter empty_correct :
forall x, contains (convert empty) x -> False.
Parameter real_correct :
forall xi, real xi = match convert xi with Inan => false | _ => true end.
Local Notation subset_ := subset.
Parameter subset : type -> type -> bool.
......
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