number.mlw 5.34 KB
 Jean-Christophe committed Mar 16, 2011 1 `````` `````` MARCHE Claude committed May 07, 2012 2 3 4 5 ``````(** {1 Number theory} *) (** {2 Parity properties} *) `````` Jean-Christophe committed Mar 16, 2011 6 `````` `````` Andrei Paskevich committed Dec 22, 2017 7 ``````module Parity `````` Jean-Christophe Filliatre committed Aug 05, 2011 8 `````` `````` Andrei Paskevich committed Jun 15, 2018 9 `````` use int.Int `````` Jean-Christophe Filliatre committed Aug 05, 2011 10 11 12 13 `````` predicate even (n: int) = exists k: int. n = 2 * k predicate odd (n: int) = exists k: int. n = 2 * k + 1 `````` Jean-Christophe Filliatre committed Aug 17, 2011 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) `````` Jean-Christophe Filliatre committed Aug 05, 2011 25 26 27 `````` lemma even_2k: forall k: int. even (2 * k) lemma odd_2k1: forall k: int. odd (2 * k + 1) `````` Andrei Paskevich committed Jun 15, 2018 28 `````` use int.ComputerDivision `````` MARCHE Claude committed Mar 07, 2016 29 30 `````` lemma even_mod2 : `````` Jean-Christophe Filliatre committed Apr 22, 2017 31 `````` forall n:int. even n <-> mod n 2 = 0 `````` MARCHE Claude committed Mar 07, 2016 32 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 33 34 ``````end `````` MARCHE Claude committed May 07, 2012 35 36 ``````(** {2 Divisibility} *) `````` Andrei Paskevich committed Dec 22, 2017 37 ``````module Divisibility `````` Jean-Christophe committed Mar 16, 2011 38 39 `````` use export int.Int `````` Andrei Paskevich committed Jun 15, 2018 40 `````` use int.ComputerDivision `````` Jean-Christophe committed Mar 16, 2011 41 `````` `````` Guillaume Melquiond committed Mar 25, 2016 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 committed Mar 16, 2011 45 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 committed Mar 16, 2011 49 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 committed Mar 16, 2011 52 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 committed Mar 16, 2011 57 `````` `````` Andrei Paskevich committed Jun 29, 2011 58 `````` lemma divides_plusr: `````` Jean-Christophe Filliatre committed Aug 05, 2011 59 `````` forall a b c: int. divides a b -> divides a c -> divides a (b + c) `````` Andrei Paskevich committed Jun 29, 2011 60 `````` lemma divides_minusr: `````` Jean-Christophe Filliatre committed Aug 05, 2011 61 `````` forall a b c: int. divides a b -> divides a c -> divides a (b - c) `````` Andrei Paskevich committed Jun 29, 2011 62 `````` lemma divides_multl: `````` Jean-Christophe Filliatre committed Aug 05, 2011 63 `````` forall a b c: int. divides a b -> divides a (c * b) `````` Andrei Paskevich committed Jun 29, 2011 64 `````` lemma divides_multr: `````` Jean-Christophe Filliatre committed Aug 05, 2011 65 `````` forall a b c: int. divides a b -> divides a (b * c) `````` Jean-Christophe committed Mar 16, 2011 66 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 committed Mar 16, 2011 69 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 70 `````` lemma divides_n_1: forall n: int. divides n 1 -> n = 1 \/ n = -1 `````` Jean-Christophe committed Mar 16, 2011 71 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 72 73 `````` lemma divides_antisym: forall a b: int. divides a b -> divides b a -> a = b \/ a = -b `````` Jean-Christophe committed Mar 16, 2011 74 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 75 76 `````` lemma divides_trans: forall a b c: int. divides a b -> divides b c -> divides a c `````` Jean-Christophe committed Mar 16, 2011 77 `````` `````` Andrei Paskevich committed Jun 15, 2018 78 `````` use int.Abs `````` Jean-Christophe committed Mar 16, 2011 79 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 80 81 `````` lemma divides_bounds: forall a b: int. divides a b -> b <> 0 -> abs a <= abs b `````` Jean-Christophe committed Mar 16, 2011 82 `````` `````` Andrei Paskevich committed Jun 15, 2018 83 `````` use int.EuclideanDivision as ED `````` Jean-Christophe Filliatre committed Aug 17, 2011 84 85 `````` lemma mod_divides_euclidean: `````` Andrei Paskevich committed Jun 15, 2018 86 `````` forall a b: int. b <> 0 -> ED.mod a b = 0 -> divides b a `````` Jean-Christophe Filliatre committed Aug 17, 2011 87 `````` lemma divides_mod_euclidean: `````` Andrei Paskevich committed Jun 15, 2018 88 `````` forall a b: int. b <> 0 -> divides b a -> ED.mod a b = 0 `````` Jean-Christophe committed Mar 16, 2011 89 `````` `````` Andrei Paskevich committed Jun 15, 2018 90 `````` use int.ComputerDivision as CD `````` Jean-Christophe Filliatre committed Aug 17, 2011 91 92 `````` lemma mod_divides_computer: `````` Andrei Paskevich committed Jun 15, 2018 93 `````` forall a b: int. b <> 0 -> CD.mod a b = 0 -> divides b a `````` Jean-Christophe Filliatre committed Aug 17, 2011 94 `````` lemma divides_mod_computer: `````` Andrei Paskevich committed Jun 15, 2018 95 `````` forall a b: int. b <> 0 -> divides b a -> CD.mod a b = 0 `````` Jean-Christophe Filliatre committed Aug 17, 2011 96 `````` `````` Andrei Paskevich committed Jun 15, 2018 97 `````` use Parity `````` Jean-Christophe Filliatre committed Aug 17, 2011 98 99 100 `````` 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 committed Jun 29, 2011 101 `````` `````` Jean-Christophe committed Mar 16, 2011 102 103 ``````end `````` MARCHE Claude committed May 07, 2012 104 105 ``````(** {2 Greateast Common Divisor} *) `````` Andrei Paskevich committed Dec 22, 2017 106 ``````module Gcd `````` Jean-Christophe committed Mar 16, 2011 107 108 `````` use export int.Int `````` Andrei Paskevich committed Jun 15, 2018 109 `````` use Divisibility `````` Jean-Christophe committed Mar 16, 2011 110 `````` `````` Andrei Paskevich committed Jun 29, 2011 111 `````` function gcd int int : int `````` Jean-Christophe committed Mar 16, 2011 112 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 *) `````` Andrei Paskevich committed Jun 15, 2018 126 `````` clone algebra.AC with type t = int, function op = gcd `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 committed Mar 16, 2011 134 `````` `````` Andrei Paskevich committed Jun 15, 2018 135 `````` use int.ComputerDivision as CD `````` Jean-Christophe committed Mar 16, 2011 136 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 137 `````` lemma Gcd_computer_mod: `````` Andrei Paskevich committed Jun 15, 2018 138 139 `````` forall a b: int [gcd b (CD.mod a b)]. b <> 0 -> gcd b (CD.mod a b) = gcd a b `````` Jean-Christophe Filliatre committed Aug 05, 2011 140 `````` `````` Andrei Paskevich committed Jun 15, 2018 141 `````` use int.EuclideanDivision as ED `````` Jean-Christophe Filliatre committed Aug 05, 2011 142 143 `````` lemma Gcd_euclidean_mod: `````` Andrei Paskevich committed Jun 15, 2018 144 145 `````` forall a b: int [gcd b (ED.mod a b)]. b <> 0 -> gcd b (ED.mod a b) = gcd a b `````` Jean-Christophe Filliatre committed Aug 05, 2011 146 147 `````` lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b `````` Jean-Christophe committed Mar 16, 2011 148 149 150 `````` end `````` MARCHE Claude committed May 07, 2012 151 152 ``````(** {2 Prime numbers} *) `````` Andrei Paskevich committed Dec 22, 2017 153 ``````module Prime `````` Jean-Christophe committed Mar 16, 2011 154 155 `````` use export int.Int `````` Andrei Paskevich committed Jun 15, 2018 156 `````` use Divisibility `````` Jean-Christophe committed Mar 16, 2011 157 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 158 `````` predicate prime (p: int) = `````` Jean-Christophe Filliatre committed Aug 17, 2011 159 `````` 2 <= p /\ forall n: int. 1 < n < p -> not (divides n p) `````` Jean-Christophe Filliatre committed Aug 05, 2011 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 committed Mar 16, 2011 168 `````` `````` Jean-Christophe Filliatre committed Aug 18, 2011 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 `````` Andrei Paskevich committed Jun 15, 2018 174 `````` use Parity `````` Jean-Christophe Filliatre committed Aug 17, 2011 175 176 177 178 179 `````` lemma even_prime: forall p: int. prime p -> even p -> p = 2 lemma odd_prime: forall p: int. prime p -> p >= 3 -> odd p `````` Jean-Christophe Filliatre committed Aug 05, 2011 180 181 ``````end `````` MARCHE Claude committed May 07, 2012 182 183 ``````(** {2 Coprime numbers} *) `````` Andrei Paskevich committed Dec 22, 2017 184 ``````module Coprime `````` Jean-Christophe Filliatre committed Aug 05, 2011 185 186 `````` use export int.Int `````` Andrei Paskevich committed Jun 15, 2018 187 188 `````` use Divisibility use Gcd `````` Jean-Christophe committed Mar 16, 2011 189 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 190 `````` predicate coprime (a b: int) = gcd a b = 1 `````` Jean-Christophe committed Mar 16, 2011 191 `````` `````` Andrei Paskevich committed Jun 15, 2018 192 `````` use Prime `````` Jean-Christophe committed Mar 16, 2011 193 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 194 195 196 `````` lemma prime_coprime: forall p: int. prime p <-> 2 <= p && forall n:int. 1 <= n < p -> coprime n p `````` Jean-Christophe committed Mar 16, 2011 197 `````` `````` MARCHE Claude committed Feb 07, 2014 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 `````` MARCHE Claude committed Mar 19, 2014 205 206 `````` lemma gcd_coprime: forall a b c. coprime a b -> gcd a (b*c) = gcd a c `````` MARCHE Claude committed Feb 07, 2014 207 `````` `````` Jean-Christophe committed Mar 16, 2011 208 ``end``