Commit d0a73309 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

induction on integer: init and rec cases now disjoint fix #90

parent 4a62dea0
......@@ -27,10 +27,10 @@
</goal>
<goal name="Path_shortest_path" proved="true">
<transf name="induction" proved="true" arg1="d">
<goal name="Path_shortest_path.0" proved="true">
<goal name="Path_shortest_path.0" expl="base case" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Path_shortest_path.1" proved="true">
<goal name="Path_shortest_path.1" expl="recursive case" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
......@@ -55,10 +55,10 @@
</goal>
<goal name="inside_or_exit.1" proved="true">
<transf name="case" proved="true" arg1="(mem z s)">
<goal name="inside_or_exit.1.0" proved="true">
<goal name="inside_or_exit.1.0" expl="true case" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inside_or_exit.1.1" proved="true">
<goal name="inside_or_exit.1.1" expl="false case" proved="true">
<proof prover="4"><result status="valid" time="0.84"/></proof>
</goal>
</transf>
......@@ -130,10 +130,10 @@
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6" expl="VC for shortest_path_code" proved="true">
<transf name="case" proved="true" arg1="(v = v1)">
<goal name="WP_parameter shortest_path_code.11.0.6.0" expl="VC for shortest_path_code" proved="true">
<goal name="WP_parameter shortest_path_code.11.0.6.0" expl="true case" proved="true">
<proof prover="3"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.1" expl="VC for shortest_path_code" proved="true">
<goal name="WP_parameter shortest_path_code.11.0.6.1" expl="false case" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
......
......@@ -12,12 +12,12 @@
<transf name="assert" proved="true" arg1="(forall x. 0 &lt; x &lt; j -&gt; sum a (j-x) j = sum a (j-x) (j-1) + a[j-1])">
<goal name="sum_right.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_right.0.0" proved="true">
<goal name="sum_right.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sum_right.0.1" proved="true">
<goal name="sum_right.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_right.0.1.0" proved="true">
<goal name="sum_right.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -66,12 +66,12 @@
<theory name="ExtraLemmas" proved="true">
<goal name="sum_concat" proved="true">
<transf name="induction" proved="true" arg1="k">
<goal name="sum_concat.0" proved="true">
<goal name="sum_concat.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_concat.1" proved="true">
<goal name="sum_concat.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="k">
<goal name="sum_concat.1.0" proved="true">
<goal name="sum_concat.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -82,12 +82,12 @@
<transf name="assert" proved="true" arg1="(forall x. 0 &lt;= x &lt;= j-i -&gt; sum a1 (j-x) j = sum a2 (j-x) j)">
<goal name="sum_frame.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_frame.0.0" proved="true">
<goal name="sum_frame.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_frame.0.1" proved="true">
<goal name="sum_frame.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_frame.0.1.0" proved="true">
<goal name="sum_frame.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -105,16 +105,16 @@
</goal>
<goal name="sum_update" proved="true">
<transf name="induction" proved="true" arg1="h" arg2="from" arg3="i+1">
<goal name="sum_update.0" proved="true">
<goal name="sum_update.0" expl="base case" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.0.0" proved="true">
<goal name="sum_update.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="sum_update.1" proved="true">
<goal name="sum_update.1" expl="recursive case" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.1.0" proved="true">
<goal name="sum_update.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
......
......@@ -20,8 +20,8 @@ open Args_wrapper
(* Documentation of induction:
From task [delta, x: int, delta'(x) |- G(x)], variable x and term bound, builds the tasks:
[delta, x: int, x < bound, delta'(x) |- G(x)] and
[delta, x: int, x >= bound, (forall n, n < x -> delta'(n) -> G(n)), delta'(x) |- G(x)]
[delta, x: int, x <= bound, delta'(x) |- G(x)] and
[delta, x: int, x > bound, (forall n, n < x -> delta'(n) -> G(n)), delta'(x) |- G(x)]
x cannot occur in delta as it can only appear after its declaration (by
construction of the task). Also, G is not part of delta'.
......@@ -253,15 +253,15 @@ let induction x bound env =
(t_implies (Term.t_app_infer lt_int [t_var n; x]) (t_replace x (t_var n) t_delta'))
in
(* x_ge_bound = bound <= x *)
let x_ge_bound_t = t_app_infer le_int [bound; x] in
let x_ge_bound =
create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) x_ge_bound_t in
(* x_gt_bound = bound < x *)
let x_gt_bound_t = t_app_infer lt_int [bound; x] in
let x_gt_bound =
create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) x_gt_bound_t in
let rec_pr = create_prsymbol (gen_ident "Hrec") in
let hrec = create_prop_decl Paxiom rec_pr t_delta' in
let lab_rec = Ident.create_label "expl:recursive case" in
let d = create_prop_decl Pgoal pr (t_label_add lab_rec t) in
[x_ge_bound; hrec; d]
[x_gt_bound; hrec; d]
| Dprop (_p, _pr, _t) ->
if !x_is_passed then
begin
......
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