Require ZArith.
Require Zcomplements.
Require ZArithRing.
Require Zdiv.
Require Omega.
Require Why.
Lemma sqr_gt:(x,y:Z)`x > y`->`y > 0`->`x*x > y*y`.
Proof.
Intros.
Assert `x*y > y*y`.
Apply Zgt_Zmult_right; Omega.
Assert `x*x > x*y`.
Apply Zgt_Zmult_left; Omega.
Omega.
Save.
Lemma Z_mod_same : (a:Z)`a>0`->`a%a=0`.
Proof.
Intros a aPos.
Generalize (Z_mod_plus `0` `1` a aPos).
Replace `0+1*a` with `a`.
Intros.
Rewrite H.
Compute.
Trivial.
Ring.
Save.
Lemma Z_div_same : (a:Z)`a>0`->`a/a=1`.
Proof.
Intros a aPos.
Generalize (Z_div_plus `0` `1` a aPos).
Replace `0+1*a` with `a`.
Intros.
Rewrite H.
Compute.
Trivial.
Ring.
Save.
Lemma iter_sqrt_pos: (x,z:Z)`x>0`->`z>0`->`(x/z+z)/2>0`.
Proof.
Intros x z xPos zPos.
Assert `(x/z+z)>=2`.
Assert `(x+z*z)>=z+z`.
Assert `x+(z-1)*(z-1) >= 1`.
Generalize (sqr_pos `z-1`).
Intros.
Omega.
Replace `z*z` with `(z-1)*(z-1)+z+z-1`.
Omega.
Ring.
Generalize (Z_div_ge `x+z*z` `z+z` `z` zPos H).
Intro.
Generalize (Z_div_plus x z z zPos).
Intro H1.
Rewrite H1 in H0.
Clear H1.
Generalize (Z_div_plus z `1` z zPos).
Replace `1*z` with `z`.
Intro H2.
Rewrite H2 in H0.
Clear H2.
Generalize (Z_div_plus `0` `1` z zPos).
Replace `1*z` with `z`.
Replace `0+z` with `z`.
Intro.
Rewrite H1 in H0.
Simpl in H0.
Trivial.
Trivial.
Ring.
Ring.
Assert `2>0`.
Omega.
Generalize (Z_div_ge `x/z+z` `2` `2` H0 H).
Replace `2/2` with `1`.
Intro; Omega.
Compute.
Trivial.
Save.
Lemma iter_sqrt_pos2 : (x:Z)`x>0`->`(x+1)/2>0`.
Proof.
Intros.
Assert `x+1 >= 2`. Omega.
Assert `(x+1)/2 >= 2/2`.
Apply Z_div_ge; Try Omega.
Assert `2/2 > 0`; Try Omega.
Compute; Trivial.
Save.
Lemma iter_sqrt_invar1: (x,y,z:Z)
`x>0`->`y>0`->`z=(x/y+y)/2`->`2*y*z<=x+y*y`.
Proof.
Intros x y z xPos yPos zVal.
Assert `2*z <= x/y+y`.
Rewrite zVal.
Apply Z_mult_div_ge; Omega.
Assert `2*y*z <= y*(x/y+y)`.
Replace `2*y*z` with `y*(2*z)`; Try Ring.
Apply Zle_Zmult_pos_left; Trivial Orelse Omega.
Assert `y*(x/y+y) <= x+y*y`.
Assert `y*(x/y+y) = y*(x/y)+y*y`; Try Ring.
Assert `y*(x/y) <= x`.
Apply Z_mult_div_ge; Omega.
Omega.
Omega.
Save.
Lemma iter_sqrt_invar2: (x,y,z:Z)
`x>0`->`y>0`->`z=(x/y+y)/2`->`2*y*(z+1)>x+y*y`.
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)` with `y*(2*((x/y+y)/2))+y+y`;
Try Ring.
Replace `2*((x/y+y)/2)` with `x/y+y - (x/y+y)%2`.
Replace `y*(x/y+y-(x/y+y)%2)` with `y*(x/y)+y*y-y*((x/y+y)%2)`.
Replace `y*(x/y)` with `x - x%y`.
Assert `y >= y*((x/y+y)%2)`.
Pattern 1 y; Replace `y` with `y*1`.
Apply Zge_Zmult_pos_left.
Omega.
Omega.
Ring.
Omega.
Omega.
Ring.
Omega.
Save.
Lemma iter_sqrt_invar3: (x,y,z:Z)
`x>0` -> `y>0` -> `z=(x/y+y)/2` -> `x<(z+1)*(z+1)`.
Proof.
Intros x y z xPos yPos zVal.
Cut `(z+1)*(z+1)-x > 0 `; Try Omega.
Assert `(4*y*y)*((z+1)*(z+1)-x) >= 1`.
Replace `(4*y*y)*((z+1)*(z+1)-x)` with
`(2*y*(z+1))*(2*y*(z+1)) - 4*y*y*x`; 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)`.
Assert `2*y*(z+1)*(x+y*y) > (x+y*y)*(x+y*y)`.
Apply Zgt_Zmult_right.
Generalize (sqr_pos y).
Omega.
Assumption.
Assert `2*y*(z+1)*(2*y*(z+1)) > 2*y*(z+1)*(x+y*y)`; Try Omega.
Apply Zgt_Zmult_left; Try Assumption.
Apply Zgt_ZERO_mult; Try Omega.
Assert `z>=0`; Try Omega.
Rewrite zVal.
Apply Z_div_ge0; Try Omega.
Assert `x/y>=0`; Try Omega.
Apply Z_div_ge0; Try Omega.
Assert `(x+y*y)*(x+y*y)-4*y*y*x >=0`; Try Omega.
Replace `(x+y*y)*(x+y*y)-4*y*y*x` with `(x-y*y)*(x-y*y)`; Try Ring.
Apply sqr_pos.
Apply (Zmult_gt `4*y*y`).
Apply Zgt_ZERO_mult; Try Omega.
Omega.
Save.
Lemma iter_sqrt_invar4: (x,y,z:Z)
`x>0` -> `y>0` -> `z=(x/y+y)/2` -> `z>=y` -> `y*y<= x`.
Proof.
Intros x y z xPos yPos zVal zGey.
Generalize (iter_sqrt_invar1 x y z xPos yPos zVal); Intros.
Assert `y*y <= y*z`.
Apply Zle_Zmult_pos_left; Try Omega.
Assert `2*y*z = y*z+y*z`; Try Ring.
Omega.
Save.
Lemma sqrt_po_1 :
(x: Z)
(Pre6: `x >= 0`)
(Test6: `x = 0`)
`0 * 0 <= x` /\ `x < (0 + 1) * (0 + 1)`.
Proof.
Auto with *.
Save.
Lemma sqrt_po_2 :
(x: Z)
(Pre6: `x >= 0`)
(Test5: `x <> 0`)
(Test4: `x <= 3`)
`1 * 1 <= x` /\ `x < (1 + 1) * (1 + 1)`.
Proof.
Auto with *.
Save.
Lemma sqrt_po_3 :
(x: Z)
(Pre6: `x >= 0`)
(Test5: `x <> 0`)
(Test3: `x > 3`)
(result1: Z)
(Post5: result1 = x)
~(`2` = `0`).
Proof.
Auto with *.
Save.
Lemma sqrt_po_4 :
(x: Z)
(Pre6: `x >= 0`)
(Test5: `x <> 0`)
(Test3: `x > 3`)
(result1: Z)
(Post5: result1 = x)
(Pre5: ~(`2` = `0`))
(result2: Z)
(Post4: result2 = (Zdiv (`x + 1`) `2`))
(Variant1: Z)
(y0: Z)
(z0: Z)
(Pre4: Variant1 = y0)
(Pre3: `z0 > 0` /\ `y0 > 0` /\ `z0 = (Zdiv ((Zdiv x y0) + y0) 2)` /\
`x < (y0 + 1) * (y0 + 1)` /\ `x < (z0 + 1) * (z0 + 1)`)
(Test2: `z0 < y0`)
(y1: Z)
(Post1: y1 = z0)
(Pre2: ~(`2` = `0`))
(z1: Z)
(Post2: z1 = (Zdiv (`(Zdiv x z0) + z0`) `2`))
(`z1 > 0` /\ `y1 > 0` /\ `z1 = (Zdiv ((Zdiv x y1) + y1) 2)` /\
`x < (y1 + 1) * (y1 + 1)` /\ `x < (z1 + 1) * (z1 + 1)`) /\ (Zwf `0` y1 y0).
Proof.
Unfold Zwf.
Intuition.
Subst z1.
Apply iter_sqrt_pos; Omega.
Subst y1; Assumption.
Subst y1; Assumption.
Apply (iter_sqrt_invar3 x z0); Auto.
Omega.
Save.
Lemma sqrt_po_5 :
(x: Z)
(Pre6: `x >= 0`)
(Test5: `x <> 0`)
(Test3: `x > 3`)
(result1: Z)
(Post5: result1 = x)
(Pre5: ~(`2` = `0`))
(result2: Z)
(Post4: result2 = (Zdiv (`x + 1`) `2`))
`result2 > 0` /\ `result1 > 0` /\
`result2 = (Zdiv ((Zdiv x result1) + result1) 2)` /\
`x < (result1 + 1) * (result1 + 1)` /\ `x < (result2 + 1) * (result2 + 1)`.
Proof.
Intuition.
Subst result2.
Assert `(x+1)/2 >= 1`.
Pattern 2 `1`; Replace `1` with `2/2`; Trivial.
Apply Z_div_ge; Try Omega.
Omega.
Subst result1.
Assert `x/x+x = x+1`.
Assert xPos:`x>0`; Try Omega.
Generalize (Z_div_same x xPos).
Intro.
Rewrite H; Omega.
Rewrite H; Trivial.
Subst result1.
Assert `(x+1)*(x+1) >= (x+1)*1`.
Apply Zge_Zmult_pos_left; Try Omega.
Assert `(x+1)*1 = x+1`; Try Ring.
Omega.
Subst result2.
Apply (iter_sqrt_invar3 x x); Try Omega.
Assert `x/x+x = x+1`.
Assert xPos:`x>0`; Try Omega.
Generalize (Z_div_same x xPos).
Intro.
Rewrite H; Omega.
Rewrite H; Trivial.
Save.
Lemma sqrt_po_6 :
(x: Z)
(Pre6: `x >= 0`)
(Test5: `x <> 0`)
(Test3: `x > 3`)
(result1: Z)
(Post5: result1 = x)
(Pre5: ~(`2` = `0`))
(result2: Z)
(Post4: result2 = (Zdiv (`x + 1`) `2`))
(y0: Z)
(z0: Z)
(Post3: (`z0 > 0` /\ `y0 > 0` /\ `z0 = (Zdiv ((Zdiv x y0) + y0) 2)` /\
`x < (y0 + 1) * (y0 + 1)` /\ `x < (z0 + 1) * (z0 + 1)`) /\
`z0 >= y0`)
`y0 * y0 <= x` /\ `x < (y0 + 1) * (y0 + 1)`.
Proof.
Intuition.
Apply (iter_sqrt_invar4 x y0 z0); Try Omega.
Save.