Commit 72b7667e by Jean-Christophe Filliâtre

### optimal replay: fixed (and simplified) proof

parent 97466b34
 ... ... @@ -57,7 +57,7 @@ module OptimalReplay 0 < d[k] = d[g[k]] + 1 /\ forall k': int. g[k] < k' < k -> d[g[k]] < d[k'] } (* could be deduced from above, but avoids induction *) invariant { forall k: int. 0 <= k < i -> path d[k] k } invariant { forall k: int. 0 <= k < i -> distance d[k] k } let j = ref (i-1) in while g[!j] >= f i do invariant { f i <= !j < i /\ !count + d[!j] <= i-1 } ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. (* Why3 assumption *) Definition unit := unit. Axiom qtmark : Type. Parameter qtmark_WhyType : WhyType qtmark. Existing Instance qtmark_WhyType. (* 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 x) => x end. (* Why3 assumption *) Inductive array (a:Type) := | mk_array : Z -> (map.Map.map Z a) -> array a. Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). Existing Instance array_WhyType. Implicit Arguments mk_array [[a]]. (* Why3 assumption *) Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) := match v with | (mk_array x x1) => x1 end. (* Why3 assumption *) Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z := match v with | (mk_array x x1) => x end. (* Why3 assumption *) Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a := (map.Map.get (elts a1) i). (* Why3 assumption *) Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (map.Map.set (elts a1) i v)). Parameter n: Z. Axiom n_nonneg : (0%Z < n)%Z. Parameter f: Z -> Z. Axiom f_prop : forall (k:Z), ((0%Z < k)%Z /\ (k < n)%Z) -> ((0%Z <= (f k))%Z /\ ((f k) < k)%Z). (* Why3 assumption *) Inductive path: Z -> Z -> Prop := | path0 : (path 0%Z 0%Z) | paths : forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> forall (d:Z) (j:Z), (path d j) -> ((((f i) <= j)%Z /\ (j < i)%Z) -> (path (d + 1%Z)%Z i)). (* Why3 assumption *) Definition distance (d:Z) (i:Z): Prop := (path d i) /\ forall (d':Z), (path d' i) -> (d <= d')%Z. Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.2," timelimit 30. Ltac z3 := why3 "Z3,4.3.1," timelimit 30. (* Why3 goal *) Theorem WP_parameter_distance : let o := n in ((0%Z <= o)%Z -> forall (g:Z) (g1:(map.Map.map Z Z)), (((0%Z < g)%Z \/ (0%Z = g)) /\ ((g = o) /\ forall (i:Z), (((0%Z < i)%Z \/ (0%Z = i)) /\ (i < o)%Z) -> ((map.Map.get g1 i) = 0%Z))) -> ((0%Z < g)%Z -> forall (g2:(map.Map.map Z Z)), (((0%Z < g)%Z \/ (0%Z = g)) /\ (g2 = (map.Map.set g1 0%Z (-1%Z)%Z))) -> let o1 := n in ((0%Z <= o1)%Z -> forall (d:Z) (d1:(map.Map.map Z Z)), (((0%Z < d)%Z \/ (0%Z = d)) /\ ((d = o1) /\ forall (i:Z), (((0%Z < i)%Z \/ (0%Z = i)) /\ (i < o1)%Z) -> ((map.Map.get d1 i) = 0%Z))) -> let o2 := (n - 1%Z)%Z in (((1%Z < o2)%Z \/ (1%Z = o2)) -> forall (count:Z) (d2:(map.Map.map Z Z)) (g3:(map.Map.map Z Z)), ((((map.Map.get d2 0%Z) = 0%Z) /\ (((map.Map.get g3 0%Z) = (-1%Z)%Z) /\ (((count + (map.Map.get d2 ((o2 + 1%Z)%Z - 1%Z)%Z))%Z < ((o2 + 1%Z)%Z - 1%Z)%Z)%Z \/ ((count + (map.Map.get d2 ((o2 + 1%Z)%Z - 1%Z)%Z))%Z = ((o2 + 1%Z)%Z - 1%Z)%Z)))) /\ ((forall (k:Z), ((0%Z < k)%Z /\ (k < (o2 + 1%Z)%Z)%Z) -> ((((map.Map.get g3 (map.Map.get g3 k)) < (f k))%Z /\ ((((f k) < (map.Map.get g3 k))%Z \/ ((f k) = (map.Map.get g3 k))) /\ ((map.Map.get g3 k) < k)%Z)) /\ (((0%Z < (map.Map.get d2 k))%Z /\ ((map.Map.get d2 k) = ((map.Map.get d2 (map.Map.get g3 k)) + 1%Z)%Z)) /\ forall (k':Z), (((map.Map.get g3 k) < k')%Z /\ (k' < k)%Z) -> ((map.Map.get d2 (map.Map.get g3 k)) < (map.Map.get d2 k'))%Z))) /\ forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < (o2 + 1%Z)%Z)%Z) -> (path (map.Map.get d2 k) k))) -> ((count < n)%Z -> forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < n)%Z) -> forall (d':Z), (path d' k) -> ((map.Map.get d2 k) <= d')%Z))))). (* Why3 intros o h1 g g1 (h2,(h3,h4)) h5 g2 (h6,h7) o1 h8 d d1 (h9,(h10,h11)) o2 h12 count d2 g3 ((h13,(h14,h15)),(h16,h17)) h18 k (h19,h20) d' h21. *) (* intros o _ _ h3 g _ o1 h4 h5 o2 h6 count d g1 ((h7,(h8,h9)),(h10,h11)) h12 k (h13,h14) d' h15. *) intros o h1 g g1 (h2,(h3,h4)) h5 g2 (h6,h7) o1 h8 d d1 (h9,(h10,h11)) o2 h12 count d2 g3 ((h13,(h14,h15)),(h16,h17)) h18 k (h19,h20) d' h21. subst o o1 o2. (* clear h4 h5 h6. *) replace (n-1+1)%Z with n in * by omega. (* clear count h9 h12. *) generalize h19 h20 d' h21. pattern k. apply Z_lt_induction; [clear k h19 h20 d' h21 | omega]. intros k IH hk1 hk2 d' hd'. assert (case: (Map.get d2 k <= d' \/ d' < Map.get d2 k)%Z) by omega. destruct case; auto. destruct hk1. (* 0 < k *) inversion hd'. omega. subst i. assert (h: (0 < k < n)%Z) by omega. generalize (h16 k h). intros h16k. assert (case: (j < Map.get g1 k \/ j = Map.get g1 k \/ j > Map.get g1 k)%Z) by omega. destruct case. (* j < g[k] *) z3. destruct H5. (* j = g[k] *) z3. (* j > g[k] *) z3. (* k = 0 *) ae. Qed.
 ... ... @@ -4,12 +4,11 @@ ... ... @@ -25,7 +24,7 @@ ... ... @@ -34,7 +33,7 @@ ... ... @@ -59,10 +58,10 @@ ... ... @@ -84,25 +83,25 @@ ... ...
No preview for this file type
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!