(* 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.