From 90e65eb4da7fac5a6fb7690820d3bfacf0e7e178 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Thu, 22 May 2025 13:49:19 +0100 Subject: [PATCH] extend results on ceil 'for free' This opaquely defines ceil from floor so all results on ceil apply to floor and don't need copied. We still start copying them. --- theories/datatypes/Real.ec | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/theories/datatypes/Real.ec b/theories/datatypes/Real.ec index 0d2a8836f..ec068845d 100644 --- a/theories/datatypes/Real.ec +++ b/theories/datatypes/Real.ec @@ -218,12 +218,16 @@ instance field with real (* -------------------------------------------------------------------- *) op floor : real -> int. -op ceil : real -> int. +op [opaque] ceil : real -> int = fun (x : real)=> -(floor (Self.([-]) x)). axiom floor_bound (x:real) : x - 1%r < (floor x)%r <= x. -axiom ceil_bound (x:real) : x <= (ceil x)%r < x + 1%r. axiom from_int_floor n : floor n%r = n. -axiom from_int_ceil n : ceil n%r = n. + +lemma ceil_bound (x:real) : x <= (ceil x)%r < x + 1%r. +proof. by rewrite /ceil; smt(floor_bound). qed. + +lemma from_int_ceil n : ceil n%r = n. +proof. by rewrite /ceil -fromintN from_int_floor oppzK. qed. lemma floor_gt x : x - 1%r < (floor x)%r. proof. by case: (floor_bound x). qed. @@ -246,6 +250,12 @@ proof. smt(floor_bound). qed. lemma from_int_floor_addr n x : floor (x + n%r) = floor x + n. proof. smt(floor_bound). qed. +lemma from_int_ceil_addl n x : ceil (n%r + x) = n + ceil x. +proof. smt(ceil_bound). qed. + +lemma from_int_ceil_addr n x : ceil (x + n%r) = ceil x + n. +proof. smt(ceil_bound). qed. + lemma floor_mono (x y : real) : x <= y => floor x <= floor y. proof. smt(floor_bound). qed.