Commit 7c1dbac9 authored by Martin Clochard's avatar Martin Clochard

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system

parents 7b0f17c1 4d03eb99
......@@ -4,7 +4,6 @@ bignum.mlw
bitcount.mlw
bitvector_examples.mlw
bitwalker.mlw
coincidence_count_list.mlw
counting_sort.mlw
cursor.mlw
dijkstra.mlw
......@@ -13,11 +12,6 @@ ewd673.mlw
fibonacci.mlw
find.mlw
finite_tarski.mlw
flag2.mlw
foveoos11_challenge1.mlw
foveoos11_challenge2.mlw
foveoos11_challenge3.mlw
gcd_bezout.mlw
gcd.mlw
hackers-delight.mlw
hashtbl_impl.mlw
......@@ -25,9 +19,7 @@ ieee_float.mlw
kmp.mlw
knuth_prime_numbers.mlw
koda_ruskey.mlw
lcp.mlw
linked_list_rev.mlw
my_cosine.mlw
optimal_replay.mlw
queens_bv.mlw
queens.mlw
......@@ -39,7 +31,6 @@ schorr_waite_via_recursion.mlw
sieve.mlw
sudoku.mlw
sum_of_digits.mlw
there_and_back_again.mlw
topological_sorting.mlw
tortoise_and_hare.mlw
tree_height.mlw
......@@ -55,5 +46,3 @@ vstte10_inverting.mlw
vstte10_search_list.mlw
vstte12_bfs.mlw
vstte12_combinators.mlw
vstte12_ring_buffer.mlw
vstte12_tree_reconstruction.mlw
......@@ -2,120 +2,30 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count_list.mlw" expanded="true">
<theory name="CoincidenceCount" sum="9a0ad21c9ece5af6e3bf77ad2c0d1d81">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<theory name="CoincidenceCount" sum="905b884a839c618907ffebe24b767896" expanded="true">
<goal name="Transitive.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
<transf name="split_goal_wp">
<goal name="WP_parameter coincidence_count.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.82" steps="2661"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="1.24" steps="3244"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="2.71" steps="6776"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
<goal name="VC coincidence_count" expl="VC for coincidence_count" expanded="true">
<proof prover="2"><result status="valid" time="2.20" steps="9859"/></proof>
</goal>
</theory>
<theory name="CoincidenceCountAnyType" sum="2effd4ea5f064da956ab4d367f092582">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<theory name="CoincidenceCountAnyType" sum="a063592bd4e78e3599214a54a49c4910" expanded="true">
<goal name="Transitive.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
<proof prover="0"><result status="valid" time="3.63" steps="12168"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter coincidence_count.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.57" steps="2400"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.36" steps="1750"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="0.52" steps="1823"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
</transf>
<goal name="VC coincidence_count" expl="VC for coincidence_count">
<proof prover="2"><result status="valid" time="0.65" steps="4194"/></proof>
</goal>
</theory>
<theory name="CoincidenceCountList" sum="66d71efd5b320baab93930df25784477">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<theory name="CoincidenceCountList" sum="e75739bbd76111eb2670e596d18c2279" expanded="true">
<goal name="Transitive.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
<proof prover="0"><result status="valid" time="0.24" steps="657"/></proof>
<goal name="VC coincidence_count" expl="VC for coincidence_count">
<proof prover="2"><result status="valid" time="0.15" steps="1000"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -19,65 +19,69 @@ module Flag
| _,_ -> False
end
predicate monochrome (a:map int color) (i:int) (j:int) (c:color) =
forall k:int. i <= k < j -> a[k]=c
predicate monochrome (a: map int color) (i: int) (j: int) (c: color) =
forall k: int. i <= k < j -> a[k]=c
let rec function nb_occ (a:map int color) (i:int) (j:int) (c:color) : int
let rec function nb_occ (a: map int color) (i: int) (j: int) (c: color) : int
variant { j - i }
= if i >= j then 0 else
if eq_color a[j-1] c then 1 + nb_occ a i (j-1) c else nb_occ a i (j-1) c
let rec lemma nb_occ_split (a:map int color) (i j k:int) (c:color)
let rec lemma nb_occ_split (a: map int color) (i j k: int) (c: color)
requires { i <= j <= k }
variant { k - j }
ensures { nb_occ a i k c = nb_occ a i j c + nb_occ a j k c }
= if k = j then () else nb_occ_split a i j (k-1) c
let rec lemma nb_occ_ext (a1 a2:map int color) (i j:int) (c:color)
requires { forall k:int. i <= k < j -> a1[k] = a2[k] }
let rec lemma nb_occ_ext (a1 a2: map int color) (i j: int) (c: color)
requires { forall k: int. i <= k < j -> a1[k] = a2[k] }
variant { j - i }
ensures { nb_occ a1 i j c = nb_occ a2 i j c }
= if i >= j then () else nb_occ_ext a1 a2 i (j-1) c
lemma nb_occ_store_outside_up:
forall a:map int color, i j k:int, c:color.
forall a: map int color, i j k: int, c: color.
i <= j <= k -> nb_occ (set a k c) i j c = nb_occ a i j c
lemma nb_occ_store_outside_down:
forall a:map int color, i j k:int, c:color.
forall a: map int color, i j k: int, c: color.
k < i <= j -> nb_occ (set a k c) i j c = nb_occ a i j c
lemma nb_occ_store_eq_eq:
forall a:map int color, i j k:int, c:color.
forall a: map int color, i j k: int, c: color.
i <= k < j -> a[k] = c ->
nb_occ (set a k c) i j c = nb_occ a i j c
let rec lemma nb_occ_store_eq_neq (a:map int color) (i j k:int) (c:color)
let rec lemma nb_occ_store_eq_neq (a: map int color) (i j k: int) (c: color)
requires { i <= k < j }
requires { a[k] <> c }
variant { j - k }
ensures { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
variant { j - k }
ensures { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
= if k = j - 1 then () else nb_occ_store_eq_neq a i (j-1) k c
lemma nb_occ_store_neq_eq:
forall a:map int color, i j k:int, c c':color.
i <= k < j -> c <> c' -> a[k] = c ->
nb_occ (set a k c') i j c = nb_occ a i j c - 1
let lemma nb_occ_store_neq_eq
(a: map int color) (i j k: int) (c c': color)
requires { i <= k < j } requires { c <> c' } requires { a[k] = c }
ensures { nb_occ (set a k c') i j c = nb_occ a i j c - 1 }
= nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
lemma nb_occ_store_neq_neq:
forall a:map int color, i j k:int, c c':color.
i <= k < j -> c <> c' -> a[k] <> c ->
nb_occ (set a k c') i j c = nb_occ a i j c
let lemma nb_occ_store_neq_neq
(a: map int color) (i j k: int) (c c': color)
requires { i <= k < j } requires { c <> c' } requires { a[k] <> c }
ensures { nb_occ (set a k c') i j c = nb_occ a i j c }
= nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
use import array.Array
let swap (a:array color) (i:int) (j:int) : unit
let swap (a:array color) (i: int) (j: int) : unit
requires { 0 <= i < a.length }
requires { 0 <= j < a.length }
ensures { a[i] = old a[j] }
ensures { a[j] = old a[i] }
ensures { forall k:int. k <> i /\ k <> j -> a[k] = old a[k] }
ensures { forall k1 k2:int, c:color. k1 <= i < k2 /\ k1 <= j < k2 ->
ensures { forall k: int. k <> i /\ k <> j -> a[k] = old a[k] }
ensures { forall k1 k2: int, c: color. k1 <= i < k2 /\ k1 <= j < k2 ->
nb_occ a.elts k1 k2 c = nb_occ (old a.elts) k1 k2 c }
= let ai = a[i] in
let aj = a[j] in
......@@ -86,11 +90,11 @@ module Flag
let dutch_flag (a:array color)
ensures { (exists b:int. exists r:int.
ensures { (exists b: int. exists r: int.
monochrome a.elts 0 b Blue /\
monochrome a.elts b r White /\
monochrome a.elts r a.length Red) }
ensures { forall c:color.
ensures { forall c: color.
nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
= let b = ref 0 in
let i = ref 0 in
......@@ -101,7 +105,7 @@ module Flag
invariant { monochrome a.elts !b !i White }
invariant { monochrome a.elts !r a.length Red }
invariant {
forall c:color.
forall c: color.
nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
variant { !r - !i }
match a[!i] with
......
This diff is collapsed.
......@@ -2,48 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../foveoos11_challenge1.mlw" expanded="true">
<theory name="Max" sum="4d062e300c422dd912abe62a0612e474" expanded="true">
<goal name="WP_parameter max" expl="VC for max" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter max.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter max.2" expl="2. loop invariant init">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter max.3" expl="3. index in array bounds">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter max.4" expl="4. index in array bounds">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter max.5" expl="5. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter max.7" expl="7. loop variant decrease">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.8" expl="8. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.9" expl="9. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter max.10" expl="10. loop variant decrease">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter max.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
<theory name="Max" sum="d07f3e92fc559af0ac7bb5338d945993" expanded="true">
<goal name="VC max" expl="VC for max" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../foveoos11_challenge2.mlw" expanded="true">
<theory name="MaximumTree" sum="a00e1f9c636259085c5337c363a52ea1" expanded="true">
<theory name="MaximumTree" sum="fce5c2a3c40462a4ace022ab88c3a4e9" expanded="true">
<goal name="size_nonneg" expanded="true">
<proof prover="0" edited="foveoos11_challenge2_WP_MaximumTree_size_nonneg_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter maximum" expl="VC for maximum" expanded="true">
<proof prover="2"><result status="valid" time="0.56" steps="812"/></proof>
<goal name="VC maximum" expl="VC for maximum" expanded="true">
<proof prover="1"><result status="valid" time="0.25" steps="1474"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -31,7 +31,6 @@
</goal>
<goal name="VC gcd.8" expl="8. loop variant decrease">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><undone/></proof>
</goal>
<goal name="VC gcd.9" expl="9. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.18" steps="42"/></proof>
......
This diff is collapsed.
......@@ -2,57 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../lcp.mlw" expanded="true">
<theory name="LCP" sum="b7b041689ff58a3f4d1518790558ac63" expanded="true">
<theory name="LCP" sum="50feeeaf6717c74702bac9e115a2b860" expanded="true">
<goal name="not_eqseq" expanded="true">
<proof prover="4"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter lcp" expl="VC for lcp" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter lcp.1" expl="1. loop invariant init">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter lcp.2" expl="2. index in array bounds">
<proof prover="4"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter lcp.3" expl="3. index in array bounds">
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter lcp.4" expl="4. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter lcp.5" expl="5. loop variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter lcp.6" expl="6. postcondition">
<proof prover="4"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter lcp.7" expl="7. postcondition" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter lcp.7.1" expl="1. postcondition" expanded="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.18"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter lcp.8" expl="8. postcondition">
<proof prover="4"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter lcp.9" expl="9. postcondition">
<proof prover="4"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter lcp.10" expl="10. postcondition">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter lcp.11" expl="11. postcondition">
<proof prover="4" timelimit="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
<goal name="VC lcp" expl="VC for lcp" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="79"/></proof>
</goal>
</theory>
</file>
......
......@@ -23,14 +23,11 @@ Definition unit := unit.
Require Import Interval.Interval_tactic.
(* Why3 goal *)
Theorem WP_parameter_my_cosine : forall (x:floating_point.SingleFormat.single),
Theorem VC_my_cosine : forall (x:floating_point.SingleFormat.single),
((Reals.Rbasic_fun.Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R ->
((Reals.Rbasic_fun.Rabs ((1%R - (((floating_point.Single.value x) * (floating_point.Single.value x))%R * (05 / 10)%R)%R)%R - (Reals.Rtrigo_def.cos (floating_point.Single.value x)))%R) <= (1 / 16777216)%R)%R.
(* Why3 intros x h1. *)
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
intros x h1.
interval with (i_bisect_diff (Single.value x)).
Qed.
......@@ -2,28 +2,29 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../my_cosine.mlw" expanded="true">
<theory name="M" sum="e6984a9af2ab6c45ac0e8af4e992df4e" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true">
<theory name="M" sum="9703bc37ded6a61396b1df1dc41b18d6" expanded="true">
<goal name="VC my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion" expanded="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
<proof prover="3" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="1.79"/></proof>
<goal name="VC my_cosine.1" expl="1. assertion" expanded="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="3" edited="my_cosine_M_VC_my_cosine_1.v"><result status="valid" time="1.79"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. precondition" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<goal name="VC my_cosine.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter my_cosine.3" expl="3. precondition" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<goal name="VC my_cosine.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.05" steps="188"/></proof>
</goal>
<goal name="WP_parameter my_cosine.4" expl="4. precondition" expanded="true">
<goal name="VC my_cosine.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter my_cosine.5" expl="5. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<goal name="VC my_cosine.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Nth.
Require option.Option.
Require list.NthLength.
Require list.Append.
Require list.NthLengthAppend.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Definition pal {a:Type} {a_WT:WhyType a} (x:(list a)) (n:Z): Prop :=
forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((list.Nth.nth i
x) = (list.Nth.nth ((n - 1%Z)%Z - i)%Z x)).
Axiom elt : Type.
Parameter elt_WhyType : WhyType elt.
Existing Instance elt_WhyType.
Parameter eq: elt -> elt -> Prop.
Axiom eq_spec : forall (x:elt) (y:elt), (eq x y) <-> (x = y).
(* Why3 goal *)
Theorem VC_palindrome_rec : forall (x:(list elt)) (y:(list elt)),
((list.Length.length y) <= (list.Length.length x))%Z -> forall (x1:elt)
(x2:(list elt)), (y = (Init.Datatypes.cons x1 x2)) -> forall (x3:elt)
(x4:(list elt)), (x2 = (Init.Datatypes.cons x3 x4)) -> forall (x5:elt)
(x6:(list elt)), (x = (Init.Datatypes.cons x5 x6)) -> ((exists i:Z,
((0%Z <= i)%Z /\ (i < (list.Length.length x4))%Z) /\ ~ ((list.Nth.nth i
x6) = (list.Nth.nth (((list.Length.length x4) - 1%Z)%Z - i)%Z x6))) ->
exists i:Z, ((0%Z <= i)%Z /\ (i < (list.Length.length y))%Z) /\
~ ((list.Nth.nth i
x) = (list.Nth.nth (((list.Length.length y) - 1%Z)%Z - i)%Z x))).
intros x y h1 x1 x2 h2 x3 x4 h3 x5 x6 h4 (i,(hi1,hi2)).
subst.
exists (i+1)%Z; intuition.
unfold Length.length. fold Length.length.
omega.
unfold Length.length in *. fold Length.length in *.
assert (Nth.nth (i+1) (x5 :: x6) = Nth.nth i x6).
unfold Nth.nth; fold Nth.nth.
generalize (Zeq_bool_eq (i+1) 0).
destruct (Zeq_bool (i+1) 0).
intuition.
elimtype False.
omega.
intuition.
replace (i+1-1)%Z with i by omega. auto.
replace (1 + (1 + Length.length x4) - 1 - (i + 1))%Z
with (1 + Length.length x4 - 1 - i)%Z
in H1 by omega.
assert (Nth.nth (1 + Length.length x4 - 1 - i) (x5 :: x6) =
Nth.nth (Length.length x4 - 1 - i) x6).
unfold Nth.nth; fold Nth.nth.
generalize (Zeq_bool_eq (1 + Length.length x4 - 1 - i) 0).
destruct (Zeq_bool (1 + Length.length x4 - 1 - i) 0).
intuition; elimtype False; omega.
intuition.
replace (1 + Length.length x4 - 1 - i - 1)%Z with (Length.length x4 - 1 - i)%Z
by omega; auto.
congruence.
Qed.