more proofs on isqrt example

examples/programs/isqrt/isqrt_WP_NewtonMethod_WP_parameter_sqrt_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import ZOdiv.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+
+(* Why3 assumption *)
+Definition unit  := unit.
+
+Parameter qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+Implicit Arguments old.
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Inductive ref (a:Type) :=
+  | mk_ref : a -> ref a.
+Implicit Arguments mk_ref.
+
+(* Why3 assumption *)
+Definition contents (a:Type)(v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
+  end.
+Implicit Arguments contents.
+
+Open Scope Z_scope.
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 3.
+
+Lemma iter_sqrt_invar2 :
+ forall x y z:Z,
+   (x > 0)%Z ->
+   (y > 0)%Z ->
+   z = ((x / y + y) / 2)%Z -> (2 * y * (z + 1) > x + y * y)%Z.
+Proof.
+intros x y z xPos yPos zVal.
+assert (TwoPos: (2 > 0)); try omega.
+generalize (Z_div_mod_eq x y yPos).
+generalize (Z_mod_lt x y yPos).
+generalize (Z_div_mod_eq (x / y + y) 2 TwoPos).
+generalize (Z_mod_lt (x / y + y) 2 TwoPos).
+intros.
+rewrite zVal.
+replace (2 * y * ((x / y + y) / 2 + 1))%Z with
+ (y * (2 * ((x / y + y) / 2)) + y + y)%Z; try ring.
+replace (2 * ((x / y + y) / 2))%Z with
+ (x / y + y - (x / y + y) mod 2)%Z.
+2: rewrite H0 at 1.
+Focus 2.
+
+replace (y * (x / y + y - (x / y + y) mod 2))%Z with
+ (y * (x / y) + y * y - y * ((x / y + y) mod 2))%Z; try ring.
+replace (y * (x / y))%Z with (x - x mod y)%Z.
+assert (y >= y * ((x / y + y) mod 2))%Z.
+pattern y at 1; replace y with (y * 1)%Z; auto with zarith.
+apply Zmult_ge_compat_l; auto with zarith.
+Admitted.
+
+Lemma iter_sqrt_invar3 :
+ forall x y z:Z,
+   (x > 0)%Z ->
+   (y > 0)%Z -> z = ((x / y + y) / 2)%Z -> (x < (z + 1) * (z + 1))%Z.
+Proof.
+intros x y z xPos yPos zVal.
+cut ((z + 1) * (z + 1) - x > 0)%Z; try omega.
+assert (4 * y * y * ((z + 1) * (z + 1) - x) >= 1)%Z.
+replace (4 * y * y * ((z + 1) * (z + 1) - x))%Z with
+ (2 * y * (z + 1) * (2 * y * (z + 1)) - 4 * y * y * x)%Z; try ring.
+generalize (iter_sqrt_invar2 x y z xPos yPos zVal).
+intro.
+assert
+ (2 * y * (z + 1) * (2 * y * (z + 1)) > (x + y * y) * (x + y * y))%Z.
+assert (2 * y * (z + 1) * (x + y * y) > (x + y * y) * (x + y * y))%Z.
+apply Zmult_gt_compat_r.
+generalize (sqr_pos y).
+omega.
+assumption.
+assert
+ (2 * y * (z + 1) * (2 * y * (z + 1)) > 2 * y * (z + 1) * (x + y * y))%Z;
+ try omega.
+apply Zmult_gt_compat_l; try assumption.
+apply Zmult_gt_0_compat; try omega.
+assert (z >= 0)%Z; try omega.
+rewrite zVal.
+(*
+apply Z_div_ge0; try omega.
+assert (x / y >= 0)%Z; try omega.
+apply Z_div_ge0; try omega
+assert ((x + y * y) * (x + y * y) - 4 * y * y * x >= 0)%Z; try omega.
+replace ((x + y * y) * (x + y * y) - 4 * y * y * x)%Z with
+ ((x - y * y) * (x - y * y))%Z; try ring.
+apply sqr_pos.
+apply (Zmult_gt_0_reg_l (4 * y * y)).
+apply Zmult_gt_0_compat; try omega.
+omega.
+*)
+Admitted.
+
+(* Why3 goal *)
+Theorem WP_parameter_sqrt : forall (x:Z), (0%Z <= x)%Z -> ((~ (x = 0%Z)) ->
+  ((~ (x <= 3%Z)%Z) -> forall (z:Z), forall (y:Z), ((0%Z < z)%Z /\
+  ((0%Z < y)%Z /\ ((z = (ZOdiv ((ZOdiv x y) + y)%Z 2%Z)) /\
+  ((x < ((y + 1%Z)%Z * (y + 1%Z)%Z)%Z)%Z /\
+  (x < ((z + 1%Z)%Z * (z + 1%Z)%Z)%Z)%Z)))) -> ((z < y)%Z -> forall (y1:Z),
+  (y1 = z) -> forall (z1:Z), (z1 = (ZOdiv ((ZOdiv x z) + z)%Z 2%Z)) ->
+  (x < ((z1 + 1%Z)%Z * (z1 + 1%Z)%Z)%Z)%Z))).
+intuition.
+subst y1.
+apply iter_sqrt_invar3 with (y:=z); auto with zarith.
+Qed.
+
+