bitvectors: removed a Coq proof

parent c148dc7b
......@@ -216,7 +216,7 @@ Axiom Power_non_null : forall (n:Z), ~ ((pow21 n) = 0%R).
Axiom Power_neg : forall (n:Z), ((pow21 (-n)%Z) = (1%R / (pow21 n))%R).
Axiom Power_sum_aux :
forall (n:Z) (m:Z), (0%Z <= m)%Z ->
forall (m:Z) (n:Z), (0%Z <= m)%Z ->
((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R).
Axiom Power_sum1 :
......@@ -352,7 +352,7 @@ Axiom to_nat_of_zero2 :
((to_nat_sub b j 0%Z) = (to_nat_sub b i 0%Z)).
Axiom to_nat_of_zero :
forall (b:bv) (i:Z) (j:Z), ((j < 32%Z)%Z /\ (0%Z <= i)%Z) ->
forall (b:bv) (j:Z) (i:Z), ((j < 32%Z)%Z /\ (0%Z <= i)%Z) ->
(forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) ->
((to_nat_sub b j i) = 0%Z).
......@@ -562,7 +562,7 @@ Axiom to_nat_of_zero21 :
((to_nat_sub1 b j 0%Z) = (to_nat_sub1 b i 0%Z)).
Axiom to_nat_of_zero1 :
forall (b:bv1) (i:Z) (j:Z), ((j < 64%Z)%Z /\ (0%Z <= i)%Z) ->
forall (b:bv1) (j:Z) (i:Z), ((j < 64%Z)%Z /\ (0%Z <= i)%Z) ->
(forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b k) = false)) ->
((to_nat_sub1 b j i) = 0%Z).
......@@ -5,12 +5,13 @@
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="4000"/>
<prover id="11" name="CVC4" version="1.5" timelimit="30" steplimit="0" memlimit="4000"/>
<prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="4000"/>
<prover id="11" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../double_of_int.why" proved="true">
<theory name="DoubleOfInt" proved="true">
<goal name="nth_j1" proved="true">
......@@ -169,7 +170,7 @@
<goal name="lemma1_pos" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_pos.0" proved="true">
<proof prover="10" timelimit="10"><result status="valid" time="7.27" steps="1022"/></proof>
<proof prover="10"><result status="valid" time="7.27" steps="1022"/></proof>
......@@ -185,7 +186,7 @@
<goal name="lemma1_neg" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_neg.0" proved="true">
<proof prover="10" timelimit="10"><result status="valid" time="4.97" steps="827"/></proof>
<proof prover="10"><result status="valid" time="4.97" steps="827"/></proof>
......@@ -204,10 +205,10 @@
<goal name="to_nat_bv32_bv64_aux.0" proved="true">
<transf name="induction" proved="true" arg1="j">
<goal name="to_nat_bv32_bv64_aux.0.0" expl="base case" proved="true">
<proof prover="10" memlimit="1000"><result status="valid" time="0.58" steps="333"/></proof>
<proof prover="10" timelimit="1" memlimit="1000"><result status="valid" time="0.58" steps="333"/></proof>
<goal name="to_nat_bv32_bv64_aux.0.1" expl="recursive case" proved="true">
<proof prover="10" memlimit="1000"><result status="valid" time="0.62" steps="305"/></proof>
<proof prover="10" timelimit="1" memlimit="1000"><result status="valid" time="0.62" steps="305"/></proof>
......@@ -240,7 +241,7 @@
<goal name="lemma2.0.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="lemma2.0.0.0" proved="true">
<proof prover="11"><result status="valid" time="5.66"/></proof>
<proof prover="11" timelimit="30" memlimit="4000"><result status="valid" time="5.66"/></proof>
......@@ -300,7 +301,34 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
<goal name="var_value0" proved="true">
<proof prover="5" timelimit="0" memlimit="0" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.95"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="var_value0.0" proved="true">
<transf name="unfold" proved="true" arg1="var_as_double">
<goal name="var_value0.0.0" proved="true">
<transf name="rewrite" proved="true" arg1="double_of_bv64_value">
<goal name="var_value0.0.0.0" proved="true">
<transf name="rewrite" proved="true" arg1="sign_var">
<goal name="var_value0." proved="true">
<proof prover="3"><result status="valid" time="0.84"/></proof>
<transf name="split_all_full" proved="true" >
<goal name="var_value0." proved="true">
<proof prover="10"><result status="valid" time="1.05" steps="271"/></proof>
<goal name="var_value0." proved="true">
<proof prover="11"><result status="valid" time="0.06"/></proof>
<goal name="var_value0.0.0.1" proved="true">
<proof prover="11"><result status="valid" time="0.16"/></proof>
<goal name="from_int_sum" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
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