Commit fe74f428 authored by MARCHE Claude's avatar MARCHE Claude

porting in progress

parent 4902aafd
......@@ -10,7 +10,7 @@
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector.why" expanded="true">
<theory name="BitVector" sum="b2cd28e32ab19383fab97d17f1c06340">
<theory name="BitVector" sum="cf09ae6ceccc267e51756124a86867ef">
<goal name="Nth_bw_xor_v1true">
<proof prover="2"><result status="valid" time="0.08" steps="85"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -32,7 +32,7 @@
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="to_nat_of_zero2">
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.27"/></proof>
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="to_nat_of_zero">
<proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
......@@ -73,23 +73,23 @@
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_from_int2c_plus_pow2">
<proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.69"/></proof>
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
</goal>
</theory>
<theory name="BV32" sum="aca7c0cfc347d6aa55e9170b1e60b820" expanded="true">
<theory name="BV32" sum="ac9d9f7894cd9d82b25b70ad928e2811" expanded="true">
<goal name="size_positive">
<proof prover="0"><result status="valid" time="0.01" steps="65"/></proof>
</goal>
</theory>
<theory name="BV64" sum="0b730c9c3adbbeb86d176c0a5e901d00" expanded="true">
<theory name="BV64" sum="a16ca62eddacd5e53e6aaaea7e7def6f" expanded="true">
<goal name="size_positive">
<proof prover="0"><result status="valid" time="0.01" steps="65"/></proof>
</goal>
</theory>
<theory name="BV32_64" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestBv32" sum="b190969d7fef326d2a90129cfd540796" expanded="true">
<theory name="TestBv32" sum="e5e61fc809fac1f0a1a2f25dfd9c4f36" expanded="true">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.06" steps="72"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
......@@ -142,61 +142,61 @@
<proof prover="6" timelimit="120"><result status="valid" time="84.22"/></proof>
</goal>
<goal name="to_nat_0x00000003">
<proof prover="6" timelimit="120"><result status="valid" time="62.48"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="74.14"/></proof>
</goal>
<goal name="to_nat_0x00000007">
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="54.25"/></proof>
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="61.79"/></proof>
</goal>
<goal name="to_nat_0x0000000F">
<proof prover="6" timelimit="120"><result status="valid" time="46.07"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="53.42"/></proof>
</goal>
<goal name="to_nat_0x0000001F">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="38.43"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="44.75"/></proof>
</goal>
<goal name="to_nat_0x0000003F">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="31.33"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="36.10"/></proof>
</goal>
<goal name="to_nat_0x0000007F">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="25.66"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="30.37"/></proof>
</goal>
<goal name="to_nat_0x000000FF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="21.04"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="26.19"/></proof>
</goal>
<goal name="to_nat_0x000001FF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="17.53"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="21.56"/></proof>
</goal>
<goal name="to_nat_0x000003FF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="16.69"/></proof>
</goal>
<goal name="to_nat_0x000007FF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="11.02"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="13.27"/></proof>
</goal>
<goal name="to_nat_0x00000FFF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="8.79"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="10.99"/></proof>
</goal>
<goal name="to_nat_0x00001FFF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.88"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="8.72"/></proof>
</goal>
<goal name="to_nat_0x00003FFF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="5.48"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.87"/></proof>
</goal>
<goal name="to_nat_0x00007FFF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.14"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="5.07"/></proof>
</goal>
<goal name="to_nat_0x0000FFFF">
<proof prover="6"><result status="valid" time="3.18"/></proof>
<proof prover="6"><result status="valid" time="4.06"/></proof>
</goal>
<goal name="to_nat_0x0001FFFF">
<proof prover="6"><result status="valid" time="2.32"/></proof>
<proof prover="6"><result status="valid" time="3.07"/></proof>
</goal>
<goal name="to_nat_0x0003FFFF">
<proof prover="6"><result status="valid" time="1.77"/></proof>
<proof prover="6"><result status="valid" time="2.33"/></proof>
</goal>
<goal name="to_nat_0x0007FFFF">
<proof prover="6"><result status="valid" time="1.26"/></proof>
<proof prover="6"><result status="valid" time="1.72"/></proof>
</goal>
<goal name="to_nat_0x000FFFFF">
<proof prover="6"><result status="valid" time="0.89"/></proof>
<proof prover="6"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="to_nat_0x00FFFFFF">
<proof prover="6"><result status="valid" time="0.28"/></proof>
......
......@@ -10,7 +10,7 @@
<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"/>
<file name="../double_of_int.why" expanded="true">
<theory name="DoubleOfInt" sum="9eea9904f8def8dce1913bb1dd128170" expanded="true">
<theory name="DoubleOfInt" sum="4c46508ef9fd4ec555fcc94debaa957d" expanded="true">
<goal name="nth_j1">
<proof prover="1"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
......@@ -28,7 +28,7 @@
</goal>
<goal name="nth_j6">
<proof prover="1"><result status="valid" time="0.07" steps="76"/></proof>
<proof prover="4"><result status="valid" time="2.46"/></proof>
<proof prover="4"><result status="valid" time="2.85"/></proof>
</goal>
<goal name="nth_j7">
<proof prover="1"><result status="valid" time="0.04" steps="76"/></proof>
......@@ -49,7 +49,7 @@
</goal>
<goal name="nth_const4">
<proof prover="1"><result status="valid" time="0.10" steps="99"/></proof>
<proof prover="4"><result status="valid" time="0.87"/></proof>
<proof prover="4"><result status="valid" time="1.12"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="nth_const5">
......@@ -59,12 +59,12 @@
</goal>
<goal name="nth_const6">
<proof prover="1"><result status="valid" time="0.09" steps="99"/></proof>
<proof prover="4"><result status="valid" time="0.89"/></proof>
<proof prover="4"><result status="valid" time="1.12"/></proof>
<proof prover="8"><result status="valid" time="0.79"/></proof>
</goal>
<goal name="nth_const7">
<proof prover="1"><result status="valid" time="0.11" steps="99"/></proof>
<proof prover="4"><result status="valid" time="0.88"/></proof>
<proof prover="4"><result status="valid" time="1.09"/></proof>
<proof prover="8"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="nth_const8">
......@@ -90,7 +90,7 @@
</goal>
<goal name="to_nat_mantissa_1">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
<proof prover="4"><result status="valid" time="0.82"/></proof>
<proof prover="4"><result status="valid" time="1.13"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.87"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
......@@ -108,7 +108,7 @@
</goal>
<goal name="mantissa_const">
<proof prover="1"><result status="valid" time="0.08" steps="104"/></proof>
<proof prover="4"><result status="valid" time="2.40"/></proof>
<proof prover="4"><result status="valid" time="2.96"/></proof>
</goal>
<goal name="real1075m1023">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -138,7 +138,7 @@
</goal>
<goal name="nth_0_30">
<proof prover="2"><result status="valid" time="0.46"/></proof>
<proof prover="4"><result status="valid" time="2.24"/></proof>
<proof prover="4"><result status="valid" time="2.77"/></proof>
</goal>
<goal name="nth_jpxor_0_30">
<proof prover="1"><result status="valid" time="0.08" steps="98"/></proof>
......@@ -146,11 +146,11 @@
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_var31">
<proof prover="1" timelimit="125"><result status="valid" time="3.62" steps="253"/></proof>
<proof prover="4"><result status="valid" time="1.90"/></proof>
<proof prover="1" timelimit="125"><result status="valid" time="4.67" steps="253"/></proof>
<proof prover="4"><result status="valid" time="2.28"/></proof>
</goal>
<goal name="to_nat_sub_0_30">
<proof prover="4"><result status="valid" time="0.98"/></proof>
<proof prover="4"><result status="valid" time="1.25"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.20"/></proof>
<proof prover="8"><result status="valid" time="0.84"/></proof>
</goal>
......@@ -187,7 +187,7 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="nth_var_0_31">
<proof prover="4" timelimit="10"><result status="valid" time="1.98"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="2.35"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux">
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="2.08"/></proof>
......@@ -205,7 +205,7 @@
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="nth_var32to63">
<proof prover="4"><result status="valid" time="2.00"/></proof>
<proof prover="4"><result status="valid" time="2.33"/></proof>
</goal>
<goal name="nth_var3">
<proof prover="1"><result status="valid" time="1.39" steps="146"/></proof>
......@@ -213,26 +213,26 @@
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="lemma2">
<proof prover="5" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="23.13"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="26.24"/></proof>
</goal>
<goal name="nth_var4">
<proof prover="1"><result status="valid" time="1.44" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.06"/></proof>
<proof prover="4"><result status="valid" time="1.27"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="nth_var5">
<proof prover="1"><result status="valid" time="1.20" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.06"/></proof>
<proof prover="4"><result status="valid" time="1.31"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="nth_var6">
<proof prover="1"><result status="valid" time="1.41" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.08"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="8"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="nth_var7">
<proof prover="1"><result status="valid" time="1.39" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.07"/></proof>
<proof prover="4"><result status="valid" time="1.31"/></proof>
<proof prover="8"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="nth_var8">
......@@ -243,7 +243,7 @@
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="lemma3">
<proof prover="4"><result status="valid" time="2.03"/></proof>
<proof prover="4"><result status="valid" time="2.39"/></proof>
</goal>
<goal name="nth_var9">
<proof prover="1"><result status="valid" time="0.10" steps="95"/></proof>
......@@ -298,13 +298,13 @@
<proof prover="2"><result status="valid" time="0.22"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
<proof prover="8"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="MainResult">
<proof prover="1"><result status="valid" time="1.56" steps="139"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="2.18"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.99"/></proof>
<proof prover="4"><result status="valid" time="2.78"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.63"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
</theory>
......
......@@ -11,7 +11,7 @@
<prover id="11" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="12" name="Eprover" version="1.8-001" timelimit="2" steplimit="0" memlimit="1000"/>
<file name="../div_real.why" expanded="true">
<theory name="DivTest" sum="01c52807a8aba94889dc4b2844d409db" expanded="true">
<theory name="DivTest" sum="784f9ce8dac0be6df495813cc1672f9c" expanded="true">
<goal name="ok1">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -25,7 +25,7 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="2.06"/></proof>
<proof prover="8"><result status="unknown" time="1.72"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
......@@ -34,7 +34,7 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="2.06"/></proof>
<proof prover="8"><result status="unknown" time="1.38"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
......@@ -42,7 +42,7 @@
<goal name="smoke1">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="2.06"/></proof>
<proof prover="8"><result status="unknown" time="1.42"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="unknown" time="0.02"/></proof>
<proof prover="11"><result status="unknown" time="0.16"/></proof>
......@@ -50,7 +50,7 @@
<goal name="smoke3">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="8"><result status="unknown" time="2.06"/></proof>
<proof prover="8"><result status="unknown" time="1.66"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="unknown" time="0.01"/></proof>
<proof prover="11"><result status="unknown" time="0.17"/></proof>
......@@ -58,24 +58,24 @@
<goal name="smoke5">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="2.04"/></proof>
<proof prover="8"><result status="unknown" time="1.63"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="unknown" time="0.01"/></proof>
<proof prover="11"><result status="unknown" time="0.15"/></proof>
<proof prover="12"><result status="timeout" time="1.97"/></proof>
</goal>
<goal name="div_bound0">
<proof prover="8"><result status="unknown" time="2.04"/></proof>
<proof prover="8"><result status="unknown" time="1.72"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="div_le">
<proof prover="8"><result status="unknown" time="2.05"/></proof>
<proof prover="8"><result status="unknown" time="1.69"/></proof>
<proof prover="10"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="div_lt">
<proof prover="8"><result status="unknown" time="2.06"/></proof>
<proof prover="8"><result status="unknown" time="1.70"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -2,6 +2,7 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
......@@ -11,13 +12,6 @@ Require number.Divisibility.
Require number.Prime.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
......@@ -41,73 +35,78 @@ Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> 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]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
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)): 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)) (i:Z): a :=
(map.Map.get (elts a1) i).
Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
a)), (0%Z <= (length self))%Z.
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
((elts a1) i).
Parameter mixfix_lblsmnrb: forall {a:Type} {a_WT:WhyType a}, (array a) ->
Z -> a -> (array a).
Axiom mixfix_lblsmnrb_spec : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (i:Z) (v:a), ((length (mixfix_lblsmnrb a1 i
v)) = (length a1)) /\ ((elts (mixfix_lblsmnrb a1 i
v)) = (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition no_prime_in (l:Z) (u:Z): Prop := forall (x:Z), ((l < x)%Z /\
(x < u)%Z) -> ~ (number.Prime.prime x).
(* Why3 assumption *)
Definition first_primes (p:(array Z)) (u:Z): Prop := ((get p 0%Z) = 2%Z) /\
((forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ ((i < j)%Z /\ (j < u)%Z)) -> ((get p
i) < (get p j))%Z) /\ ((forall (i:Z), ((0%Z <= i)%Z /\ (i < u)%Z) ->
(number.Prime.prime (get p i))) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < (u - 1%Z)%Z)%Z) -> (no_prime_in (get p i) (get p (i + 1%Z)%Z)))).
Definition first_primes (p:(array Z)) (u:Z): Prop := ((mixfix_lbrb p
0%Z) = 2%Z) /\ ((forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ ((i < j)%Z /\
(j < u)%Z)) -> ((mixfix_lbrb p i) < (mixfix_lbrb p j))%Z) /\
((forall (i:Z), ((0%Z <= i)%Z /\ (i < u)%Z) -> (number.Prime.prime
(mixfix_lbrb p i))) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < (u - 1%Z)%Z)%Z) -> (no_prime_in (mixfix_lbrb p i) (mixfix_lbrb p
(i + 1%Z)%Z)))).
Axiom exists_prime : forall (p:(array Z)) (u:Z), (1%Z <= u)%Z ->
((first_primes p u) -> forall (d:Z), ((2%Z <= d)%Z /\ (d <= (get p
((first_primes p u) -> forall (d:Z), ((2%Z <= d)%Z /\ (d <= (mixfix_lbrb p
(u - 1%Z)%Z))%Z) -> ((number.Prime.prime d) -> exists i:Z, ((0%Z <= i)%Z /\
(i < u)%Z) /\ (d = (get p i)))).
(i < u)%Z) /\ (d = (mixfix_lbrb p i)))).
Axiom Bertrand_postulate : forall (p:Z), (number.Prime.prime p) ->
~ (no_prime_in p (2%Z * p)%Z).
(* Why3 goal *)
Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z ->
((0%Z <= m)%Z -> forall (p:Z) (p1:(map.Map.map Z Z)), ((0%Z <= p)%Z /\
((p = m) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < m)%Z) -> ((map.Map.get p1
i) = 0%Z))) -> (((0%Z <= 0%Z)%Z /\ (0%Z < p)%Z) -> forall (p2:(map.Map.map
Z Z)), ((0%Z <= p)%Z /\ (p2 = (map.Map.set p1 0%Z 2%Z))) ->
(((0%Z <= 1%Z)%Z /\ (1%Z < p)%Z) -> forall (p3:(map.Map.map Z Z)),
((0%Z <= p)%Z /\ (p3 = (map.Map.set p2 1%Z 3%Z))) -> let o :=
(m - 1%Z)%Z in ((2%Z <= o)%Z -> forall (n:Z) (p4:(map.Map.map Z Z)),
forall (j:Z), ((2%Z <= j)%Z /\ (j <= o)%Z) -> (((first_primes (mk_array p
p4) j) /\ ((((map.Map.get p4 (j - 1%Z)%Z) < n)%Z /\
(n < (2%Z * (map.Map.get p4 (j - 1%Z)%Z))%Z)%Z) /\ ((number.Parity.odd
n) /\ (no_prime_in (map.Map.get p4 (j - 1%Z)%Z) n)))) -> forall (k:Z),
forall (n1:Z) (p5:(map.Map.map Z Z)), ((0%Z <= p)%Z /\ (((1%Z <= k)%Z /\
(k < j)%Z) /\ ((first_primes (mk_array p p5) j) /\ ((((map.Map.get p5
(j - 1%Z)%Z) < n1)%Z /\ (n1 < (2%Z * (map.Map.get p5 (j - 1%Z)%Z))%Z)%Z) /\
((number.Parity.odd n1) /\ ((no_prime_in (map.Map.get p5 (j - 1%Z)%Z)
n1) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < k)%Z) ->
~ (number.Divisibility.divides (map.Map.get p5 i) n1))))))) ->
(((0%Z <= k)%Z /\ (k < p)%Z) -> (((ZArith.BinInt.Z.rem n1 (map.Map.get p5
k)) = 0%Z) -> ~ (number.Prime.prime n1)))))))).
Theorem VC_prime_numbers : forall (m:Z), (2%Z <= m)%Z -> forall (p:(array
Z)), ((forall (i:Z), ((0%Z <= i)%Z /\ (i < m)%Z) -> ((mixfix_lbrb p
i) = 0%Z)) /\ ((length p) = m)) -> forall (p1:(array Z)),
((length p1) = (length p)) -> (((elts p1) = (map.Map.set (elts p) 0%Z
2%Z)) -> forall (p2:(array Z)), ((length p2) = (length p1)) ->
(((elts p2) = (map.Map.set (elts p1) 1%Z 3%Z)) -> let o := (m - 1%Z)%Z in
((2%Z <= (o + 1%Z)%Z)%Z -> forall (n:Z) (p3:(array Z)),
((length p3) = (length p2)) -> forall (j:Z), (((2%Z <= j)%Z /\
(j <= o)%Z) /\ ((first_primes p3 j) /\ ((((mixfix_lbrb p3
(j - 1%Z)%Z) < n)%Z /\ (n < (2%Z * (mixfix_lbrb p3 (j - 1%Z)%Z))%Z)%Z) /\
((number.Parity.odd n) /\ (no_prime_in (mixfix_lbrb p3 (j - 1%Z)%Z)
n))))) -> forall (n1:Z) (p4:(array Z)), ((length p4) = (length p3)) ->
forall (k:Z), (((1%Z <= k)%Z /\ (k < j)%Z) /\ ((first_primes p4 j) /\
((((mixfix_lbrb p4 (j - 1%Z)%Z) < n1)%Z /\ (n1 < (2%Z * (mixfix_lbrb p4
(j - 1%Z)%Z))%Z)%Z) /\ ((number.Parity.odd n1) /\ ((no_prime_in
(mixfix_lbrb p4 (j - 1%Z)%Z) n1) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < k)%Z) -> ~ (number.Divisibility.divides (mixfix_lbrb p4 i) n1)))))) ->
(((ZArith.BinInt.Z.rem n1 (mixfix_lbrb p4 k)) = 0%Z) ->
~ (number.Prime.prime n1))))).
intros m h1 p (h2,h3) p1 h4 h5 p2 h6 h7 o h8 n p3 h9 j
((h10,h11),(h12,((h13,h14),(h15,h16)))) n1 p4 h17 k
((h18,h19),(h20,((h21,h22),(h23,(h24,h25))))) h26.
Qed.
(* Unused content named WP_parameter_prime_numbers
intros m h1 h2 p p1 (h3,(h4,h5)) (h6,h7) p2 (h8,h9) (h10,h11) p3 (h12,h13) o
h14 n p4 j (h15,h16) (h17,((h18,h19),(h20,h21))) k n1 p5
(h22,((h23,h24),(h25,((h26,h27),(h28,(h29,h30)))))) (h31,h32) h33.
......@@ -135,4 +134,4 @@ rewrite <- H1.
apply H3; omega.
omega.
Qed.
*)
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