bitvectors: removed/simplified some Coq proofs

parent a22b3f29
......@@ -853,7 +853,8 @@ assert (h:(i=0 \/ 0 < i)) by omega.
destruct h.
(* case i = 0 *)
ae.
rewrite to_nat_sub_high.
subst i; simpl in Hj. rewrite pow2_0 in Hj. omega. omega.
(* case i > 0 *)
......@@ -874,8 +875,10 @@ rewrite to_nat_sub_one; auto with zarith.
rewrite to_nat_sub_footprint with
(b2 := (from_int2c (j - pow2 (i-1)))); auto with zarith.
rewrite Hind; auto with zarith.
ae.
ae.
replace (i-1-0) with (i-1); omega.
assert (pow2 ((i-1)+1) = 2 * pow2 (i-1)).
rewrite (Power_s (i-1)); omega.
replace (i-1+1) with i in H1; omega.
intros k Hk.
replace j with (j - pow2 (i - 1) + pow2 (i - 1)) by omega.
replace (j - pow2 (i - 1) + pow2 (i - 1) - pow2 (i - 1))
......
......@@ -31,7 +31,7 @@
</goal>
<goal name="nth_j6" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="76"/></proof>
<proof prover="4"><result status="valid" time="4.40"/></proof>
<proof prover="4"><result status="valid" time="3.23"/></proof>
</goal>
<goal name="nth_j7" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="76"/></proof>
......@@ -52,12 +52,12 @@
</goal>
<goal name="nth_const4" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="100"/></proof>
<proof prover="4"><result status="valid" time="1.87"/></proof>
<proof prover="4"><result status="valid" time="1.48"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="nth_const5" proved="true">
<proof prover="1"><result status="valid" time="0.11" steps="100"/></proof>
<proof prover="4"><result status="valid" time="2.05"/></proof>
<proof prover="4"><result status="valid" time="1.52"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="nth_const6" proved="true">
......@@ -67,7 +67,7 @@
</goal>
<goal name="nth_const7" proved="true">
<proof prover="1"><result status="valid" time="0.11" steps="100"/></proof>
<proof prover="4"><result status="valid" time="1.92"/></proof>
<proof prover="4"><result status="valid" time="1.50"/></proof>
<proof prover="8"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="nth_const8" proved="true">
......@@ -93,7 +93,7 @@
</goal>
<goal name="to_nat_mantissa_1" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
<proof prover="4"><result status="valid" time="1.43"/></proof>
<proof prover="4"><result status="valid" time="1.11"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.87"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
......@@ -105,13 +105,13 @@
</goal>
<goal name="mantissa_const_to_nat51" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="132"/></proof>
<proof prover="4"><result status="valid" time="1.44"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.71"/></proof>
<proof prover="4"><result status="valid" time="1.09"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.04"/></proof>
<proof prover="8"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="mantissa_const" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="104"/></proof>
<proof prover="4"><result status="valid" time="4.19"/></proof>
<proof prover="4"><result status="valid" time="3.08"/></proof>
</goal>
<goal name="real1075m1023" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -141,7 +141,7 @@
</goal>
<goal name="nth_0_30" proved="true">
<proof prover="2"><result status="valid" time="0.46"/></proof>
<proof prover="4"><result status="valid" time="3.97"/></proof>
<proof prover="4"><result status="valid" time="3.12"/></proof>
</goal>
<goal name="nth_jpxor_0_30" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="98"/></proof>
......@@ -150,10 +150,10 @@
</goal>
<goal name="nth_var31" proved="true">
<proof prover="1" timelimit="125"><result status="valid" time="3.53" steps="253"/></proof>
<proof prover="4"><result status="valid" time="3.55"/></proof>
<proof prover="4"><result status="valid" time="2.76"/></proof>
</goal>
<goal name="to_nat_sub_0_30" proved="true">
<proof prover="4"><result status="valid" time="1.75"/></proof>
<proof prover="4"><result status="valid" time="1.21"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.16"/></proof>
<proof prover="8"><result status="valid" time="0.84"/></proof>
</goal>
......@@ -165,12 +165,12 @@
<proof prover="8"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_pos" proved="true">
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.29"/></proof>
</goal>
<goal name="lemma1_pos" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_pos.0" proved="true">
<proof prover="10"><result status="valid" time="7.27" steps="1022"/></proof>
<proof prover="10"><result status="valid" time="6.20" steps="1022"/></proof>
</goal>
</transf>
</goal>
......@@ -186,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"><result status="valid" time="4.97" steps="827"/></proof>
<proof prover="10"><result status="valid" time="4.16" steps="827"/></proof>
</goal>
</transf>
</goal>
......@@ -198,7 +198,7 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="nth_var_0_31" proved="true">
<proof prover="4" timelimit="10"><result status="valid" time="3.72"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="2.86"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" proved="true">
<transf name="introduce_premises" proved="true" >
......@@ -222,16 +222,16 @@
<proof prover="8"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="to_nat_var_0_31" proved="true">
<proof prover="4"><result status="valid" time="1.64"/></proof>
<proof prover="4"><result status="valid" time="1.24"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="0.14"/></proof>
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="nth_var32to63" proved="true">
<proof prover="4"><result status="valid" time="3.64"/></proof>
<proof prover="4"><result status="valid" time="2.89"/></proof>
</goal>
<goal name="nth_var3" proved="true">
<proof prover="1"><result status="valid" time="1.39" steps="146"/></proof>
<proof prover="4"><result status="valid" time="1.55"/></proof>
<proof prover="4"><result status="valid" time="1.25"/></proof>
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="lemma2" proved="true">
......@@ -241,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" timelimit="30" memlimit="4000"><result status="valid" time="5.66"/></proof>
<proof prover="11" timelimit="30" memlimit="4000"><result status="valid" time="3.95"/></proof>
</goal>
</transf>
</goal>
......@@ -256,17 +256,17 @@
</goal>
<goal name="nth_var5" proved="true">
<proof prover="1"><result status="valid" time="1.20" steps="148"/></proof>
<proof prover="4"><result status="valid" time="2.07"/></proof>
<proof prover="4"><result status="valid" time="1.60"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="nth_var6" proved="true">
<proof prover="1"><result status="valid" time="1.17" steps="148"/></proof>
<proof prover="4"><result status="valid" time="2.14"/></proof>
<proof prover="4"><result status="valid" time="1.64"/></proof>
<proof prover="8"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="nth_var7" proved="true">
<proof prover="1"><result status="valid" time="1.39" steps="148"/></proof>
<proof prover="4"><result status="valid" time="2.06"/></proof>
<proof prover="4"><result status="valid" time="1.58"/></proof>
<proof prover="8"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="nth_var8" proved="true">
......@@ -277,7 +277,7 @@
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="lemma3" proved="true">
<proof prover="4"><result status="valid" time="3.82"/></proof>
<proof prover="4"><result status="valid" time="3.00"/></proof>
</goal>
<goal name="nth_var9" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="95"/></proof>
......@@ -364,7 +364,7 @@
<goal name="MainResult" proved="true">
<proof prover="1"><result status="valid" time="1.56" steps="143"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="4.72"/></proof>
<proof prover="4"><result status="valid" time="3.62"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.12"/></proof>
<proof prover="8"><result status="valid" time="0.95"/></proof>
</goal>
......
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