mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
209 lines
5.3 KiB
Plaintext
209 lines
5.3 KiB
Plaintext
|
|
(** {1 Number theory} *)
|
|
|
|
|
|
(** {2 Parity properties} *)
|
|
|
|
module Parity
|
|
|
|
use int.Int
|
|
|
|
predicate even (n: int) = exists k: int. n = 2 * k
|
|
predicate odd (n: int) = exists k: int. n = 2 * k + 1
|
|
|
|
lemma even_or_odd: forall n: int. even n \/ odd n
|
|
|
|
lemma even_not_odd: forall n: int. even n -> not (odd n)
|
|
lemma odd_not_even: forall n: int. odd n -> not (even n)
|
|
|
|
lemma even_odd: forall n: int. even n -> odd (n + 1)
|
|
lemma odd_even: forall n: int. odd n -> even (n + 1)
|
|
|
|
lemma even_even: forall n: int. even n -> even (n + 2)
|
|
lemma odd_odd: forall n: int. odd n -> odd (n + 2)
|
|
|
|
lemma even_2k: forall k: int. even (2 * k)
|
|
lemma odd_2k1: forall k: int. odd (2 * k + 1)
|
|
|
|
use int.ComputerDivision
|
|
|
|
lemma even_mod2 :
|
|
forall n:int. even n <-> mod n 2 = 0
|
|
|
|
end
|
|
|
|
(** {2 Divisibility} *)
|
|
|
|
module Divisibility
|
|
|
|
use export int.Int
|
|
use int.ComputerDivision
|
|
|
|
let predicate divides (d:int) (n:int)
|
|
ensures { result <-> exists q:int. n = q * d }
|
|
= if d = 0 then n = 0 else mod n d = 0
|
|
|
|
lemma divides_refl: forall n:int. divides n n
|
|
lemma divides_1_n : forall n:int. divides 1 n
|
|
lemma divides_0 : forall n:int. divides n 0
|
|
|
|
lemma divides_left : forall a b c: int. divides a b -> divides (c*a) (c*b)
|
|
lemma divides_right: forall a b c: int. divides a b -> divides (a*c) (b*c)
|
|
|
|
lemma divides_oppr: forall a b: int. divides a b -> divides a (-b)
|
|
lemma divides_oppl: forall a b: int. divides a b -> divides (-a) b
|
|
lemma divides_oppr_rev: forall a b: int. divides (-a) b -> divides a b
|
|
lemma divides_oppl_rev: forall a b: int. divides a (-b) -> divides a b
|
|
|
|
lemma divides_plusr:
|
|
forall a b c: int. divides a b -> divides a c -> divides a (b + c)
|
|
lemma divides_minusr:
|
|
forall a b c: int. divides a b -> divides a c -> divides a (b - c)
|
|
lemma divides_multl:
|
|
forall a b c: int. divides a b -> divides a (c * b)
|
|
lemma divides_multr:
|
|
forall a b c: int. divides a b -> divides a (b * c)
|
|
|
|
lemma divides_factorl: forall a b: int. divides a (b * a)
|
|
lemma divides_factorr: forall a b: int. divides a (a * b)
|
|
|
|
lemma divides_n_1: forall n: int. divides n 1 -> n = 1 \/ n = -1
|
|
|
|
lemma divides_antisym:
|
|
forall a b: int. divides a b -> divides b a -> a = b \/ a = -b
|
|
|
|
lemma divides_trans:
|
|
forall a b c: int. divides a b -> divides b c -> divides a c
|
|
|
|
use int.Abs
|
|
|
|
lemma divides_bounds:
|
|
forall a b: int. divides a b -> b <> 0 -> abs a <= abs b
|
|
|
|
use int.EuclideanDivision as ED
|
|
|
|
lemma mod_divides_euclidean:
|
|
forall a b: int. b <> 0 -> ED.mod a b = 0 -> divides b a
|
|
lemma divides_mod_euclidean:
|
|
forall a b: int. b <> 0 -> divides b a -> ED.mod a b = 0
|
|
|
|
use int.ComputerDivision as CD
|
|
|
|
lemma mod_divides_computer:
|
|
forall a b: int. b <> 0 -> CD.mod a b = 0 -> divides b a
|
|
lemma divides_mod_computer:
|
|
forall a b: int. b <> 0 -> divides b a -> CD.mod a b = 0
|
|
|
|
use Parity
|
|
|
|
lemma even_divides: forall a: int. even a <-> divides 2 a
|
|
lemma odd_divides: forall a: int. odd a <-> not (divides 2 a)
|
|
|
|
end
|
|
|
|
(** {2 Greateast Common Divisor} *)
|
|
|
|
module Gcd
|
|
|
|
use export int.Int
|
|
use Divisibility
|
|
|
|
function gcd int int : int
|
|
|
|
axiom gcd_nonneg: forall a b: int. 0 <= gcd a b
|
|
axiom gcd_def1 : forall a b: int. divides (gcd a b) a
|
|
axiom gcd_def2 : forall a b: int. divides (gcd a b) b
|
|
axiom gcd_def3 :
|
|
forall a b x: int. divides x a -> divides x b -> divides x (gcd a b)
|
|
axiom gcd_unique:
|
|
forall a b 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
|
|
|
|
(* gcd is associative commutative *)
|
|
|
|
clone algebra.AC with type t = int, function op = gcd
|
|
|
|
lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a
|
|
lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a
|
|
|
|
lemma gcd_opp: forall a b: int. gcd a b = gcd (-a) b
|
|
|
|
lemma gcd_euclid: forall a b q: int. gcd a b = gcd a (b - q * a)
|
|
|
|
use int.ComputerDivision as CD
|
|
|
|
lemma Gcd_computer_mod:
|
|
forall a b: int [gcd b (CD.mod a b)].
|
|
b <> 0 -> gcd b (CD.mod a b) = gcd a b
|
|
|
|
use int.EuclideanDivision as ED
|
|
|
|
lemma Gcd_euclidean_mod:
|
|
forall a b: int [gcd b (ED.mod a b)].
|
|
b <> 0 -> gcd b (ED.mod a b) = gcd a b
|
|
|
|
lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b
|
|
|
|
end
|
|
|
|
(** {2 Prime numbers} *)
|
|
|
|
module Prime
|
|
|
|
use export int.Int
|
|
use Divisibility
|
|
|
|
predicate prime (p: int) =
|
|
2 <= p /\ forall n: int. 1 < n < p -> not (divides n p)
|
|
|
|
lemma not_prime_1: not (prime 1)
|
|
lemma prime_2 : prime 2
|
|
lemma prime_3 : prime 3
|
|
|
|
lemma prime_divisors:
|
|
forall p: int. prime p ->
|
|
forall d: int. divides d p -> d = 1 \/ d = -1 \/ d = p \/ d = -p
|
|
|
|
lemma small_divisors:
|
|
forall p: int. 2 <= p ->
|
|
(forall d: int. 2 <= d -> prime d -> 1 < d*d <= p -> not (divides d p)) ->
|
|
prime p
|
|
|
|
use Parity
|
|
|
|
lemma even_prime: forall p: int. prime p -> even p -> p = 2
|
|
|
|
lemma odd_prime: forall p: int. prime p -> p >= 3 -> odd p
|
|
|
|
end
|
|
|
|
(** {2 Coprime numbers} *)
|
|
|
|
module Coprime
|
|
|
|
use export int.Int
|
|
use Divisibility
|
|
use Gcd
|
|
|
|
predicate coprime (a b: int) = gcd a b = 1
|
|
|
|
use Prime
|
|
|
|
lemma prime_coprime:
|
|
forall p: int.
|
|
prime p <-> 2 <= p && forall n:int. 1 <= n < p -> coprime n p
|
|
|
|
lemma Gauss:
|
|
forall a b c:int. divides a (b*c) /\ coprime a b -> divides a c
|
|
|
|
lemma Euclid:
|
|
forall p a b:int.
|
|
prime p /\ divides p (a*b) -> divides p a \/ divides p b
|
|
|
|
lemma gcd_coprime:
|
|
forall a b c. coprime a b -> gcd a (b*c) = gcd a c
|
|
|
|
end
|