diff --git a/examples/in_progress/multiprecision/toom/why3session.xml b/examples/in_progress/multiprecision/toom/why3session.xml index fbeb025d30f1a08308c044e9de54eb9cc82a8610..a62e783fc54df50f4b40dadf1718318cdd3321f8 100644 --- a/examples/in_progress/multiprecision/toom/why3session.xml +++ b/examples/in_progress/multiprecision/toom/why3session.xml @@ -4,9 +4,9 @@ - + @@ -22,7 +22,7 @@ - + @@ -42,7 +42,7 @@ - + @@ -78,7 +78,7 @@ - + @@ -93,10 +93,10 @@ - + - + @@ -105,10 +105,10 @@ - + - + @@ -133,10 +133,10 @@ - + - + @@ -145,46 +145,73 @@ - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + @@ -192,23 +219,23 @@ - + - + - + - + - + @@ -220,18 +247,18 @@ - + - + - + @@ -241,41 +268,41 @@ - + - + - + - + - + - + - + - + - + - + @@ -284,19 +311,19 @@ - + - + - + - + - + @@ -306,7 +333,7 @@ - + @@ -314,61 +341,61 @@ - + - + - + - + - + - + - + - + - + - + - + @@ -381,46 +408,19 @@ - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -429,13 +429,13 @@ - + - + @@ -443,12 +443,12 @@ - + - + @@ -458,19 +458,19 @@ - + - + - + - + - + @@ -479,7 +479,7 @@ - + @@ -487,12 +487,12 @@ - + - + @@ -505,57 +505,62 @@ - + - + - + - + - + - + - + - + - + - + - + - - - + + + + + + + + - + - + @@ -579,7 +584,7 @@ - + @@ -592,7 +597,7 @@ - + @@ -607,16 +612,16 @@ - + - + - + @@ -631,15 +636,15 @@ - + - + - + @@ -664,7 +669,7 @@ - + @@ -673,36 +678,36 @@ - + - + - + - + - + - + - + - + - + @@ -713,7 +718,7 @@ - + @@ -723,7 +728,7 @@ - + @@ -731,16 +736,43 @@ - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + @@ -749,10 +781,10 @@ - + - + @@ -774,7 +806,7 @@ - + @@ -783,10 +815,15 @@ - + - - + + + + + + + @@ -798,20 +835,20 @@ - - + + - + - + @@ -820,13 +857,13 @@ - + - + - + @@ -835,7 +872,7 @@ - + @@ -844,22 +881,22 @@ - + - + - + - + - + - + @@ -872,10 +909,10 @@ - + - + @@ -884,31 +921,31 @@ - + - + - + - + - + - + @@ -917,22 +954,22 @@ - + - + - + - + - + @@ -950,43 +987,43 @@ - + - + - + - + - + - + - + - + - + - + @@ -1001,16 +1038,16 @@ - + - + - + @@ -1019,35 +1056,28 @@ - + - + - + - + - - - - - - - - + - + @@ -1077,16 +1107,16 @@ - + - + - + - + @@ -1134,22 +1164,22 @@ - + - + - + - + - + @@ -1158,34 +1188,7 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -1237,10 +1240,25 @@ - + - + + + + + + + + + + + + + + + + @@ -1252,22 +1270,22 @@ - + - + - + - + - + - + @@ -1356,7 +1374,7 @@ - + @@ -1364,7 +1382,7 @@ - + @@ -1412,10 +1430,17 @@ - + - + + + + + + + + @@ -1453,12 +1478,10 @@ - - - + @@ -1471,15 +1494,22 @@ - + + + + + + + + - + - + @@ -1490,10 +1520,18 @@ + + + + + + + + - + @@ -1509,7 +1547,7 @@ - + @@ -1530,18 +1568,18 @@ - + - + - + - + @@ -1552,22 +1590,22 @@ - + - + - + - + - + @@ -1633,36 +1671,43 @@ - + - + - + - + - + - + - + - + + + + + + + + @@ -1671,22 +1716,22 @@ - + - + - + - + - + @@ -1773,22 +1818,22 @@ - + - + - + - + - + @@ -1824,13 +1869,13 @@ - + - + @@ -1845,7 +1890,7 @@ - + @@ -1878,10 +1923,25 @@ - + + + + + + + + + + + + + + + + - + @@ -1896,7 +1956,7 @@ - + @@ -1945,7 +2005,7 @@ - + @@ -1953,7 +2013,7 @@ - + @@ -1983,7 +2043,7 @@ - + @@ -2009,7 +2069,22 @@ - + + + + + + + + + + + + + + + + @@ -2021,36 +2096,20 @@ - + - + - + - - - - - - - - - - - - - - - - - - + + @@ -2106,10 +2165,10 @@ - + - + @@ -2230,12 +2289,12 @@ - + - + @@ -2243,7 +2302,7 @@ - + @@ -2286,13 +2345,13 @@ - + - + @@ -2414,10 +2473,10 @@ - + - + @@ -2564,10 +2623,10 @@ - + - + @@ -2604,7 +2663,7 @@ - + @@ -2652,7 +2711,7 @@ - + @@ -2662,7 +2721,7 @@ - + @@ -2817,14 +2876,14 @@ - + - + @@ -2872,14 +2931,14 @@ - + - + @@ -2931,7 +2990,7 @@ - + @@ -2955,7 +3014,7 @@ - + @@ -2975,7 +3034,7 @@ - + @@ -3033,7 +3092,7 @@ - + @@ -3134,11 +3193,11 @@ - - + - + + @@ -3412,18 +3471,26 @@ - + + + + + - + + + + + - + - + @@ -3434,10 +3501,10 @@ - + - + @@ -3446,7 +3513,7 @@ - + @@ -3474,7 +3541,7 @@ - + @@ -3502,7 +3569,7 @@ - + @@ -3520,20 +3587,13 @@ - + - + - - - - - - - - + @@ -3542,10 +3602,10 @@ - + - + @@ -3554,15 +3614,12 @@ - + - - - - - - - + + + + @@ -3571,12 +3628,12 @@ - - + + - + - + @@ -3618,20 +3675,16 @@ - + - + - - - - - + - + @@ -3639,39 +3692,14 @@ - + - - - - - - - - - - - - + - - - - - - - - - - - - - - - + @@ -3686,10 +3714,10 @@ - + - + @@ -3704,21 +3732,14 @@ - + - - - - - - - - + @@ -3727,10 +3748,10 @@ - + - + @@ -3751,7 +3772,7 @@ - + @@ -3847,7 +3868,11 @@ - + + + + + @@ -3856,23 +3881,23 @@ - + - + - - + - + + - + - + @@ -3887,20 +3912,13 @@ - + - - - - - - - - + @@ -3911,7 +3929,7 @@ - + @@ -3921,13 +3939,10 @@ - - - - - - - + + + + @@ -3936,15 +3951,15 @@ - - + + - + - + - + @@ -3998,34 +4013,24 @@ - + - - - - - - - - - - - - - - - + - + + + + + - + @@ -4064,15 +4069,7 @@ - - - - - - - - - + @@ -4081,36 +4078,36 @@ - + - + - + - + - + - - + + - - + + - + - + @@ -4129,7 +4126,7 @@ - + @@ -4167,40 +4164,10 @@ - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - + @@ -4209,23 +4176,23 @@ - + - + - + + - - + - + - + @@ -4247,14 +4214,28 @@ - + + + + + + + + - + + + + + + + + @@ -4273,17 +4254,10 @@ - + - - - - - - - - - + + @@ -4350,30 +4324,18 @@ - + - + - - - - - - - - - - - - + - - + - + @@ -4390,7 +4352,7 @@ - + @@ -4408,7 +4370,15 @@ - + + + + + + + + + @@ -4426,28 +4396,31 @@ - + - + - + - - + + - - + + - - - - + + + + + + + @@ -4459,24 +4432,22 @@ - + - + - + - + - - - - + + @@ -4485,12 +4456,10 @@ - + - - - + @@ -4498,7 +4467,7 @@ - + @@ -4515,7 +4484,7 @@ - + @@ -4544,10 +4513,10 @@ - - + + - + @@ -4557,7 +4526,7 @@ - + @@ -4572,7 +4541,7 @@ - + @@ -4581,12 +4550,12 @@ - + - - + + - + @@ -4598,20 +4567,20 @@ - + - + - + - + @@ -4632,15 +4601,13 @@ - + - - + + - - - - + + @@ -4700,13 +4667,13 @@ - + - - + + - - + + diff --git a/examples/in_progress/multiprecision/toom/why3shapes.gz b/examples/in_progress/multiprecision/toom/why3shapes.gz index 0865d6a07ea967a6264d54ca688be9b72584cea4..c2e8dacc8fc8f71293e28c796caa23b3ca96825b 100644 Binary files a/examples/in_progress/multiprecision/toom/why3shapes.gz and b/examples/in_progress/multiprecision/toom/why3shapes.gz differ diff --git a/examples/in_progress/multiprecision/valuation.mlw b/examples/in_progress/multiprecision/valuation.mlw index fff2c74feec849e39052295c2e9a7a57fdb92717..b93c0698bd8c6d7f4b6c1db7ca155cff610a32b5 100644 --- a/examples/in_progress/multiprecision/valuation.mlw +++ b/examples/in_progress/multiprecision/valuation.mlw @@ -42,6 +42,10 @@ module Valuation = 1 + valuation (n * power p (k-1)) p } end + lemma valuation_split: forall n p. 1 <= n -> prime p -> + let v = valuation n p in + valuation (div n (power p v)) p = 0 (* only altergo proves this? *) + let lemma valuation_lower_bound (n p v:int) requires { 1 <= n /\ 1 < p /\ 0 <= v } requires { divides (power p v) n } @@ -76,10 +80,6 @@ module Valuation lemma valuation_zero_prod: forall c1 c2 p. 1 <= c1 -> 1 <= c2 -> prime p -> valuation c1 p = 0 -> valuation c2 p = 0 -> valuation (c1 * c2) p = 0 - lemma valuation_split: forall n p. 1 <= n -> prime p -> - let v = valuation n p in - valuation (div n (power p v)) p = 0 (* only altergo proves this? *) - let rec lemma valuation_times_nondiv (n c p:int) requires { 1 <= n /\ 1 <= c } requires { prime p } diff --git a/examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.agr b/examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.agr new file mode 100644 index 0000000000000000000000000000000000000000..411a9aea4186a68ab430f54210fcd08eed45b590 Binary files /dev/null and b/examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.agr differ diff --git a/examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.why b/examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.why new file mode 100644 index 0000000000000000000000000000000000000000..550fcee1b8a76f95509b4c83c30cbb2f6ee72fc7 --- /dev/null +++ b/examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.why @@ -0,0 +1,426 @@ +(* this is the prelude for Alt-Ergo, version >= 0.95.2 *) +(* this is a prelude for Alt-Ergo integer arithmetic *) +logic comp_div: int, int -> int +axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y +logic comp_mod: int, int -> int +axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y +logic match_bool : bool, 'a, 'a -> 'a + +axiom match_bool_True : + (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z)) + +axiom match_bool_False : + (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1)) + +axiom CompatOrderMult : + (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) -> + ((x * z) <= (y * z))))) + +logic power : int, int -> int + +axiom Power_0 : (forall x:int. (power(x, 0) = 1)) + +axiom Power_s : + (forall x:int. forall n:int. ((0 <= n) -> (power(x, + (n + 1)) = (x * power(x, n))))) + +axiom Power_s_alt : + (forall x:int. forall n:int. ((0 < n) -> (power(x, n) = (x * power(x, + (n - 1)))))) + +axiom Power_1 : (forall x:int. (power(x, 1) = x)) + +axiom Power_sum : + (forall x:int. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) -> + (power(x, (n + m)) = (power(x, n) * power(x, m)))))) + +axiom Power_mult : + (forall x:int. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) -> + (power(x, (n * m)) = power(power(x, n), m))))) + +axiom Power_comm1 : + (forall x:int. forall y:int. (((x * y) = (y * x)) -> + (forall n:int. ((0 <= n) -> ((power(x, n) * y) = (y * power(x, n))))))) + +axiom Power_comm2 : + (forall x:int. forall y:int. (((x * y) = (y * x)) -> + (forall n:int. ((0 <= n) -> (power((x * y), n) = (power(x, n) * power(y, + n))))))) + +axiom Power_non_neg : + (forall x:int. forall y:int. (((0 <= x) and (0 <= y)) -> (0 <= power(x, + y)))) + +axiom Power_monotonic : + (forall x:int. forall n:int. forall m:int. (((0 < x) and ((0 <= n) and + (n <= m))) -> (power(x, n) <= power(x, m)))) + +logic abs : int -> int + +axiom abs_def : (forall x:int. ((0 <= x) -> (abs(x) = x))) + +axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs(x) = (-x)))) + +axiom Abs_le : (forall x:int. forall y:int. ((abs(x) <= y) -> ((-y) <= x))) + +axiom Abs_le1 : (forall x:int. forall y:int. ((abs(x) <= y) -> (x <= y))) + +axiom Abs_le2 : + (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) -> (abs(x) <= y))) + +axiom Abs_pos : (forall x:int. (0 <= abs(x))) + +axiom Div_mod : + (forall x:int. forall y:int. ((not (y = 0)) -> + (x = ((y * comp_div(x,y)) + comp_mod(x,y))))) + +axiom Div_bound : + (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> + (0 <= comp_div(x,y)))) + +axiom Div_bound1 : + (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> + (comp_div(x,y) <= x))) + +axiom Mod_bound : + (forall x:int. forall y:int. ((not (y = 0)) -> + ((-abs(y)) < comp_mod(x,y)))) + +axiom Mod_bound1 : + (forall x:int. forall y:int. ((not (y = 0)) -> (comp_mod(x,y) < abs(y)))) + +axiom Div_sign_pos : + (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> + (0 <= comp_div(x,y)))) + +axiom Div_sign_neg : + (forall x:int. forall y:int. (((x <= 0) and (0 < y)) -> + (comp_div(x,y) <= 0))) + +axiom Mod_sign_pos : + (forall x:int. forall y:int. (((0 <= x) and (not (y = 0))) -> + (0 <= comp_mod(x,y)))) + +axiom Mod_sign_neg : + (forall x:int. forall y:int. (((x <= 0) and (not (y = 0))) -> + (comp_mod(x,y) <= 0))) + +axiom Rounds_toward_zero : + (forall x:int. forall y:int. ((not (y = 0)) -> + (abs((comp_div(x,y) * y)) <= abs(x)))) + +axiom Div_1 : (forall x:int. (comp_div(x,1) = x)) + +axiom Mod_1 : (forall x:int. (comp_mod(x,1) = 0)) + +axiom Div_inf : + (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> + (comp_div(x,y) = 0))) + +axiom Mod_inf : + (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> + (comp_mod(x,y) = x))) + +axiom Div_mult : + (forall x:int. forall y:int. forall z:int [comp_div(((x * y) + z),x)]. + (((0 < x) and ((0 <= y) and (0 <= z))) -> + (comp_div(((x * y) + z),x) = (y + comp_div(z,x))))) + +axiom Mod_mult : + (forall x:int. forall y:int. forall z:int [comp_mod(((x * y) + z),x)]. + (((0 < x) and ((0 <= y) and (0 <= z))) -> + (comp_mod(((x * y) + z),x) = comp_mod(z,x)))) + +predicate divides(d: int, n: int) = (((d = 0) -> (n = 0)) and + ((not (d = 0)) -> (comp_mod(n,d) = 0))) + +axiom divides_spec : + (forall d:int. forall n:int. (divides(d, n) -> + (exists q:int. (n = (q * d))))) + +axiom divides_spec1 : + (forall d:int. forall n:int. ((exists q:int. (n = (q * d))) -> divides(d, + n))) + +axiom divides_refl : (forall n:int. divides(n, n)) + +axiom divides_1_n : (forall n:int. divides(1, n)) + +axiom divides_0 : (forall n:int. divides(n, 0)) + +axiom divides_left : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> + divides((c * a), (c * b)))) + +axiom divides_right : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> + divides((a * c), (b * c)))) + +axiom divides_oppr : + (forall a:int. forall b:int. (divides(a, b) -> divides(a, (-b)))) + +axiom divides_oppl : + (forall a:int. forall b:int. (divides(a, b) -> divides((-a), b))) + +axiom divides_oppr_rev : + (forall a:int. forall b:int. (divides((-a), b) -> divides(a, b))) + +axiom divides_oppl_rev : + (forall a:int. forall b:int. (divides(a, (-b)) -> divides(a, b))) + +axiom divides_plusr : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(a, + c) -> divides(a, (b + c))))) + +axiom divides_minusr : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(a, + c) -> divides(a, (b - c))))) + +axiom divides_multl : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides(a, + (c * b)))) + +axiom divides_multr : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides(a, + (b * c)))) + +axiom divides_factorl : (forall a:int. forall b:int. divides(a, (b * a))) + +axiom divides_factorr : (forall a:int. forall b:int. divides(a, (a * b))) + +axiom divides_n_1 : + (forall n:int. (divides(n, 1) -> ((n = 1) or (n = (- 1))))) + +axiom divides_antisym : + (forall a:int. forall b:int. (divides(a, b) -> (divides(b, a) -> + ((a = b) or (a = (-b)))))) + +axiom divides_trans : + (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(b, + c) -> divides(a, c)))) + +axiom divides_bounds : + (forall a:int. forall b:int. (divides(a, b) -> ((not (b = 0)) -> + (abs(a) <= abs(b))))) + +axiom Div_mod1 : + (forall x:int. forall y:int. ((not (y = 0)) -> + (x = ((y * (x / y)) + (x % y))))) + +axiom Mod_bound2 : + (forall x:int. forall y:int. ((not (y = 0)) -> (0 <= (x % y)))) + +axiom Mod_bound3 : + (forall x:int. forall y:int. ((not (y = 0)) -> ((x % y) < abs(y)))) + +axiom Div_unique : + (forall x:int. forall y:int. forall q:int. ((0 < y) -> + ((((q * y) <= x) and (x < ((q * y) + y))) -> ((x / y) = q)))) + +axiom Div_bound2 : + (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= (x / y)))) + +axiom Div_bound3 : + (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> ((x / y) <= x))) + +axiom Mod_11 : (forall x:int. ((x % 1) = 0)) + +axiom Div_11 : (forall x:int. ((x / 1) = x)) + +axiom Div_inf1 : + (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> ((x / y) = 0))) + +axiom Div_inf_neg : + (forall x:int. forall y:int. (((0 < x) and (x <= y)) -> + (((-x) / y) = (- 1)))) + +axiom Mod_0 : (forall y:int. ((not (y = 0)) -> ((0 % y) = 0))) + +axiom Div_1_left : (forall y:int. ((1 < y) -> ((1 / y) = 0))) + +axiom Div_minus1_left : (forall y:int. ((1 < y) -> (((- 1) / y) = (- 1)))) + +axiom Mod_1_left : (forall y:int. ((1 < y) -> ((1 % y) = 1))) + +axiom Mod_minus1_left : (forall y:int. ((1 < y) -> (((- 1) % y) = (y - 1)))) + +axiom Div_mult1 : + (forall x:int. forall y:int. forall z:int [(((x * y) + z) / x)]. + ((0 < x) -> ((((x * y) + z) / x) = (y + (z / x))))) + +axiom Mod_mult1 : + (forall x:int. forall y:int. forall z:int [(((x * y) + z) % x)]. + ((0 < x) -> ((((x * y) + z) % x) = (z % x)))) + +axiom mod_divides_euclidean : + (forall a:int. forall b:int. ((not (b = 0)) -> (((a % b) = 0) -> divides(b, + a)))) + +axiom divides_mod_euclidean : + (forall a:int. forall b:int. ((not (b = 0)) -> (divides(b, a) -> + ((a % b) = 0)))) + +axiom mod_divides_computer : + (forall a:int. forall b:int. ((not (b = 0)) -> ((comp_mod(a,b) = 0) -> + divides(b, a)))) + +axiom divides_mod_computer : + (forall a:int. forall b:int. ((not (b = 0)) -> (divides(b, a) -> + (comp_mod(a,b) = 0)))) + +predicate even(n: int) = (exists k:int. (n = (2 * k))) + +predicate odd(n: int) = (exists k:int. (n = ((2 * k) + 1))) + +axiom even_or_odd : (forall n:int. (even(n) or odd(n))) + +axiom even_not_odd : (forall n:int. (even(n) -> (not odd(n)))) + +axiom odd_not_even : (forall n:int. (odd(n) -> (not even(n)))) + +axiom even_odd : (forall n:int. (even(n) -> odd((n + 1)))) + +axiom odd_even : (forall n:int. (odd(n) -> even((n + 1)))) + +axiom even_even : (forall n:int. (even(n) -> even((n + 2)))) + +axiom odd_odd : (forall n:int. (odd(n) -> odd((n + 2)))) + +axiom even_2k : (forall k:int. even((2 * k))) + +axiom odd_2k1 : (forall k:int. odd(((2 * k) + 1))) + +axiom even_mod2 : (forall n:int. (even(n) -> (comp_mod(n,2) = 0))) + +axiom even_mod21 : (forall n:int. ((comp_mod(n,2) = 0) -> even(n))) + +axiom even_divides : (forall a:int. (even(a) -> divides(2, a))) + +axiom even_divides1 : (forall a:int. (divides(2, a) -> even(a))) + +axiom odd_divides : (forall a:int. (odd(a) -> (not divides(2, a)))) + +axiom odd_divides1 : (forall a:int. ((not divides(2, a)) -> odd(a))) + +predicate prime(p: int) = ((2 <= p) and + (forall n:int. (((1 < n) and (n < p)) -> (not divides(n, p))))) + +axiom not_prime_1 : (not prime(1)) + +axiom prime_2 : prime(2) + +axiom prime_3 : prime(3) + +axiom prime_divisors : + (forall p:int. (prime(p) -> + (forall d:int. (divides(d, p) -> ((d = 1) or ((d = (- 1)) or ((d = p) or + (d = (-p))))))))) + +axiom small_divisors : + (forall p:int. ((2 <= p) -> + ((forall d:int. ((2 <= d) -> (prime(d) -> (((1 < (d * d)) and + ((d * d) <= p)) -> (not divides(d, p)))))) -> + prime(p)))) + +axiom even_prime : (forall p:int. (prime(p) -> (even(p) -> (p = 2)))) + +axiom odd_prime : (forall p:int. (prime(p) -> ((3 <= p) -> odd(p)))) + +logic ac gcd : int, int -> int + +axiom gcd_nonneg : (forall a:int. forall b:int. (0 <= gcd(a, b))) + +axiom gcd_def1 : (forall a:int. forall b:int. divides(gcd(a, b), a)) + +axiom gcd_def2 : (forall a:int. forall b:int. divides(gcd(a, b), b)) + +axiom gcd_def3 : + (forall a:int. forall b:int. forall x:int. (divides(x, a) -> (divides(x, + b) -> divides(x, gcd(a, b))))) + +axiom gcd_unique : + (forall a:int. forall b:int. forall d:int. ((0 <= d) -> (divides(d, a) -> + (divides(d, b) -> + ((forall x:int. (divides(x, a) -> (divides(x, b) -> divides(x, d)))) -> + (d = gcd(a, b))))))) + +axiom gcd_0_pos : (forall a:int. ((0 <= a) -> (gcd(a, 0) = a))) + +axiom gcd_0_neg : (forall a:int. ((a < 0) -> (gcd(a, 0) = (-a)))) + +axiom gcd_opp : (forall a:int. forall b:int. (gcd(a, b) = gcd((-a), b))) + +axiom gcd_euclid : + (forall a:int. forall b:int. forall q:int. (gcd(a, b) = gcd(a, + (b - (q * a))))) + +axiom Gcd_computer_mod : + (forall a:int. forall b:int [gcd(b, comp_mod(a,b))]. ((not (b = 0)) -> + (gcd(b, comp_mod(a,b)) = gcd(a, b)))) + +axiom Gcd_euclidean_mod : + (forall a:int. forall b:int [gcd(b, (a % b))]. ((not (b = 0)) -> (gcd(b, + (a % b)) = gcd(a, b)))) + +axiom gcd_mult : + (forall a:int. forall b:int. forall c:int. ((0 <= c) -> (gcd((c * a), + (c * b)) = (c * gcd(a, b))))) + +predicate coprime(a: int, b: int) = (gcd(a, b) = 1) + +axiom prime_coprime : (forall p:int. (prime(p) -> (2 <= p))) + +axiom prime_coprime1 : + (forall p:int. (prime(p) -> + (forall n:int. (((1 <= n) and (n < p)) -> coprime(n, p))))) + +axiom prime_coprime2 : + (forall p:int. (((2 <= p) and + (forall n:int. (((1 <= n) and (n < p)) -> coprime(n, p)))) -> prime(p))) + +axiom Gauss : + (forall a:int. forall b:int. forall c:int. ((divides(a, (b * c)) and + coprime(a, b)) -> divides(a, c))) + +axiom Euclid : + (forall p:int. forall a:int. forall b:int. ((prime(p) and divides(p, + (a * b))) -> (divides(p, a) or divides(p, b)))) + +axiom gcd_coprime : + (forall a:int. forall b:int. forall c:int. (coprime(a, b) -> (gcd(a, + (b * c)) = gcd(a, c)))) + +logic valuation : int, int -> int + +axiom valuation_def : + (forall n:int. forall p:int. ((1 < p) -> ((1 <= n) -> + ((comp_mod(n,p) = 0) -> (valuation(n, p) = (valuation(comp_div(n,p), + p) + 1)))))) + +axiom valuation_def1 : + (forall n:int. forall p:int. ((1 < p) -> ((1 <= n) -> + ((not (comp_mod(n,p) = 0)) -> (valuation(n, p) = 0))))) + +axiom valuation_spec : + (forall n:int. forall p:int. ((1 < p) -> ((1 <= n) -> (0 <= valuation(n, + p))))) + +axiom valuation_spec1 : + (forall n:int. forall p:int. ((1 < p) -> ((1 <= n) -> divides(power(p, + valuation(n, p)), n)))) + +axiom valuation_mul : + (forall n:int. forall p:int. ((1 <= n) -> ((1 < p) -> (valuation((n * p), + p) = (1 + valuation(n, p)))))) + +axiom power_ge_1 : + (forall b:int. forall e:int. ((1 <= b) -> ((0 <= e) -> (1 <= power(b, + e))))) + +axiom valuation_times_pow : + (forall n:int. forall p:int. forall k:int. (((1 <= n) and ((1 < p) and + (0 <= k))) -> (valuation((n * power(p, k)), p) = (k + valuation(n, p))))) + +goal valuation_split : + (forall n:int. forall p:int. ((1 <= n) -> (prime(p) -> + (valuation(comp_div(n,power(p, valuation(n, p))), p) = 0)))) diff --git a/examples/in_progress/multiprecision/valuation/why3session.xml b/examples/in_progress/multiprecision/valuation/why3session.xml index 0daee06c099a8038729b674fbae264f4dde7fcd0..09804de6b8b432d25579c3acf36350ca5fc4e613 100644 --- a/examples/in_progress/multiprecision/valuation/why3session.xml +++ b/examples/in_progress/multiprecision/valuation/why3session.xml @@ -5,8 +5,8 @@ - + @@ -26,12 +26,6 @@ - - - - - - @@ -52,8 +46,8 @@ - + @@ -62,13 +56,13 @@ - + - + - + @@ -98,10 +92,10 @@ - + - + @@ -113,19 +107,23 @@ + + + + - + - + - + @@ -134,7 +132,7 @@ - + @@ -146,10 +144,10 @@ - + - + @@ -166,13 +164,13 @@ - + - + @@ -180,39 +178,23 @@ - + - - - - + - - - - - - - - - - - - - - + - + - + @@ -240,7 +222,7 @@ - + @@ -253,19 +235,17 @@ - - - + - + - + @@ -285,15 +265,15 @@ - + - + - + @@ -309,13 +289,13 @@ - + - + - + @@ -344,12 +324,12 @@ - + - + @@ -357,7 +337,7 @@ - + diff --git a/examples/in_progress/multiprecision/valuation/why3shapes.gz b/examples/in_progress/multiprecision/valuation/why3shapes.gz index ae98327408dbcdddb8253f02a4abedd7980a2591..6ffffa3a4c02e03694871b77c7e56272c109dcd6 100644 Binary files a/examples/in_progress/multiprecision/valuation/why3shapes.gz and b/examples/in_progress/multiprecision/valuation/why3shapes.gz differ diff --git a/examples/multiprecision/util.mlw b/examples/multiprecision/util.mlw index c899342e3f545c1623a965b4e29d92b71ad89caf..8c3ea49ba08be8788fcf6b072af868cac4c72401 100644 --- a/examples/multiprecision/util.mlw +++ b/examples/multiprecision/util.mlw @@ -42,6 +42,39 @@ module Util i := Int32.(+) !i one; done + (* [is_zero] checks if [x[0..sz-1]] is zero. It corresponds to [mpn_zero_p]. *) + let is_zero (x:t) (sz:int32) : int32 + requires { valid x sz } + ensures { 0 <= Int32.to_int result <= 1 } + ensures { Int32.to_int result = 1 <-> value x sz = 0 } + = + let i = ref sz in + let uzero = Limb.of_int 0 in + let lx = ref uzero in + try + while Int32.(>=) !i (Int32.of_int 1) do + variant { p2i !i } + invariant { 0 <= !i <= sz } + invariant { value_sub (pelts x) (x.offset + !i) (x.offset + sz)=0 } + let ghost k = p2i !i in + i := Int32.(-) !i (Int32.of_int 1); + assert { 0 <= !i < sz }; + lx := get_ofs x !i; + if not (Limb.(=) !lx uzero) + then begin + value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset + p2i sz); + value_sub_lower_bound_tight (pelts x) x.offset (x.offset+k); + value_sub_lower_bound (pelts x) (x.offset+k) (x.offset + p2i sz); + raise Return32 (Int32.of_int 0); + end + else begin + assert { 1+2=3 }; + end + done; + Int32.of_int 1 + with Return32 r -> r + end + (** [zero r sz] sets [(r,sz)] to zero. Corresponds to [mpn_zero]. *) let zero (r:t) (sz:int32) : unit requires { valid r sz } diff --git a/examples/multiprecision/util/why3session.xml b/examples/multiprecision/util/why3session.xml index 13d81b38ae919e9cd35dde6fc5f3dc7031c2c664..00fa441900187c2fbfc4e26a34d7456a07c2509c 100644 --- a/examples/multiprecision/util/why3session.xml +++ b/examples/multiprecision/util/why3session.xml @@ -115,6 +115,74 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/multiprecision/util/why3shapes.gz b/examples/multiprecision/util/why3shapes.gz index 6239efc4c94f3abea733c1eb69df93c94af07f37..100b2cd6760dae69c8d35840630a2483e3f5b759 100644 Binary files a/examples/multiprecision/util/why3shapes.gz and b/examples/multiprecision/util/why3shapes.gz differ