Commit 96f51ca0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make I.empty part of IntervalOps.

parent 4ebc8e4a
......@@ -75,7 +75,20 @@ Qed.
Lemma zero_correct :
convert zero = Interval.Ibnd (Xreal 0) (Xreal 0).
Proof. now simpl; rewrite F.zero_correct. Qed.
Proof.
simpl.
now rewrite F.zero_correct.
Qed.
Lemma empty_correct :
forall x, contains (convert empty) x -> False.
Proof.
intros [|x].
easy.
simpl.
rewrite F.fromZ_correct, F.zero_correct.
lra.
Qed.
Definition bounded xi :=
match xi with
......
......@@ -254,6 +254,7 @@ Parameter type : Type.
Parameter convert : type -> interval.
Parameter zero : type.
Parameter nai : type.
Parameter empty : type.
Parameter bnd : bound_type -> bound_type -> type.
Parameter bnd_correct :
......@@ -266,6 +267,9 @@ Parameter zero_correct :
Parameter nai_correct :
convert nai = Inan.
Parameter empty_correct :
forall x, contains (convert empty) x -> False.
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