tortoise and hare: fixed variant relation (was not well-founded)

parent f2b21f65
......@@ -53,8 +53,18 @@ module TortoiseAndHare
use import module ref.Ref
(* the minimal distance between x i and x j *)
function dist int int : int
(* it is defined as soon as i,j >= mu *)
axiom dist_def: forall i j: int. mu <= i -> mu <= j ->
dist i j >= 0 /\
x (i + dist i j) = x j /\
forall k: int. 0 <= k -> x (i + k) = x j -> dist i j <= k
predicate rel (t2 t1: t) =
exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda
exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda /\
(i >= mu -> dist (2*i+2) (i+1) < dist (2*i) i)
let tortoise_hare () =
let tortoise = ref (f x0) in
......
(* 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.
Parameter t : Type.
Parameter f: t -> t.
Parameter x0: t.
Parameter iter: Z -> t -> t.
Axiom iter_0 : forall (x:t), ((iter 0%Z x) = x).
Axiom iter_s : forall (k:Z) (x:t), (0%Z < k)%Z -> ((iter k
x) = (iter (k - 1%Z)%Z (f x))).
Axiom iter_1 : forall (x:t), ((iter 1%Z x) = (f x)).
Axiom iter_s2 : forall (k:Z) (x:t), (0%Z < k)%Z -> ((iter k
x) = (f (iter (k - 1%Z)%Z x))).
Parameter mu: Z.
Parameter lambda: Z.
Axiom mu_range : (0%Z <= (mu ))%Z.
Axiom lambda_range : (1%Z <= (lambda ))%Z.
Axiom distinct : forall (i:Z) (j:Z), ((0%Z <= i)%Z /\
(i < ((mu ) + (lambda ))%Z)%Z) -> (((0%Z <= j)%Z /\
(j < ((mu ) + (lambda ))%Z)%Z) -> ((~ (i = j)) -> ~ ((iter i
(x0 )) = (iter j (x0 ))))).
Axiom cycle : forall (n:Z), ((mu ) <= n)%Z -> ((iter (n + (lambda ))%Z
(x0 )) = (iter n (x0 ))).
Axiom cycle_induction : forall (n:Z), ((mu ) <= n)%Z -> forall (k:Z),
(0%Z <= k)%Z -> ((iter (n + ((lambda ) * k)%Z)%Z (x0 )) = (iter n (x0 ))).
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 dist: Z -> Z -> Z.
Axiom dist_def : forall (i:Z) (j:Z), ((mu ) <= i)%Z -> (((mu ) <= j)%Z ->
((0%Z <= (dist i j))%Z /\ (((iter (i + (dist i j))%Z (x0 )) = (iter j
(x0 ))) /\ forall (k:Z), (0%Z <= k)%Z -> (((iter (i + k)%Z (x0 )) = (iter j
(x0 ))) -> ((dist i j) <= k)%Z)))).
Definition rel(t2:t) (t1:t): Prop := exists i:Z, (t1 = (iter i (x0 ))) /\
((t2 = (iter (i + 1%Z)%Z (x0 ))) /\ (((1%Z <= i)%Z /\
(i <= ((mu ) + (lambda ))%Z)%Z) /\ (((mu ) <= i)%Z ->
((dist ((2%Z * i)%Z + 2%Z)%Z (i + 1%Z)%Z) < (dist (2%Z * i)%Z i))%Z))).
Theorem WP_parameter_tortoise_hare : forall (hare:t), forall (tortoise:t),
(exists t1:Z, ((1%Z <= t1)%Z /\ (t1 <= ((mu ) + (lambda ))%Z)%Z) /\
((tortoise = (iter t1 (x0 ))) /\ ((hare = (iter (2%Z * t1)%Z (x0 ))) /\
forall (i:Z), ((1%Z <= i)%Z /\ (i < t1)%Z) -> ~ ((iter i
(x0 )) = (iter (2%Z * i)%Z (x0 )))))) -> ((~ (tortoise = hare)) ->
forall (tortoise1:t), (tortoise1 = (f tortoise)) -> forall (hare1:t),
(hare1 = (f (f hare))) -> ((exists t1:Z, ((1%Z <= t1)%Z /\
(t1 <= ((mu ) + (lambda ))%Z)%Z) /\ ((tortoise1 = (iter t1 (x0 ))) /\
((hare1 = (iter (2%Z * t1)%Z (x0 ))) /\ forall (i:Z), ((1%Z <= i)%Z /\
(i < t1)%Z) -> ~ ((iter i (x0 )) = (iter (2%Z * i)%Z (x0 )))))) ->
(rel tortoise1 tortoise))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
clear H3.
destruct H as (i, (h1, (h2, (h3, h4)))).
red.
exists i; intuition.
subst.
rewrite iter_s2 with (k := (i+1)%Z).
apply f_equal.
ring_simplify (i+1-1)%Z; auto.
omega.
assert (mu1: (mu <= 2*i+2)%Z) by omega.
assert (mu2: (mu <= i+1)%Z) by omega.
generalize (dist_def (2*i+2) (i+1) mu1 mu2)%Z.
intros (d1, (d2, d3)).
clear mu1 mu2.
assert (mu1: (mu <= 2*i)%Z) by omega.
generalize (dist_def (2*i) i mu1 H4)%Z.
intros (d'1, (d'2, d'3)).
apply Zle_lt_trans with (dist (2 * i) i - 1)%Z.
apply d3.
assert (case: (dist (2*i) i = 0 \/ dist (2*i) i > 0)%Z) by omega. destruct case.
rewrite H5 in d'2.
subst.
absurd (iter i x0 = iter (2 * i) x0)%Z; auto.
symmetry.
ring_simplify (2*i+0)%Z in d'2.
auto.
omega.
rewrite iter_s2; try omega.
rewrite iter_s2 with (k:=(i+1)%Z); try omega.
apply f_equal.
ring_simplify (i+1-1)%Z.
ring_simplify (2 * i + 2 + (dist (2 * i) i - 1) - 1)%Z.
auto.
omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -66,9 +66,18 @@ Definition contents (a:Type)(u:(ref a)): a :=
end.
Implicit Arguments contents.
Parameter dist: Z -> Z -> Z.
Axiom dist_def : forall (i:Z) (j:Z), ((mu ) <= i)%Z -> (((mu ) <= j)%Z ->
((0%Z <= (dist i j))%Z /\ (((iter (i + (dist i j))%Z (x0 )) = (iter j
(x0 ))) /\ forall (k:Z), (0%Z <= k)%Z -> (((iter (i + k)%Z (x0 )) = (iter j
(x0 ))) -> ((dist i j) <= k)%Z)))).
Definition rel(t2:t) (t1:t): Prop := exists i:Z, (t1 = (iter i (x0 ))) /\
((t2 = (iter (i + 1%Z)%Z (x0 ))) /\ ((1%Z <= i)%Z /\
(i <= ((mu ) + (lambda ))%Z)%Z)).
((t2 = (iter (i + 1%Z)%Z (x0 ))) /\ (((1%Z <= i)%Z /\
(i <= ((mu ) + (lambda ))%Z)%Z) /\ (((mu ) <= i)%Z ->
((dist ((2%Z * i)%Z + 2%Z)%Z (i + 1%Z)%Z) < (dist (2%Z * i)%Z i))%Z))).
Theorem WP_parameter_tortoise_hare : forall (hare:t), forall (tortoise:t),
(exists t1:Z, ((1%Z <= t1)%Z /\ (t1 <= ((mu ) + (lambda ))%Z)%Z) /\
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/tortoise_and_hare/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<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="../tortoise_and_hare.mlw" verified="true" expanded="true">
<theory name="WP TortoiseAndHare" verified="true" expanded="true">
<goal name="cycle_induction" sum="8659f3dab2f3a5008349cef96ac38e76" proved="true" expanded="true">
<goal name="cycle_induction" sum="8659f3dab2f3a5008349cef96ac38e76" proved="true" expanded="true" shape="ainfix =axainfix +V0ainfix *alambdaV1axV0Iainfix <=c0V1FIainfix <=amuV0F">
<proof prover="coq" timelimit="10" edited="tortoise_and_hare_WP_TortoiseAndHare_cycle_induction_1.v" obsolete="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare" expl="correctness of parameter tortoise_hare" sum="3b8223899a3507ff2191c4d541bd6b68" proved="true" expanded="true">
<goal name="WP_parameter tortoise_hare" expl="correctness of parameter tortoise_hare" sum="d6e9d75196256880a379574cca2ebe20" proved="true" expanded="true" shape="iainfix =V1V0NarelV2V1Aainfix =axV5axainfix *c2V5NIainfix <V5V4Aainfix <=c1V5FAainfix =V3axainfix *c2V4Aainfix =V2axV4Aainfix <=V4ainfix +amualambdaAainfix <=c1V4EIainfix =V3afafV0FIainfix =V2afV1FtIainfix =axV7axainfix *c2V7NIainfix <V7V6Aainfix <=c1V7FAainfix =V0axainfix *c2V6Aainfix =V1axV6Aainfix <=V6ainfix +amualambdaAainfix <=c1V6EFFAainfix =axV9axainfix *c2V9NIainfix <V9V8Aainfix <=c1V9FAainfix =afafax0axainfix *c2V8Aainfix =afax0axV8Aainfix <=V8ainfix +amualambdaAainfix <=c1V8E">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter tortoise_hare.1" expl="loop invariant init" sum="01ab8eb4fc1286d62c9ac669eafd74ab" proved="true" expanded="true">
<goal name="WP_parameter tortoise_hare.1" expl="loop invariant init" sum="07f80d0dfb5985b1b01f74251c85ab1e" proved="true" expanded="true" shape="ainfix =axV1axainfix *c2V1NIainfix <V1V0Aainfix <=c1V1FAainfix =afafax0axainfix *c2V0Aainfix =afax0axV0Aainfix <=V0ainfix +amualambdaAainfix <=c1V0E">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare.2" expl="loop invariant preservation" sum="3cfb58d4bd4498e2b72ee3004fe49be2" proved="true" expanded="true">
<goal name="WP_parameter tortoise_hare.2" expl="loop invariant preservation" sum="521036be3a2083ccb50ee29dd1609b3a" proved="true" expanded="true" shape="ainfix =axV5axainfix *c2V5NIainfix <V5V4Aainfix <=c1V5FAainfix =V3axainfix *c2V4Aainfix =V2axV4Aainfix <=V4ainfix +amualambdaAainfix <=c1V4EIainfix =V3afafV0FIainfix =V2afV1FIainfix =V1V0NIainfix =axV7axainfix *c2V7NIainfix <V7V6Aainfix <=c1V7FAainfix =V0axainfix *c2V6Aainfix =V1axV6Aainfix <=V6ainfix +amualambdaAainfix <=c1V6EFF">
<proof prover="coq" timelimit="10" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v" obsolete="false">
<result status="valid" time="0.95"/>
<result status="valid" time="0.94"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare.3" expl="loop variant decreases" sum="15ca1bc4cde2b54b14d6e9adc5d5ca67" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.34"/>
<goal name="WP_parameter tortoise_hare.3" expl="loop variant decreases" sum="890862abe98aa7ebf28c819b14028671" proved="true" expanded="true" shape="arelV2V1Iainfix =axV5axainfix *c2V5NIainfix <V5V4Aainfix <=c1V5FAainfix =V3axainfix *c2V4Aainfix =V2axV4Aainfix <=V4ainfix +amualambdaAainfix <=c1V4EIainfix =V3afafV0FIainfix =V2afV1FIainfix =V1V0NIainfix =axV7axainfix *c2V7NIainfix <V7V6Aainfix <=c1V7FAainfix =V0axainfix *c2V6Aainfix =V1axV6Aainfix <=V6ainfix +amualambdaAainfix <=c1V6EFF">
<proof prover="coq" timelimit="10" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_1.v" obsolete="false">
<result status="valid" time="0.81"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare.4" expl="normal postcondition" sum="e698959e67b54437dd880cff04dfdaca" proved="true" expanded="true">
<goal name="WP_parameter tortoise_hare.4" expl="normal postcondition" sum="1d9481e1562156fe54c6a0d1f99ef4c8" proved="true" expanded="true" shape="tIainfix =V1V0NNIainfix =axV3axainfix *c2V3NIainfix <V3V2Aainfix <=c1V3FAainfix =V0axainfix *c2V2Aainfix =V1axV2Aainfix <=V2ainfix +amualambdaAainfix <=c1V2EFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</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