[gallery] simplified Coq proof for bresenham

this is a contribution of Laurent Théry
parent e2131f24
......@@ -32,7 +32,7 @@ module M
We express this property using integers by multiplying everything by [2a]. *)
lemma closest :
forall a b c: int. 0 < a ->
forall a b c: int.
abs (2 * a * b - 2 * c) <= a ->
forall b': int. abs (a * b - c) <= abs (a * b' - c)
......
......@@ -31,138 +31,15 @@ Axiom first_octant : (0%Z <= y2)%Z /\ (y2 <= x2)%Z.
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 [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 ].
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3.
(* The following short and nice proof is due to Laurent Théry *)
Require Import Psatz.
(* 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.
Theorem closest : forall (a:Z) (b:Z) (c: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.
intros a b c H b'.
assert (H1: b = b' \/ b <> b') by nia.
nia.
Qed.
......@@ -7,14 +7,18 @@
version="0.95.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
id="3"
name="Coq"
version="8.4pl2"/>
<prover
id="3"
id="4"
name="Z3"
version="2.19"/>
<file
......@@ -31,18 +35,18 @@
name="closest"
locfile="../bresenham.mlw"
loclnum="34" loccnumb="8" loccnume="15"
sum="2da4d109f40a504c6240248e6e9ff056"
sum="c18e4a733a845b9d1202d0b801bbf0f3"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix &lt;=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0Iainfix &lt;c0V0F">
shape="ainfix &lt;=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix &lt;=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F">
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
edited="bresenham_M_closest_1.v"
obsolete="false"
archived="false">
<result status="valid" time="4.20"/>
<result status="valid" time="3.74"/>
</proof>
</goal>
<goal
......@@ -50,7 +54,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="VC for bresenham"
sum="145c3afb9565db0c8a64db135f0f44de"
sum="9b8128bb23b676133822da0cac2fea53"
proved="true"
expanded="true"
shape="iainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix &lt;=V6ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix &lt;V1c0AabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFAainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2">
......@@ -65,7 +69,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="1. loop invariant init"
sum="a7d59511d637bd777ac8a33a539550bc"
sum="818d60808053e43e7be4da19c039bf40"
proved="true"
expanded="true"
shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2">
......@@ -80,7 +84,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -88,7 +92,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -101,7 +105,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="2. loop invariant init"
sum="a47e474878fd2e9638b69c1ea3cae179"
sum="4ed4f3c9453360f984689a439a94d03a"
proved="true"
expanded="true"
shape="loop invariant initainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix &lt;=c0V0Lax2">
......@@ -121,7 +125,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="3. assertion"
sum="b4fdabc8784d3fff3a314c29c063b44e"
sum="fcbcee9000353217b3dbca58d7cc9146"
proved="true"
expanded="true"
shape="assertionabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
......@@ -129,11 +133,19 @@
name="expl:VC for bresenham"/>
<proof
prover="0"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.10"/>
<result status="valid" time="6.17"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="6.86"/>
</proof>
</goal>
<goal
......@@ -141,7 +153,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="4. loop invariant preservation"
sum="0bef89498ad79d5da5ff76cc66a9751d"
sum="0926f96b84b6aebff66f2379e7c0e76e"
proved="true"
expanded="true"
shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
......@@ -156,7 +168,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -164,7 +176,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -177,7 +189,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="5. loop invariant preservation"
sum="e6aba1a5d837387369af060369d26120"
sum="46f21c9ec9008592af315031d0658467"
proved="true"
expanded="true"
shape="loop invariant preservationainfix &lt;=V4ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
......@@ -197,14 +209,14 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="6. loop invariant preservation"
sum="8bf10f587c91043c58241ffb93901f35"
sum="effb2332ccb437bc6e30129ae779efb0"
proved="true"
expanded="true"
shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
<label
name="expl:VC for bresenham"/>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -212,12 +224,12 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.24"/>
<result status="valid" time="0.95"/>
</proof>
</goal>
<goal
......@@ -225,7 +237,7 @@
locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15"
expl="7. loop invariant preservation"
sum="dfc6df2fc87f993588f5515228babc75"
sum="60e316bbceaf72ebb290a196c9b2d99f"
proved="true"
expanded="true"
shape="loop invariant preservationainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
......
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