new VC to prove well-foundedness of user-provided variants

fixes issue #57

a new theory relations.WellFounded is introduced for this purpose
(and must be imported whenever one wants to make use of a custom
relation for a variant)

it defines, inductively, a notion of accessibility for a given
predicate R (x is accessible whenever all elements smaller than x for R
are alreay accessible)

whenever one has to prove that a variant decreases, a new VC is also
generated, to show that the old value of the variant is accessible
for the order relation

note: accessibility being defined inductively, proving well-foundedness
is out of reach of SMT solvers; but at least this is sound now
parent 6af5c237
......@@ -8,7 +8,6 @@ module TortoiseAndHare
use import int.Int
use int.Iter
type t
val predicate eq (x y : t)
ensures { result <-> x = y }
......@@ -56,6 +55,7 @@ module TortoiseAndHare
Actually, we even prove that the code runs in time O(lambda + mu). *)
use import ref.Ref
use import relations.WellFounded
(* the minimal distance between x i and x j *)
function dist int int : int
......@@ -70,6 +70,8 @@ module TortoiseAndHare
exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda /\
(i >= mu -> dist (2*i+2) (i+1) < dist (2*i) i)
axiom wfrel: well_founded rel
let tortoise_hare () =
let tortoise = ref (f x0) in
let hare = ref (f (f x0)) in
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
......@@ -7,15 +7,20 @@ 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_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_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 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.
......@@ -30,7 +35,7 @@ Parameter f: t -> t.
Parameter x0: t.
(* Why3 assumption *)
Definition x (i:Z): t := (iter (fun (y0:t) => (f y0)) i x0).
Definition x (i:Z) : t := iter (fun (y0:t) => (f y0)) i x0.
Parameter mu: Z.
......@@ -40,51 +45,82 @@ 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 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)).
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]].
Arguments mk_ref {a}.
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:ref a) : a :=
match v with
| (mk_ref x1) => x1
| mk_ref x1 => x1
end.
(* Why3 assumption *)
Inductive acc {a:Type} {a_WT:WhyType a}: (a -> a -> bool) -> a -> Prop :=
| acc_x :
forall (r:a -> a -> bool) (x1:a),
(forall (y:a), (((r y) x1) = true) -> acc r y) -> acc r x1.
(* Why3 assumption *)
Definition well_founded {a:Type} {a_WT:WhyType a} (r:a -> a -> bool) : Prop :=
forall (x1:a), acc r x1.
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)))).
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))).
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))).
Parameter rel_closure: t -> t -> bool.
Axiom rel_closure_def :
forall (y:t) (y1:t), (((rel_closure y) y1) = true) <-> (rel y y1).
Axiom wfrel : well_founded rel_closure.
(* 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))) ->
(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) /\ (acc rel_closure tortoise).
(* Why3 intros hare tortoise (t1,((h1,h2),(h3,(h4,h5)))) h6 h7 tortoise1 h8
hare1 h9. *)
Proof.
intros hare tortoise (i,((h1,h2),(h3,(h4,h5)))) h6 h7 tortoise1 h8 hare1 h9.
split. 2: apply wfrel.
exists i; intuition.
subst.
unfold x.
......
......@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tortoise_and_hare.mlw" proved="true">
......@@ -17,14 +18,14 @@
<goal name="VC tortoise_hare" expl="VC for tortoise_hare" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC tortoise_hare.0" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="77"/></proof>
<proof prover="4" obsolete="true"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC tortoise_hare.1" expl="loop variant decrease" proved="true">
<proof prover="0" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_1.v"><result status="valid" time="0.44"/></proof>
<proof prover="1" memlimit="1000" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_1.v"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC tortoise_hare.2" expl="loop invariant preservation" proved="true">
<proof prover="0" timelimit="10" memlimit="0" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v"><result status="valid" time="0.56"/></proof>
<proof prover="1" timelimit="10" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v"><result status="valid" time="0.56"/></proof>
</goal>
</transf>
</goal>
......
......@@ -76,6 +76,7 @@ module TreeReconstruction
use export Tree
use import list.Length
use import relations.WellFounded
(* termination of build_rec (below) requires a lexicographic order *)
predicate lex (x1 x2: (list int, int)) =
......@@ -88,6 +89,8 @@ module TreeReconstruction
| _ -> false
end
axiom wflex: well_founded lex
exception Failure
(* used to signal the algorithm's failure i.e. there is no tree *)
......
......@@ -3,8 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="29" steplimit="0" memlimit="0"/>
<prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vstte12_tree_reconstruction.mlw" proved="true">
......@@ -44,28 +45,28 @@
<goal name="VC build_rec" expl="VC for build_rec" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC build_rec.0" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC build_rec.1" expl="exceptional postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC build_rec.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC build_rec.3" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="46"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="59"/></proof>
</goal>
<goal name="VC build_rec.4" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="82"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="VC build_rec.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC build_rec.6" expl="exceptional postcondition" proved="true">
<proof prover="5" edited="vstte12_tree_reconstruction_TreeReconstruction_VC_build_rec_1.v"><result status="valid" time="0.48"/></proof>
<proof prover="1" edited="vstte12_tree_reconstruction_TreeReconstruction_VC_build_rec_1.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="VC build_rec.7" expl="exceptional postcondition" proved="true">
<proof prover="5" edited="vstte12_tree_reconstruction_TreeReconstruction_VC_build_rec_2.v"><result status="valid" time="0.36"/></proof>
<proof prover="1" edited="vstte12_tree_reconstruction_TreeReconstruction_VC_build_rec_2.v"><result status="valid" time="0.36"/></proof>
</goal>
</transf>
</goal>
......@@ -77,15 +78,15 @@
<goal name="VC harness" expl="VC for harness" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC harness.0" expl="postcondition" proved="true">
<proof prover="5" edited="vstte12_tree_reconstruction_Harness_VC_harness_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="1" edited="vstte12_tree_reconstruction_Harness_VC_harness_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="VC harness.1" expl="exceptional postcondition" proved="true">
<proof prover="5" edited="vstte12_tree_reconstruction_Harness_VC_harness_2.v"><result status="valid" time="0.35"/></proof>
<proof prover="1" edited="vstte12_tree_reconstruction_Harness_VC_harness_2.v"><result status="valid" time="0.35"/></proof>
</goal>
</transf>
</goal>
<goal name="VC harness2" expl="VC for harness2" proved="true">
<proof prover="5" edited="vstte12_tree_reconstruction_Harness_VC_harness2_1.v"><result status="valid" time="0.49"/></proof>
<proof prover="1" edited="vstte12_tree_reconstruction_Harness_VC_harness2_1.v"><result status="valid" time="0.49"/></proof>
</goal>
</theory>
<theory name="ZipperBasedTermination" proved="true">
......@@ -95,7 +96,7 @@
</theory>
<theory name="ZipperBased" proved="true">
<goal name="forest_depths_append" proved="true">
<proof prover="5" timelimit="10" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="5" timelimit="10" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="g_append" proved="true">
<transf name="induction_ty_lex" proved="true" >
......@@ -126,10 +127,10 @@
</transf>
</goal>
<goal name="key_lemma" proved="true">
<proof prover="5" edited="vstte12_tree_reconstruction_ZipperBased_key_lemma_2.v"><result status="valid" time="0.71"/></proof>
<proof prover="5" timelimit="5" memlimit="1000" edited="vstte12_tree_reconstruction_ZipperBased_key_lemma_2.v"><result status="valid" time="0.71"/></proof>
</goal>
<goal name="right_nil" proved="true">
<proof prover="5" timelimit="29" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="0.42"/></proof>
<proof prover="5" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="main_lemma" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.07"/></proof>
......
......@@ -78,9 +78,10 @@ type vc_env = {
fs_int_pl : lsymbol;
fs_int_mn : lsymbol;
exn_count : int ref;
ps_wf_acc : lsymbol;
}
let mk_env {Theory.th_export = ns} kn tuc = {
let mk_env {Theory.th_export = ns} {Theory.th_export = ns2} kn tuc = {
known_map = kn;
ts_ranges = tuc.Theory.uc_ranges;
ps_int_le = Theory.ns_find_ls ns ["infix <="];
......@@ -90,8 +91,17 @@ let mk_env {Theory.th_export = ns} kn tuc = {
fs_int_pl = Theory.ns_find_ls ns ["infix +"];
fs_int_mn = Theory.ns_find_ls ns ["infix -"];
exn_count = ref 0;
ps_wf_acc = Theory.ns_find_ls ns2 ["acc"];
}
let acc env r t =
let ps = env.ps_wf_acc in
if not (Mid.mem ps.ls_name env.known_map) then
Loc.errorm ?loc:t.t_loc "please import relations.WellFounded";
let ty = t_type t in
let r = t_closure r [ty; ty] None in
ps_app ps [r; t]
(* every exception-catching clause is represented by
a unique integer, so that we can move code inside
try-with expressions without capturing exceptions *)
......@@ -100,7 +110,10 @@ let new_exn env = incr env.exn_count; !(env.exn_count)
(* FIXME: cannot verify int.why because of a cyclic dependency.
int.Int is used for the "for" loops and for integer variants.
We should be able to extract the necessary lsymbols from kn. *)
let mk_env env kn tuc = mk_env (Env.read_theory env ["int"] "Int") kn tuc
let mk_env env kn tuc =
let th_int = Env.read_theory env ["int"] "Int" in
let th_wf = Env.read_theory env ["relations"] "WellFounded" in
mk_env th_int th_wf kn tuc
(* explanation labels *)
......@@ -245,7 +258,7 @@ let decrease env loc lab expl olds news =
let rec decr olds news = match olds, news with
| (old_t, Some old_r)::olds, (t, Some r)::news
when oty_equal old_t.t_ty t.t_ty && ls_equal old_r r ->
let dt = ps_app r [t; old_t] in
let dt = t_and (ps_app r [t; old_t]) (acc env r old_t) in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
| (old_t, None)::olds, (t, None)::news
when oty_equal old_t.t_ty t.t_ty ->
......
......@@ -161,13 +161,34 @@ end
module WellFounded
inductive acc (r: 'a -> 'a -> bool) (x: 'a) =
| acc_x: forall r, x: 'a. (forall y. r y x -> acc r y) -> acc r x
predicate well_founded (r: 'a -> 'a -> bool) =
forall x. acc r x
end
(* the following module introduces a circular dependency *)
(*
module WFltof
use import int.Int
use import WellFounded
type t
function f t : int
axiom f_nonneg: forall x. 0 <= f x
predicate r t t
predicate ltof (x y: t) = f x < f y
inductive acc (x: t) =
| acc_x: forall x: t. (forall y: t. r y x -> acc y) -> acc x
let rec lemma acc_ltof (n: int)
requires { 0 <= n }
ensures { forall x. f x < n -> acc ltof x }
variant { n }
= if n > 0 then acc_ltof (n-1)
axiom well_founded: forall x: t. acc x
lemma wf_ltof: well_founded ltof
end
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment