bresenham: completed proof

parent e367b4b4
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter x2: Z.
Parameter y2: Z.
Axiom first_octant : (0%Z <= (y2 ))%Z /\ ((y2 ) <= (x2 ))%Z.
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Definition best(x:Z) (y:Z): Prop := forall (yqt:Z),
((Zabs (((x2 ) * y)%Z - (x * (y2 ))%Z)%Z) <= (Zabs (((x2 ) * yqt)%Z - (x * (y2 ))%Z)%Z))%Z.
Definition invariant_(x:Z) (y:Z) (e:Z): Prop :=
(e = (((2%Z * (x + 1%Z)%Z)%Z * (y2 ))%Z - (((2%Z * y)%Z + 1%Z)%Z * (x2 ))%Z)%Z) /\
(((2%Z * ((y2 ) - (x2 ))%Z)%Z <= e)%Z /\ (e <= (2%Z * (y2 ))%Z)%Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(*s First a tactic [Case_Zabs] to do case split over [(Zabs x)]:
introduces two subgoals, one where [x] is assumed to be non negative
and thus where [Zabs x] is replaced by [x]; and another where
[x] is assumed to be non positive and thus where [Zabs x] is
replaced by [-x]. *)
Lemma Z_gt_le : forall x y:Z, (x > y)%Z -> (y <= x)%Z.
Proof.
intros; omega.
Qed.
Ltac Case_Zabs a Ha :=
elim (Z_le_gt_dec 0 a); intro Ha;
[ rewrite (Zabs_eq a Ha)
| rewrite (Zabs_non_eq a (Z_gt_le 0 a Ha)) ].
(*s A useful lemma to establish $|a| \le |b|$. *)
Lemma Zabs_le_Zabs :
forall a b:Z,
(b <= a <= 0)%Z \/ (0 <= a <= b)%Z -> (Zabs a <= Zabs b)%Z.
Proof.
intro a; Case_Zabs a Ha; intro b; Case_Zabs b Hb; omega.
Qed.
(*s A useful lemma to establish $|a| \le $. *)
Lemma Zabs_le :
forall a b:Z, (0 <= b)%Z -> ((Zopp b <= a <= b)%Z <-> (Zabs a <= b)%Z).
Proof.
intros a b Hb.
Case_Zabs a Ha; split; omega.
Qed.
(*s Two tactics. [ZCompare x y H] discriminates between [x<y], [x=y] and
[x>y] ([H] is the hypothesis name). [RingSimpl x y] rewrites [x] by [y]
using the [Ring] tactic. *)
Ltac ZCompare x y H :=
elim (Z_gt_le_dec x y); intro H;
[ idtac | elim (Z_le_lt_eq_dec x y H); clear H; intro H ].
Ltac RingSimpl x y := replace x with y; [ idtac | ring ].
(*s Key lemma for Bresenham's proof: if [b] is at distance less or equal
than [1/2] from the rational [c/a], then it is the closest such integer.
We express this property in [Z], thus multiplying everything by [2a]. *)
Lemma closest :
forall a b c:Z,
(0 <= a)%Z ->
(Zabs (2 * a * b - 2 * c) <= a)%Z ->
forall b':Z, (Zabs (a * b - c) <= Zabs (a * b' - c))%Z.
Proof.
intros a b c Ha Hmin.
generalize (proj2 (Zabs_le (2 * a * b - 2 * c) a Ha) Hmin).
intros Hmin' b'.
elim (Z_le_gt_dec (2 * a * b) (2 * c)); intro Habc.
(* 2ab <= 2c *)
rewrite (Zabs_non_eq (a * b - c)).
ZCompare b b' Hbb'.
(* b > b' *)
rewrite (Zabs_non_eq (a * b' - c)).
apply Zle_left_rev.
RingSimpl (Zopp (a * b' - c) + Zopp (Zopp (a * b - c)))%Z
(a * (b - b'))%Z.
apply Zmult_le_0_compat; omega.
apply Zge_le.
apply Zge_trans with (m := (a * b - c)%Z).
apply Zmult_ge_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
RingSimpl (a * b' - c)%Z (a * b' + Zopp c)%Z.
RingSimpl (a * b - c)%Z (a * b + Zopp c)%Z.
apply Zle_ge.
apply Zplus_le_compat_r.
apply Zmult_le_compat_l; omega.
(* b < b' *)
rewrite (Zabs_eq (a * b' - c)).
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl ((a * b' - c) * 2)%Z
(2 * (a * b' - a * b) + 2 * (a * b - c))%Z.
apply Zle_trans with a.
RingSimpl (Zopp (a * b - c) * 2)%Z (Zopp (2 * a * b - 2 * c)).
omega.
apply Zle_trans with (2 * a + Zopp a)%Z.
omega.
apply Zplus_le_compat.
RingSimpl (2 * a)%Z (2 * a * 1)%Z.
RingSimpl (2 * (a * b' - a * b))%Z (2 * a * (b' - b))%Z.
apply Zmult_le_compat_l; omega.
RingSimpl (2 * (a * b - c))%Z (2 * a * b - 2 * c)%Z.
omega.
(* 0 <= ab'-c *)
RingSimpl (a * b' - c)%Z (a * b' - a * b + (a * b - c))%Z.
RingSimpl 0%Z (a + Zopp a)%Z.
apply Zplus_le_compat.
RingSimpl a (a * 1)%Z.
RingSimpl (a * 1 * b' - a * 1 * b)%Z (a * (b' - b))%Z.
apply Zmult_le_compat_l; omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
apply Zle_trans with (Zopp a).
omega.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
(* b = b' *)
rewrite <- Hbb'.
rewrite (Zabs_non_eq (a * b - c)).
omega.
apply Zge_le.
apply Zmult_ge_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
apply Zge_le.
apply Zmult_ge_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
(* 2ab > 2c *)
rewrite (Zabs_eq (a * b - c)).
ZCompare b b' Hbb'.
(* b > b' *)
rewrite (Zabs_non_eq (a * b' - c)).
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (Zopp (a * b' - c) * 2)%Z
(2 * (c - a * b) + 2 * (a * b - a * b'))%Z.
apply Zle_trans with a.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
apply Zle_trans with (Zopp a + 2 * a)%Z.
omega.
apply Zplus_le_compat.
RingSimpl (2 * (c - a * b))%Z (2 * c - 2 * a * b)%Z.
omega.
RingSimpl (2 * a)%Z (2 * a * 1)%Z.
RingSimpl (2 * (a * b - a * b'))%Z (2 * a * (b - b'))%Z.
apply Zmult_le_compat_l; omega.
(* 0 >= ab'-c *)
RingSimpl (a * b' - c)%Z (a * b' - a * b + (a * b - c))%Z.
RingSimpl 0%Z (Zopp a + a)%Z.
apply Zplus_le_compat.
RingSimpl (Zopp a) (a * (-1))%Z.
RingSimpl (a * b' - a * b)%Z (a * (b' - b))%Z.
apply Zmult_le_compat_l; omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
apply Zle_trans with a.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
omega.
(* b < b' *)
rewrite (Zabs_eq (a * b' - c)).
apply Zle_left_rev.
RingSimpl (a * b' - c + Zopp (a * b - c))%Z (a * (b' - b))%Z.
apply Zmult_le_0_compat; omega.
apply Zle_trans with (m := (a * b - c)%Z).
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
RingSimpl (a * b' - c)%Z (a * b' + Zopp c)%Z.
RingSimpl (a * b - c)%Z (a * b + Zopp c)%Z.
apply Zplus_le_compat_r.
apply Zmult_le_compat_l; omega.
(* b = b' *)
rewrite <- Hbb'.
rewrite (Zabs_eq (a * b - c)).
omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
Qed.
(* DO NOT EDIT BELOW *)
Theorem invariant_is_ok : forall (x:Z) (y:Z) (e:Z), (invariant_ x y e) ->
(best x y).
(* YOU MAY EDIT THE PROOF BELOW *)
Proof.
intros x y e.
unfold invariant_; unfold best; intros [E I'] y'.
cut (0 <= x2)%Z; [ intro Hx2 | idtac ].
apply closest.
assumption.
apply (proj1 (Zabs_le (2 * x2 * y - 2 * (x * y2)) x2 Hx2)).
rewrite E in I'.
split.
(* 0 <= x2 *)
generalize (proj2 I').
RingSimpl (2 * (x + 1) * y2 - (2 * y + 1) * x2)%Z
(2 * x * y2 - 2 * x2 * y + 2 * y2 - x2)%Z.
intro.
RingSimpl (2 * (x * y2))%Z (2 * x * y2)%Z.
omega.
(* 0 <= x2 *)
generalize (proj1 I').
RingSimpl (2 * (x + 1) * y2 - (2 * y + 1) * x2)%Z
(2 * x * y2 - 2 * x2 * y + 2 * y2 - x2)%Z.
RingSimpl (2 * (y2 - x2))%Z (2 * y2 - 2 * x2)%Z.
RingSimpl (2 * (x * y2))%Z (2 * x * y2)%Z.
omega.
omega.
Qed.
(* DO NOT EDIT BELOW *)
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd"> <!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/bresenham/why3session.xml"> <why3session name="examples/programs/bresenham/why3session.xml">
<file name="../bresenham.mlw" verified="false" expanded="true"> <prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<theory name="WP M" verified="false" expanded="true"> <prover id="coq" name="Coq" version="8.2pl1"/>
<goal name="invariant_is_ok" sum="a18992b264d84141d8761ca70ad6be8d" proved="false" expanded="true"> <prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="eprover" name="Eprover" version="1.0-004 Temi"/>
<prover id="gappa" name="Gappa" version="0.14.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.5"/>
<prover id="yices" name="Yices" version="1.0.27"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../bresenham.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="invariant_is_ok" sum="a18992b264d84141d8761ca70ad6be8d" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<proof prover="coq" timelimit="10" edited="bresenham_WP_M_invariant_is_ok_1.v" obsolete="false">
<result status="valid" time="1.75"/>
</proof>
</goal> </goal>
<goal name="WP_parameter bresenham" expl="correctness of parameter bresenham" sum="e21d55e7ef3bbb885c18d91e544577f6" proved="true" expanded="true"> <goal name="WP_parameter bresenham" expl="correctness of parameter bresenham" sum="e21d55e7ef3bbb885c18d91e544577f6" proved="true" expanded="true" shape="iainfix <=V2ax2iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1tIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<transf name="split_goal" proved="true" expanded="true"> <transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="17124999e917b5c053f6e76b259bcb7c" proved="true" expanded="true"> <goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="17124999e917b5c053f6e76b259bcb7c" proved="true" expanded="true" shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false"> <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.2" expl="assertion" sum="6a4211d9f59e4c91dd774b5f26851c4a" proved="true" expanded="true"> <goal name="WP_parameter bresenham.2" expl="assertion" sum="6a4211d9f59e4c91dd774b5f26851c4a" proved="true" expanded="true" shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false"> <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/> <result status="valid" time="0.16"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="cc7e4371357729bd73f6d31bb228d35e" proved="true" expanded="true"> <goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="cc7e4371357729bd73f6d31bb228d35e" proved="true" expanded="true" shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false"> <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="38653e4347933a962e5aa5d8faf55aaf" proved="true" expanded="true"> <goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="38653e4347933a962e5aa5d8faf55aaf" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false"> <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/> <result status="valid" time="0.03"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="694c94aaa6e82005f68c8636fcf6fa15" proved="true" expanded="true"> <goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="694c94aaa6e82005f68c8636fcf6fa15" proved="true" expanded="true" shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false"> <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/> <result status="valid" time="0.04"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="169f4e236bbdd35bc03b2b6daf8f3b7f" proved="true" expanded="true"> <goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="169f4e236bbdd35bc03b2b6daf8f3b7f" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false"> <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.7" expl="normal postcondition" sum="bd112799fb9e847a8546c1fac8ba4617" proved="true" expanded="true"> <goal name="WP_parameter bresenham.7" expl="normal postcondition" sum="bd112799fb9e847a8546c1fac8ba4617" proved="true" expanded="true" shape="tIainfix <=V2ax2NIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false"> <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment