euler001.mlw 2.07 KB
 MARCHE Claude committed Apr 10, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ``````(* Euler Project, problem 1 If we list all the natural numbers below 10 that are multiples of 3 or 5, we get 3, 5, 6 and 9. The sum of these multiples is 23. Find the sum of all the multiples of 3 or 5 below 1000. *) theory SumMultiple use import int.Int use import int.EuclideanDivision `````` Jean-Christophe Filliâtre committed May 20, 2011 16 `````` (* [sum_multiple_3_5_lt n] is the sum of all the multiples `````` MARCHE Claude committed Apr 10, 2011 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 `````` of 3 or 5 below n] *) logic sum_multiple_3_5_lt int : int axiom SumEmpty: sum_multiple_3_5_lt 0 = 0 axiom SumNo : forall n:int. n >= 0 -> mod n 3 <> 0 and mod n 5 <> 0 -> sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n axiom SumYes: forall n:int. n >= 0 -> mod n 3 = 0 or mod n 5 = 0 -> sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n lemma div_minus1_1 : forall x y:int. x >= 0 and y > 0 -> mod (x+1) y = 0 -> div (x+1) y = (div x y) + 1 lemma div_minus1_2 : forall x y:int. x >= 0 and y > 0 -> `````` Jean-Christophe Filliâtre committed May 20, 2011 36 `````` mod (x+1) y <> 0 -> div (x+1) y = (div x y) `````` MARCHE Claude committed Apr 10, 2011 37 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 38 `````` logic closed_formula (n:int) : int = `````` MARCHE Claude committed Apr 10, 2011 39 40 41 `````` let n3 = div n 3 in let n5 = div n 5 in let n15 = div n 15 in `````` Jean-Christophe Filliâtre committed May 20, 2011 42 43 44 `````` div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2 `````` MARCHE Claude committed Apr 10, 2011 45 46 47 `````` lemma mod_15 : forall n:int. n >= 0 -> `````` Jean-Christophe Filliâtre committed May 20, 2011 48 `````` mod n 15 = 0 <-> (mod n 3 = 0 and mod n 5 = 0) `````` MARCHE Claude committed Apr 10, 2011 49 50 51 52 53 `````` logic p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n lemma Closed_formula_0: p 0 `````` Jean-Christophe Filliâtre committed May 20, 2011 54 55 `````` lemma Closed_formula_n_1: forall n:int. n > 0 -> p (n-1) -> `````` MARCHE Claude committed Apr 10, 2011 56 57 `````` mod n 3 <> 0 and mod n 5 <> 0 -> p n `````` Jean-Christophe Filliâtre committed May 20, 2011 58 `````` lemma Closed_formula_n_2: `````` MARCHE Claude committed Apr 10, 2011 59 60 61 62 63 `````` forall n:int. n > 0 -> p (n-1) -> mod n 3 = 0 or mod n 5 = 0 -> p n clone int.Induction as I with logic p = p `````` Jean-Christophe Filliâtre committed May 20, 2011 64 `````` lemma Closed_formula: `````` MARCHE Claude committed Apr 10, 2011 65 66 67 68 69 70 71 72 73 74 `````` forall n:int. 0 <= n -> p n end module Euler001 use import SumMultiple use import int.Int use import int.EuclideanDivision `````` Jean-Christophe Filliâtre committed May 20, 2011 75 `````` let solve n = `````` MARCHE Claude committed Apr 10, 2011 76 77 78 79 80 81 82 `````` { n >= 1 } let n3 = div (n-1) 3 in let n5 = div (n-1) 5 in let n15 = div (n-1) 15 in div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2 { result = sum_multiple_3_5_lt n } `````` Jean-Christophe Filliâtre committed May 20, 2011 83 84 85 86 87 88 89 90 ``````end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/euler001.gui" End: *) ``````
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "https://gitlab.inria.fr/why3/why3/-/blame/e5cbb752d8c608c4274ae511ec388983db74cda3/examples/programs/euler001.mlw", "fetch_time": 1600660147000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2020-40/segments/1600400198887.3/warc/CC-MAIN-20200921014923-20200921044923-00114.warc.gz", "warc_record_offset": 439604186, "warc_record_length": 13474, "token_count": 1324, "char_count": 3337, "score": 3.5, "int_score": 4, "crawl": "CC-MAIN-2020-40", "snapshot_type": "latest", "language": "en", "language_score": 0.6183009147644043, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00045-of-00064.parquet"}