tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v 3.89 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
(* 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 f: Z  -> Z.


Parameter m:  Z.


Axiom dom_f : forall (x:Z), ((0%Z <= x)%Z /\ (x <  (m ))%Z) ->
  ((0%Z <= (f x))%Z /\ ((f x) <  (m ))%Z).

Parameter x0:  Z.


Axiom x0_range : (0%Z <= (x0 ))%Z /\ ((x0 ) <  (m ))%Z.

Parameter iter: Z -> Z  -> Z.


Axiom iter_0 : forall (x:Z), ((iter 0%Z x) = x).

Axiom iter_s : forall (k:Z) (x:Z), (0%Z <  k)%Z -> ((iter k
  x) = (iter (k - 1%Z)%Z (f x))).

Axiom iter_1 : forall (x:Z), ((iter 1%Z x) = (f x)).

Axiom iter_s2 : forall (k:Z) (x:Z), (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 ))).

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.

Definition rel(t2:Z) (t1:Z): Prop := exists i:Z, (t1 = (iter i (x0 ))) /\
  ((t2 = (iter (i + 1%Z)%Z (x0 ))) /\ ((1%Z <= i)%Z /\
  (i <= ((lambda ) + (mu ))%Z)%Z)).

Theorem WP_parameter_tortoise_hare : forall (hare:Z), forall (tortoise:Z),
  (exists t:Z, ((1%Z <= t)%Z /\ (t <= ((lambda ) + (mu ))%Z)%Z) /\
  ((tortoise = (iter t (x0 ))) /\ ((hare = (iter (2%Z * t)%Z (x0 ))) /\
  forall (i:Z), ((1%Z <= i)%Z /\ (i <  t)%Z) -> ~ ((iter i
  (x0 )) = (iter (2%Z * i)%Z (x0 )))))) -> ((~ (tortoise = hare)) ->
  forall (tortoise1:Z), (tortoise1 = (f tortoise)) -> forall (hare1:Z),
  (hare1 = (f (f hare))) -> exists t:Z, ((1%Z <= t)%Z /\
  (t <= ((lambda ) + (mu ))%Z)%Z) /\ ((tortoise1 = (iter t (x0 ))) /\
  ((hare1 = (iter (2%Z * t)%Z (x0 ))) /\ forall (i:Z), ((1%Z <= i)%Z /\
  (i <  t)%Z) -> ~ ((iter i (x0 )) = (iter (2%Z * i)%Z (x0 )))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros hare tortoise (t, (ht, (eqt, (eqh, h)))).
intros; subst.
assert (dis: forall i : Z, (1 <= i <= t)%Z -> iter i x0 <> iter (2 * i) x0).
intros i hi.
assert (case: (i < t \/ i = t)%Z) by omega. destruct case.
apply (h i); omega.
subst; omega. clear h H.

exists (t + 1)%Z; intuition.
assert (case: (t+1 <= lambda + mu \/ t+1> lambda+mu)%Z) by omega.
  destruct case.
assumption.
assert (t = lambda+mu)%Z by omega. subst.
clear H0 H1.
pose (i := (lambda+mu-(lambda+mu) mod lambda)%Z).
generalize lambda_range mu_range. intros hlam hmu.
assert (lambda_pos: (lambda > 0)%Z) by omega.
generalize (Z_mod_lt (lambda+mu) lambda lambda_pos)%Z. intro hr.
generalize (Z_div_mod_eq (lambda+mu) 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).
assert (ind: (forall k: Z, 0 <= k -> iter (i + lambda*k) x0 = iter i x0)%Z).
apply natlike_ind.
ring_simplify (i + lambda * 0)%Z; auto.
intros.
unfold Zsucc.
replace (i + lambda * (x + 1))%Z with ((i+lambda*x)+lambda)%Z by ring.
rewrite cycle; auto.
assert (0 <= lambda * x)%Z.
apply Zmult_le_0_compat; omega.
omega.
replace (2*i)%Z with (i + lambda * ((lambda + mu) / lambda))%Z.
symmetry. apply ind.
apply Z_div_pos; omega.
subst i; omega.

rewrite (iter_s2 (t+1)%Z); intuition.
ring_simplify (t+1-1)%Z; auto.
rewrite (iter_s2 (2*(t+1))%Z); intuition.
ring_simplify (2 * (t + 1) - 1) %Z.
rewrite (iter_s2 (2*t+1)%Z); intuition.
ring_simplify (2 * t + 1 - 1) %Z; auto.
apply (dis i); omega.
Qed.
(* DO NOT EDIT BELOW *)