Commit a9386d3c by Jean-Christophe Filliâtre

cleaning up tortoise and hare proof

parent ae6604e2
 ... ... @@ -41,6 +41,9 @@ module TortoiseAndHare axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n lemma cycle_induction: forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n (* Now comes the code. Two references, tortoise and hare, traverses the sequence (xi) at speed 1 and 2 respectively. We stop whenever they are equal. ... ... @@ -51,7 +54,7 @@ module TortoiseAndHare use import module ref.Ref predicate rel (t2 t1: t) = exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= lambda + mu exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda let tortoise_hare () = let tortoise = ref (f x0) in ... ... @@ -59,7 +62,7 @@ module TortoiseAndHare while !tortoise <> !hare do invariant { exists t: int. 1 <= t <= lambda+mu /\ !tortoise = x t /\ !hare = x (2 * t) /\ 1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\ forall i: int. 1 <= i < t -> x i <> x (2*i) } variant { !tortoise } with rel tortoise := f !tortoise; ... ...
 ... ... @@ -53,6 +53,9 @@ Axiom distinct : forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ 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. ... ... @@ -65,16 +68,16 @@ Implicit Arguments contents. 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 <= ((lambda ) + (mu ))%Z)%Z)). (i <= ((mu ) + (lambda ))%Z)%Z)). Theorem WP_parameter_tortoise_hare : forall (hare:t), forall (tortoise:t), (exists t1:Z, ((1%Z <= t1)%Z /\ (t1 <= ((lambda ) + (mu ))%Z)%Z) /\ (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 <= ((lambda ) + (mu ))%Z)%Z) /\ ((tortoise1 = (iter t1 (x0 ))) /\ (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 *) ... ... @@ -88,32 +91,22 @@ subst; auto. clear h H. exists (t0 + 1)%Z; intuition. assert (case: (t0+1 <= lambda + mu \/ t0+1> lambda+mu)%Z) by omega. assert (case: (t0+1 <= mu+lambda \/ t0+1> mu+lambda)%Z) by omega. destruct case. assumption. assert (t0 = lambda+mu)%Z by omega. subst. assert (t0 = mu+lambda)%Z by omega. subst. clear H0 H1. pose (i := (lambda+mu-(lambda+mu) mod lambda)%Z). 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 (lambda+mu) lambda lambda_pos)%Z. intro hr. generalize (Z_div_mod_eq (lambda+mu) lambda lambda_pos)%Z. intro hq. 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). 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. replace (2*i)%Z with (i + lambda * ((mu+lambda) / lambda))%Z. symmetry. apply cycle_induction; auto. apply Z_div_pos; omega. subst i; omega. ... ...
 (* 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 ))). Theorem 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 ))). (* YOU MAY EDIT THE PROOF BELOW *) intros n hn. apply natlike_ind. ring_simplify (n + lambda * 0)%Z; auto. intros. unfold Zsucc. replace (n + lambda * (x + 1))%Z with ((n+lambda*x)+lambda)%Z by ring. rewrite cycle; auto. assert (0 <= lambda * x)%Z. apply Zmult_le_0_compat; (generalize lambda_range; omega). omega. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -3,26 +3,31 @@ ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!