[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Regarding floor and ceiling of reals



Nikhil D. Kikkeri writes:
   
   Lets assume I have a real number x > 1 and x < 2
   
   Now I would assume that 2^-52*ceiling(x*2^52) would be less than or equal to 
   2
   
   Now if this is true (and i think it is), why am I finding it difficult to 
   prove this as a lemma? Grind just expands "^"
   
You have to invest a bit more. I prove 

  c : Lemma Forall(x : real) : 
    x > 1 And x < 2 Implies
      2^-52 * ceiling(x*2^52) <= 2

with

;;; Proof c-1 for formula A.c
;;; developed with shostak decision procedures
(""
 (skosimp* :preds? t)
 (use "ceiling_def")
 (flatten)
 (case "ceiling(x!1 * 2 ^ 52) <= 2 * 2 ^ 52")
 (("1"
   (hide-all-but (-1 1))
   (use "both_sides_times_pos_le1" :subst
        ("x" "ceiling(x!1 * 2 ^ 52)" "y" "2 * 2 ^ 52" "pz" "2^-52"))
   (assert)
   (rewrite "expt_plus" :dir rl)
   (rewrite "expt_x0")
   (assert))
  ("2"
   (hide 2)
   (use "both_sides_times_pos_lt1" :subst ("x" "x!1" "y" "2"))
   (use "both_sides_plus_lt2" :subst
        ("x" "x!1 * 2 ^ 52" "y" "2 * 2 ^ 52" "z" "1"))
   (name-replace "xx" "2*2^52")
   (assert))))


Bye,

Hendrik