More results on floor/ceil (isint)

theories/analysis/RealLub.ec

@@ -117,3 +117,23 @@ apply eqr_le; split => [|_].
 rewrite -ler_pdivl_mull //; apply lub_le_ub => // x Ex.
 by rewrite ler_pdivl_mull //; smt(lub_upper_bound has_lub_scale). 
 qed.
+
+(* -------------------------------------------------------------------- *)
+lemma lub_cBf (E : real -> bool) : nonempty E =>
+  lub (fun x => exists y, E y /\ x = (ceil y - floor y)%r)
+    = b2r (exists x, E x /\ !isint x).
+proof.
+case=> z Ez; pose P (x : real) := exists (y : real),
+  E y /\ x = (ceil y - floor y)%r.
+have hlP: has_lub P; first split.
+- exists ((ceil z)%r - (floor z)%r); smt().
+  exists 1%r => x [y] [_ ->>]; smt(cBf_eq0P cBf_eq1P).
+rewrite RealOrder.eqr_le; split=> [|_].
+- apply: lub_le_ub => // x [y] [Ey ->>]; case: (isint y).
+  - by move/cBf_eq0P => -> /#.
+  - by move=> ^/cBf_eq1P -> Nint_y; rewrite iftrue //; exists y.
+- apply: lub_upper_bound => //; case: (exists x, E x /\ !isint x).
+  - by case=> x [Ex /cBf_eq1P Nint_x] @/P; exists x; rewrite Nint_x.
+  rewrite negb_exists /= => /(_ z); rewrite Ez /=.
+  by move/cBf_eq0P => int_z; exists z; rewrite int_z.
+qed.

theories/datatypes/Real.ec

@@ -249,6 +249,26 @@ proof. smt(floor_bound). qed.
 lemma floor_mono (x y : real) : x <= y => floor x <= floor y.
 proof. smt(floor_bound). qed.
 
+op isint (x : real) = exists n, x = n%r.
+
+lemma ceil_eqP (x : real) : (ceil x)%r = x <=> isint x.
+proof. by split=> [/#|[n ->>]]; last by rewrite from_int_ceil. qed.
+
+lemma floor_eqP (x : real) : (floor x)%r = x <=> isint x.
+proof. by split=> [/#|[n ->>]]; last by rewrite from_int_floor. qed.
+
+lemma cBf_eq0P (x : real) : (ceil x - floor x = 0) <=> isint x.
+proof.
+split=> [|[n ->>]]; last by rewrite from_int_floor from_int_ceil.
+smt(ceil_bound floor_bound).
+qed.
+
+lemma cBf_eq1P (x : real) : (ceil x - floor x = 1) <=> !isint x.
+proof.
+move=> /=; case: (isint x) => /= [/cBf_eq0P -> //|].
+smt(ceil_bound floor_bound).
+qed.
+
 (* -------------------------------------------------------------------- *)
 (* WARNING Lemmas used by tactics: *)
 lemma upto2_abs (x1 x2 x3 x4 x5:real):