Commit 889e6779 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Port examples/tortoise_and_hare.

parent 75a60941
(* 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 )))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros hare tortoise (t0, (ht, (eqt, (eqh, h)))).
intros; subst.
assert (dis: forall i : Z, (1 <= i <= t0)%Z -> iter i x0 <> iter (2 * i) x0).
intros i hi.
assert (case: (i < t0 \/ i = t0)%Z) by omega. destruct case.
apply (h i); omega.
subst; auto.
clear h H.
exists (t0 + 1)%Z; intuition.
assert (case: (t0+1 <= mu+lambda \/ t0+1> mu+lambda)%Z) by omega.
destruct case.
assumption.
assert (t0 = mu+lambda)%Z by omega. subst.
clear H0 H1.
pose (i := (mu+lambda-(mu+lambda) mod lambda)%Z).
generalize lambda_range mu_range. intros hlam hmu.
assert (lambda_pos: (lambda > 0)%Z) by omega.
generalize (Z_mod_lt (mu+lambda) lambda lambda_pos)%Z. intro hr.
generalize (Z_div_mod_eq (mu+lambda) lambda lambda_pos)%Z. intro hq.
absurd (iter i x0 = iter (2*i) x0).
red; intro; apply (dis i); auto.
subst i; omega.
assert (hi: (mu <= i)%Z) by (subst i; omega).
replace (2*i)%Z with (i + lambda * ((mu+lambda) / lambda))%Z.
symmetry. apply cycle_induction; auto.
apply Z_div_pos; omega.
subst i; omega.
rewrite (iter_s2 (t0+1)%Z); intuition.
ring_simplify (t0+1-1)%Z; auto.
rewrite (iter_s2 (2*(t0+1))%Z); intuition.
ring_simplify (2 * (t0 + 1) - 1) %Z.
rewrite (iter_s2 (2*t0+1)%Z); intuition.
ring_simplify (2 * t0 + 1 - 1) %Z; auto.
apply (dis i); auto.
omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -5,9 +5,6 @@ Require BuiltIn.
Require HighOrd.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
Parameter iter: forall {a:Type} {a_WT:WhyType a}, (a -> a) -> Z -> a -> a.
Axiom iter_def : forall {a:Type} {a_WT:WhyType a}, forall (f:(a -> a)) (k:Z)
......@@ -86,20 +83,12 @@ Theorem VC_tortoise_hare : forall (hare:t) (tortoise:t), (exists t1:Z,
(tortoise = hare)) -> ((~ (eq tortoise hare)) -> forall (tortoise1:t),
(tortoise1 = (f tortoise)) -> forall (hare1:t), (hare1 = (f (f hare))) ->
(rel tortoise1 tortoise))).
intros hare tortoise (t1,((h1,h2),(h3,(h4,h5)))) h6 h7 tortoise1 h8 hare1 h9.
Qed.
(* Unused content named WP_parameter_tortoise_hare
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
clear H2.
destruct H as (i, (h1, (h2, (h3, h4)))).
red.
Proof.
intros hare tortoise (i,((h1,h2),(h3,(h4,h5)))) h6 h7 tortoise1 h8 hare1 h9.
exists i; intuition.
subst.
rewrite iter_s2 with (k := (i+1)%Z).
apply f_equal.
unfold x.
rewrite iter_s with (k := (i+1)%Z).
ring_simplify (i+1-1)%Z; auto.
omega.
assert (mu1: (mu <= 2*i+2)%Z) by omega.
......@@ -108,24 +97,25 @@ 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 H3)%Z.
generalize (dist_def (2*i) i mu1 H1)%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 H4 in d'2.
rewrite H2 in d'2.
subst.
absurd (iter i x0 = iter (2 * i) x0)%Z; auto.
absurd (iter f i x0 = iter f (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.
unfold x.
rewrite iter_s; try omega.
rewrite iter_s 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.
*)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Parameter iter: forall {a:Type} {a_WT:WhyType a}, (a -> a) -> Z -> a -> a.
Axiom iter_def : forall {a:Type} {a_WT:WhyType a}, forall (f:(a -> a)) (k:Z)
(x:a), (0%Z <= k)%Z -> (((k = 0%Z) -> ((iter f k x) = x)) /\
((~ (k = 0%Z)) -> ((iter f k x) = (iter f (k - 1%Z)%Z (f x))))).
Axiom iter_1 : forall {a:Type} {a_WT:WhyType a}, forall (f:(a -> a)) (x:a),
((iter f 1%Z x) = (f x)).
Axiom iter_s : forall {a:Type} {a_WT:WhyType a}, forall (f:(a -> a)) (k:Z)
(x:a), (0%Z < k)%Z -> ((iter f k x) = (f (iter f (k - 1%Z)%Z x))).
Axiom t : Type.
Parameter t_WhyType : WhyType t.
Existing Instance t_WhyType.
Parameter eq: t -> t -> Prop.
Axiom eq_spec : forall (x:t) (y:t), (eq x y) <-> (x = y).
Parameter f: t -> t.
Parameter x0: t.
(* Why3 assumption *)
Definition x (i:Z): t := (iter (fun (y0:t) => (f y0)) i x0).
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)) -> ~ ((x i) = (x j)))).
Axiom cycle : forall (n:Z), (mu <= n)%Z -> ((x (n + lambda)%Z) = (x n)).
Axiom cycle_induction : forall (n:Z), (mu <= n)%Z -> forall (k:Z),
(0%Z <= k)%Z -> ((x (n + (lambda * k)%Z)%Z) = (x n)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
| 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]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x1) => x1
end.
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 /\ (((x (i + (dist i j))%Z) = (x j)) /\
forall (k:Z), (0%Z <= k)%Z -> (((x (i + k)%Z) = (x j)) -> ((dist i
j) <= k)%Z)))).
(* Why3 assumption *)
Definition rel (t2:t) (t1:t): Prop := exists i:Z, (t1 = (x i)) /\
((t2 = (x (i + 1%Z)%Z)) /\ (((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))).
(* Why3 goal *)
Theorem VC_tortoise_hare : forall (hare:t) (tortoise:t), (exists t1:Z,
((1%Z <= t1)%Z /\ (t1 <= (mu + lambda)%Z)%Z) /\ ((tortoise = (x t1)) /\
((hare = (x (2%Z * t1)%Z)) /\ forall (i:Z), ((1%Z <= i)%Z /\ (i < t1)%Z) ->
~ ((x i) = (x (2%Z * i)%Z))))) -> (((eq tortoise hare) <->
(tortoise = hare)) -> ((~ (eq 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 = (x t1)) /\ ((hare1 = (x (2%Z * t1)%Z)) /\ forall (i:Z),
((1%Z <= i)%Z /\ (i < t1)%Z) -> ~ ((x i) = (x (2%Z * i)%Z)))))).
Proof.
intros hare tortoise (t0,(ht,(h3,(h4,h)))) h6 h7 tortoise1 h8 hare1 h9.
subst.
assert (dis: forall i : Z, (1 <= i <= t0)%Z -> x i <> x (2 * i)).
intros i hi.
assert (case: (i < t0 \/ i = t0)%Z) by omega. destruct case.
apply (h i); omega.
now subst; intuition.
clear h h6 h7.
exists (t0 + 1)%Z; intuition.
assert (case: (t0+1 <= mu+lambda \/ t0+1> mu+lambda)%Z) by omega.
destruct case.
assumption.
assert (t0 = mu+lambda)%Z by omega. subst.
clear H0 H1.
pose (i := (mu+lambda-(mu+lambda) mod lambda)%Z).
generalize lambda_range mu_range. intros hlam hmu.
assert (lambda_pos: (lambda > 0)%Z) by omega.
generalize (Z_mod_lt (mu+lambda) lambda lambda_pos)%Z. intro hr.
generalize (Z_div_mod_eq (mu+lambda) lambda lambda_pos)%Z. intro hq.
absurd (x i = x (2*i)).
red; intro; apply (dis i); auto.
subst i; omega.
assert (hi: (mu <= i)%Z) by (subst i; omega).
replace (2*i)%Z with (i + lambda * ((mu+lambda) / lambda))%Z.
symmetry. apply cycle_induction; auto.
apply Z_div_pos; omega.
subst i; omega.
unfold x.
rewrite (iter_s f (t0+1)%Z); intuition.
ring_simplify (t0+1-1)%Z; auto.
unfold x.
rewrite (iter_s f (2*(t0+1))%Z); intuition.
ring_simplify (2 * (t0 + 1) - 1) %Z.
rewrite (iter_s f (2*t0+1)%Z); intuition.
ring_simplify (2 * t0 + 1 - 1) %Z; auto.
apply (dis i); auto.
omega.
Qed.
......@@ -2,27 +2,29 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tortoise_and_hare.mlw" expanded="true">
<theory name="TortoiseAndHare" sum="7cea2bafc0941407491255aaac08300b" expanded="true">
<theory name="TortoiseAndHare" sum="0f115aa19db42adfa5a102e578b43dba" expanded="true">
<goal name="VC x0" expl="VC for x0">
<transf name="split_goal_wp">
</transf>
</goal>
<goal name="cycle_induction">
<proof prover="0" edited="tortoise_and_hare_WP_TortoiseAndHare_cycle_induction_1.v"><result status="valid" time="0.36"/></proof>
<goal name="cycle_induction" expl="">
<proof prover="1" edited="tortoise_and_hare_WP_TortoiseAndHare_cycle_induction_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC tortoise_hare" expl="VC for tortoise_hare" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC tortoise_hare.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="102"/></proof>
<goal name="VC tortoise_hare" expl="VC for tortoise_hare">
<transf name="split_goal_wp">
<goal name="VC tortoise_hare.1" expl="loop invariant init">
<proof prover="3"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC tortoise_hare.2" expl="2. loop variant decrease" expanded="true">
<proof prover="0" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_1.v" obsolete="true"><undone/></proof>
<goal name="VC tortoise_hare.2" expl="loop variant decrease">
<proof prover="1" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_1.v"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="VC tortoise_hare.3" expl="3. loop invariant preservation" expanded="true">
<proof prover="0" timelimit="10" memlimit="0" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v"><result status="unknown" time="0.27"/></proof>
<goal name="VC tortoise_hare.3" expl="loop invariant preservation">
<proof prover="1" timelimit="10" memlimit="0" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v"><result status="valid" time="0.56"/></proof>
</goal>
</transf>
</goal>
......
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