int.mlw 13 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` MARCHE Claude committed Apr 20, 2012 2 ``````(** {1 Theory of integers} `````` MARCHE Claude committed Apr 19, 2012 3 `````` `````` MARCHE Claude committed Apr 20, 2012 4 ``````This file provides the basic theory of integers, and several additional `````` 5 ``````theories for classical functions. `````` MARCHE Claude committed Apr 19, 2012 6 7 8 9 10 `````` *) (** {2 Integers and the basic operators} *) `````` Andrei Paskevich committed Dec 22, 2017 11 ``````module Int `````` Jean-Christophe Filliâtre committed Mar 23, 2010 12 `````` `````` Mário Pereira committed Feb 23, 2017 13 14 `````` let constant zero : int = 0 let constant one : int = 1 `````` MARCHE Claude committed Oct 19, 2010 15 `````` `````` Andrei Paskevich committed Aug 20, 2015 16 `````` val (=) (x y : int) : bool ensures { result <-> x = y } `````` Andrei Paskevich committed Apr 02, 2010 17 `````` `````` Andrei Paskevich committed Aug 20, 2015 18 19 20 21 22 23 24 25 26 27 28 29 30 `````` val function (-_) int : int val function (+) int int : int val function (*) int int : int val predicate (<) int int : bool let function (-) (x y : int) = x + -y let predicate (>) (x y : int) = y < x let predicate (<=) (x y : int) = x < y || x = y let predicate (>=) (x y : int) = y <= x clone export algebra.OrderedUnitaryCommutativeRing with type t = int, constant zero = zero, constant one = one, function (-_) = (-_), function (+) = (+), `````` Andrei Paskevich committed Jun 14, 2018 31 `````` function (*) = (*), predicate (<=) = (<=) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 32 `````` `````` Jean-Christophe Filliâtre committed May 26, 2010 33 ``````end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 34 `````` `````` MARCHE Claude committed Apr 19, 2012 35 36 ``````(** {2 Absolute Value} *) `````` Andrei Paskevich committed Dec 22, 2017 37 ``````module Abs `````` Jean-Christophe Filliâtre committed Mar 23, 2010 38 `````` `````` Andrei Paskevich committed Jun 15, 2018 39 `````` use Int `````` Jean-Christophe Filliâtre committed Mar 23, 2010 40 `````` `````` Andrei Paskevich committed Aug 20, 2015 41 `````` let function abs (x:int) : int = if x >= 0 then x else -x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 42 `````` `````` MARCHE Claude committed Sep 04, 2011 43 44 `````` lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y `````` Andrei Paskevich committed Jun 21, 2010 45 `````` lemma Abs_pos: forall x:int. abs x >= 0 `````` MARCHE Claude committed Mar 26, 2010 46 `````` `````` MARCHE Claude committed Apr 19, 2012 47 ``````(*** `````` MARCHE Claude committed Sep 04, 2011 48 `````` lemma Abs_zero: forall x:int. abs x = 0 -> x = 0 `````` MARCHE Claude committed Sep 05, 2011 49 ``````*) `````` MARCHE Claude committed Sep 04, 2011 50 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 51 52 ``````end `````` MARCHE Claude committed Apr 19, 2012 53 54 ``````(** {2 Minimum and Maximum} *) `````` Andrei Paskevich committed Dec 22, 2017 55 ``````module MinMax `````` Jean-Christophe Filliâtre committed Mar 23, 2010 56 `````` `````` Andrei Paskevich committed Jun 15, 2018 57 `````` use Int `````` MARCHE Claude committed Mar 09, 2016 58 `````` `````` Andrei Paskevich committed Jun 15, 2018 59 `````` clone export relations.MinMax with type t = int, predicate le = (<=), goal . `````` Jean-Christophe Filliâtre committed Mar 23, 2010 60 `````` `````` MARCHE Claude committed Mar 09, 2016 61 62 63 64 65 66 67 68 69 `````` let min (x y : int) : int ensures { result = min x y } = if x <= y then x else y let max (x y : int) : int ensures { result = max x y } = if x <= y then y else x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 70 71 ``````end `````` MARCHE Claude committed Apr 19, 2012 72 73 ``````(** {2 The Basic Well-Founded Order on Integers} *) `````` Andrei Paskevich committed Dec 22, 2017 74 ``````module Lex2 `````` Jean-Christophe Filliatre committed Aug 01, 2011 75 `````` `````` Andrei Paskevich committed Jun 15, 2018 76 `````` use Int `````` Jean-Christophe Filliatre committed Aug 01, 2011 77 78 79 80 81 82 83 84 `````` predicate lt_nat (x y: int) = 0 <= y /\ x < y clone export relations.Lex with type t1 = int, type t2 = int, predicate rel1 = lt_nat, predicate rel2 = lt_nat end `````` MARCHE Claude committed Apr 19, 2012 85 86 ``````(** {2 Euclidean Division} `````` Jean-Christophe Filliatre committed Nov 23, 2014 87 ``````Division and modulo operators with the convention `````` MARCHE Claude committed Feb 17, 2013 88 89 90 91 ``````that modulo is always non-negative. It implies that division rounds down when divisor is positive, and rounds up when divisor is negative. `````` MARCHE Claude committed Apr 19, 2012 92 93 94 `````` *) `````` Andrei Paskevich committed Dec 22, 2017 95 ``````module EuclideanDivision `````` MARCHE Claude committed Mar 26, 2010 96 `````` `````` Andrei Paskevich committed Jun 15, 2018 97 98 `````` use Int use Abs `````` MARCHE Claude committed Mar 26, 2010 99 `````` `````` MARCHE Claude committed Mar 07, 2016 100 101 `````` function div (x y: int) : int function mod (x y: int) : int `````` MARCHE Claude committed Mar 26, 2010 102 `````` `````` MARCHE Claude committed Oct 19, 2010 103 `````` axiom Div_mod: `````` Andrei Paskevich committed Jun 21, 2010 104 `````` forall x y:int. y <> 0 -> x = y * div x y + mod x y `````` MARCHE Claude committed Mar 26, 2010 105 `````` `````` MARCHE Claude committed Oct 19, 2010 106 `````` axiom Mod_bound: `````` Andrei Paskevich committed Jun 21, 2010 107 `````` forall x y:int. y <> 0 -> 0 <= mod x y < abs y `````` MARCHE Claude committed Mar 26, 2010 108 `````` `````` MARCHE Claude committed Nov 19, 2014 109 110 111 112 113 114 `````` lemma Div_unique: forall x y q:int. y > 0 -> q * y <= x < q * y + y -> div x y = q lemma Div_bound: forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x `````` Andrei Paskevich committed Jun 21, 2010 115 `````` lemma Mod_1: forall x:int. mod x 1 = 0 `````` MARCHE Claude committed Mar 26, 2010 116 `````` `````` Andrei Paskevich committed Jun 21, 2010 117 `````` lemma Div_1: forall x:int. div x 1 = x `````` MARCHE Claude committed Mar 26, 2010 118 `````` `````` MARCHE Claude committed Jan 17, 2012 119 120 `````` lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0 `````` MARCHE Claude committed May 24, 2012 121 122 `````` lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1 `````` MARCHE Claude committed Jan 17, 2012 123 124 `````` lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0 `````` MARCHE Claude committed May 24, 2012 125 126 127 128 129 130 131 132 `````` lemma Div_1_left: forall y:int. y > 1 -> div 1 y = 0 lemma Div_minus1_left: forall y:int. y > 1 -> div (-1) y = -1 lemma Mod_1_left: forall y:int. y > 1 -> mod 1 y = 1 lemma Mod_minus1_left: forall y:int. y > 1 -> mod (-1) y = y - 1 `````` MARCHE Claude committed Feb 17, 2013 133 134 135 136 137 138 139 `````` lemma Div_mult: forall x y z:int [div (x * y + z) x]. x > 0 -> div (x * y + z) x = y + div z x lemma Mod_mult: forall x y z:int [mod (x * y + z) x]. x > 0 -> mod (x * y + z) x = mod z x `````` MARCHE Claude committed May 24, 2012 140 `````` `````` MARCHE Claude committed Mar 11, 2016 141 142 143 144 145 146 147 148 149 `````` val div (x y:int) : int requires { y <> 0 } ensures { result = div x y } val mod (x y:int) : int requires { y <> 0 } ensures { result = mod x y } `````` Jean-Christophe Filliâtre committed Mar 23, 2010 150 151 ``````end `````` MARCHE Claude committed Apr 19, 2012 152 153 ``````(** {2 Division by 2} `````` MARCHE Claude committed Apr 20, 2012 154 ``````The particular case of Euclidean division by 2 `````` MARCHE Claude committed Apr 19, 2012 155 156 `````` *) `````` 157 `````` `````` Andrei Paskevich committed Dec 22, 2017 158 ``````module Div2 `````` 159 `````` `````` Andrei Paskevich committed Jun 15, 2018 160 `````` use Int `````` 161 162 163 164 165 166 `````` lemma div2: forall x: int. exists y: int. x = 2*y \/ x = 2*y+1 end `````` MARCHE Claude committed Apr 19, 2012 167 ``````(** {2 Computer Division} `````` MARCHE Claude committed Mar 26, 2010 168 `````` `````` MARCHE Claude committed Apr 20, 2012 169 ``````Division and modulo operators with the same conventions as mainstream `````` 170 ``````programming language such as C, Java, OCaml, that is, division rounds `````` Jean-Christophe Filliatre committed Jun 14, 2018 171 ``````towards zero, and thus `mod x y` has the same sign as `x`. `````` MARCHE Claude committed Apr 19, 2012 172 173 174 `````` *) `````` Andrei Paskevich committed Dec 22, 2017 175 ``````module ComputerDivision `````` MARCHE Claude committed Apr 19, 2012 176 `````` `````` Andrei Paskevich committed Jun 15, 2018 177 178 `````` use Int use Abs `````` MARCHE Claude committed Mar 26, 2010 179 `````` `````` MARCHE Claude committed Mar 07, 2016 180 181 `````` function div (x y: int) : int function mod (x y: int) : int `````` MARCHE Claude committed Mar 26, 2010 182 `````` `````` MARCHE Claude committed Oct 19, 2010 183 `````` axiom Div_mod: `````` Andrei Paskevich committed Jun 21, 2010 184 `````` forall x y:int. y <> 0 -> x = y * div x y + mod x y `````` MARCHE Claude committed Mar 26, 2010 185 `````` `````` MARCHE Claude committed Oct 19, 2010 186 `````` axiom Div_bound: `````` Jean-Christophe Filliatre committed Apr 18, 2011 187 `````` forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x `````` MARCHE Claude committed Oct 19, 2010 188 189 `````` axiom Mod_bound: `````` MARCHE Claude committed Jul 05, 2010 190 191 `````` forall x y:int. y <> 0 -> - abs y < mod x y < abs y `````` MARCHE Claude committed Oct 07, 2010 192 `````` axiom Div_sign_pos: `````` Jean-Christophe Filliatre committed Apr 18, 2011 193 `````` forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0 `````` MARCHE Claude committed Oct 07, 2010 194 195 `````` axiom Div_sign_neg: `````` Jean-Christophe Filliatre committed Apr 18, 2011 196 `````` forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0 `````` MARCHE Claude committed Oct 07, 2010 197 `````` `````` MARCHE Claude committed Jul 05, 2010 198 `````` axiom Mod_sign_pos: `````` Jean-Christophe Filliatre committed Apr 18, 2011 199 `````` forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0 `````` MARCHE Claude committed Jul 05, 2010 200 201 `````` axiom Mod_sign_neg: `````` Jean-Christophe Filliatre committed Apr 18, 2011 202 `````` forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0 `````` MARCHE Claude committed Jul 05, 2010 203 204 205 `````` lemma Rounds_toward_zero: forall x y:int. y <> 0 -> abs (div x y * y) <= abs x `````` MARCHE Claude committed Mar 26, 2010 206 `````` `````` MARCHE Claude committed Mar 16, 2011 207 208 `````` lemma Div_1: forall x:int. div x 1 = x `````` Andrei Paskevich committed Jun 21, 2010 209 `````` lemma Mod_1: forall x:int. mod x 1 = 0 `````` MARCHE Claude committed Mar 26, 2010 210 `````` `````` MARCHE Claude committed Mar 16, 2011 211 212 213 214 `````` lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0 lemma Mod_inf: forall x y:int. 0 <= x < y -> mod x y = x `````` Jean-Christophe Filliatre committed Jun 21, 2011 215 `````` lemma Div_mult: forall x y z:int [div (x * y + z) x]. `````` Jean-Christophe Filliatre committed Apr 18, 2011 216 `````` x > 0 /\ y >= 0 /\ z >= 0 -> `````` MARCHE Claude committed Mar 16, 2011 217 218 `````` div (x * y + z) x = y + div z x `````` Jean-Christophe Filliatre committed Jun 21, 2011 219 `````` lemma Mod_mult: forall x y z:int [mod (x * y + z) x]. `````` Jean-Christophe Filliatre committed Apr 18, 2011 220 `````` x > 0 /\ y >= 0 /\ z >= 0 -> `````` MARCHE Claude committed Mar 16, 2011 221 `````` mod (x * y + z) x = mod z x `````` MARCHE Claude committed Mar 26, 2010 222 `````` `````` MARCHE Claude committed Mar 07, 2016 223 224 225 226 227 228 229 230 `````` val div (x y:int) : int requires { y <> 0 } ensures { result = div x y } val mod (x y:int) : int requires { y <> 0 } ensures { result = mod x y } `````` Jean-Christophe Filliâtre committed Mar 23, 2010 231 232 ``````end `````` 233 ``````(** {2 Generic Exponentiation of something to an integer exponent} *) `````` MARCHE Claude committed Apr 20, 2012 234 `````` `````` Andrei Paskevich committed Dec 22, 2017 235 ``````module Exponentiation `````` 236 `````` `````` Andrei Paskevich committed Jun 15, 2018 237 `````` use Int `````` Jean-Christophe Filliâtre committed Jun 25, 2010 238 `````` `````` Jean-Christophe Filliatre committed Apr 08, 2011 239 `````` type t `````` Jean-Christophe Filliatre committed Feb 06, 2012 240 `````` constant one : t `````` Andrei Paskevich committed Jun 29, 2011 241 `````` function (*) t t : t `````` Andrei Paskevich committed Aug 20, 2015 242 `````` `````` MARCHE Claude committed May 22, 2017 243 `````` clone export algebra.Monoid `````` Andrei Paskevich committed Jun 14, 2018 244 `````` with type t = t, constant unit = one, function op = (*), axiom . `````` Jean-Christophe Filliatre committed Jun 21, 2011 245 `````` `````` Andrei Paskevich committed Aug 20, 2015 246 `````` (* TODO: implement with let rec once let cloning is done *) `````` Andrei Paskevich committed Jun 29, 2011 247 `````` function power t int : t `````` Jean-Christophe Filliatre committed Apr 08, 2011 248 249 250 251 `````` axiom Power_0 : forall x: t. power x 0 = one axiom Power_s : forall x: t, n: int. n >= 0 -> power x (n+1) = x * power x n `````` Andrei Paskevich committed Oct 26, 2010 252 `````` `````` Jean-Christophe committed Sep 07, 2012 253 254 `````` lemma Power_s_alt: forall x: t, n: int. n > 0 -> power x n = x * power x (n-1) `````` MARCHE Claude committed Sep 23, 2011 255 256 `````` lemma Power_1 : forall x : t. power x 1 = x `````` Guillaume Melquiond committed Sep 01, 2012 257 `````` lemma Power_sum : forall x: t, n m: int. 0 <= n -> 0 <= m -> `````` MARCHE Claude committed Sep 23, 2011 258 259 260 `````` power x (n+m) = power x n * power x m lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m -> `````` Andrei Paskevich committed Aug 20, 2015 261 `````` power x (Int.(*) n m) = power (power x n) m `````` MARCHE Claude committed Sep 23, 2011 262 `````` `````` MARCHE Claude committed Jun 02, 2017 263 264 265 266 267 268 `````` lemma Power_comm1 : forall x y: t. x * y = y * x -> forall n:int. 0 <= n -> power x n * y = y * power x n lemma Power_comm2 : forall x y: t. x * y = y * x -> forall n:int. 0 <= n -> `````` Jean-Christophe committed Jul 26, 2012 269 270 `````` power (x * y) n = power x n * power y n `````` MARCHE Claude committed Jan 06, 2015 271 272 ``````(* TODO `````` Andrei Paskevich committed Jun 15, 2018 273 `````` use ComputerDivision `````` MARCHE Claude committed Jan 06, 2015 274 275 276 277 278 279 280 281 `````` lemma Power_even : forall x:t, n:int. n >= 0 -> mod n 2 = 0 -> power x n = power (x*x) (div n 2) lemma power_odd : forall x:t, n:int. n >= 0 -> mod n 2 <> 0 -> power x n = x * power (x*x) (div n 2) *) `````` Jean-Christophe Filliatre committed Apr 08, 2011 282 283 ``````end `````` MARCHE Claude committed Apr 19, 2012 284 ``````(** {2 Power of an integer to an integer } *) `````` 285 `````` `````` Andrei Paskevich committed Dec 22, 2017 286 ``````module Power `````` Jean-Christophe Filliatre committed Jan 24, 2011 287 `````` `````` Andrei Paskevich committed Jun 15, 2018 288 `````` use Int `````` Jean-Christophe Filliatre committed Apr 08, 2011 289 `````` `````` Andrei Paskevich committed Aug 20, 2015 290 291 292 293 294 295 `````` (* TODO: remove once power is implemented in Exponentiation *) val function power int int : int clone export Exponentiation with type t = int, constant one = one, function (*) = (*), function power = power, `````` Andrei Paskevich committed Jun 14, 2018 296 297 `````` goal Assoc, goal Unit_def_l, goal Unit_def_r, axiom Power_0, axiom Power_s `````` Jean-Christophe Filliatre committed Jan 24, 2011 298 `````` `````` MARCHE Claude committed May 11, 2014 299 300 301 `````` lemma Power_non_neg: forall x y. x >= 0 /\ y >= 0 -> power x y >= 0 `````` DAILLER Sylvain committed Dec 03, 2018 302 303 304 `````` lemma Power_pos: forall x y. x > 0 /\ y >= 0 -> power x y > 0 `````` MARCHE Claude committed May 05, 2014 305 306 307 `````` lemma Power_monotonic: forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m `````` Jean-Christophe Filliâtre committed Jun 25, 2010 308 309 ``````end `````` Jean-Christophe Filliatre committed Nov 23, 2014 310 ``````(** {2 Number of integers satisfying a given predicate} *) `````` MARCHE Claude committed Apr 19, 2012 311 `````` `````` Andrei Paskevich committed Dec 22, 2017 312 ``````module NumOf `````` Jean-Christophe Filliâtre committed Jun 25, 2010 313 `````` `````` Andrei Paskevich committed Jun 15, 2018 314 `````` use Int `````` Jean-Christophe Filliâtre committed Jun 25, 2010 315 `````` `````` Jean-Christophe Filliatre committed Jun 14, 2018 316 `````` (** number of `n` such that `a <= n < b` and `p n` *) `````` Andrei Paskevich committed Aug 20, 2015 317 318 319 `````` let rec function numof (p: int -> bool) (a b: int) : int variant { b - a } = if b <= a then 0 else `````` Jean-Christophe Filliatre committed Feb 22, 2016 320 321 `````` if p (b - 1) then 1 + numof p a (b - 1) else numof p a (b - 1) `````` 322 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 323 `````` lemma Numof_bounds : `````` Jean-Christophe Filliatre committed Nov 24, 2014 324 `````` forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a `````` MARCHE Claude committed Apr 06, 2011 325 326 `````` (* direct when a>=b, by induction on b when a <= b *) `````` Jean-Christophe Filliatre committed Nov 23, 2014 327 `````` lemma Numof_append : `````` Jean-Christophe Filliatre committed Nov 24, 2014 328 `````` forall p : int -> bool, a b c : int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 329 `````` a <= b <= c -> numof p a c = numof p a b + numof p b c `````` MARCHE Claude committed Apr 06, 2011 330 `````` (* by induction on c *) `````` Jean-Christophe Filliâtre committed Jun 25, 2010 331 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 332 `````` lemma Numof_left_no_add : `````` Jean-Christophe Filliatre committed Nov 24, 2014 333 `````` forall p : int -> bool, a b : int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 334 335 336 `````` a < b -> not p a -> numof p a b = numof p (a+1) b (* by Numof_append *) lemma Numof_left_add : `````` Jean-Christophe Filliatre committed Nov 24, 2014 337 `````` forall p : int -> bool, a b : int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 338 339 `````` a < b -> p a -> numof p a b = 1 + numof p (a+1) b (* by Numof_append *) `````` MARCHE Claude committed Apr 06, 2011 340 341 `````` lemma Empty : `````` Jean-Christophe Filliatre committed Nov 24, 2014 342 `````` forall p : int -> bool, a b : int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 343 `````` (forall n : int. a <= n < b -> not p n) -> numof p a b = 0 `````` MARCHE Claude committed Apr 06, 2011 344 345 `````` (* by induction on b *) `````` Jean-Christophe Filliatre committed Sep 18, 2011 346 `````` lemma Full : `````` Jean-Christophe Filliatre committed Nov 24, 2014 347 `````` forall p : int -> bool, a b : int. a <= b -> `````` Jean-Christophe Filliatre committed Nov 23, 2014 348 `````` (forall n : int. a <= n < b -> p n) -> numof p a b = b - a `````` Jean-Christophe Filliatre committed Sep 18, 2011 349 350 `````` (* by induction on b *) `````` Jean-Christophe Filliatre committed Nov 23, 2014 351 `````` lemma numof_increasing: `````` Jean-Christophe Filliatre committed Nov 24, 2014 352 `````` forall p : int -> bool, i j k : int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 353 354 `````` i <= j <= k -> numof p i j <= numof p i k (* by Numof_append and Numof_non_negative *) `````` Jean-Christophe Filliâtre committed Jul 04, 2010 355 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 356 `````` lemma numof_strictly_increasing: `````` Jean-Christophe Filliatre committed Nov 24, 2014 357 `````` forall p: int -> bool, i j k l: int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 358 359 `````` i <= j <= k < l -> p k -> numof p i j < numof p i l (* by Numof_append and numof_increasing *) `````` Jean-Christophe committed Apr 04, 2011 360 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 361 `````` lemma numof_change_any: `````` Jean-Christophe Filliatre committed Nov 24, 2014 362 `````` forall p1 p2: int -> bool, a b: int. `````` Jean-Christophe Filliatre committed Nov 23, 2014 363 364 `````` (forall j: int. a <= j < b -> p1 j -> p2 j) -> numof p2 a b >= numof p1 a b `````` Jean-Christophe Filliatre committed Sep 08, 2011 365 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 366 `````` lemma numof_change_some: `````` Jean-Christophe Filliatre committed Nov 24, 2014 367 `````` forall p1 p2: int -> bool, a b i: int. a <= i < b -> `````` Jean-Christophe Filliatre committed Nov 23, 2014 368 369 370 `````` (forall j: int. a <= j < b -> p1 j -> p2 j) -> not (p1 i) -> p2 i -> numof p2 a b > numof p1 a b `````` Jean-Christophe Filliâtre committed Jun 25, 2010 371 `````` `````` Clément Fumex committed Jun 02, 2015 372 373 374 375 376 `````` lemma numof_change_equiv: forall p1 p2: int -> bool, a b: int. (forall j: int. a <= j < b -> p1 j <-> p2 j) -> numof p2 a b = numof p1 a b `````` Jean-Christophe Filliâtre committed Jun 25, 2010 377 ``````end `````` Jean-Christophe Filliâtre committed Aug 18, 2010 378 `````` `````` Jean-Christophe Filliatre committed May 27, 2015 379 380 ``````(** {2 Sum} *) `````` Andrei Paskevich committed Dec 22, 2017 381 ``````module Sum `````` Jean-Christophe Filliatre committed May 27, 2015 382 `````` `````` Andrei Paskevich committed Jun 15, 2018 383 `````` use Int `````` Jean-Christophe Filliatre committed May 27, 2015 384 `````` `````` Jean-Christophe Filliatre committed Jun 14, 2018 385 `````` (** sum of `f n` for `a <= n < b` *) `````` Andrei Paskevich committed Aug 20, 2015 386 387 388 `````` let rec function sum (f: int -> int) (a b: int) : int variant { b - a } = if b <= a then 0 else sum f a (b - 1) + f (b - 1) `````` Jean-Christophe Filliatre committed May 27, 2015 389 390 391 `````` lemma sum_left: forall f: int -> int, a b: int. `````` Andrei Paskevich committed Aug 20, 2015 392 `````` a < b -> sum f a b = f a + sum f (a + 1) b `````` Jean-Christophe Filliatre committed May 27, 2015 393 394 395 `````` lemma sum_ext: forall f g: int -> int, a b: int. `````` Andrei Paskevich committed Aug 20, 2015 396 397 `````` (forall i. a <= i < b -> f i = g i) -> sum f a b = sum g a b `````` Jean-Christophe Filliatre committed May 27, 2015 398 `````` `````` Jean-Christophe Filliatre committed Jun 07, 2015 399 400 `````` lemma sum_le: forall f g: int -> int, a b: int. `````` Andrei Paskevich committed Aug 20, 2015 401 402 403 404 405 406 407 `````` (forall i. a <= i < b -> f i <= g i) -> sum f a b <= sum g a b lemma sum_zero: forall f: int -> int, a b: int. (forall i. a <= i < b -> f i = 0) -> sum f a b = 0 `````` Jean-Christophe Filliatre committed Jun 07, 2015 408 `````` `````` Jean-Christophe Filliatre committed May 27, 2015 409 410 `````` lemma sum_nonneg: forall f: int -> int, a b: int. `````` Andrei Paskevich committed Aug 20, 2015 411 412 `````` (forall i. a <= i < b -> 0 <= f i) -> 0 <= sum f a b `````` Jean-Christophe Filliatre committed May 27, 2015 413 414 415 `````` lemma sum_decomp: forall f: int -> int, a b c: int. a <= b <= c -> `````` Andrei Paskevich committed Aug 20, 2015 416 `````` sum f a c = sum f a b + sum f b c `````` Jean-Christophe Filliatre committed May 27, 2015 417 `````` `````` Mário Pereira committed Jul 19, 2017 418 419 420 421 422 423 424 `````` let rec lemma shift_left (f g: int -> int) (a b c d: int) requires { b - a = d - c } requires { forall i. a <= i < b -> f i = g (c + i - a) } variant { b - a } ensures { sum f a b = sum g c d } = if a < b then shift_left f g (a+1) b (c+1) d `````` Jean-Christophe Filliatre committed May 27, 2015 425 426 ``````end `````` MARCHE Claude committed Apr 19, 2012 427 428 ``````(** {2 Factorial function} *) `````` Andrei Paskevich committed Dec 22, 2017 429 ``````module Fact `````` Jean-Christophe Filliatre committed Aug 03, 2011 430 `````` `````` Andrei Paskevich committed Jun 15, 2018 431 `````` use Int `````` Jean-Christophe Filliatre committed Aug 03, 2011 432 `````` `````` Jean-Christophe Filliatre committed Aug 20, 2015 433 `````` let rec function fact (n: int) : int `````` MARCHE Claude committed Jun 22, 2014 434 435 436 437 `````` requires { n >= 0 } variant { n } = if n = 0 then 1 else n * fact (n-1) `````` Jean-Christophe Filliatre committed Aug 03, 2011 438 439 ``````end `````` MARCHE Claude committed Apr 19, 2012 440 441 ``````(** {2 Generic iteration of a function} *) `````` Andrei Paskevich committed Dec 22, 2017 442 ``````module Iter `````` Jean-Christophe Filliatre committed Aug 05, 2011 443 `````` `````` Andrei Paskevich committed Jun 15, 2018 444 `````` use Int `````` Jean-Christophe Filliatre committed Aug 05, 2011 445 `````` `````` Jean-Christophe Filliatre committed Jun 14, 2018 446 `````` (** `iter k x` is `f^k(x)` *) `````` Jean-Christophe Filliatre committed Aug 20, 2015 447 448 449 450 `````` let rec function iter (f: 'a -> 'a) (k: int) (x: 'a) : 'a requires { k >= 0 } variant { k } = if k = 0 then x else iter f (k - 1) (f x) `````` Jean-Christophe Filliatre committed Aug 05, 2011 451 `````` `````` Jean-Christophe Filliatre committed Aug 20, 2015 452 `````` lemma iter_1: forall f, x: 'a. iter f 1 x = f x `````` Jean-Christophe Filliatre committed Aug 05, 2011 453 `````` `````` Jean-Christophe Filliatre committed Aug 20, 2015 454 `````` lemma iter_s: forall f, k, x: 'a. 0 < k -> iter f k x = f (iter f (k - 1) x) `````` Jean-Christophe Filliatre committed Aug 05, 2011 455 456 457 `````` end `````` MARCHE Claude committed Apr 19, 2012 458 ``````(** {2 Integers extended with an infinite value} *) `````` MARCHE Claude committed Apr 20, 2012 459 `````` `````` Andrei Paskevich committed Dec 22, 2017 460 ``````module IntInf `````` Jean-Christophe Filliatre committed Apr 04, 2012 461 `````` `````` Andrei Paskevich committed Jun 15, 2018 462 `````` use Int `````` Jean-Christophe Filliatre committed Apr 04, 2012 463 464 465 `````` type t = Finite int | Infinite `````` Andrei Paskevich committed Aug 20, 2015 466 `````` let function add (x: t) (y: t) : t = `````` Jean-Christophe Filliatre committed Apr 04, 2012 467 468 469 470 471 472 473 474 475 `````` match x with | Infinite -> Infinite | Finite x -> match y with | Infinite -> Infinite | Finite y -> Finite (x + y) end end `````` Andrei Paskevich committed Aug 20, 2015 476 477 478 479 480 481 482 483 `````` let predicate eq (x y: t) = match x, y with | Infinite, Infinite -> true | Finite x, Finite y -> x = y | _, _ -> false end let predicate lt (x y: t) = `````` Jean-Christophe Filliatre committed Apr 04, 2012 484 485 486 487 488 489 490 491 492 `````` match x with | Infinite -> false | Finite x -> match y with | Infinite -> true | Finite y -> x < y end end `````` Andrei Paskevich committed Aug 20, 2015 493 `````` let predicate le (x y: t) = lt x y || eq x y `````` Jean-Christophe Filliatre committed Apr 04, 2012 494 495 496 497 498 499 `````` clone export relations.TotalOrder with type t = t, predicate rel = le, lemma Refl, lemma Antisymm, lemma Trans, lemma Total end `````` MARCHE Claude committed Apr 19, 2012 500 501 ``````(** {2 Induction principle on integers} `````` MARCHE Claude committed Apr 20, 2012 502 ``````This theory can be cloned with the wanted predicate, to perform an `````` 503 ``````induction, either on nonnegative integers, or more generally on `````` MARCHE Claude committed Apr 20, 2012 504 ``````integers greater or equal a given bound. `````` MARCHE Claude committed Apr 19, 2012 505 `````` `````` 506 ``````*) `````` Jean-Christophe Filliatre committed Apr 04, 2012 507 `````` `````` Andrei Paskevich committed Dec 22, 2017 508 ``````module SimpleInduction `````` Jean-Christophe Filliatre committed Mar 02, 2013 509 `````` `````` Andrei Paskevich committed Jun 15, 2018 510 `````` use Int `````` Jean-Christophe Filliatre committed Mar 02, 2013 511 512 513 514 515 516 517 518 519 520 521 `````` predicate p int axiom base: p 0 axiom induction_step: forall n:int. 0 <= n -> p n -> p (n+1) lemma SimpleInduction : forall n:int. 0 <= n -> p n end `````` Andrei Paskevich committed Dec 22, 2017 522 ``````module Induction `````` Jean-Christophe Filliatre committed Aug 05, 2011 523 `````` `````` Andrei Paskevich committed Jun 15, 2018 524 `````` use Int `````` Jean-Christophe Filliatre committed Apr 08, 2011 525 `````` `````` Andrei Paskevich committed Jun 29, 2011 526 `````` predicate p int `````` Jean-Christophe Filliatre committed Apr 08, 2011 527 `````` `````` MARCHE Claude committed Apr 10, 2011 528 `````` lemma Induction : `````` Jean-Christophe Filliatre committed Apr 08, 2011 529 530 531 `````` (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) -> forall n:int. 0 <= n -> p n `````` Jean-Christophe Filliatre committed Feb 06, 2012 532 `````` constant bound : int `````` MARCHE Claude committed Apr 10, 2011 533 534 `````` lemma Induction_bound : `````` Jean-Christophe Filliatre committed Jun 21, 2011 535 `````` (forall n:int. bound <= n -> `````` MARCHE Claude committed Apr 10, 2011 536 537 538 `````` (forall k:int. bound <= k < n -> p k) -> p n) -> forall n:int. bound <= n -> p n `````` Jean-Christophe Filliatre committed Apr 08, 2011 539 ``````end `````` Jean-Christophe Filliatre committed Feb 18, 2014 540 `````` `````` Jean-Christophe Filliatre committed Apr 30, 2018 541 542 ``````module HOInduction `````` Andrei Paskevich committed Jun 15, 2018 543 `````` use Int `````` Jean-Christophe Filliatre committed Apr 30, 2018 544 545 546 547 548 549 550 551 552 553 `````` let lemma induction (p: int -> bool) requires { p 0 } requires { forall n. 0 <= n >= 0 -> p n -> p (n+1) } ensures { forall n. 0 <= n -> p n } = let rec lemma f (n: int) requires { n >= 0 } ensures { p n } variant {n} = if n > 0 then f (n-1) in f 0 end `````` Guillaume Melquiond committed Jan 12, 2018 554 555 556 ``````(** {2 Fibonacci numbers} *) module Fibonacci `````` Jean-Christophe Filliatre committed Feb 18, 2014 557 `````` `````` Andrei Paskevich committed Jun 15, 2018 558 `````` use Int `````` Jean-Christophe Filliatre committed Feb 18, 2014 559 `````` `````` Jean-Christophe Filliatre committed Aug 20, 2015 560 561 562 563 564 565 `````` let rec function fib (n: int) : int requires { n >= 0 } variant { n } = if n = 0 then 0 else if n = 1 then 1 else fib (n-1) + fib (n-2) `````` Jean-Christophe Filliatre committed Feb 18, 2014 566 567 `````` end `````` Jean-Christophe Filliatre committed Jun 01, 2018 568 569 `````` module WFltof `````` Andrei Paskevich committed Jun 15, 2018 570 571 `````` use Int use relations.WellFounded `````` Jean-Christophe Filliatre committed Jun 01, 2018 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 `````` type t function f t : int axiom f_nonneg: forall x. 0 <= f x predicate ltof (x y: t) = f x < f y let rec lemma acc_ltof (n: int) requires { 0 <= n } ensures { forall x. f x < n -> acc ltof x } variant { n } = if n > 0 then acc_ltof (n-1) lemma wf_ltof: well_founded ltof end``````