summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lammich <lammich@in.tum.de> |

Mon, 14 Aug 2017 18:32:46 -0400 | |

changeset 69892 | e8e97a214e48 |

parent 69891 | 6625f13189b9 |

child 69893 | 7ca4cbbd7bb9 |

updated

--- a/Exercises/hwsubm/OR/Keinholz_Jonas_jonas.keinholz@tum.de_658/project_euler.thy Fri Aug 11 13:40:41 2017 +0200 +++ b/Exercises/hwsubm/OR/Keinholz_Jonas_jonas.keinholz@tum.de_658/project_euler.thy Mon Aug 14 18:32:46 2017 -0400 @@ -1,7 +1,44 @@ -(*\<Rightarrow> Max *) +(** Score: 13/15 + +The student took the first two problems of Project Euler and came up with solutions +via functional programs, proved that the programs compute the desired results and +finally extracted the code equations to Haskell. +With some unverified wrapper the two programscould be submitted to hackerrank and be tested. +The students does not state what the results of these submissions are, but it seems +reasonable that they perform well. + +The two problems are: + +1: +for a number n, find the sum of all numbers smaller n that are multiples of 3 or 5. + +evaluation: ++ direct definition of the desired result (solve001) ++ naive implementation + correctness proof (solve001_naive) ++ implementation with closed form + correctness proof (solve001_ap) ++ successfull code extraction + +2: +for a number n, find the sum of all even-valued fibonacci numbers smaller than n. +evaluation: ++ definition of fibonacci sequence (generalized starting numbers) (fibonacci_seq) ++ efficient enumeration of fibonacci sequence (fibonaccis) ++ correctness proof wrt to fibonacci_seq ++ implementation of desired result with "fibonaccis", filter, sum (solve002) +- missing proof whether this matches the desired result (definition, + correctness proof), which + on the other hand would not have been too much more work. ++ successfull code extraction + +ideas for improvements: +for a better runtime one could as a first step observe that every forth fib-number is even... + + + +*) section \<open>Formally verified solutions to Project Euler problems\<close> + text \<open> Formally verified solutions to the first two Project Euler problems (https://projecteuler.net) @@ -89,6 +126,22 @@ finally show ?thesis . qed +(** maybe a shorter proof is possible, + try to reuse the lemmas you find in the library to ease your life :) +lemma assumes inj_f: "inj f" + shows "\<Sum>{f k | k. k \<le> n} = sum f {..n}" +proof - + have "{f k | k. k \<le> n} = (f ` {..n})" by auto + then + have "\<Sum>{f k | k. k \<le> n} = \<Sum> (f ` {..n})" by auto + moreover have + "\<dots> = sum f {..n}" using inj_f + by (metis injD inj_on_def sum.reindex_cong) + finally show ?thesis . +qed +*) + + lemma Sum_f: fixes f :: "nat \<Rightarrow> nat" assumes "inj f" @@ -184,7 +237,7 @@ using sum_distrib_left[where r = m and f = "\<lambda>k. k"] by auto also have "\<dots> = m * (((n - 1) div m) * ((n - 1) div m + 1) div 2)" proof - - { + { (** move out as a lemma for better proof structure *) fix n :: nat have "\<Sum>{..n} = n * (n + 1) div 2" by (induction n) auto