Commit 17ff099b authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

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

parents f20e0585 3cd1432f
arm.mlw
bag.mlw
bellman_ford.mlw
bignum.mlw
......@@ -6,14 +5,9 @@ bitcount.mlw
bitvector_examples.mlw
bitwalker.mlw
coincidence_count_list.mlw
conjugate.mlw
counting_sort.mlw
cursor.mlw
dfa_example.mlw
dijkstra.mlw
division.mlw
dyck.mlw
edit_distance.mlw
esterel.mlw
ewd673.mlw
fibonacci.mlw
......@@ -32,9 +26,7 @@ kmp.mlw
knuth_prime_numbers.mlw
koda_ruskey.mlw
lcp.mlw
linear_probing.mlw
linked_list_rev.mlw
maximum_subarray.mlw
my_cosine.mlw
optimal_replay.mlw
patience.mlw
......@@ -43,13 +35,10 @@ queens_bv.mlw
queens.mlw
random_access_list.mlw
register_allocation.mlw
relabel.mlw
residual.mlw
rightmostbittrick.mlw
schorr_waite_via_recursion.mlw
sieve.mlw
skew_heaps.mlw
snapshotable_trees.mlw
sudoku.mlw
sum_of_digits.mlw
there_and_back_again.mlw
......@@ -60,9 +49,6 @@ unraveling_a_card_trick.mlw
vacid_0_build_maze.mlw
vacid_0_red_black_trees.mlw
vacid_0_sparse_array.mlw
verifythis_2015_dancing_links.mlw
verifythis_2015_parallel_gcd.mlw
verifythis_2015_relaxed_prefix.mlw
verifythis_2016_tree_traversal.mlw
verifythis_fm2012_LRS.mlw
verifythis_fm2012_treedel.mlw
......
......@@ -2,69 +2,21 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" 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="../arm.mlw" expanded="true">
<theory name="M" sum="0d719c3e6262bb28f7a388d2aa2d5410" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="1. loop invariant init">
<proof prover="3"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.2" expl="2. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.3" expl="3. type invariant">
<proof prover="3"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.4" expl="4. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.5" expl="5. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.6" expl="6. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.7" expl="7. index in array bounds">
<proof prover="3"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.8" expl="8. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.9" expl="9. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.10" expl="10. loop invariant preservation">
<proof prover="3"><result status="valid" time="1.17" steps="75"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.11" expl="11. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.12" expl="12. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.13" expl="13. loop variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.14" expl="14. type invariant">
<proof prover="3"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.15" expl="15. postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
<theory name="M" sum="83f2283fac8c57590845cb85004d97a2" expanded="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="165"/></proof>
</goal>
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="InsertionSortExample" sum="8f826701fa05e53c78b726425a76d7d8" expanded="true">
<goal name="WP_parameter path_init_l2" expl="VC for path_init_l2">
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
<theory name="InsertionSortExample" sum="7e99ff01a5c559f0be758aebea3a63a2" expanded="true">
<goal name="VC path_init_l2" expl="VC for path_init_l2" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="WP_parameter path_l2_exit" expl="VC for path_l2_exit">
<proof prover="3" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC path_l2_exit" expl="VC for path_l2_exit" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,101 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" 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="../conjugate.mlw" expanded="true">
<theory name="Conjugate" sum="d5ae5eea60f1c7dfc09f6ff24ea83b48" expanded="true">
<goal name="WP_parameter conjugate" expl="VC for conjugate" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter conjugate.1" expl="1. index in array bounds">
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter conjugate.2" expl="2. array creation size">
<proof prover="2"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter conjugate.3" expl="3. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="WP_parameter conjugate.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter conjugate.5" expl="5. index in array bounds">
<proof prover="2"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter conjugate.6" expl="6. index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter conjugate.7" expl="7. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter conjugate.8" expl="8. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter conjugate.9" expl="9. index in array bounds">
<proof prover="2"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter conjugate.10" expl="10. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter conjugate.11" expl="11. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter conjugate.12" expl="12. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.13" expl="13. index in array bounds">
<proof prover="2"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="WP_parameter conjugate.14" expl="14. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.15" expl="15. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter conjugate.16" expl="16. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.17" expl="17. loop invariant init">
<proof prover="2" timelimit="10"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter conjugate.18" expl="18. type invariant">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter conjugate.19" expl="19. index in array bounds">
<proof prover="2"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="WP_parameter conjugate.20" expl="20. loop invariant preservation">
<proof prover="2" timelimit="10"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="WP_parameter conjugate.21" expl="21. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="WP_parameter conjugate.22" expl="22. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.23" expl="23. loop invariant preservation">
<proof prover="2" timelimit="10"><result status="valid" time="0.25" steps="150"/></proof>
</goal>
<goal name="WP_parameter conjugate.24" expl="24. loop variant decrease">
<proof prover="2"><result status="valid" time="0.06" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.25" expl="25. assertion">
<proof prover="2"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter conjugate.26" expl="26. type invariant">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter conjugate.27" expl="27. postcondition">
<proof prover="2" timelimit="10"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
</transf>
<theory name="Conjugate" sum="4ddfb31b3cb62b7bc08bc34c419e39f0" expanded="true">
<goal name="VC conjugate" expl="VC for conjugate" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="315"/></proof>
</goal>
</theory>
<theory name="Test" sum="b22149320dd0c24e561e0d5940d4fa12" expanded="true">
<goal name="WP_parameter test" expl="VC for test" expanded="true">
<proof prover="2"><result status="valid" time="0.09" steps="36"/></proof>
<theory name="Test" sum="f7b1400c556a52fd7e125f1fc01fdac8" expanded="true">
<goal name="VC test" expl="VC for test" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="185"/></proof>
</goal>
<goal name="WP_parameter bench" expl="VC for bench" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
<goal name="VC bench" expl="VC for bench" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,111 +4,51 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="8" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../dfa_example.mlw" expanded="true">
<theory name="DfaExample" sum="660b70fa1d4035d9e6c3f57fd8521252" expanded="true">
<theory name="DfaExample" sum="eb5f1df76193c1ab904132bdd41a5217" expanded="true">
<goal name="nil_notin_r1">
<proof prover="0" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="7" memlimit="4000"><result status="valid" time="0.08" steps="140"/></proof>
<proof prover="7"><result status="valid" time="0.08" steps="140"/></proof>
</goal>
<goal name="WP_parameter all_in_r0" expl="VC for all_in_r0">
<proof prover="7" memlimit="4000"><result status="valid" time="2.51" steps="2624"/></proof>
<goal name="VC all_in_r0" expl="VC for all_in_r0" expanded="true">
<proof prover="2"><result status="valid" time="0.03" steps="222"/></proof>
</goal>
<goal name="words_in_r1_end_with_one">
<proof prover="8"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter words_in_r1_suffix_in_r1" expl="VC for words_in_r1_suffix_in_r1">
<transf name="split_goal_wp">
<goal name="WP_parameter words_in_r1_suffix_in_r1.1" expl="1. assertion">
<proof prover="7"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
<goal name="WP_parameter words_in_r1_suffix_in_r1.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
<goal name="VC words_in_r1_suffix_in_r1" expl="VC for words_in_r1_suffix_in_r1" expanded="true">
<proof prover="1"><result status="valid" time="3.06"/></proof>
</goal>
<goal name="WP_parameter zero_w_in_r1" expl="VC for zero_w_in_r1">
<proof prover="8"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1" expl="VC for one_w_in_r1">
<transf name="split_goal_wp">
<goal name="WP_parameter one_w_in_r1.1" expl="1. postcondition">
<proof prover="7"><result status="valid" time="0.28" steps="376"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.2" expl="2. assertion">
<proof prover="7"><result status="valid" time="0.24" steps="386"/></proof>
<goal name="VC zero_w_in_r1" expl="VC for zero_w_in_r1" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC zero_w_in_r1.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.01" steps="42"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.3" expl="3. assertion">
<proof prover="7"><result status="valid" time="0.04" steps="40"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.4" expl="4. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter one_w_in_r1.4.1" expl="1. VC for one_w_in_r1">
<proof prover="7"><result status="valid" time="0.25" steps="337"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.4.2" expl="2. VC for one_w_in_r1">
<proof prover="7"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</transf>
<goal name="VC zero_w_in_r1.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.50"/></proof>
</goal>
</transf>
</goal>
<goal name="VC one_w_in_r1" expl="VC for one_w_in_r1" expanded="true">
<proof prover="2"><result status="valid" time="2.22" steps="6899"/></proof>
</goal>
<goal name="zero_w_in_r2">
<proof prover="7"><result status="valid" time="0.04" steps="75"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
<goal name="one_w_in_r2">
<proof prover="7"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="WP_parameter astate1" expl="VC for astate1">
<transf name="split_goal_wp">
<goal name="WP_parameter astate1.1" expl="1. postcondition">
<proof prover="7"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="WP_parameter astate1.2" expl="2. variant decrease">
<proof prover="7"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate1.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter astate1.3.1" expl="1. VC for astate1">
<proof prover="7"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter astate1.3.2" expl="2. VC for astate1">
<proof prover="7"><result status="valid" time="0.06" steps="48"/></proof>
</goal>
<goal name="WP_parameter astate1.3.3" expl="3. VC for astate1">
<proof prover="7"><result status="valid" time="0.05" steps="37"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter astate1.4" expl="4. variant decrease">
<proof prover="7"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate1.5" expl="5. postcondition">
<proof prover="7"><result status="valid" time="0.12" steps="244"/></proof>
</goal>
</transf>
<goal name="VC astate1" expl="VC for astate1" expanded="true">
<proof prover="2"><result status="valid" time="0.59" steps="3042"/></proof>
</goal>
<goal name="WP_parameter astate2" expl="VC for astate2">
<transf name="split_goal_wp">
<goal name="WP_parameter astate2.1" expl="1. postcondition">
<proof prover="7"><result status="valid" time="0.02" steps="62"/></proof>
</goal>
<goal name="WP_parameter astate2.2" expl="2. variant decrease">
<proof prover="7"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate2.3" expl="3. postcondition">
<proof prover="7"><result status="valid" time="0.06" steps="163"/></proof>
</goal>
<goal name="WP_parameter astate2.4" expl="4. variant decrease">
<proof prover="7"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate2.5" expl="5. postcondition">
<proof prover="7"><result status="valid" time="0.12" steps="117"/></proof>
</goal>
</transf>
<goal name="VC astate2" expl="VC for astate2" expanded="true">
<proof prover="2"><result status="valid" time="0.75" steps="3708"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,24 +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="../division.mlw" expanded="true">
<theory name="Division" sum="201c4cf57a1faa33f124622cb758936e" expanded="true">
<goal name="WP_parameter division" expl="VC for division" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter division.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter division.2" expl="2. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter division.3" expl="3. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter division.4" expl="4. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</transf>
<theory name="Division" sum="55bb79e69a63dfaf165ceec93b4fe785" expanded="true">
<goal name="VC division" expl="VC for division" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,6 +2,7 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require int.MinMax.
Require list.List.
......@@ -21,14 +22,17 @@ Existing Instance char_WhyType.
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist nil nil 0%Z)
Inductive dist: (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist Init.Datatypes.nil Init.Datatypes.nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (cons a w1) w2 (n + 1%Z)%Z)
w2 n) -> forall (a:char), (dist (Init.Datatypes.cons a w1) w2
(n + 1%Z)%Z)
| dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist w1 (cons a w2) (n + 1%Z)%Z)
w2 n) -> forall (a:char), (dist w1 (Init.Datatypes.cons a w2)
(n + 1%Z)%Z)
| dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (cons a w1) (cons a w2) n).
w2 n) -> forall (a:char), (dist (Init.Datatypes.cons a w1)
(Init.Datatypes.cons a w2) n).
(* Why3 assumption *)
Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
......@@ -37,123 +41,119 @@ Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
(* Why3 assumption *)
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| nil => a
| (cons c u') => (last_char c u')
| Init.Datatypes.nil => a
| (Init.Datatypes.cons c u') => (last_char c u')
end.
(* Why3 assumption *)
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
match u with
| nil => nil
| (cons c u') => (cons a (but_last c u'))
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons c u') => (Init.Datatypes.cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
((Init.Datatypes.app (but_last a u) (Init.Datatypes.cons (last_char a
u) Init.Datatypes.nil)) = (Init.Datatypes.cons a u)).
Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
exists b:char,
((Init.Datatypes.app v (Init.Datatypes.cons b Init.Datatypes.nil)) = (Init.Datatypes.cons a u)) /\
((list.Length.length v) = (list.Length.length u)).
Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
(a:char), (dist w1 w'2 m) -> forall (w2:(list char)),
(w'2 = (cons a w2)) -> exists u1:(list char), exists v1:(list char),
exists k:Z, (w1 = (List.app u1 v1)) /\ ((dist v1 w2 k) /\
((k + (list.Length.length u1))%Z <= (m + 1%Z)%Z)%Z).
(w'2 = (Init.Datatypes.cons a w2)) -> exists u1:(list char),
exists v1:(list char), exists k:Z, (w1 = (Init.Datatypes.app u1 v1)) /\
((dist v1 w2 k) /\ ((k + (list.Length.length u1))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> (dist w2 w1 n).
Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
(a:char), (dist (cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (List.app u2 v2)) /\ ((dist w1 v2
k) /\ ((k + (list.Length.length u2))%Z <= (m + 1%Z)%Z)%Z).
(a:char), (dist (Init.Datatypes.cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (Init.Datatypes.app u2 v2)) /\
((dist w1 v2 k) /\ ((k + (list.Length.length u2))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist (List.app u v) w
(w:(list char)) (n:Z), (dist v w n) -> (dist (Init.Datatypes.app u v) w
((list.Length.length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist v (List.app u w)
(w:(list char)) (n:Z), (dist v w n) -> (dist v (Init.Datatypes.app u w)
((list.Length.length u) + n)%Z).
Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
(n:Z), (min_dist w1 w2 n) -> (min_dist (cons a w1) (cons a w2) n).
(n:Z), (min_dist w1 w2 n) -> (min_dist (Init.Datatypes.cons a w1)
(Init.Datatypes.cons a w2) n).
Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (cons a w1) w2 p) ->
((min_dist w1 (cons b w2) m) -> (min_dist (cons a w1) (cons b w2)
((Zmin m p) + 1%Z)%Z))).
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (Init.Datatypes.cons a w1)
w2 p) -> ((min_dist w1 (Init.Datatypes.cons b w2) m) -> (min_dist
(Init.Datatypes.cons a w1) (Init.Datatypes.cons b w2)
((ZArith.BinInt.Z.min m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w nil
n) -> (min_dist (cons a w) nil (n + 1%Z)%Z).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w
Init.Datatypes.nil n) -> (min_dist (Init.Datatypes.cons a w)
Init.Datatypes.nil (n + 1%Z)%Z).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist nil w
(list.Length.length w)).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist
Init.Datatypes.nil w (list.Length.length w)).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
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] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
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) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Axiom array : forall (a:Type), Type.
Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a},
WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).