Commit 09096e79 by Jean-Christophe Filliatre

### updated proof sessions

parent d49323d1
 ... ... @@ -4,7 +4,6 @@ bignum.mlw counting_sort.mlw cursor.mlw dijkstra.mlw ewd673.mlw fibonacci.mlw find.mlw gcd.mlw ... ...
 ... ... @@ -2,11 +2,11 @@ ... ...
No preview for this file type
 ... ... @@ -4,75 +4,98 @@ ... ...
No preview for this file type
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import BuiltIn. Require BuiltIn. Require HighOrd. Require int.Int. (* Why3 assumption *) Definition unit := unit. Parameter t : Type. Parameter iter: forall {a:Type} {a_WT:WhyType a}, (a -> a) -> Z -> a -> a. Parameter f: t -> t. 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))))). Parameter x0: t. Axiom iter_1 : forall {a:Type} {a_WT:WhyType a}, forall (f:(a -> a)) (x:a), ((iter f 1%Z x) = (f x)). Parameter iter: Z -> t -> t. 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 iter_0 : forall (x:t), ((iter 0%Z x) = x). Axiom t : Type. Parameter t_WhyType : WhyType t. Existing Instance t_WhyType. Axiom iter_s : forall (k:Z) (x:t), (0%Z < k)%Z -> ((iter k x) = (iter (k - 1%Z)%Z (f x))). Parameter eq: t -> t -> Prop. Axiom iter_1 : forall (x:t), ((iter 1%Z x) = (f x)). Axiom eq_spec : forall (x:t) (y:t), (eq x y) <-> (x = y). Parameter f: t -> t. Axiom iter_s2 : forall (k:Z) (x:t), (0%Z < k)%Z -> ((iter k x) = (f (iter (k - 1%Z)%Z x))). Parameter x0: t. (* Why3 assumption *) Definition x (i:Z): t := (iter (fun (y0:t) => (f y0)) i x0). Parameter mu: Z. ... ... @@ -35,48 +45,52 @@ 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)))). ((~ (i = j)) -> ~ ((x i) = (x j)))). Axiom cycle : forall (n:Z), (mu <= n)%Z -> ((iter (n + lambda)%Z x0) = (iter n x0)). 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 -> ((iter (n + (lambda * k)%Z)%Z x0) = (iter n x0)). (0%Z <= k)%Z -> ((x (n + (lambda * k)%Z)%Z) = (x n)). (* Why3 assumption *) Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. 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)(v:(ref a)): a := Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a := match v with | (mk_ref x) => x | (mk_ref x1) => x1 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)))). ((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 = (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 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 WP_parameter_tortoise_hare : forall (hare:t) (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))) -> (rel tortoise1 tortoise)). 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))) -> (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. ... ... @@ -114,5 +128,4 @@ 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 ZArith. Require Import Rbase. Require Import BuiltIn. Require BuiltIn. Require HighOrd. Require int.Int. (* Why3 assumption *) Definition unit := unit. Parameter mark : Type. Parameter iter: forall {a:Type} {a_WT:WhyType a}, (a -> a) -> Z -> a -> a. Parameter at1: forall (a:Type), a -> mark -> 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))))). Implicit Arguments at1. Axiom iter_1 : forall {a:Type} {a_WT:WhyType a}, forall (f:(a -> a)) (x:a), ((iter f 1%Z x) = (f x)). Parameter old: forall (a:Type), a -> a. 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))). Implicit Arguments old. Axiom t : Type. Parameter t_WhyType : WhyType t. Existing Instance t_WhyType. Parameter t : Type. Parameter eq: t -> t -> Prop. Parameter f: t -> t. Axiom eq_spec : forall (x:t) (y:t), (eq x y) <-> (x = y). 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))). (* 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 mu_range : (0%Z <= (mu ))%Z. Axiom lambda_range : (1%Z <= (lambda ))%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 ))))). (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 -> ((iter (n + (lambda ))%Z (x0 )) = (iter n (x0 ))). Axiom cycle : forall (n:Z), (mu <= n)%Z -> ((x (n + lambda)%Z) = (x n)). 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 ))). (* Why3 goal *) Theorem cycle_induction : forall (n:Z), (mu <= n)%Z -> forall (k:Z), (0%Z <= k)%Z -> ((x (n + (lambda * k)%Z)%Z) = (x n)). (* Why3 intros n h1 k h2. *) (* 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. replace (n + lambda * (x1 + 1))%Z with ((n+lambda*x1)+lambda)%Z by ring. rewrite cycle; auto. assert (0 <= lambda * x)%Z. assert (0 <= lambda * x1)%Z. apply Zmult_le_0_compat; (generalize lambda_range; omega). omega. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -2,23 +2,27 @@ ... ...
No preview for this file type
 ... ... @@ -4,15 +4,10 @@ ... ... @@ -20,46 +15,11 @@ ... ... @@ -76,29 +36,121 @@