isqrt.mlw_M_WP_main_2.v 880 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
(* Beware! Only edit allowed sections below    *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.

Definition unit  := unit.

Parameter ignore: forall (a:Type), a  -> unit.

Implicit Arguments ignore.

Parameter label_ : Type.

Parameter at1: forall (a:Type), a -> label_  -> a.

Implicit Arguments at1.

Parameter old: forall (a:Type), a  -> a.

Implicit Arguments old.

Parameter ref : forall (a:Type), Type.

Definition sqr(x:Z): Z := (x * x)%Z.

Theorem WP_main : (0%Z <= 17%Z)%Z -> forall (result:Z), ((0%Z <= result)%Z /\
  (((sqr result) <= 17%Z)%Z /\ (17%Z <  (sqr (result + 1%Z)%Z))%Z)) ->
  (result = 4%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
assert (h:(result < 4 \/ result = 4 \/ result > 4)%Z) by omega. 
destruct h as [h1|[h2|h3]]; auto.


Qed.
(* DO NOT EDIT BELOW *)