Commit 079015c7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

koda_ruskey: updated Coq proofs for Coq 8.6

parent 04c5c6ce
......@@ -310,7 +310,7 @@ Axiom white_white : forall (f:forest) (c:( Z color)) (i:Z),
(white_forest f c) -> (white_forest f (map.Map.set c i White)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Ltac ae := why3 "Alt-Ergo,1.30," timelimit 3; admit.
(* Why3 goal *)
Theorem WP_parameter_sub_valid_coloring_white : forall (f0:forest) (i:Z)
......@@ -374,5 +374,5 @@ trivial.
......@@ -338,8 +338,6 @@ Axiom H6 : (no_repeated_forest f0).
Axiom H7 : (valid_coloring f0 c1).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 15.
Ltac cvc4 := why3 "cvc4" timelimit 15.
(* Why3 goal *)
Theorem sub_valid_coloring : forall (x:Z) (x1:forest) (x2:forest), (f0 = (N x
......@@ -354,6 +352,7 @@ generalize H7. rewrite H4. inversion 1. trivial.
destruct (head_and_tail (N i1 f11 f21) f2 st1 st). apply H5.
red; intro. generalize H. rewrite H0. apply sub_not_nil.
generalize H6. rewrite H4. inversion 1.
why3 "CVC4,1.4," timelimit 5; admit.
......@@ -6,9 +6,9 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="36" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="36" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../koda_ruskey.mlw">
<file name="../koda_ruskey.mlw" expanded="true">
<theory name="KodaRuskey_Spec" sum="8e518d6f01f787c2ba93abeff13d48b2">
<goal name="size_forest_nonneg">
<transf name="induction_ty_lex">
......@@ -25,7 +25,7 @@
<theory name="Lemmas" sum="69586628d3c613c629b078044197f281">
<theory name="Lemmas" sum="69586628d3c613c629b078044197f281" expanded="true">
<goal name="mem_app">
<transf name="induction_ty_lex">
<goal name="mem_app.1" expl="1.">
......@@ -439,7 +439,7 @@
<goal name="sub_valid_coloring." expl="1.">
<transf name="split_goal_wp">
<goal name="sub_valid_coloring." expl="1.">
<proof prover="9" edited="koda_ruskey_KodaRuskey_Spec_sub_valid_coloring_1.v"><result status="valid" time="6.55"/></proof>
<proof prover="4" edited="koda_ruskey_KodaRuskey_Spec_sub_valid_coloring_1.v"><result status="valid" time="4.48"/></proof>
<goal name="sub_valid_coloring." expl="2.">
<proof prover="0" timelimit="6"><result status="valid" time="0.04"/></proof>
......@@ -474,8 +474,8 @@
<goal name="white_white">
<proof prover="1"><result status="valid" time="0.02" steps="29"/></proof>
<goal name="WP_parameter sub_valid_coloring_white" expl="VC for sub_valid_coloring_white">
<transf name="split_goal_wp">
<goal name="WP_parameter sub_valid_coloring_white" expl="VC for sub_valid_coloring_white" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sub_valid_coloring_white.1" expl="1. postcondition">
<proof prover="1" timelimit="11"><result status="valid" time="0.01" steps="12"/></proof>
......@@ -503,8 +503,8 @@
<goal name="WP_parameter sub_valid_coloring_white.9" expl="9. precondition">
<proof prover="1" timelimit="11"><result status="valid" time="0.01" steps="12"/></proof>
<goal name="WP_parameter sub_valid_coloring_white.10" expl="10. postcondition">
<proof prover="9" edited="koda_ruskey_KodaRuskey_Spec_WP_parameter_sub_valid_coloring_white_1.v"><result status="valid" time="4.84"/></proof>
<goal name="WP_parameter sub_valid_coloring_white.10" expl="10. postcondition" expanded="true">
<proof prover="4" edited="koda_ruskey_KodaRuskey_Spec_WP_parameter_sub_valid_coloring_white_1.v"><result status="valid" time="2.31"/></proof>
Supports Markdown
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