Commit 5c906623 authored by Martin Clochard's avatar Martin Clochard

random_access_list: replaced Coq proof with simple lemma function

parent c70f085d
......@@ -30,8 +30,16 @@ module RandomAccessList
| Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
end
lemma length_flatten:
forall l: list ('a, 'a). length (flatten l) = 2 * length l
let rec lemma length_flatten (l:list ('a,'a))
ensures { length (flatten l) = 2 * length l }
variant { l }
= match l with
| Cons (_,_) q -> length_flatten q
| Nil -> ()
end
(*lemma length_flatten:
forall l: list ('a, 'a). length (flatten l) = 2 * length l*)
function elements (l: ral 'a) : list 'a
= match l with
......
......@@ -4,19 +4,27 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="6" memlimit="1000"/>
<prover id="5" name="Coq" version="8.4pl2" timelimit="6" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="1" memlimit="1000"/>
<file name="../random_access_list.mlw" expanded="true">
<theory name="RandomAccessList" sum="d4e729fc281cff0f1f6b9c21461a02b6" expanded="true">
<goal name="length_flatten" expanded="true">
<proof prover="5" edited="random_access_list_RandomAccessList_length_flatten_1.v"><result status="valid" time="0.83"/></proof>
<theory name="RandomAccessList" sum="d952bd09a31c38ca601c47b7856a5416" expanded="true">
<goal name="WP_parameter length_flatten" expl="VC for length_flatten">
<transf name="split_goal_wp">
<goal name="WP_parameter length_flatten.1" expl="1. variant decrease">
<proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter length_flatten.2" expl="2. postcondition">
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter length_flatten.3" expl="3. postcondition">
<proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter size" expl="VC for size">
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="0"><result status="valid" time="0.02" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter nth_flatten" expl="VC for nth_flatten">
<transf name="split_goal_wp">
......@@ -33,27 +41,27 @@
<proof prover="6"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter nth_flatten.5" expl="5. postcondition">
<proof prover="0"><result status="unknown" time="0.04"/></proof>
<proof prover="0" obsolete="true"><result status="unknown" time="0.04"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter get" expl="VC for get" expanded="true">
<goal name="WP_parameter get" expl="VC for get">
<proof prover="0"><result status="valid" time="0.34" steps="410"/></proof>
</goal>
</theory>
<theory name="RAL" sum="ef67f0d6811c1a4189d9e2bd83248eb7" expanded="true">
<goal name="WP_parameter empty" expl="VC for empty" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter size" expl="VC for size" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
<goal name="WP_parameter size" expl="VC for size">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="WP_parameter cons" expl="VC for cons" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
<goal name="WP_parameter cons" expl="VC for cons">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter get" expl="VC for get" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
<goal name="WP_parameter get" expl="VC for get">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
</file>
......
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