From 993d49160498625bbd61c7a47012b28bc3d9223f Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Mon, 20 May 2013 05:33:52 +0200 Subject: [PATCH] bresenham: simplified spec and proof --- examples/bresenham.mlw | 35 +-- examples/bresenham/bresenham_M_closest_1.v | 168 +++++++++++ .../bresenham_WP_M_invariant_is_ok_1.v | 266 ------------------ examples/bresenham/why3session.xml | 152 +++++----- 4 files changed, 256 insertions(+), 365 deletions(-) create mode 100644 examples/bresenham/bresenham_M_closest_1.v delete mode 100644 examples/bresenham/bresenham_WP_M_invariant_is_ok_1.v diff --git a/examples/bresenham.mlw b/examples/bresenham.mlw index 9c5c5e551..e7c3041fb 100644 --- a/examples/bresenham.mlw +++ b/examples/bresenham.mlw @@ -17,39 +17,40 @@ module M constant y2: int axiom first_octant: 0 <= y2 <= x2 - (* The code. - [(best x y)] expresses that the point [(x,y)] is the best - possible point i.e. the closest to the real line (see the Coq file). - The invariant relates [x], [y], and [e] and - gives lower and upper bound for [e] (see the Coq file). *) + (* [best x y] expresses that the point [(x,y)] is the best + possible point i.e. the closest to the real line + i.e. for all y', we have |y - x*y2/x2| <= |y' - x*y2/x2| + We stay in type [int] by multiplying everything by [x2]. *) use import int.Abs predicate best (x y: int) = forall y': int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2) - predicate invariant_ (x y e: int) = - e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 /\ - 2 * (y2 - x2) <= e <= 2 * y2 + (** 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 using integers by multiplying everything by [2a]. *) - lemma invariant_is_ok: forall x y e: int. invariant_ x y e -> best x y + lemma closest : + forall a b c: int. 0 < a -> + abs (2 * a * b - 2 * c) <= a -> + forall b': int. abs (a * b - c) <= abs (a * b' - c) let bresenham () = - let x = ref 0 in let y = ref 0 in let e = ref (2 * y2 - x2) in - while !x <= x2 do - invariant { 0 <= !x <= x2 + 1 /\ invariant_ !x !y !e } - variant { x2 + 1 - !x } - (* here we would plot (x, y) *) - assert { best !x !y }; + for x = 0 to x2 do + invariant { !e = 2 * (x + 1) * y2 - (2 * !y + 1) * x2 } + invariant { 2 * (y2 - x2) <= !e <= 2 * y2 } + (* here we would plot (x, y), + so we assert this is the best possible row y for column x *) + assert { best x !y }; if !e < 0 then e := !e + 2 * y2 else begin y := !y + 1; e := !e + 2 * (y2 - x2) - end; - x := !x + 1 + end done end diff --git a/examples/bresenham/bresenham_M_closest_1.v b/examples/bresenham/bresenham_M_closest_1.v new file mode 100644 index 000000000..4832c2983 --- /dev/null +++ b/examples/bresenham/bresenham_M_closest_1.v @@ -0,0 +1,168 @@ +(* This file is generated by Why3's Coq 8.4 driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. +Require int.Abs. + +(* Why3 assumption *) +Definition unit := unit. + +(* Why3 assumption *) +Inductive ref (a:Type) {a_WT:WhyType a} := + | mk_ref : a -> ref a. +Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a). +Existing Instance ref_WhyType. +Implicit Arguments mk_ref [[a] [a_WT]]. + +(* Why3 assumption *) +Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a := + match v with + | (mk_ref x) => x + end. + +Parameter x2: Z. + +Parameter y2: Z. + +Axiom first_octant : (0%Z <= y2)%Z /\ (y2 <= x2)%Z. + +(* Why3 assumption *) +Definition best (x:Z) (y:Z): Prop := forall (y':Z), + ((Zabs ((x2 * y)%Z - (x * y2)%Z)%Z) <= (Zabs ((x2 * y')%Z - (x * y2)%Z)%Z))%Z. + +(*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 [xy] ([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 ]. + +Require Import Why3. +Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3. + +(* Why3 goal *) +Theorem closest : forall (a:Z) (b:Z) (c:Z), (0%Z < a)%Z -> + (((Zabs (((2%Z * a)%Z * b)%Z - (2%Z * c)%Z)%Z) <= a)%Z -> forall (b':Z), + ((Zabs ((a * b)%Z - c)%Z) <= (Zabs ((a * b')%Z - c)%Z))%Z). +(* Why3 intros a b c h1 h2 b'. *) +intros a b c Ha Hmin. +assert (Ha': (0 <= a)%Z) by omega. +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)). +ae. +ae. + (* 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. +ae. + 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. +ae. + apply Zle_trans with (Zopp a). + omega. + RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z. +ae. + (* b = b' *) +ae. +ae. + +(* 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. +ae. + apply Zle_trans with (Zopp a + 2 * a)%Z. + omega. + apply Zplus_le_compat. +ae. + RingSimpl (2 * a)%Z (2 * a * 1)%Z. + RingSimpl (2 * (a * b - a * b'))%Z (2 * a * (b - b'))%Z. +ae. + (* 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. +ae. +ae. + (* 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. +ae. + apply Zle_trans with (m := (a * b - c)%Z). +ae. +ae. +ae. +ae. +Qed. + + diff --git a/examples/bresenham/bresenham_WP_M_invariant_is_ok_1.v b/examples/bresenham/bresenham_WP_M_invariant_is_ok_1.v deleted file mode 100644 index 017dc8726..000000000 --- a/examples/bresenham/bresenham_WP_M_invariant_is_ok_1.v +++ /dev/null @@ -1,266 +0,0 @@ -(* 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 [xy] ([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 *) - - diff --git a/examples/bresenham/why3session.xml b/examples/bresenham/why3session.xml index c870375a3..30ec20d1d 100644 --- a/examples/bresenham/why3session.xml +++ b/examples/bresenham/why3session.xml @@ -12,7 +12,7 @@ + version="8.4pl1"/> + expanded="true"> + shape="ainfix <=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix <=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0Iainfix <c0V0F"> - + + shape="iainfix <=V5ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix <=V6ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix <V1c0AabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFAainfix <=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix <=c0V0Lax2">