examples/tests-provers/ceil.why

   1 theory Ceil
   2   use real.Real
   3   use real.RealInfix
   4   use real.Truncate
   5
   6   goal ceil_obvious: ceil 0.1 = 1
   7
   8   lemma unity:
   9    forall b: real. b > 0.0 -> b = 1.0 *. b
  10
  11   lemma unity2:
  12    forall b: real. b > 0.0 -> b /. b = (1.0 *. b) /. b
  13
  14   lemma perm_div:
  15    forall a b:real. a > 0.0 /\ b > 0.0 -> (a *. b) /. b = a *. (b /. b)
  16
  17   lemma perm_div2:
  18    forall a b:real. a > 0.0 /\ b > 0.0 -> a *. b /. b = a /. b *. b
  19
  20   lemma div_mult_perm:
  21    forall b: real. b > 0.0 -> (1.0 /. b) *. b = (1.0 *. b) /. b
  22
  23   lemma b_div_b_is_one:
  24     forall b: real. b > 0.0 -> 1.0 = b /. b
  25
  26   lemma inverse_inverse_is_same:
  27     forall b: real. b > 0.0 -> 1.0 = (1.0 /. b) *. b
  28
  29   lemma inverse_bigger_zero:
  30     forall b: real. b > 0.0 -> 1.0 /. b > 0.0
  31
  32   lemma div_equals_mult_w_inverse:
  33     forall a b:real. b > 0.0 -> a /. b = a *. (1.0 /. b)
  34
  35   lemma mult_bigger_zero:
  36     forall a b: real. a > 0.0 /\ b > 0.0 -> a *. b > 0.0
  37
  38   goal ceil_never_zero:
  39     forall a b: real. a > 0.0 /\ b > 0.0 -> ceil (a /. b) <> 0
  40 end