number.why 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 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 7 8 9 10 11 12 13 ``````theory Parity 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 `````` 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 28 29 `````` lemma even_2k: forall k: int. even (2 * k) lemma odd_2k1: forall k: int. odd (2 * k + 1) end `````` MARCHE Claude committed May 07, 2012 30 31 ``````(** {2 Divisibility} *) `````` Jean-Christophe committed Mar 16, 2011 32 33 34 35 ``````theory Divisibility use export int.Int `````` Andrei Paskevich committed Jun 29, 2011 36 `````` predicate divides (d:int) (n:int) = exists q:int. n = q * d `````` Jean-Christophe committed Mar 16, 2011 37 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 38 39 40 `````` 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 41 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 42 43 `````` 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 44 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 45 46 47 48 `````` 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 49 `````` `````` Andrei Paskevich committed Jun 29, 2011 50 `````` lemma divides_plusr: `````` Jean-Christophe Filliatre committed Aug 05, 2011 51 `````` forall a b c: int. divides a b -> divides a c -> divides a (b + c) `````` Andrei Paskevich committed Jun 29, 2011 52 `````` lemma divides_minusr: `````` Jean-Christophe Filliatre committed Aug 05, 2011 53 `````` forall a b c: int. divides a b -> divides a c -> divides a (b - c) `````` Andrei Paskevich committed Jun 29, 2011 54 `````` lemma divides_multl: `````` Jean-Christophe Filliatre committed Aug 05, 2011 55 `````` forall a b c: int. divides a b -> divides a (c * b) `````` Andrei Paskevich committed Jun 29, 2011 56 `````` lemma divides_multr: `````` Jean-Christophe Filliatre committed Aug 05, 2011 57 `````` forall a b c: int. divides a b -> divides a (b * c) `````` Jean-Christophe committed Mar 16, 2011 58 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 59 60 `````` 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 61 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 62 `````` lemma divides_n_1: forall n: int. divides n 1 -> n = 1 \/ n = -1 `````` Jean-Christophe committed Mar 16, 2011 63 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 64 65 `````` lemma divides_antisym: forall a b: int. divides a b -> divides b a -> a = b \/ a = -b `````` Jean-Christophe committed Mar 16, 2011 66 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 67 68 `````` lemma divides_trans: forall a b c: int. divides a b -> divides b c -> divides a c `````` Jean-Christophe committed Mar 16, 2011 69 70 71 `````` use import int.Abs `````` Jean-Christophe Filliatre committed Aug 05, 2011 72 73 `````` lemma divides_bounds: forall a b: int. divides a b -> b <> 0 -> abs a <= abs b `````` Jean-Christophe committed Mar 16, 2011 74 `````` `````` Jean-Christophe Filliatre committed Aug 17, 2011 75 76 77 78 79 80 `````` 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 committed Mar 16, 2011 81 `````` `````` Jean-Christophe Filliatre committed Aug 17, 2011 82 83 84 85 86 87 88 89 90 91 92 `````` 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 committed Jun 29, 2011 93 `````` `````` Jean-Christophe committed Mar 16, 2011 94 95 ``````end `````` MARCHE Claude committed May 07, 2012 96 97 ``````(** {2 Greateast Common Divisor} *) `````` Jean-Christophe committed Mar 16, 2011 98 99 100 101 102 ``````theory Gcd use export int.Int use import Divisibility `````` Andrei Paskevich committed Jun 29, 2011 103 `````` function gcd int int : int `````` Jean-Christophe committed Mar 16, 2011 104 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 105 106 107 108 109 110 111 112 113 114 115 116 117 118 `````` 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, `````` 119 `````` lemma Comm.Comm, lemma Assoc `````` Jean-Christophe Filliatre committed Aug 05, 2011 120 121 122 123 124 125 126 `````` 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 127 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 128 `````` use int.ComputerDivision `````` Jean-Christophe committed Mar 16, 2011 129 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 130 `````` lemma Gcd_computer_mod: `````` Guillaume Melquiond committed Apr 21, 2012 131 132 `````` forall a b: int [gcd b (ComputerDivision.mod a b)]. b <> 0 -> gcd b (ComputerDivision.mod a b) = gcd a b `````` Jean-Christophe Filliatre committed Aug 05, 2011 133 134 135 136 `````` use int.EuclideanDivision lemma Gcd_euclidean_mod: `````` MARCHE Claude committed Sep 03, 2012 137 `````` forall a b: int [gcd b (EuclideanDivision.mod a b)]. `````` Guillaume Melquiond committed Apr 21, 2012 138 `````` b <> 0 -> gcd b (EuclideanDivision.mod a b) = gcd a b `````` Jean-Christophe Filliatre committed Aug 05, 2011 139 140 `````` 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 141 142 143 `````` end `````` MARCHE Claude committed May 07, 2012 144 145 ``````(** {2 Prime numbers} *) `````` Jean-Christophe committed Mar 16, 2011 146 147 148 149 150 ``````theory Prime use export int.Int use import Divisibility `````` Jean-Christophe Filliatre committed Aug 05, 2011 151 `````` predicate prime (p: int) = `````` Jean-Christophe Filliatre committed Aug 17, 2011 152 `````` 2 <= p /\ forall n: int. 1 < n < p -> not (divides n p) `````` Jean-Christophe Filliatre committed Aug 05, 2011 153 154 155 156 157 158 159 160 `````` 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 161 `````` `````` Jean-Christophe Filliatre committed Aug 18, 2011 162 163 164 165 166 `````` 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 `````` Jean-Christophe Filliatre committed Aug 17, 2011 167 168 169 170 171 172 `````` 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 `````` Jean-Christophe Filliatre committed Aug 05, 2011 173 174 ``````end `````` MARCHE Claude committed May 07, 2012 175 176 ``````(** {2 Coprime numbers} *) `````` Jean-Christophe Filliatre committed Aug 05, 2011 177 178 179 180 181 ``````theory Coprime use export int.Int use import Divisibility use import Gcd `````` Jean-Christophe committed Mar 16, 2011 182 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 183 `````` predicate coprime (a b: int) = gcd a b = 1 `````` Jean-Christophe committed Mar 16, 2011 184 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 185 `````` use import Prime `````` Jean-Christophe committed Mar 16, 2011 186 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 187 188 189 `````` 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 190 `````` `````` MARCHE Claude committed Feb 07, 2014 191 192 193 194 195 196 197 `````` 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 198 199 `````` lemma gcd_coprime: forall a b c. coprime a b -> gcd a (b*c) = gcd a c `````` MARCHE Claude committed Feb 07, 2014 200 `````` `````` Jean-Christophe committed Mar 16, 2011 201 ``end``