number.mlw 5.5 KB
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3 4 5
(** {1 Number theory} *)


(** {2 Parity properties} *)
Jean-Christophe's avatar
Jean-Christophe committed
6

7
module Parity
8 9 10 11 12 13

  use import int.Int

  predicate even (n: int) = exists k: int. n = 2 * k
  predicate odd (n: int) = exists k: int. n = 2 * k + 1

14 15 16 17 18 19 20 21 22 23 24
  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)

25 26 27
  lemma even_2k: forall k: int. even (2 * k)
  lemma odd_2k1: forall k: int. odd (2 * k + 1)

28 29 30
  use import int.ComputerDivision

  lemma even_mod2 :
31
    forall n:int. even n <-> mod n 2 = 0
32

33 34
end

MARCHE Claude's avatar
MARCHE Claude committed
35 36
(** {2 Divisibility} *)

37
module Divisibility
Jean-Christophe's avatar
Jean-Christophe committed
38 39

  use export int.Int
40
  use import int.ComputerDivision
Jean-Christophe's avatar
Jean-Christophe committed
41

42 43 44
  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
Jean-Christophe's avatar
Jean-Christophe committed
45

46 47 48
  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
Jean-Christophe's avatar
Jean-Christophe committed
49

50 51
  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)
Jean-Christophe's avatar
Jean-Christophe committed
52

53 54 55 56
  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
Jean-Christophe's avatar
Jean-Christophe committed
57

Andrei Paskevich's avatar
Andrei Paskevich committed
58
  lemma divides_plusr:
59
    forall a b c: int. divides a b -> divides a c -> divides a (b + c)
Andrei Paskevich's avatar
Andrei Paskevich committed
60
  lemma divides_minusr:
61
    forall a b c: int. divides a b -> divides a c -> divides a (b - c)
Andrei Paskevich's avatar
Andrei Paskevich committed
62
  lemma divides_multl:
63
    forall a b c: int. divides a b -> divides a (c * b)
Andrei Paskevich's avatar
Andrei Paskevich committed
64
  lemma divides_multr:
65
    forall a b c: int. divides a b -> divides a (b * c)
Jean-Christophe's avatar
Jean-Christophe committed
66

67 68
  lemma divides_factorl: forall a b: int. divides a (b * a)
  lemma divides_factorr: forall a b: int. divides a (a * b)
Jean-Christophe's avatar
Jean-Christophe committed
69

70
  lemma divides_n_1: forall n: int. divides n 1 -> n = 1 \/ n = -1
Jean-Christophe's avatar
Jean-Christophe committed
71

72 73
  lemma divides_antisym:
    forall a b: int. divides a b -> divides b a -> a = b \/ a = -b
Jean-Christophe's avatar
Jean-Christophe committed
74

75 76
  lemma divides_trans:
    forall a b c: int. divides a b -> divides b c -> divides a c
Jean-Christophe's avatar
Jean-Christophe committed
77 78 79

  use import int.Abs

80 81
  lemma divides_bounds:
    forall a b: int. divides a b -> b <> 0 -> abs a <= abs b
Jean-Christophe's avatar
Jean-Christophe committed
82

83 84 85 86 87 88
  use int.EuclideanDivision

  lemma mod_divides_euclidean:
    forall a b: int. b <> 0 -> EuclideanDivision.mod a b = 0 -> divides b a
  lemma divides_mod_euclidean:
    forall a b: int. b <> 0 -> divides b a -> EuclideanDivision.mod a b = 0
Jean-Christophe's avatar
Jean-Christophe committed
89

90 91 92 93 94 95 96 97 98 99 100
  use int.ComputerDivision

  lemma mod_divides_computer:
    forall a b: int. b <> 0 -> ComputerDivision.mod a b = 0 -> divides b a
  lemma divides_mod_computer:
    forall a b: int. b <> 0 -> divides b a -> ComputerDivision.mod a b = 0

  use import Parity

  lemma even_divides: forall a: int. even a <-> divides 2 a
  lemma odd_divides: forall a: int. odd a <-> not (divides 2 a)
Andrei Paskevich's avatar
Andrei Paskevich committed
101

Jean-Christophe's avatar
Jean-Christophe committed
102 103
end

MARCHE Claude's avatar
MARCHE Claude committed
104 105
(** {2 Greateast Common Divisor} *)

106
module Gcd
Jean-Christophe's avatar
Jean-Christophe committed
107 108 109 110

  use export int.Int
  use import Divisibility

Andrei Paskevich's avatar
Andrei Paskevich committed
111
  function gcd int int : int
Jean-Christophe's avatar
Jean-Christophe committed
112

113 114 115 116 117 118 119 120 121 122 123 124 125
  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 *)

126
  clone algebra.AC with type t = int, function op = gcd
127 128 129 130 131 132 133

  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)
Jean-Christophe's avatar
Jean-Christophe committed
134

135
  use int.ComputerDivision
Jean-Christophe's avatar
Jean-Christophe committed
136

137
  lemma Gcd_computer_mod:
138 139
    forall a b: int [gcd b (ComputerDivision.mod a b)].
    b <> 0 -> gcd b (ComputerDivision.mod a b) = gcd a b
140 141 142 143

  use int.EuclideanDivision

  lemma Gcd_euclidean_mod:
144
    forall a b: int [gcd b (EuclideanDivision.mod a b)].
145
    b <> 0 -> gcd b (EuclideanDivision.mod a b) = gcd a b
146 147

  lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b
Jean-Christophe's avatar
Jean-Christophe committed
148 149 150

end

MARCHE Claude's avatar
MARCHE Claude committed
151 152
(** {2 Prime numbers} *)

153
module Prime
Jean-Christophe's avatar
Jean-Christophe committed
154 155 156 157

  use export int.Int
  use import Divisibility

158
  predicate prime (p: int) =
159
    2 <= p /\ forall n: int. 1 < n < p -> not (divides n p)
160 161 162 163 164 165 166 167

  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
Jean-Christophe's avatar
Jean-Christophe committed
168

169 170 171 172 173
  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

174 175 176 177 178 179
  use import 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

180 181
end

MARCHE Claude's avatar
MARCHE Claude committed
182 183
(** {2 Coprime numbers} *)

184
module Coprime
185 186 187 188

  use export int.Int
  use import Divisibility
  use import Gcd
Jean-Christophe's avatar
Jean-Christophe committed
189

190
  predicate coprime (a b: int) = gcd a b = 1
Jean-Christophe's avatar
Jean-Christophe committed
191

192
  use import Prime
Jean-Christophe's avatar
Jean-Christophe committed
193

194 195 196
  lemma prime_coprime:
    forall p: int.
    prime p <-> 2 <= p && forall n:int. 1 <= n < p -> coprime n p
Jean-Christophe's avatar
Jean-Christophe committed
197

198 199 200 201 202 203 204
  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

205 206
  lemma gcd_coprime:
    forall a b c. coprime a b -> gcd a (b*c) = gcd a c
207

Jean-Christophe's avatar
Jean-Christophe committed
208
end